Index: src/ResolvExpr/CandidateFinder.cpp
===================================================================
--- src/ResolvExpr/CandidateFinder.cpp	(revision 6be3b7d6ed5a2dcd01f8b0e3c15be17e81544fe5)
+++ src/ResolvExpr/CandidateFinder.cpp	(revision e0e9a0be9170b7c4033834533d5ce2734166eb97)
@@ -548,5 +548,5 @@
 		genStart = genEnd;
 
-		return genEnd != results.size();
+		return genEnd != results.size();  // were any new results added?
 	}
 
@@ -677,6 +677,6 @@
 			ast::TypeEnvironment funcEnv{ func->env };
 			makeUnifiableVars( funcType, funcOpen, funcNeed );
-			// add all type variables as open variables now so that those not used in the parameter 
-			// list are still considered open
+			// add all type variables as open variables now so that those not used in the 
+			// parameter list are still considered open
 			funcEnv.add( funcType->forall );
 
Index: src/ResolvExpr/RenameVars.cc
===================================================================
--- src/ResolvExpr/RenameVars.cc	(revision 6be3b7d6ed5a2dcd01f8b0e3c15be17e81544fe5)
+++ src/ResolvExpr/RenameVars.cc	(revision e0e9a0be9170b7c4033834533d5ce2734166eb97)
@@ -19,4 +19,5 @@
 #include <utility>                 // for pair
 
+#include "AST/ForallSubstitutionTable.hpp"
 #include "AST/Pass.hpp"
 #include "AST/Type.hpp"
@@ -37,6 +38,7 @@
 		int resetCount = 0;
 		ScopedMap< std::string, std::string > nameMap;
+	public:
+		ast::ForallSubstitutionTable subs;
 
-	public:
 		void reset() {
 			level = 0;
@@ -44,8 +46,6 @@
 		}
 
-		using mapConstIterator = ScopedMap< std::string, std::string >::const_iterator;
-
 		void rename( TypeInstType * type ) {
-			mapConstIterator it = nameMap.find( type->name );
+			auto it = nameMap.find( type->name );
 			if ( it != nameMap.end() ) {
 				type->name = it->second;
@@ -65,7 +65,6 @@
 					// ditto for assertion names, the next level in
 					level++;
-					// acceptAll( td->assertions, *this );
-				} // for
-			} // if
+				}
+			}
 		}
 
@@ -77,10 +76,16 @@
 
 		const ast::TypeInstType * rename( const ast::TypeInstType * type ) {
-			mapConstIterator it = nameMap.find( type->name );
+			// re-linking of base type handled by WithForallSubstitutor
+
+			// rename
+			auto it = nameMap.find( type->name );
 			if ( it != nameMap.end() ) {
-				ast::TypeInstType * mutType = ast::mutate( type );
-				mutType->name = it->second;
-	            type = mutType;
+				// unconditionally mutate because map will *always* have different name, 
+				// if this mutates, will *always* have been mutated by ForallSubstitutor above
+				ast::TypeInstType * mut = ast::mutate( type );
+				mut->name = it->second;
+	            type = mut;
 			}
+
 			return type;
 		}
@@ -88,29 +93,32 @@
 		template<typename NodeT>
 		const NodeT * openLevel( const NodeT * type ) {
-			if ( !type->forall.empty() ) {
-				nameMap.beginScope();
-				// Load new names from this forall clause and perform renaming.
-				NodeT * mutType = ast::mutate( type );
-				for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
-					std::ostringstream output;
-					output << "_" << resetCount << "_" << level << "_" << td->name;
-					std::string newname( output.str() );
-					nameMap[ td->name ] = newname;
-					++level;
+			if ( type->forall.empty() ) return type;
+			
+			nameMap.beginScope();
 
-					ast::TypeDecl * decl = ast::mutate( td.get() );
-					decl->name = newname;
-					td = decl;
-				}
+			// Load new names from this forall clause and perform renaming.
+			NodeT * mutType = ast::mutate( type );
+			assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
+			for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
+				std::ostringstream output;
+				output << "_" << resetCount << "_" << level << "_" << td->name;
+				std::string newname =  output.str();
+				nameMap[ td->name ] = newname;
+				++level;
+
+				ast::TypeDecl * mutDecl = ast::mutate( td.get() );
+				assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" );
+				mutDecl->name = newname;
+				// assertion above means `td = mutDecl;` is unnecessary
 			}
+			// assertion above means `type = mutType;` is unnecessary
+
 			return type;
 		}
 
-		template<typename NodeT>
-		const NodeT * closeLevel( const NodeT * type ) {
-			if ( !type->forall.empty() ) {
-				nameMap.endScope();
-			}
-			return type;
+		void closeLevel( const ast::ParameterizedType * type ) {
+			if ( type->forall.empty() ) return;
+			
+			nameMap.endScope();
 		}
 	};
@@ -119,5 +127,5 @@
 	RenamingData renaming;
 
-	struct RenameVars {
+	struct RenameVars_old {
 		void previsit( TypeInstType * instType ) {
 			renaming.openLevel( (Type*)instType );
@@ -130,4 +138,9 @@
 			renaming.closeLevel( type );
 		}
+	};
+	
+	struct RenameVars_new /*: public ast::WithForallSubstitutor*/ {
+		#warning when old RenameVars goes away, replace hack below with global pass inheriting from WithForallSubstitutor
+		ast::ForallSubstitutionTable & subs = renaming.subs;
 
 		const ast::FunctionType * previsit( const ast::FunctionType * type ) {
@@ -146,6 +159,6 @@
 			return renaming.rename( renaming.openLevel( type ) );
 		}
-		const ast::ParameterizedType * postvisit( const ast::ParameterizedType * type ) {
-			return renaming.closeLevel( type );
+		void postvisit( const ast::ParameterizedType * type ) {
+			renaming.closeLevel( type );
 		}
 	};
@@ -154,10 +167,10 @@
 
 void renameTyVars( Type * t ) {
-	PassVisitor<RenameVars> renamer;
+	PassVisitor<RenameVars_old> renamer;
 	t->accept( renamer );
 }
 
 const ast::Type * renameTyVars( const ast::Type * t ) {
-	ast::Pass<RenameVars> renamer;
+	ast::Pass<RenameVars_new> renamer;
 	return t->accept( renamer );
 }