Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision 052cd7138ff5b8149b63ee8fba41fa31770761c4)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision 768b3b4fc6eef10132c548773dc967965b9aeff5)
@@ -155,4 +155,18 @@
 					k += computeConversionCost( 
 						assn.match.adjType, assn.decl->get_type(), indexer, x.env );
+					
+					// mark vars+specialization cost on function-type assertions
+					PointerType* ptr = dynamic_cast< PointerType* >( assn.decl->get_type() );
+					if ( ! ptr ) continue;
+					FunctionType* func = dynamic_cast< FunctionType* >( ptr->base );
+					if ( ! func ) continue;
+					
+					for ( DeclarationWithType* formal : func->parameters ) {
+						k.decSpec( specCost( formal->get_type() ) );
+					}
+					k.incVar( func->forall.size() );
+					for ( TypeDecl* td : func->forall ) {
+						k.decSpec( td->assertions.size() );
+					}
 				}
 				it = cache.emplace_hint( it, &x, k );