Index: src/ResolvExpr/AdjustExprType.cc
===================================================================
--- src/ResolvExpr/AdjustExprType.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/AdjustExprType.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -133,5 +133,5 @@
 		const ast::Type * postvisit( const ast::TypeInstType * inst ) {
 			// replace known function-type-variables with pointer-to-function
-			if ( const ast::EqvClass * eqvClass = tenv.lookup( inst->name ) ) {
+			if ( const ast::EqvClass * eqvClass = tenv.lookup( *inst ) ) {
 				if ( eqvClass->data.kind == ast::TypeDecl::Ftype ) {
 					return new ast::PointerType{ inst };
Index: src/ResolvExpr/CandidateFinder.cpp
===================================================================
--- src/ResolvExpr/CandidateFinder.cpp	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/CandidateFinder.cpp	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -212,7 +212,5 @@
 		// mark type variable and specialization cost of forall clause
 		convCost.incVar( function->forall.size() );
-		for ( const ast::TypeDecl * td : function->forall ) {
-			convCost.decSpec( td->assertions.size() );
-		}
+		convCost.decSpec( function->assertions.size() );
 
 		return convCost;
@@ -223,9 +221,9 @@
 		ast::AssertionSet & need
 	) {
-		for ( const ast::TypeDecl * tyvar : type->forall ) {
-			unifiableVars[ tyvar->name ] = ast::TypeDecl::Data{ tyvar };
-			for ( const ast::DeclWithType * assn : tyvar->assertions ) {
-				need[ assn ].isUsed = true;
-			}
+		for ( auto & tyvar : type->forall ) {
+			unifiableVars[ *tyvar ] = ast::TypeDecl::Data{ tyvar->base };
+		}
+		for ( auto & assn : type->assertions ) {
+			need[ assn ].isUsed = true;
 		}
 	}
@@ -953,5 +951,5 @@
 						auto inst = dynamic_cast< const ast::TypeInstType * >( funcResult )
 					) {
-						if ( const ast::EqvClass * clz = func->env.lookup( inst->name ) ) {
+						if ( const ast::EqvClass * clz = func->env.lookup( *inst ) ) {
 							if ( auto function = clz->bound.as< ast::FunctionType >() ) {
 								CandidateRef newFunc{ new Candidate{ *func } };
@@ -1077,5 +1075,5 @@
 			assert( toType );
 			toType = resolveTypeof( toType, symtab );
-			toType = SymTab::validateType( castExpr->location, toType, symtab );
+			// toType = SymTab::validateType( castExpr->location, toType, symtab );
 			toType = adjustExprType( toType, tenv, symtab );
 
@@ -1162,5 +1160,5 @@
 
 					if(auto insttype = dynamic_cast<const ast::TypeInstType*>(expr)) {
-						auto td = cand->env.lookup(insttype->name);
+						auto td = cand->env.lookup(*insttype);
 						if(!td) { continue; }
 						expr = td->bound.get();
@@ -1568,5 +1566,5 @@
 				// calculate target type
 				const ast::Type * toType = resolveTypeof( initAlt.type, symtab );
-				toType = SymTab::validateType( initExpr->location, toType, symtab );
+				// toType = SymTab::validateType( initExpr->location, toType, symtab );
 				toType = adjustExprType( toType, tenv, symtab );
 				// The call to find must occur inside this loop, otherwise polymorphic return
Index: src/ResolvExpr/CastCost.cc
===================================================================
--- src/ResolvExpr/CastCost.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/CastCost.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -202,5 +202,5 @@
 ) {
 	if ( auto typeInst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-		if ( const ast::EqvClass * eqvClass = env.lookup( typeInst->name ) ) {
+		if ( const ast::EqvClass * eqvClass = env.lookup( *typeInst ) ) {
 			// check cast cost against bound type, if present
 			if ( eqvClass->bound ) {
Index: src/ResolvExpr/CommonType.cc
===================================================================
--- src/ResolvExpr/CommonType.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/CommonType.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -713,5 +713,5 @@
 			const ast::Type * base = oPtr->base;
 			if ( auto var = dynamic_cast< const ast::TypeInstType * >( base ) ) {
-				auto entry = open.find( var->name );
+				auto entry = open.find( *var );
 				if ( entry != open.end() ) {
 					ast::AssertionSet need, have;
Index: src/ResolvExpr/ConversionCost.cc
===================================================================
--- src/ResolvExpr/ConversionCost.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/ConversionCost.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -498,5 +498,5 @@
 ) {
 	if ( const ast::TypeInstType * inst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-		if ( const ast::EqvClass * eqv = env.lookup( inst->name ) ) {
+		if ( const ast::EqvClass * eqv = env.lookup( *inst ) ) {
 			if ( eqv->bound ) {
 				return conversionCost(src, eqv->bound, srcIsLvalue, symtab, env );
@@ -675,9 +675,9 @@
 
 void ConversionCost_new::postvisit( const ast::TypeInstType * typeInstType ) {
-	if ( const ast::EqvClass * eqv = env.lookup( typeInstType->name ) ) {
+	if ( const ast::EqvClass * eqv = env.lookup( *typeInstType ) ) {
 		cost = costCalc( eqv->bound, dst, srcIsLvalue, symtab, env );
 	} else if ( const ast::TypeInstType * dstAsInst =
 			dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-		if ( typeInstType->name == dstAsInst->name ) {
+		if ( *typeInstType == *dstAsInst ) {
 			cost = Cost::zero;
 		}
Index: src/ResolvExpr/FindOpenVars.cc
===================================================================
--- src/ResolvExpr/FindOpenVars.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/FindOpenVars.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -112,16 +112,16 @@
 				// mark open/closed variables
 				if ( nextIsOpen ) {
-					for ( const ast::TypeDecl * decl : type->forall ) {
-						open[ decl->name ] = ast::TypeDecl::Data{ decl };
-						for ( const ast::DeclWithType * assert : decl->assertions ) {
-							need[ assert ].isUsed = false;
-						}
+					for ( auto & decl : type->forall ) {
+						open[ *decl ] = ast::TypeDecl::Data{ decl->base };
+					}
+					for ( auto & assert : type->assertions ) {
+						need[ assert ].isUsed = false;
 					}
 				} else {
-					for ( const ast::TypeDecl * decl : type->forall ) {
-						closed[ decl->name ] = ast::TypeDecl::Data{ decl };
-						for ( const ast::DeclWithType * assert : decl->assertions ) {
-							have[ assert ].isUsed = false;
-						}
+					for ( auto & decl : type->forall ) {
+						closed[ *decl ] = ast::TypeDecl::Data{ decl->base };	
+					}
+					for ( auto & assert : type->assertions ) {
+						have[ assert ].isUsed = false;
 					}
 				}
Index: src/ResolvExpr/PolyCost.cc
===================================================================
--- src/ResolvExpr/PolyCost.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/PolyCost.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -68,5 +68,5 @@
 
 	void previsit( const ast::TypeInstType * type ) {
-		if ( const ast::EqvClass * eqv = env_.lookup( type->name ) ) /* && */ if ( eqv->bound ) {
+		if ( const ast::EqvClass * eqv = env_.lookup( *type ) ) /* && */ if ( eqv->bound ) {
 			if ( const ast::TypeInstType * otherType = eqv->bound.as< ast::TypeInstType >() ) {
 				if ( symtab.lookupType( otherType->name ) ) {
Index: src/ResolvExpr/PtrsAssignable.cc
===================================================================
--- src/ResolvExpr/PtrsAssignable.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/PtrsAssignable.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -134,5 +134,5 @@
 	}
 	void postvisit( const ast::TypeInstType * inst ) {
-		if ( const ast::EqvClass * eqv = typeEnv.lookup( inst->name ) ) {
+		if ( const ast::EqvClass * eqv = typeEnv.lookup( *inst ) ) {
 			if ( eqv->bound ) {
 				// T * = S * for any S depends on the type bound to T
@@ -146,5 +146,5 @@
 		const ast::TypeEnvironment & env ) {
 	if ( const ast::TypeInstType * dstAsInst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-		if ( const ast::EqvClass * eqv = env.lookup( dstAsInst->name ) ) {
+		if ( const ast::EqvClass * eqv = env.lookup( *dstAsInst ) ) {
 			return ptrsAssignable( src, eqv->bound, env );
 		}
Index: src/ResolvExpr/PtrsCastable.cc
===================================================================
--- src/ResolvExpr/PtrsCastable.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/PtrsCastable.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -180,5 +180,5 @@
 					}
 				}
-			} else if ( const ast::EqvClass * eqvClass = env.lookup( inst->name ) ) {
+			} else if ( const ast::EqvClass * eqvClass = env.lookup( *inst ) ) {
 				if ( eqvClass->data.kind == ast::TypeDecl::Ftype ) {
 					return -1;
@@ -283,5 +283,5 @@
 ) {
 	if ( auto inst = dynamic_cast< const ast::TypeInstType * >( dst ) ) {
-		if ( const ast::EqvClass * eqvClass = env.lookup( inst->name ) ) {
+		if ( const ast::EqvClass * eqvClass = env.lookup( *inst ) ) {
 			return ptrsAssignable( src, eqvClass->bound, env );
 		}
Index: src/ResolvExpr/RenameVars.cc
===================================================================
--- src/ResolvExpr/RenameVars.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/RenameVars.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -19,5 +19,4 @@
 #include <utility>                 // for pair
 
-#include "AST/ForallSubstitutionTable.hpp"
 #include "AST/Pass.hpp"
 #include "AST/Type.hpp"
@@ -39,8 +38,10 @@
 		int level = 0;
 		int resetCount = 0;
+
+		int next_expr_id = 1;
+		int next_usage_id = 1;
 		ScopedMap< std::string, std::string > nameMap;
+		ScopedMap< std::string, ast::TypeInstType::TypeEnvKey > idMap;
 	public:
-		ast::ForallSubstitutionTable subs;
-
 		void reset() {
 			level = 0;
@@ -53,4 +54,8 @@
 				type->name = it->second;
 			}
+		}
+
+		void nextUsage() {
+			++next_usage_id;
 		}
 
@@ -78,13 +83,13 @@
 
 		const ast::TypeInstType * rename( const ast::TypeInstType * type ) {
-			// re-linking of base type handled by WithForallSubstitutor
-
 			// rename
-			auto it = nameMap.find( type->name );
-			if ( it != nameMap.end() ) {
-				// 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;
+			auto it = idMap.find( type->name );
+			if ( it != idMap.end() ) {
+				// unconditionally mutate because map will *always* have different name
+				ast::TypeInstType * mut = ast::shallowCopy( type );
+				// reconcile base node since some copies might have been made
+				mut->base = it->second.base;
+				mut->formal_usage = it->second.formal_usage;
+				mut->expr_id = it->second.expr_id;
 	            type = mut;
 			}
@@ -93,34 +98,38 @@
 		}
 
-		const ast::FunctionType * openLevel( const ast::FunctionType * type ) {
+		const ast::FunctionType * openLevel( const ast::FunctionType * type, RenameMode mode ) {
 			if ( type->forall.empty() ) return type;
-
-			nameMap.beginScope();
+			idMap.beginScope();
 
 			// Load new names from this forall clause and perform renaming.
-			auto mutType = ast::mutate( type );
-			assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
-			for ( ast::ptr< ast::TypeDecl > & td : mutType->forall ) {
-				assertf(dynamic_cast<ast::FunctionType *>(mutType), "renaming vars in non-function type");
-				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;
+			auto mutType = ast::shallowCopy( type );
+			// assert( type == mutType && "mutated type must be unique from ForallSubstitutor" );
+			for ( auto & td : mutType->forall ) {
+				auto mut = ast::shallowCopy( td.get() );
+				// assert( td == mutDecl && "mutated decl must be unique from ForallSubstitutor" );
+
+				if (mode == GEN_EXPR_ID) {
+					mut->expr_id = next_expr_id;
+					mut->formal_usage = -1;
+					++next_expr_id;
+				}
+				else if (mode == GEN_USAGE) {
+					assertf(mut->expr_id, "unfilled expression id in generating candidate type");
+					mut->formal_usage = next_usage_id;
+				}
+				else {
+					assert(false);
+				}
+				idMap[ td->name ] = ast::TypeInstType::TypeEnvKey(*mut);
+				
+				td = mut;
+			}
+
+			return mutType;
 		}
 
 		void closeLevel( const ast::FunctionType * type ) {
 			if ( type->forall.empty() ) return;
-
-			nameMap.endScope();
+			idMap.endScope();
 		}
 	};
@@ -142,10 +151,9 @@
 	};
 
-	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;
+	struct RenameVars_new : public ast::PureVisitor /*: public ast::WithForallSubstitutor*/ {
+		RenameMode mode;
 
 		const ast::FunctionType * previsit( const ast::FunctionType * type ) {
-			return renaming.openLevel( type );
+			return renaming.openLevel( type, mode );
 		}
 
@@ -163,4 +171,5 @@
 
 		const ast::TypeInstType * previsit( const ast::TypeInstType * type ) {
+			if (mode == GEN_USAGE && !type->formal_usage) return type; // do not rename an actual type
 			return renaming.rename( type );
 		}
@@ -177,9 +186,12 @@
 }
 
-const ast::Type * renameTyVars( const ast::Type * t ) {
-	ast::Type *tc = ast::deepCopy(t);
+const ast::Type * renameTyVars( const ast::Type * t, RenameMode mode ) {
+	// ast::Type *tc = ast::deepCopy(t);
 	ast::Pass<RenameVars_new> renamer;
-//	return t->accept( renamer );
-	return tc->accept( renamer );
+	renamer.core.mode = mode;
+	if (mode == GEN_USAGE) {
+		renaming.nextUsage();
+	}
+	return t->accept( renamer );
 }
 
Index: src/ResolvExpr/RenameVars.h
===================================================================
--- src/ResolvExpr/RenameVars.h	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/RenameVars.h	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -30,8 +30,15 @@
 	/// Provides a consistent renaming of forall type names in a hierarchy by prefixing them with a unique "level" ID
 	void renameTyVars( Type * );
-	const ast::Type * renameTyVars( const ast::Type * );
+
+	enum RenameMode {
+		GEN_USAGE, // for type in VariableExpr
+		GEN_EXPR_ID // for type in decl
+	};
+	const ast::Type * renameTyVars( const ast::Type *, RenameMode mode = GEN_USAGE );
 
 	/// resets internal state of renamer to avoid overflow
 	void resetTyVarRenaming();
+
+	
 } // namespace ResolvExpr
 
Index: src/ResolvExpr/ResolveTypeof.cc
===================================================================
--- src/ResolvExpr/ResolveTypeof.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/ResolveTypeof.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -15,4 +15,5 @@
 
 #include "ResolveTypeof.h"
+#include "RenameVars.h"
 
 #include <cassert>               // for assert
@@ -218,4 +219,5 @@
 			mutDecl->mangleName = Mangle::mangle(mutDecl); // do not mangle unnamed variables
 		
+		mutDecl->type = renameTyVars(mutDecl->type, RenameMode::GEN_EXPR_ID);
 		mutDecl->isTypeFixed = true;
 		return mutDecl;
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/Resolver.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -986,5 +986,4 @@
 		};
 	} // anonymous namespace
-
 	/// Check if this expression is or includes a deleted expression
 	const ast::DeletedExpr * findDeletedExpr( const ast::Expr * expr ) {
@@ -1375,15 +1374,17 @@
 			}
 
-			// handle assertions. (seems deep)
+			// handle assertions
 
 			symtab.enterScope();
-			for (auto & typeParam : mutType->forall) {
-				auto mutParam = typeParam.get_and_mutate();
-				symtab.addType(mutParam);
-				for (auto & asst : mutParam->assertions) {
-					asst = fixObjectType(asst.strict_as<ast::ObjectDecl>(), symtab);
-					symtab.addId(asst);
-				}
-				typeParam = mutParam;
+			mutType->forall.clear();
+			mutType->assertions.clear();
+			for (auto & typeParam : mutDecl->type_params) {
+				symtab.addType(typeParam);
+				mutType->forall.emplace_back(new ast::TypeInstType(typeParam->name, typeParam));
+			}
+			for (auto & asst : mutDecl->assertions) {
+				asst = fixObjectType(asst.strict_as<ast::ObjectDecl>(), symtab);
+				symtab.addId(asst);
+				mutType->assertions.emplace_back(new ast::VariableExpr(functionDecl->location, asst));
 			}
 
@@ -1407,4 +1408,6 @@
 			mutType->returns = std::move(returnTypes);
 
+			auto renamedType = strict_dynamic_cast<const ast::FunctionType *>(renameTyVars(mutType, RenameMode::GEN_EXPR_ID));
+
 			std::list<ast::ptr<ast::Stmt>> newStmts;
 			resolveWithExprs (mutDecl->withExprs, newStmts);
@@ -1418,4 +1421,5 @@
 			symtab.leaveScope();
 
+			mutDecl->type = renamedType;
 			mutDecl->mangleName = Mangle::mangle(mutDecl);
 			mutDecl->isTypeFixed = true;
Index: src/ResolvExpr/SatisfyAssertions.cpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.cpp	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/SatisfyAssertions.cpp	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -69,5 +69,5 @@
 	/// Reference to a single deferred item
 	struct DeferRef {
-		const ast::DeclWithType * decl;
+		const ast::VariableExpr * expr;
 		const ast::AssertionSetValue & info;
 		const AssnCandidate & match;
@@ -77,11 +77,11 @@
 	/// Acts like an indexed list of DeferRef
 	struct DeferItem {
-		const ast::DeclWithType * decl;
+		const ast::VariableExpr * expr;
 		const ast::AssertionSetValue & info;
 		AssnCandidateList matches;
 
 		DeferItem( 
-			const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
-		: decl( d ), info( i ), matches( std::move( ms ) ) {}
+			const ast::VariableExpr * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
+		: expr( d ), info( i ), matches( std::move( ms ) ) {}
 
 		bool empty() const { return matches.empty(); }
@@ -89,5 +89,5 @@
 		AssnCandidateList::size_type size() const { return matches.size(); }
 
-		DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+		DeferRef operator[] ( unsigned i ) const { return { expr, info, matches[i] }; }
 	};
 
@@ -138,5 +138,5 @@
 	void addToSymbolTable( const ast::AssertionSet & have, ast::SymbolTable & symtab ) {
 		for ( auto & i : have ) {
-			if ( i.second.isUsed ) { symtab.addId( i.first ); }
+			if ( i.second.isUsed ) { symtab.addId( i.first->var ); }
 		}
 	}
@@ -144,5 +144,5 @@
 	/// Binds a single assertion, updating satisfaction state
 	void bindAssertion( 
-		const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 
+		const ast::VariableExpr * expr, const ast::AssertionSetValue & info, CandidateRef & cand, 
 		AssnCandidate & match, InferCache & inferred
 	) {
@@ -156,6 +156,6 @@
 
 		// place newly-inferred assertion in proper location in cache
-		inferred[ info.resnSlot ][ decl->uniqueId ] = ast::ParamEntry{
-			candidate->uniqueId, candidate, match.adjType, decl->get_type(), varExpr };
+		inferred[ info.resnSlot ][ expr->var->uniqueId ] = ast::ParamEntry{
+			candidate->uniqueId, candidate, match.adjType, expr->result, varExpr };
 	}
 
@@ -169,8 +169,8 @@
 
 		std::vector<ast::SymbolTable::IdData> candidates;
-		auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->name);
+		auto kind = ast::SymbolTable::getSpecialFunctionKind(assn.first->var->name);
 		if (kind != ast::SymbolTable::SpecialFunctionKind::NUMBER_OF_KINDS) {
 			// prefilter special decls by argument type, if already known
-			ast::ptr<ast::Type> thisArgType = strict_dynamic_cast<const ast::PointerType *>(assn.first->get_type())->base
+			ast::ptr<ast::Type> thisArgType = assn.first->result.strict_as<ast::PointerType>()->base
 				.strict_as<ast::FunctionType>()->params[0]
 				.strict_as<ast::ReferenceType>()->base;
@@ -184,5 +184,5 @@
 		}
 		else {
-			candidates = sat.symtab.lookupId(assn.first->name);
+			candidates = sat.symtab.lookupId(assn.first->var->name);
 		}
 		for ( const ast::SymbolTable::IdData & cdata : candidates ) {
@@ -200,5 +200,5 @@
 			ast::TypeEnvironment newEnv{ sat.cand->env };
 			ast::OpenVarSet newOpen{ sat.cand->open };
-			ast::ptr< ast::Type > toType = assn.first->get_type();
+			ast::ptr< ast::Type > toType = assn.first->result;
 			ast::ptr< ast::Type > adjType = 
 				renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
@@ -337,5 +337,5 @@
 					// compute conversion cost from satisfying decl to assertion
 					cost += computeConversionCost(
-						assn.match.adjType, assn.decl->get_type(), false, symtab, env );
+						assn.match.adjType, assn.expr->result, false, symtab, env );
 
 					// mark vars+specialization on function-type assertions
@@ -350,7 +350,5 @@
 					cost.incVar( func->forall.size() );
 
-					for ( const ast::TypeDecl * td : func->forall ) {
-						cost.decSpec( td->assertions.size() );
-					}
+					cost.decSpec( func->assertions.size() );
 				}
 			}
@@ -451,5 +449,5 @@
 				ss << (tabs-1) << "Too many non-unique satisfying assignments for assertions:\n";
 				for ( const auto & d : sat.deferred ) {
-					ast::print( ss, d.decl, tabs );
+					ast::print( ss, d.expr, tabs );
 				}
 
@@ -469,5 +467,5 @@
 					ss << (tabs-1) << "No mutually-compatible satisfaction for assertions:\n";
 					for ( const auto& d : sat.deferred ) {
-						ast::print( ss, d.decl, tabs );
+						ast::print( ss, d.expr, tabs );
 					}
 
@@ -501,5 +499,5 @@
 						nextNewNeed.insert( match.need.begin(), match.need.end() );
 
-						bindAssertion( r.decl, r.info, nextCand, match, nextInferred );
+						bindAssertion( r.expr, r.info, nextCand, match, nextInferred );
 					}
 
Index: src/ResolvExpr/Unify.cc
===================================================================
--- src/ResolvExpr/Unify.cc	(revision 2dda05dc482e5dd5d6074e405c5d8c0c5e35654e)
+++ src/ResolvExpr/Unify.cc	(revision 3e5dd91354f39b161547cc1119ecef5890aa765f)
@@ -773,5 +773,5 @@
 
 			const ast::Type * postvisit( const ast::TypeInstType * typeInst ) {
-				if ( const ast::EqvClass * clz = tenv.lookup( typeInst->name ) ) {
+				if ( const ast::EqvClass * clz = tenv.lookup( *typeInst ) ) {
 					// expand ttype parameter into its actual type
 					if ( clz->data.kind == ast::TypeDecl::Ttype && clz->bound ) {
@@ -888,5 +888,5 @@
 		}
 
-		static void markAssertionSet( ast::AssertionSet & assns, const ast::DeclWithType * assn ) {
+		static void markAssertionSet( ast::AssertionSet & assns, const ast::VariableExpr * assn ) {
 			auto i = assns.find( assn );
 			if ( i != assns.end() ) {
@@ -900,9 +900,7 @@
 			const ast::FunctionType * type
 		) {
-			for ( const auto & tyvar : type->forall ) {
-				for ( const ast::DeclWithType * assert : tyvar->assertions ) {
-					markAssertionSet( assn1, assert );
-					markAssertionSet( assn2, assert );
-				}
+			for ( auto & assert : type->assertions ) {
+				markAssertionSet( assn1, assert );
+				markAssertionSet( assn2, assert );
 			}
 		}
@@ -1030,5 +1028,5 @@
 
 		void postvisit( const ast::TypeInstType * typeInst ) {
-			assert( open.find( typeInst->name ) == open.end() );
+			assert( open.find( *typeInst ) == open.end() );
 			handleRefType( typeInst, type2 );
 		}
@@ -1171,6 +1169,6 @@
 		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();
+			entry1 = var1 ? open.find( *var1 ) : open.end(),
+			entry2 = var2 ? open.find( *var2 ) : open.end();
 		bool isopen1 = entry1 != open.end();
 		bool isopen2 = entry2 != open.end();