Index: src/ResolvExpr/RenameVars.cc
===================================================================
--- src/ResolvExpr/RenameVars.cc	(revision 09867ec142e286bf62a9931b33bc4405e86de912)
+++ src/ResolvExpr/RenameVars.cc	(revision 7583c027898ebc37d8fd806c221f4dfba3d9e80b)
@@ -186,9 +186,9 @@
 }
 
-const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode ) {
+const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode, bool reset ) {
 	// ast::Type *tc = ast::deepCopy(t);
 	ast::Pass<RenameVars_new> renamer;
 	renamer.core.mode = mode;
-	if (mode == GEN_USAGE) {
+	if (mode == GEN_USAGE && reset) {
 		renaming.nextUsage();
 	}
@@ -198,4 +198,5 @@
 void resetTyVarRenaming() {
 	renaming.reset();
+	renaming.nextUsage();
 }
 
Index: src/ResolvExpr/RenameVars.h
===================================================================
--- src/ResolvExpr/RenameVars.h	(revision 09867ec142e286bf62a9931b33bc4405e86de912)
+++ src/ResolvExpr/RenameVars.h	(revision 7583c027898ebc37d8fd806c221f4dfba3d9e80b)
@@ -35,5 +35,6 @@
 		GEN_EXPR_ID // for type in decl
 	};
-	const ast::Type * renameTyVars( const ast::Type *, RenameMode mode = GEN_USAGE );
+	const ast::Type * renameTyVars( const ast::Type *, RenameMode mode = GEN_USAGE, bool reset = true );
+	
 
 	/// resets internal state of renamer to avoid overflow
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision 09867ec142e286bf62a9931b33bc4405e86de912)
+++ src/ResolvExpr/Resolver.cc	(revision 7583c027898ebc37d8fd806c221f4dfba3d9e80b)
@@ -1151,5 +1151,4 @@
 			const ast::Expr * untyped, const ast::SymbolTable & symtab
 		) {
-			resetTyVarRenaming();
 			ast::TypeEnvironment env;
 			ast::ptr< ast::Expr > newExpr = resolveInVoidContext( untyped, symtab, env );
Index: src/ResolvExpr/SatisfyAssertions.cpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.cpp	(revision 09867ec142e286bf62a9931b33bc4405e86de912)
+++ src/ResolvExpr/SatisfyAssertions.cpp	(revision 7583c027898ebc37d8fd806c221f4dfba3d9e80b)
@@ -202,5 +202,5 @@
 			ast::ptr< ast::Type > toType = assn.first->result;
 			ast::ptr< ast::Type > adjType = 
-				renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
+				renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ), GEN_USAGE, false );
 
 			// only keep candidates which unify
@@ -417,8 +417,20 @@
 			if ( it != thresholds.end() && it->second < sat.costs ) goto nextSat;
 
-			// make initial pass at matching assertions
-			for ( auto & assn : sat.need ) {
-				// fail early if any assertion is not satisfiable
-				if ( ! satisfyAssertion( assn, sat ) ) {
+			// should a limit be imposed? worst case here is O(n^2) but very unlikely to happen.
+			for (unsigned resetCount = 0; ; ++resetCount) { 
+				ast::AssertionList next;
+				resetTyVarRenaming();
+				// make initial pass at matching assertions
+				for ( auto & assn : sat.need ) {
+					// fail early if any assertion is not satisfiable
+					if ( ! satisfyAssertion( assn, sat ) ) {
+						next.emplace_back(assn);
+						// goto nextSat;
+					}
+				}
+				// success
+				if (next.empty()) break;
+				// fail if nothing resolves
+				else if (next.size() == sat.need.size()) {
 					Indenter tabs{ 3 };
 					std::ostringstream ss;
@@ -426,9 +438,10 @@
 					print( ss, *sat.cand, ++tabs );
 					ss << (tabs-1) << "Could not satisfy assertion:\n";
-					ast::print( ss, assn.first, tabs );
+					ast::print( ss, next[0].first, tabs );
 
 					errors.emplace_back( ss.str() );
 					goto nextSat;
 				}
+				sat.need = std::move(next);
 			}