Index: src/ResolvExpr/CommonType.cc
===================================================================
--- src/ResolvExpr/CommonType.cc	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/CommonType.cc	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -176,4 +176,14 @@
 	}
 
+	const ast::Type * commonType(
+			const ast::Type * type1, const ast::Type * type2, WidenMode widen, 
+			const ast::SymbolTable & symtab, ast::TypeEnvironment & env, 
+			const ast::OpenVarSet & open ) {
+		#warning unimplemented
+		(void)type1; (void)type2; (void)widen; (void)symtab; (void)env; (void)open;
+		assert(false);
+		return nullptr;
+	}
+
 	// GENERATED START, DO NOT EDIT
 	// GENERATED BY BasicTypes-gen.cc
Index: src/ResolvExpr/FindOpenVars.cc
===================================================================
--- src/ResolvExpr/FindOpenVars.cc	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/FindOpenVars.cc	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -93,4 +93,12 @@
 		common_action( tupleType );
 	}
+
+	void findOpenVars( 
+			const ast::Type * type, ast::OpenVarSet & open, ast::OpenVarSet & closed, 
+			ast::AssertionSet & need, ast::AssertionSet & have, FirstMode firstIsOpen ) {
+		#warning unimplemented
+		(void)type; (void)open; (void)closed; (void)need; (void)have; (void)firstIsOpen;
+		assert(false);
+	}
 } // namespace ResolvExpr
 
Index: src/ResolvExpr/FindOpenVars.h
===================================================================
--- src/ResolvExpr/FindOpenVars.h	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/FindOpenVars.h	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -16,11 +16,22 @@
 #pragma once
 
+#include "AST/TypeEnvironment.hpp"  // for AssertionSet, OpenVarSet
 #include "ResolvExpr/TypeEnvironment.h"  // for AssertionSet, OpenVarSet
 
 class Type;
+namespace ast {
+	class Type;
+}
 
 namespace ResolvExpr {
 	// Updates open and closed variables and their associated assertions
 	void findOpenVars( Type *type, OpenVarSet &openVars, OpenVarSet &closedVars, AssertionSet &needAssertions, AssertionSet &haveAssertions, bool firstIsOpen );
+
+	enum FirstMode { FirstClosed, FirstOpen };
+
+	// Updates open and closed variables and their associated assertions
+	void findOpenVars( 
+		const ast::Type * type, ast::OpenVarSet & open, ast::OpenVarSet & closed, 
+		ast::AssertionSet & need, ast::AssertionSet & have, FirstMode firstIsOpen );
 } // namespace ResolvExpr
 
Index: src/ResolvExpr/TypeEnvironment.cc
===================================================================
--- src/ResolvExpr/TypeEnvironment.cc	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/TypeEnvironment.cc	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -205,8 +205,8 @@
 				// attempt to unify bound types
 				std::unique_ptr<Type> toType{ to.type->clone() }, fromType{ from.type->clone() };
-				WidenMode widenMode{ to.allowWidening, from.allowWidening };
+				WidenMode widen{ to.allowWidening, from.allowWidening };
 				Type* common = nullptr;
 				AssertionSet need, have;
-				if ( unifyInexact( toType.get(), fromType.get(), *this, need, have, openVars, widenMode, indexer, common ) ) {
+				if ( unifyInexact( toType.get(), fromType.get(), *this, need, have, openVars, widen, indexer, common ) ) {
 					// unifies, set common type if necessary
 					if ( common ) {
@@ -343,5 +343,5 @@
 	}
 
-	bool TypeEnvironment::bindVar( TypeInstType *typeInst, Type *bindTo, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
+	bool TypeEnvironment::bindVar( TypeInstType *typeInst, Type *bindTo, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer ) {
 
 		// remove references from other, so that type variables can only bind to value types
@@ -362,5 +362,5 @@
 				std::unique_ptr< Type > newType( curClass->type->clone() );
 				newType->get_qualifiers() = typeInst->get_qualifiers();
-				if ( unifyInexact( newType.get(), bindTo, *this, need, have, openVars, widenMode & WidenMode( curClass->allowWidening, true ), indexer, common ) ) {
+				if ( unifyInexact( newType.get(), bindTo, *this, need, have, openVars, widen & WidenMode( curClass->allowWidening, true ), indexer, common ) ) {
 					if ( common ) {
 						common->get_qualifiers() = Type::Qualifiers{};
@@ -372,5 +372,5 @@
 				newType->get_qualifiers() = Type::Qualifiers{};
 				curClass->set_type( newType );
-				curClass->allowWidening = widenMode.widenFirst && widenMode.widenSecond;
+				curClass->allowWidening = widen.first && widen.second;
 			} // if
 		} else {
@@ -379,5 +379,5 @@
 			newClass.type = bindTo->clone();
 			newClass.type->get_qualifiers() = Type::Qualifiers();
-			newClass.allowWidening = widenMode.widenFirst && widenMode.widenSecond;
+			newClass.allowWidening = widen.first && widen.second;
 			newClass.data = data;
 			env.push_back( std::move(newClass) );
@@ -388,5 +388,5 @@
 	bool TypeEnvironment::bindVarToVar( TypeInstType *var1, TypeInstType *var2, 
 			TypeDecl::Data && data, AssertionSet &need, AssertionSet &have, 
-			const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
+			const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer ) {
 
 		auto class1 = internal_lookup( var1->get_name() );
@@ -395,5 +395,5 @@
 		// exit early if variables already bound together
 		if ( class1 != env.end() && class1 == class2 ) {
-			class1->allowWidening &= widenMode;
+			class1->allowWidening &= widen;
 			return true;
 		}
@@ -408,5 +408,5 @@
 				type1 = class1->type;
 			} // if
-			widen1 = widenMode.widenFirst && class1->allowWidening;
+			widen1 = widen.first && class1->allowWidening;
 		} // if
 		if ( class2 != env.end() ) {
@@ -415,5 +415,5 @@
 				type2 = class2->type;
 			} // if
-			widen2 = widenMode.widenSecond && class2->allowWidening;
+			widen2 = widen.second && class2->allowWidening;
 		} // if
 
Index: src/ResolvExpr/TypeEnvironment.h
===================================================================
--- src/ResolvExpr/TypeEnvironment.h	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/TypeEnvironment.h	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -136,9 +136,9 @@
 		/// Binds the type class represented by `typeInst` to the type `bindTo`; will add 
 		/// the class if needed. Returns false on failure.
-		bool bindVar( TypeInstType *typeInst, Type *bindTo, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer );
+		bool bindVar( TypeInstType *typeInst, Type *bindTo, const TypeDecl::Data & data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer );
 		
 		/// Binds the type classes represented by `var1` and `var2` together; will add 
 		/// one or both classes if needed. Returns false on failure.
-		bool bindVarToVar( TypeInstType *var1, TypeInstType *var2, TypeDecl::Data && data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer );
+		bool bindVarToVar( TypeInstType *var1, TypeInstType *var2, TypeDecl::Data && data, AssertionSet &need, AssertionSet &have, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer );
 
 		/// Disallows widening for all bindings in the environment
Index: src/ResolvExpr/Unify.cc
===================================================================
--- src/ResolvExpr/Unify.cc	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/Unify.cc	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -14,4 +14,6 @@
 //
 
+#include "Unify.h"
+
 #include <cassert>                  // for assertf, assert
 #include <iterator>                 // for back_insert_iterator, back_inserter
@@ -23,5 +25,7 @@
 #include <vector>
 
+#include "AST/Decl.hpp"
 #include "AST/Node.hpp"
+#include "AST/Pass.hpp"
 #include "AST/Type.hpp"
 #include "AST/TypeEnvironment.hpp"
@@ -37,6 +41,9 @@
 #include "Tuples/Tuples.h"          // for isTtype
 #include "TypeEnvironment.h"        // for EqvClass, AssertionSet, OpenVarSet
-#include "Unify.h"
 #include "typeops.h"                // for flatten, occurs, commonType
+
+namespace ast {
+	class SymbolTable;
+}
 
 namespace SymTab {
@@ -48,6 +55,6 @@
 namespace ResolvExpr {
 
-	struct Unify : public WithShortCircuiting {
-		Unify( Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer );
+	struct Unify_old : public WithShortCircuiting {
+		Unify_old( Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer );
 
 		bool get_result() const { return result; }
@@ -81,5 +88,5 @@
 		AssertionSet &haveAssertions;
 		const OpenVarSet &openVars;
-		WidenMode widenMode;
+		WidenMode widen;
 		const SymTab::Indexer &indexer;
 	};
@@ -87,6 +94,11 @@
 	/// Attempts an inexact unification of type1 and type2.
 	/// Returns false if no such unification; if the types can be unified, sets common (unless they unify exactly and have identical type qualifiers)
-	bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer, Type *&common );
-	bool unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer );
+	bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer, Type *&common );
+	bool unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer );
+
+	bool unifyExact( 
+		const ast::Type * type1, const ast::Type * type2, ast::TypeEnvironment & env, 
+		ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & open, 
+		WidenMode widen, const ast::SymbolTable & symtab );
 
 	bool typesCompatible( Type *first, Type *second, const SymTab::Indexer &indexer, const TypeEnvironment &env ) {
@@ -112,7 +124,17 @@
 			const ast::Type * first, const ast::Type * second, const ast::SymbolTable & symtab, 
 			const ast::TypeEnvironment & env ) {
-		#warning unimplemented
-		assert((first, second, symtab, env, false));
-		return false;
+		ast::TypeEnvironment newEnv;
+		ast::OpenVarSet open, closed;
+		ast::AssertionSet need, have;
+
+		ast::ptr<ast::Type> newFirst{ first }, newSecond{ second };
+		env.apply( newFirst );
+		env.apply( newSecond );
+
+		findOpenVars( newFirst, open, closed, need, have, FirstClosed );
+		findOpenVars( newSecond, open, closed, need, have, FirstOpen );
+
+		return unifyExact( 
+			newFirst, newSecond, newEnv, need, have, open, WidenMode{ false, false }, symtab );
 	}
 
@@ -144,7 +166,16 @@
 			const ast::Type * first, const ast::Type * second, const ast::SymbolTable & symtab, 
 			const ast::TypeEnvironment & env ) {
-		#warning unimplemented
-		assert((first, second, symtab, env, false));
-		return false;
+		ast::TypeEnvironment newEnv;
+		ast::OpenVarSet open;
+		ast::AssertionSet need, have;
+		
+		ast::ptr<ast::Type> newFirst{ first }, newSecond{ second };
+		env.apply( newFirst );
+		env.apply( newSecond );
+		clear_qualifiers( newFirst );
+		clear_qualifiers( newSecond );
+
+		return unifyExact( 
+			newFirst, newSecond, newEnv, need, have, open, WidenMode{ false, false }, symtab );
 	}
 
@@ -171,5 +202,5 @@
 	}
 
-	bool unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer ) {
+	bool unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer ) {
 #ifdef DEBUG
 		TypeEnvironment debugEnv( env );
@@ -198,12 +229,12 @@
 				result = env.bindVarToVar(
 					var1, var2, TypeDecl::Data{ entry1->second, entry2->second }, needAssertions,
-					haveAssertions, openVars, widenMode, indexer );
+					haveAssertions, openVars, widen, indexer );
 			}
 		} else if ( isopen1 ) {
-			result = env.bindVar( var1, type2, entry1->second, needAssertions, haveAssertions, openVars, widenMode, indexer );
-		} else if ( isopen2 ) { // TODO: swap widenMode values in call, since type positions are flipped?
-			result = env.bindVar( var2, type1, entry2->second, needAssertions, haveAssertions, openVars, widenMode, indexer );
+			result = env.bindVar( var1, type2, entry1->second, needAssertions, haveAssertions, openVars, widen, indexer );
+		} else if ( isopen2 ) { // TODO: swap widen values in call, since type positions are flipped?
+			result = env.bindVar( var2, type1, entry2->second, needAssertions, haveAssertions, openVars, widen, indexer );
 		} else {
-			PassVisitor<Unify> comparator( type2, env, needAssertions, haveAssertions, openVars, widenMode, indexer );
+			PassVisitor<Unify_old> comparator( type2, env, needAssertions, haveAssertions, openVars, widen, indexer );
 			type1->accept( comparator );
 			result = comparator.pass.get_result();
@@ -230,5 +261,5 @@
 	}
 
-	bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer, Type *&common ) {
+	bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer, Type *&common ) {
 		Type::Qualifiers tq1 = type1->get_qualifiers(), tq2 = type2->get_qualifiers();
 		type1->get_qualifiers() = Type::Qualifiers();
@@ -242,9 +273,9 @@
 		std::cerr << std::endl;
 #endif
-		if ( ! unifyExact( type1, type2, env, needAssertions, haveAssertions, openVars, widenMode, indexer ) ) {
+		if ( ! unifyExact( type1, type2, env, needAssertions, haveAssertions, openVars, widen, indexer ) ) {
 #ifdef DEBUG
 			std::cerr << "unifyInexact: no exact unification found" << std::endl;
 #endif
-			if ( ( common = commonType( type1, type2, widenMode.widenFirst, widenMode.widenSecond, indexer, env, openVars ) ) ) {
+			if ( ( common = commonType( type1, type2, widen.first, widen.second, indexer, env, openVars ) ) ) {
 				common->get_qualifiers() = tq1 | tq2;
 #ifdef DEBUG
@@ -262,5 +293,5 @@
 		} else {
 			if ( tq1 != tq2 ) {
-				if ( ( tq1 > tq2 || widenMode.widenFirst ) && ( tq2 > tq1 || widenMode.widenSecond ) ) {
+				if ( ( tq1 > tq2 || widen.first ) && ( tq2 > tq1 || widen.second ) ) {
 					common = type1->clone();
 					common->get_qualifiers() = tq1 | tq2;
@@ -280,22 +311,13 @@
 	}
 
-	bool unifyInexact( 
-			const ast::Type * type1, const ast::Type * type2, ast::TypeEnvironment & env, 
-			ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & openVars, 
-			WidenMode widenMode, const ast::SymbolTable & symtab, const ast::Type *& common ) {
-		#warning unimplemented
-		assert((type1, type2, env, need, have, openVars, widenMode, symtab, common, false));
-		return false;
-	}
-
-	Unify::Unify( Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer )
-		: result( false ), type2( type2 ), env( env ), needAssertions( needAssertions ), haveAssertions( haveAssertions ), openVars( openVars ), widenMode( widenMode ), indexer( indexer ) {
-	}
-
-	void Unify::postvisit( __attribute__((unused)) VoidType *voidType) {
+	Unify_old::Unify_old( Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer )
+		: result( false ), type2( type2 ), env( env ), needAssertions( needAssertions ), haveAssertions( haveAssertions ), openVars( openVars ), widen( widen ), indexer( indexer ) {
+	}
+
+	void Unify_old::postvisit( __attribute__((unused)) VoidType *voidType) {
 		result = dynamic_cast< VoidType* >( type2 );
 	}
 
-	void Unify::postvisit(BasicType *basicType) {
+	void Unify_old::postvisit(BasicType *basicType) {
 		if ( BasicType *otherBasic = dynamic_cast< BasicType* >( type2 ) ) {
 			result = basicType->get_kind() == otherBasic->get_kind();
@@ -325,5 +347,5 @@
 	}
 
-	void Unify::postvisit(PointerType *pointerType) {
+	void Unify_old::postvisit(PointerType *pointerType) {
 		if ( PointerType *otherPointer = dynamic_cast< PointerType* >( type2 ) ) {
 			result = unifyExact( pointerType->get_base(), otherPointer->get_base(), env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
@@ -333,5 +355,5 @@
 	}
 
-	void Unify::postvisit(ReferenceType *refType) {
+	void Unify_old::postvisit(ReferenceType *refType) {
 		if ( ReferenceType *otherRef = dynamic_cast< ReferenceType* >( type2 ) ) {
 			result = unifyExact( refType->get_base(), otherRef->get_base(), env, needAssertions, haveAssertions, openVars, WidenMode( false, false ), indexer );
@@ -341,5 +363,5 @@
 	}
 
-	void Unify::postvisit(ArrayType *arrayType) {
+	void Unify_old::postvisit(ArrayType *arrayType) {
 		ArrayType *otherArray = dynamic_cast< ArrayType* >( type2 );
 		// to unify, array types must both be VLA or both not VLA
@@ -421,7 +443,7 @@
 	/// If this isn't done then argument lists can have wildly different
 	/// size and structure, when they should be compatible.
-	struct TtypeExpander : public WithShortCircuiting {
+	struct TtypeExpander_old : public WithShortCircuiting {
 		TypeEnvironment & tenv;
-		TtypeExpander( TypeEnvironment & tenv ) : tenv( tenv ) {}
+		TtypeExpander_old( TypeEnvironment & tenv ) : tenv( tenv ) {}
 		void premutate( TypeInstType * ) { visit_children = false; }
 		Type * postmutate( TypeInstType * typeInst ) {
@@ -442,5 +464,5 @@
 		dst.clear();
 		for ( DeclarationWithType * dcl : src ) {
-			PassVisitor<TtypeExpander> expander( env );
+			PassVisitor<TtypeExpander_old> expander( env );
 			dcl->acceptMutator( expander );
 			std::list< Type * > types;
@@ -457,5 +479,5 @@
 	}
 
-	void Unify::postvisit(FunctionType *functionType) {
+	void Unify_old::postvisit(FunctionType *functionType) {
 		FunctionType *otherFunction = dynamic_cast< FunctionType* >( type2 );
 		if ( otherFunction && functionType->get_isVarArgs() == otherFunction->get_isVarArgs() ) {
@@ -468,5 +490,10 @@
 
 			// sizes don't have to match if ttypes are involved; need to be more precise wrt where the ttype is to prevent errors
-			if ( (flatFunc->parameters.size() == flatOther->parameters.size() && flatFunc->returnVals.size() == flatOther->returnVals.size()) || flatFunc->isTtype() || flatOther->isTtype() ) {
+			if ( 
+					(flatFunc->parameters.size() == flatOther->parameters.size() && 
+						flatFunc->returnVals.size() == flatOther->returnVals.size()) 
+					|| flatFunc->isTtype() 
+					|| flatOther->isTtype() 
+			) {
 				if ( unifyDeclList( flatFunc->parameters.begin(), flatFunc->parameters.end(), flatOther->parameters.begin(), flatOther->parameters.end(), env, needAssertions, haveAssertions, openVars, indexer ) ) {
 					if ( unifyDeclList( flatFunc->returnVals.begin(), flatFunc->returnVals.end(), flatOther->returnVals.begin(), flatOther->returnVals.end(), env, needAssertions, haveAssertions, openVars, indexer ) ) {
@@ -484,5 +511,5 @@
 
 	template< typename RefType >
-	void Unify::handleRefType( RefType *inst, Type *other ) {
+	void Unify_old::handleRefType( RefType *inst, Type *other ) {
 		// check that other type is compatible and named the same
 		RefType *otherStruct = dynamic_cast< RefType* >( other );
@@ -491,5 +518,5 @@
 
 	template< typename RefType >
-	void Unify::handleGenericRefType( RefType *inst, Type *other ) {
+	void Unify_old::handleGenericRefType( RefType *inst, Type *other ) {
 		// Check that other type is compatible and named the same
 		handleRefType( inst, other );
@@ -559,21 +586,21 @@
 	}
 
-	void Unify::postvisit(StructInstType *structInst) {
+	void Unify_old::postvisit(StructInstType *structInst) {
 		handleGenericRefType( structInst, type2 );
 	}
 
-	void Unify::postvisit(UnionInstType *unionInst) {
+	void Unify_old::postvisit(UnionInstType *unionInst) {
 		handleGenericRefType( unionInst, type2 );
 	}
 
-	void Unify::postvisit(EnumInstType *enumInst) {
+	void Unify_old::postvisit(EnumInstType *enumInst) {
 		handleRefType( enumInst, type2 );
 	}
 
-	void Unify::postvisit(TraitInstType *contextInst) {
+	void Unify_old::postvisit(TraitInstType *contextInst) {
 		handleRefType( contextInst, type2 );
 	}
 
-	void Unify::postvisit(TypeInstType *typeInst) {
+	void Unify_old::postvisit(TypeInstType *typeInst) {
 		assert( openVars.find( typeInst->get_name() ) == openVars.end() );
 		TypeInstType *otherInst = dynamic_cast< TypeInstType* >( type2 );
@@ -630,5 +657,5 @@
 	}
 
-	void Unify::postvisit(TupleType *tupleType) {
+	void Unify_old::postvisit(TupleType *tupleType) {
 		if ( TupleType *otherTuple = dynamic_cast< TupleType* >( type2 ) ) {
 			std::unique_ptr<TupleType> flat1( tupleType->clone() );
@@ -636,5 +663,5 @@
 			std::list<Type *> types1, types2;
 
-			PassVisitor<TtypeExpander> expander( env );
+			PassVisitor<TtypeExpander_old> expander( env );
 			flat1->acceptMutator( expander );
 			flat2->acceptMutator( expander );
@@ -647,13 +674,13 @@
 	}
 
-	void Unify::postvisit( __attribute__((unused)) VarArgsType *varArgsType ) {
+	void Unify_old::postvisit( __attribute__((unused)) VarArgsType *varArgsType ) {
 		result = dynamic_cast< VarArgsType* >( type2 );
 	}
 
-	void Unify::postvisit( __attribute__((unused)) ZeroType *zeroType ) {
+	void Unify_old::postvisit( __attribute__((unused)) ZeroType *zeroType ) {
 		result = dynamic_cast< ZeroType* >( type2 );
 	}
 
-	void Unify::postvisit( __attribute__((unused)) OneType *oneType ) {
+	void Unify_old::postvisit( __attribute__((unused)) OneType *oneType ) {
 		result = dynamic_cast< OneType* >( type2 );
 	}
@@ -673,4 +700,522 @@
 	}
 
+	class Unify_new : public ast::WithShortCircuiting {
+		const ast::Type * type2;
+		ast::TypeEnvironment & tenv;
+		ast::AssertionSet & need;
+		ast::AssertionSet & have;
+		const ast::OpenVarSet & open;
+		WidenMode widen;
+		const ast::SymbolTable & symtab;
+	public:
+		bool result;
+
+		Unify_new( 
+			const ast::Type * type2, ast::TypeEnvironment & env, ast::AssertionSet & need, 
+			ast::AssertionSet & have, const ast::OpenVarSet & open, WidenMode widen, 
+			const ast::SymbolTable & symtab )
+		: type2(type2), tenv(env), need(need), have(have), open(open), widen(widen), 
+		  symtab(symtab), result(false) {}
+
+		void previsit( const ast::Node * ) { visit_children = false; }
+		
+		void previsit( const ast::VoidType * ) {
+			visit_children = false;
+			result = dynamic_cast< const ast::VoidType * >( type2 );
+		}
+
+		void previsit( const ast::BasicType * basic ) {
+			visit_children = false;
+			if ( auto basic2 = dynamic_cast< const ast::BasicType * >( type2 ) ) {
+				result = basic->kind == basic2->kind;
+			}
+		}
+
+		void previsit( const ast::PointerType * pointer ) {
+			visit_children = false;
+			if ( auto pointer2 = dynamic_cast< const ast::PointerType * >( type2 ) ) {
+				result = unifyExact( 
+					pointer->base, pointer2->base, tenv, need, have, open, 
+					WidenMode{ false, false }, symtab );
+			}
+		}
+
+		void previsit( const ast::ArrayType * array ) {
+			visit_children = false;
+			auto array2 = dynamic_cast< const ast::ArrayType * >( type2 );
+			if ( ! array2 ) return;
+
+			// to unify, array types must both be VLA or both not VLA and both must have a 
+			// dimension expression or not have a dimension
+			if ( array->isVarLen != array2->isVarLen ) return;
+			if ( ! array->isVarLen && ! array2->isVarLen 
+					&& array->dimension && array2->dimension ) {
+				auto ce1 = array->dimension.as< ast::ConstantExpr >();
+				auto ce2 = array2->dimension.as< ast::ConstantExpr >();
+
+				// see C11 Reference Manual 6.7.6.2.6
+				// two array types with size specifiers that are integer constant expressions are 
+				// compatible if both size specifiers have the same constant value
+				if ( ce1 && ce2 && ce1->intValue() != ce2->intValue() ) return;
+			}
+
+			result = unifyExact( 
+				array->base, array2->base, tenv, need, have, open, WidenMode{ false, false }, 
+				symtab );
+		}
+
+		void previsit( const ast::ReferenceType * ref ) {
+			visit_children = false;
+			if ( auto ref2 = dynamic_cast< const ast::ReferenceType * >( type2 ) ) {
+				result = unifyExact( 
+					ref->base, ref2->base, tenv, need, have, open, WidenMode{ false, false }, 
+					symtab );
+			}
+		}
+
+	private:
+		/// Replaces ttype variables with their bound types.
+		/// If this isn't done when satifying ttype assertions, then argument lists can have 
+		/// different size and structure when they should be compatible.
+		struct TtypeExpander_new : public ast::WithShortCircuiting {
+			ast::TypeEnvironment & tenv;
+
+			TtypeExpander_new( ast::TypeEnvironment & env ) : tenv( env ) {}
+
+			const ast::Type * postmutate( const ast::TypeInstType * typeInst ) {
+				if ( const ast::EqvClass * clz = tenv.lookup( typeInst->name ) ) {
+					// expand ttype parameter into its actual type
+					if ( clz->data.kind == ast::TypeVar::Ttype && clz->bound ) {
+						return clz->bound;
+					}
+				}
+				return typeInst;
+			}
+		};
+
+		/// returns flattened version of `src`
+		static std::vector< ast::ptr< ast::DeclWithType > > flattenList(
+			const std::vector< ast::ptr< ast::DeclWithType > > & src, ast::TypeEnvironment & env
+		) {
+			std::vector< ast::ptr< ast::DeclWithType > > dst;
+			dst.reserve( src.size() );
+			for ( const ast::DeclWithType * d : src ) {
+				ast::Pass<TtypeExpander_new> expander{ env };
+				d = d->accept( expander );
+				auto types = flatten( d->get_type() );
+				for ( ast::ptr< ast::Type > & t : types ) {
+					// outermost const, volatile, _Atomic qualifiers in parameters should not play 
+					// a role in the unification of function types, since they do not determine 
+					// whether a function is callable.
+					// NOTE: **must** consider at least mutex qualifier, since functions can be 
+					// overloaded on outermost mutex and a mutex function has different 
+					// requirements than a non-mutex function
+					t.get_and_mutate()->qualifiers 
+						-= ast::CV::Const | ast::CV::Volatile | ast::CV::Atomic;
+					dst.emplace_back( new ast::ObjectDecl{ d->location, "", t } );
+				}
+			}
+			return dst;
+		}
+
+		/// Creates a tuple type based on a list of DeclWithType
+		template< typename Iter >
+		static ast::ptr< ast::Type > tupleFromDecls( Iter crnt, Iter end ) {
+			std::vector< ast::ptr< ast::Type > > types;
+			while ( crnt != end ) {
+				// it is guaranteed that a ttype variable will be bound to a flat tuple, so ensure 
+				// that this results in a flat tuple
+				flatten( (*crnt)->get_type(), types );
+
+				++crnt;
+			}
+
+			return { new ast::TupleType{ std::move(types) } };
+		}
+
+		template< typename Iter >
+		static bool unifyDeclList( 
+			Iter crnt1, Iter end1, Iter crnt2, Iter end2, ast::TypeEnvironment & env, 
+			ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & open, 
+			const ast::SymbolTable & symtab
+		) {
+			while ( crnt1 != end1 && crnt2 != end2 ) {
+				const ast::Type * t1 = (*crnt1)->get_type();
+				const ast::Type * t2 = (*crnt2)->get_type();
+				bool isTuple1 = Tuples::isTtype( t1 );
+				bool isTuple2 = Tuples::isTtype( t2 );
+
+				// assumes here that ttype *must* be last parameter
+				if ( isTuple1 && ! isTuple2 ) {
+					// combine remainder of list2, then unify
+					return unifyExact( 
+						t1, tupleFromDecls( crnt2, end2 ), env, need, have, open, 
+						WidenMode{ false, false }, symtab );
+				} else if ( ! isTuple1 && isTuple2 ) {
+					// combine remainder of list1, then unify
+					return unifyExact( 
+						tupleFromDecls( crnt1, end1 ), t2, env, need, have, open, 
+						WidenMode{ false, false }, symtab );
+				}
+
+				if ( ! unifyExact( 
+					t1, t2, env, need, have, open, WidenMode{ false, false }, symtab ) 
+				) return false;
+
+				++crnt1; ++crnt2;
+			}
+
+			// May get to the end of one argument list before the other. This is only okay if the 
+			// other is a ttype
+			if ( crnt1 != end1 ) {
+				// try unifying empty tuple with ttype
+				const ast::Type * t1 = (*crnt1)->get_type();
+				if ( ! Tuples::isTtype( t1 ) ) return false;
+				return unifyExact( 
+					t1, tupleFromDecls( crnt2, end2 ), env, need, have, open, 
+					WidenMode{ false, false }, symtab );
+			} else if ( crnt2 != end2 ) {
+				// try unifying empty tuple with ttype
+				const ast::Type * t2 = (*crnt2)->get_type();
+				if ( ! Tuples::isTtype( t2 ) ) return false;
+				return unifyExact( 
+					tupleFromDecls( crnt1, end1 ), t2, env, need, have, open, 
+					WidenMode{ false, false }, symtab );
+			}
+
+			return true;
+		}
+
+		static bool unifyDeclList( 
+			const std::vector< ast::ptr< ast::DeclWithType > > & list1, 
+			const std::vector< ast::ptr< ast::DeclWithType > > & list2, 
+			ast::TypeEnvironment & env, ast::AssertionSet & need, ast::AssertionSet & have, 
+			const ast::OpenVarSet & open, const ast::SymbolTable & symtab
+		) {
+			return unifyDeclList( 
+				list1.begin(), list1.end(), list2.begin(), list2.end(), env, need, have, open, 
+				symtab );
+		}
+
+		static void markAssertionSet( ast::AssertionSet & assns, const ast::DeclWithType * assn ) {
+			auto i = assns.find( assn );
+			if ( i != assns.end() ) {
+				i->second.isUsed = true;
+			}
+		}
+
+		/// mark all assertions in `type` used in both `assn1` and `assn2`
+		static void markAssertions( 
+			ast::AssertionSet & assn1, ast::AssertionSet & assn2, 
+			const ast::ParameterizedType * type 
+		) {
+			for ( const auto & tyvar : type->forall ) {
+				for ( const ast::DeclWithType * assert : tyvar->assertions ) {
+					markAssertionSet( assn1, assert );
+					markAssertionSet( assn2, assert );
+				}
+			}
+		}
+
+	public:
+		void previsit( const ast::FunctionType * func ) {
+			visit_children = false;
+			auto func2 = dynamic_cast< const ast::FunctionType * >( type2 );
+			if ( ! func2 ) return;
+
+			if ( func->isVarArgs != func2->isVarArgs ) return;
+			
+			// Flatten the parameter lists for both functions so that tuple structure does not 
+			// affect unification. Does not actually mutate function parameters.
+			auto params = flattenList( func->params, tenv );
+			auto params2 = flattenList( func2->params, tenv );
+
+			// sizes don't have to match if ttypes are involved; need to be more precise w.r.t. 
+			// where the ttype is to prevent errors
+			if ( 
+				( params.size() != params2.size() || func->returns.size() != func2->returns.size() )
+				&& ! func->isTtype()
+				&& ! func2->isTtype()
+			) return;
+
+			if ( ! unifyDeclList( params, params2, tenv, need, have, open, symtab ) ) return;
+			if ( ! unifyDeclList( 
+				func->returns, func2->returns, tenv, need, have, open, symtab ) ) return;
+			
+			markAssertions( have, need, func );
+			markAssertions( have, need, func2 );
+
+			result = true;
+		}
+	
+	private:
+		template< typename RefType >
+		const RefType * handleRefType( const RefType * inst, const ast::Type * other ) {
+			visit_children = false;
+			// check that the other type is compatible and named the same
+			auto otherInst = dynamic_cast< const RefType * >( other );
+			result = otherInst && inst->name == otherInst->name;
+			return otherInst;
+		}
+
+		/// Creates a tuple type based on a list of TypeExpr
+		template< typename Iter >
+		static const ast::Type * tupleFromExprs( 
+			const ast::TypeExpr * param, Iter & crnt, Iter end, ast::CV::Qualifiers qs
+		) {
+			std::vector< ast::ptr< ast::Type > > types;
+			do {
+				types.emplace_back( param->type );
+
+				++crnt;
+				if ( crnt == end ) break;
+				param = strict_dynamic_cast< const ast::TypeExpr * >( crnt->get() );
+			} while(true);
+
+			return new ast::TupleType{ std::move(types), qs };
+		}
+
+		template< typename RefType >
+		void handleGenericRefType( const RefType * inst, const ast::Type * other ) {
+			// check that other type is compatible and named the same
+			const RefType * inst2 = handleRefType( inst, other );
+			if ( ! inst2 ) return;
+			
+			// check that parameters of types unify, if any
+			const std::vector< ast::ptr< ast::Expr > > & params = inst->params;
+			const std::vector< ast::ptr< ast::Expr > > & params2 = inst2->params;
+
+			auto it = params.begin();
+			auto jt = params2.begin();
+			for ( ; it != params.end() && jt != params2.end(); ++it, ++jt ) {
+				auto param = strict_dynamic_cast< const ast::TypeExpr * >( it->get() );
+				auto param2 = strict_dynamic_cast< const ast::TypeExpr * >( jt->get() );
+
+				ast::ptr< ast::Type > pty = param->type;
+				ast::ptr< ast::Type > pty2 = param2->type;
+
+				bool isTuple = Tuples::isTtype( pty );
+				bool isTuple2 = Tuples::isTtype( pty2 );
+
+				if ( isTuple && isTuple2 ) {
+					++it; ++jt;  // skip ttype parameters before break
+				} else if ( isTuple ) {
+					// bundle remaining params into tuple
+					pty2 = tupleFromExprs( param2, jt, params2.end(), pty->qualifiers );
+					++it;  // skip ttype parameter for break
+				} else if ( isTuple2 ) {
+					// bundle remaining params into tuple
+					pty = tupleFromExprs( param, it, params.end(), pty2->qualifiers );
+					++jt;  // skip ttype parameter for break
+				}
+
+				if ( ! unifyExact( 
+						pty, pty2, tenv, need, have, open, WidenMode{ false, false }, symtab ) ) {
+					result = false;
+					return;
+				}
+
+				// ttype parameter should be last
+				if ( isTuple || isTuple2 ) break;
+			}
+			result = it == params.end() && jt == params2.end();
+		}
+
+	public:
+		void previsit( const ast::StructInstType * aggrType ) {
+			handleGenericRefType( aggrType, type2 );
+		}
+
+		void previsit( const ast::UnionInstType * aggrType ) {
+			handleGenericRefType( aggrType, type2 );
+		}
+
+		void previsit( const ast::EnumInstType * aggrType ) {
+			handleRefType( aggrType, type2 );
+		}
+
+		void previsit( const ast::TraitInstType * aggrType ) {
+			handleRefType( aggrType, type2 );
+		}
+
+		void previsit( const ast::TypeInstType * typeInst ) {
+			assert( open.find( typeInst->name ) == open.end() );
+			handleRefType( typeInst, type2 );
+		}
+
+	private:
+		/// Creates a tuple type based on a list of Type
+		static ast::ptr< ast::Type > tupleFromTypes( 
+			const std::vector< ast::ptr< ast::Type > > & tys
+		) {
+			std::vector< ast::ptr< ast::Type > > out;
+			for ( const ast::Type * ty : tys ) {
+				// it is guaranteed that a ttype variable will be bound to a flat tuple, so ensure 
+				// that this results in a flat tuple
+				flatten( ty, out );
+			}
+
+			return { new ast::TupleType{ std::move(out) } };
+		}
+
+		static bool unifyList( 
+			const std::vector< ast::ptr< ast::Type > > & list1, 
+			const std::vector< ast::ptr< ast::Type > > & list2, ast::TypeEnvironment & env, 
+			ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & open, 
+			const ast::SymbolTable & symtab
+		) {
+			auto crnt1 = list1.begin();
+			auto crnt2 = list2.begin();
+			while ( crnt1 != list1.end() && crnt2 != list2.end() ) {
+				const ast::Type * t1 = *crnt1;
+				const ast::Type * t2 = *crnt2;
+				bool isTuple1 = Tuples::isTtype( t1 );
+				bool isTuple2 = Tuples::isTtype( t2 );
+
+				// assumes ttype must be last parameter
+				if ( isTuple1 && ! isTuple2 ) {
+					// combine entirety of list2, then unify
+					return unifyExact( 
+						t1, tupleFromTypes( list2 ), env, need, have, open, 
+						WidenMode{ false, false }, symtab );
+				} else if ( ! isTuple1 && isTuple2 ) {
+					// combine entirety of list1, then unify
+					return unifyExact(
+						tupleFromTypes( list1 ), t2, env, need, have, open, 
+						WidenMode{ false, false }, symtab );
+				}
+
+				if ( ! unifyExact( 
+					t1, t2, env, need, have, open, WidenMode{ false, false }, symtab ) 
+				) return false;
+
+				++crnt1; ++crnt2;
+			}
+
+			if ( crnt1 != list1.end() ) {
+				// try unifying empty tuple type with ttype
+				const ast::Type * t1 = *crnt1;
+				if ( ! Tuples::isTtype( t1 ) ) return false;
+				// xxx - this doesn't generate an empty tuple, contrary to comment; both ported 
+				// from Rob's code
+				return unifyExact( 
+						t1, tupleFromTypes( list2 ), env, need, have, open, 
+						WidenMode{ false, false }, symtab );
+			} else if ( crnt2 != list2.end() ) {
+				// try unifying empty tuple with ttype
+				const ast::Type * t2 = *crnt2;
+				if ( ! Tuples::isTtype( t2 ) ) return false;
+				// xxx - this doesn't generate an empty tuple, contrary to comment; both ported 
+				// from Rob's code
+				return unifyExact(
+						tupleFromTypes( list1 ), t2, env, need, have, open, 
+						WidenMode{ false, false }, symtab );
+			}
+
+			return true;
+		}
+
+	public:
+		void previsit( const ast::TupleType * tuple ) {
+			visit_children = false;
+			auto tuple2 = dynamic_cast< const ast::TupleType * >( type2 );
+			if ( ! tuple2 ) return;
+
+			ast::Pass<TtypeExpander_new> expander{ tenv };
+			const ast::Type * flat = tuple->accept( expander );
+			const ast::Type * flat2 = tuple2->accept( expander );
+
+			auto types = flatten( flat );
+			auto types2 = flatten( flat2 );
+
+			result = unifyList( types, types2, tenv, need, have, open, symtab );
+		}
+
+		void previsit( const ast::VarArgsType * ) {
+			visit_children = false;
+			result = dynamic_cast< const ast::VarArgsType * >( type2 );
+		}
+
+		void previsit( const ast::ZeroType * ) {
+			visit_children = false;
+			result = dynamic_cast< const ast::ZeroType * >( type2 );
+		}
+
+		void previsit( const ast::OneType * ) {
+			visit_children = false;
+			result = dynamic_cast< const ast::OneType * >( type2 );
+		}	
+
+	  private:
+		template< typename RefType > void handleRefType( RefType *inst, Type *other );
+		template< typename RefType > void handleGenericRefType( RefType *inst, Type *other );
+	};
+
+	bool unifyExact( 
+			const ast::Type * type1, const ast::Type * type2, ast::TypeEnvironment & env, 
+			ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & open, 
+			WidenMode widen, const ast::SymbolTable & symtab
+	) {
+		if ( type1->qualifiers != type2->qualifiers ) return false;
+
+		auto var1 = dynamic_cast< const ast::TypeInstType * >( type1 );
+		auto var2 = dynamic_cast< const ast::TypeInstType * >( type2 );
+		ast::OpenVarSet::const_iterator 
+			entry1 = var1 ? open.find( var1->name ) : open.end(), 
+			entry2 = var2 ? open.find( var2->name ) : open.end();
+		bool isopen1 = entry1 != open.end();
+		bool isopen2 = entry2 != open.end();
+
+		if ( isopen1 && isopen2 ) {
+			if ( entry1->second.kind != entry2->second.kind ) return false;
+			return env.bindVarToVar( 
+				var1, var2, ast::TypeDecl::Data{ entry1->second, entry2->second }, need, have, 
+				open, widen, symtab );
+		} else if ( isopen1 ) {
+			return env.bindVar( var1, type2, entry1->second, need, have, open, widen, symtab );
+		} else if ( isopen2 ) {
+			return env.bindVar( var2, type1, entry2->second, need, have, open, widen, symtab );
+		} else {
+			ast::Pass<Unify_new> comparator{ type2, env, need, have, open, widen, symtab };
+			type1->accept( comparator );
+			return comparator.pass.result;
+		}
+	}
+
+	bool unifyInexact( 
+			ast::ptr<ast::Type> & type1, ast::ptr<ast::Type> & type2, ast::TypeEnvironment & env, 
+			ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & open, 
+			WidenMode widen, const ast::SymbolTable & symtab, ast::ptr<ast::Type> & common 
+	) {
+		ast::CV::Qualifiers q1 = type1->qualifiers, q2 = type2->qualifiers;
+		
+		// force t1 and t2 to be cloned if their qualifiers must be stripped, so that type1 and 
+		// type2 are left unchanged; calling convention forces type{1,2}->strong_ref >= 1
+		ast::ptr<ast::Type> t1{ type1 }, t2{ type2 };
+		clear_qualifiers( t1 );
+		clear_qualifiers( t2 );
+		
+		if ( unifyExact( t1, t2, env, need, have, open, widen, symtab ) ) {
+			t1 = nullptr; t2 = nullptr; // release t1, t2 to avoid spurious clones
+
+			// if exact unification on unqualified types, try to merge qualifiers
+			if ( q1 == q2 || ( ( q1 > q2 || widen.first ) && ( q2 > q1 || widen.second ) ) ) {
+				common.set_and_mutate( type1 )->qualifiers = q1 | q2;
+				return true;
+			} else {
+				return false;
+			}
+
+		} else if (( common = commonType( t1, t2, widen, symtab, env, open ) )) {
+			t1 = nullptr; t2 = nullptr; // release t1, t2 to avoid spurious clones
+
+			// no exact unification, but common type
+			common.get_and_mutate()->qualifiers = q1 | q2;
+			return true;
+		} else {
+			return false;
+		}
+	}
+
 	ast::ptr<ast::Type> extractResultType( const ast::FunctionType * func ) {
 		if ( func->returns.empty() ) return new ast::VoidType{};
Index: src/ResolvExpr/Unify.h
===================================================================
--- src/ResolvExpr/Unify.h	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/Unify.h	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -18,4 +18,5 @@
 #include <list>                   // for list
 
+#include "AST/Node.hpp"             // for ptr
 #include "AST/TypeEnvironment.hpp"  // for TypeEnvironment, AssertionSet, OpenVarSet
 #include "Common/utility.h"       // for deleteAll
@@ -39,5 +40,5 @@
 	bool unify( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, OpenVarSet &openVars, const SymTab::Indexer &indexer, Type *&commonType );
 	bool unifyExact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, OpenVarSet &openVars, const SymTab::Indexer &indexer );
-	bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widenMode, const SymTab::Indexer &indexer, Type *&common );
+	bool unifyInexact( Type *type1, Type *type2, TypeEnvironment &env, AssertionSet &needAssertions, AssertionSet &haveAssertions, const OpenVarSet &openVars, WidenMode widen, const SymTab::Indexer &indexer, Type *&common );
 
 	template< typename Iterator1, typename Iterator2 >
@@ -68,8 +69,13 @@
 	}
 
+	bool unifyExact( 
+		const ast::Type * type1, const ast::Type * type2, ast::TypeEnvironment & env, 
+		ast::AssertionSet & need, ast::AssertionSet & have, ast::OpenVarSet & open, 
+		const ast::SymbolTable & symtab );
+
 	bool unifyInexact( 
-		const ast::Type * type1, const ast::Type * type2, ast::TypeEnvironment & env, 
-		ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & openVars, 
-		WidenMode widenMode, const ast::SymbolTable & symtab, const ast::Type *& common );
+		ast::ptr<ast::Type> & type1, ast::ptr<ast::Type> & type2, ast::TypeEnvironment & env, 
+		ast::AssertionSet & need, ast::AssertionSet & have, const ast::OpenVarSet & open, 
+		WidenMode widen, const ast::SymbolTable & symtab, ast::ptr<ast::Type> & common );
 
 } // namespace ResolvExpr
Index: src/ResolvExpr/WidenMode.h
===================================================================
--- src/ResolvExpr/WidenMode.h	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/WidenMode.h	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -18,12 +18,25 @@
 namespace ResolvExpr {
 	struct WidenMode {
-		WidenMode( bool widenFirst, bool widenSecond ): widenFirst( widenFirst ), widenSecond( widenSecond ) {}
-		WidenMode &operator|=( const WidenMode &other ) { widenFirst |= other.widenFirst; widenSecond |= other.widenSecond; return *this; }
-		WidenMode &operator&=( const WidenMode &other ) { widenFirst &= other.widenFirst; widenSecond &= other.widenSecond; return *this; }
-		WidenMode operator|( const WidenMode &other ) { WidenMode newWM( *this ); newWM |= other; return newWM; }
-		WidenMode operator&( const WidenMode &other ) { WidenMode newWM( *this ); newWM &= other; return newWM; }
-		operator bool() { return widenFirst && widenSecond; }
+		WidenMode( bool first, bool second ): first( first ), second( second ) {}
+		
+		WidenMode &operator|=( const WidenMode &other ) {
+			first |= other.first; second |= other.second; return *this;
+		}
 
-		bool widenFirst : 1, widenSecond : 1;
+		WidenMode &operator&=( const WidenMode &other ) {
+			first &= other.first; second &= other.second; return *this;
+		}
+
+		WidenMode operator|( const WidenMode &other ) {
+			WidenMode newWM( *this ); newWM |= other; return newWM;
+		}
+
+		WidenMode operator&( const WidenMode &other ) {
+			WidenMode newWM( *this ); newWM &= other; return newWM;
+		}
+		
+		operator bool() { return first && second; }
+
+		bool first : 1, second : 1;
 	};
 } // namespace ResolvExpr
Index: src/ResolvExpr/typeops.h
===================================================================
--- src/ResolvExpr/typeops.h	(revision 8d70648a1bc901be1455417052ead87a499b935b)
+++ src/ResolvExpr/typeops.h	(revision f474e917671c80fd81b2ffce8b4dac26709b333e)
@@ -18,4 +18,7 @@
 #include <vector>
 
+#include "Cost.h"
+#include "TypeEnvironment.h"
+#include "WidenMode.h"
 #include "AST/Fwd.hpp"
 #include "AST/Node.hpp"
@@ -26,6 +29,4 @@
 #include "SynTree/Type.h"
 #include "SymTab/Indexer.h"
-#include "Cost.h"
-#include "TypeEnvironment.h"
 
 namespace ResolvExpr {
@@ -117,4 +118,7 @@
 	// in CommonType.cc
 	Type * commonType( Type *type1, Type *type2, bool widenFirst, bool widenSecond, const SymTab::Indexer &indexer, TypeEnvironment &env, const OpenVarSet &openVars );
+	const ast::Type * commonType(
+		const ast::Type * type1, const ast::Type * type2, WidenMode widen, 
+		const ast::SymbolTable & symtab, ast::TypeEnvironment & env, const ast::OpenVarSet & open );
 
 	// in PolyCost.cc
@@ -141,5 +145,5 @@
 	const ast::Expr * referenceToRvalueConversion( const ast::Expr * expr, Cost & cost );
 
-	// flatten tuple type into list of types
+	/// flatten tuple type into list of types
 	template< typename OutputIterator >
 	void flatten( Type * type, OutputIterator out ) {
@@ -152,4 +156,25 @@
 		}
 	}
+
+	/// flatten tuple type into existing list of types
+	static inline void flatten( 
+		const ast::Type * type, std::vector< ast::ptr< ast::Type > > & out 
+	) {
+		if ( auto tupleType = dynamic_cast< const ast::TupleType * >( type ) ) {	
+			for ( const ast::Type * t : tupleType->types ) {
+				flatten( t, out );
+			}
+		} else {
+			out.emplace_back( type );
+		}
+	}
+
+	/// flatten tuple type into list of types
+	static inline std::vector< ast::ptr< ast::Type > > flatten( const ast::Type * type ) {
+		std::vector< ast::ptr< ast::Type > > out;
+		out.reserve( type->size() );
+		flatten( type, out );
+		return out;
+	}
 } // namespace ResolvExpr