Index: src/ResolvExpr/SatisfyAssertions.cpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.cpp	(revision 5b9a0ae38512f113ae8de71dd5f6eb8af77ebaaa)
+++ 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 );
 					}
 
