Changeset f474e91 for src/ResolvExpr/Unify.cc

Timestamp:

Jun 3, 2019, 5:36:43 PM (5 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, arm-eh, ast-experimental, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

4ae2364

Parents:

8d70648

Message:

Port unification calculations to new AST

File:

• src/ResolvExpr/Unify.cc (modified) (28 diffs)

src/ResolvExpr/Unify.cc

@@ -14 +14 @@
 //
 
+#include "Unify.h"
+
 #include <cassert>                  // for assertf, assert
 #include <iterator>                 // for back_insert_iterator, back_inserter
@@ -23 +25 @@
 #include <vector>
 
+#include "AST/Decl.hpp"
 #include "AST/Node.hpp"
+#include "AST/Pass.hpp"
 #include "AST/Type.hpp"
 #include "AST/TypeEnvironment.hpp"
@@ -37 +41 @@
 #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 +55 @@
 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 +88 @@
                 AssertionSet &haveAssertions;
                 const OpenVarSet &openVars;
-                WidenMode widenMode;
+                WidenMode widen;
                 const SymTab::Indexer &indexer;
         };
@@ -87 +94 @@
         /// 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 +124 @@
                         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 +166 @@
                         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 +202 @@
         }
 
-        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 +229 @@
                                 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 +261 @@
         }
 
-        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 +273 @@
                 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 +293 @@
                 } 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 +311 @@
         }
 
-        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 +347 @@
         }
 
-        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 +355 @@
         }
 
-        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 +363 @@
         }
 
-        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 +443 @@
         /// 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 +464 @@
                 dst.clear();
                 for ( DeclarationWithType * dcl : src ) {
-                        PassVisitor<TtypeExpander> expander( env );
+                        PassVisitor<TtypeExpander_old> expander( env );
                         dcl->acceptMutator( expander );
                         std::list< Type * > types;
@@ -457 +479 @@
         }
 
-        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 +490 @@
 
                         // 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 +511 @@
 
         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 +518 @@
 
         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 +586 @@
         }
 
-        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 +657 @@
         }
 
-        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 +663 @@
                         std::list<Type *> types1, types2;
 
-                        PassVisitor<TtypeExpander> expander( env );
+                        PassVisitor<TtypeExpander_old> expander( env );
                         flat1->acceptMutator( expander );
                         flat2->acceptMutator( expander );
@@ -647 +674 @@
         }
 
-        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 +700 @@
         }
 
+        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{};