Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision 07de76bb7a0e1179ac6fb9bae0cb96e709315c84)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision 596fc4ad0bfcf63b10c655b945c772325da80ac9)
@@ -390,5 +390,5 @@
 
 	/// Limit to depth of recursion of assertion satisfaction
-	static const int recursionLimit = 4;
+	static const int recursionLimit = 7;
 	/// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
 	static const int deferLimit = 10;
Index: src/ResolvExpr/SatisfyAssertions.cpp
===================================================================
--- src/ResolvExpr/SatisfyAssertions.cpp	(revision 07de76bb7a0e1179ac6fb9bae0cb96e709315c84)
+++ src/ResolvExpr/SatisfyAssertions.cpp	(revision 596fc4ad0bfcf63b10c655b945c772325da80ac9)
@@ -57,8 +57,8 @@
 		ast::UniqueId resnSlot;          ///< Slot for any recursive assertion IDs
 
-		AssnCandidate( 
-			const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e, 
+		AssnCandidate(
+			const ast::SymbolTable::IdData c, const ast::Type * at, ast::TypeEnvironment && e,
 			ast::AssertionSet && h, ast::AssertionSet && n, ast::OpenVarSet && o, ast::UniqueId rs )
-		: cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ), 
+		: cdata( c ), adjType( at ), env( std::move( e ) ), have( std::move( h ) ),
 		  need( std::move( n ) ), open( std::move( o ) ), resnSlot( rs ) {}
 	};
@@ -73,6 +73,6 @@
 		const AssnCandidate & match;
 	};
-	
-	/// Wrapper for the deferred items from a single assertion satisfaction. 
+
+	/// Wrapper for the deferred items from a single assertion satisfaction.
 	/// Acts like an indexed list of DeferRef
 	struct DeferItem {
@@ -81,5 +81,5 @@
 		AssnCandidateList matches;
 
-		DeferItem( 
+		DeferItem(
 			const ast::DeclWithType * d, const ast::AssertionSetValue & i, AssnCandidateList && ms )
 		: decl( d ), info( i ), matches( std::move( ms ) ) {}
@@ -117,18 +117,18 @@
 		/// Initial satisfaction state for a candidate
 		SatState( CandidateRef & c, const ast::SymbolTable & syms )
-		: cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero }, 
+		: cand( c ), need(), newNeed(), deferred(), inferred(), costs{ Cost::zero },
 		  symtab( syms ) { need.swap( c->need ); }
-		
+
 		/// Update satisfaction state for next step after previous state
 		SatState( SatState && o, IterateFlag )
-		: cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(), 
-		  deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ), 
+		: cand( std::move( o.cand ) ), need( o.newNeed.begin(), o.newNeed.end() ), newNeed(),
+		  deferred(), inferred( std::move( o.inferred ) ), costs( std::move( o.costs ) ),
 		  symtab( o.symtab ) { costs.emplace_back( Cost::zero ); }
-		
+
 		/// Field-wise next step constructor
 		SatState(
-			CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs, 
+			CandidateRef && c, ast::AssertionSet && nn, InferCache && i, CostVec && cs,
 			ast::SymbolTable && syms )
-		: cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(), 
+		: cand( std::move( c ) ), need( nn.begin(), nn.end() ), newNeed(), deferred(),
 		  inferred( std::move( i ) ), costs( std::move( cs ) ), symtab( std::move( syms ) )
 		  { costs.emplace_back( Cost::zero ); }
@@ -143,12 +143,12 @@
 
 	/// Binds a single assertion, updating satisfaction state
-	void bindAssertion( 
-		const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand, 
+	void bindAssertion(
+		const ast::DeclWithType * decl, const ast::AssertionSetValue & info, CandidateRef & cand,
 		AssnCandidate & match, InferCache & inferred
 	) {
 		const ast::DeclWithType * candidate = match.cdata.id;
-		assertf( candidate->uniqueId, 
+		assertf( candidate->uniqueId,
 			"Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
-		
+
 		ast::Expr * varExpr = match.cdata.combine( cand->expr->location, cand->cvtCost );
 		varExpr->result = match.adjType;
@@ -175,5 +175,5 @@
 			ast::OpenVarSet newOpen{ sat.cand->open };
 			ast::ptr< ast::Type > toType = assn.first->get_type();
-			ast::ptr< ast::Type > adjType = 
+			ast::ptr< ast::Type > adjType =
 				renameTyVars( adjustExprType( candidate->get_type(), newEnv, sat.symtab ) );
 
@@ -187,6 +187,6 @@
 				}
 
-				matches.emplace_back( 
-					cdata, adjType, std::move( newEnv ), std::move( newNeed ), std::move( have ), 
+				matches.emplace_back(
+					cdata, adjType, std::move( newEnv ), std::move( newNeed ), std::move( have ),
 					std::move( newOpen ), crntResnSlot );
 			}
@@ -257,9 +257,9 @@
 	};
 
-	/// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning 
+	/// Replace ResnSlots with InferParams and add alternative to output list, if it meets pruning
 	/// threshold.
-	void finalizeAssertions( 
-		CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs, 
-		CandidateList & out 
+	void finalizeAssertions(
+		CandidateRef & cand, InferCache & inferred, PruneMap & thresholds, CostVec && costs,
+		CandidateList & out
 	) {
 		// prune if cheaper alternative for same key has already been generated
@@ -278,6 +278,6 @@
 	}
 
-	/// Combo iterator that combines candidates into an output list, merging their environments. 
-	/// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h` 
+	/// Combo iterator that combines candidates into an output list, merging their environments.
+	/// Rejects an appended candidate if environments cannot be merged. See `Common/FilterCombos.h`
 	/// for description of "combo iterator".
 	class CandidateEnvMerger {
@@ -299,6 +299,6 @@
 			Cost cost;
 
-			OutType( 
-				const ast::TypeEnvironment & e, const ast::OpenVarSet & o, 
+			OutType(
+				const ast::TypeEnvironment & e, const ast::OpenVarSet & o,
 				const std::vector< DeferRef > & as, const ast::SymbolTable & symtab )
 			: env( e ), open( o ), assns( as ), cost( Cost::zero ) {
@@ -306,9 +306,9 @@
 				for ( const DeferRef & assn : assns ) {
 					// compute conversion cost from satisfying decl to assertion
-					cost += computeConversionCost( 
+					cost += computeConversionCost(
 						assn.match.adjType, assn.decl->get_type(), symtab, env );
-					
+
 					// mark vars+specialization on function-type assertions
-					const ast::FunctionType * func = 
+					const ast::FunctionType * func =
 						GenPoly::getFunctionType( assn.match.cdata.id->get_type() );
 					if ( ! func ) continue;
@@ -317,7 +317,7 @@
 						cost.decSpec( specCost( param->get_type() ) );
 					}
-					
+
 					cost.incVar( func->forall.size() );
-					
+
 					for ( const ast::TypeDecl * td : func->forall ) {
 						cost.decSpec( td->assertions.size() );
@@ -329,6 +329,6 @@
 		};
 
-		CandidateEnvMerger( 
-			const ast::TypeEnvironment & env, const ast::OpenVarSet & open, 
+		CandidateEnvMerger(
+			const ast::TypeEnvironment & env, const ast::OpenVarSet & open,
 			const ast::SymbolTable & syms )
 		: crnt(), envs{ env }, opens{ open }, symtab( syms ) {}
@@ -357,11 +357,11 @@
 
 	/// Limit to depth of recursion of assertion satisfaction
-	static const int recursionLimit = 4;
+	static const int recursionLimit = 7;
 	/// Maximum number of simultaneously-deferred assertions to attempt concurrent satisfaction of
 	static const int deferLimit = 10;
 } // anonymous namespace
 
-void satisfyAssertions( 
-	CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out, 
+void satisfyAssertions(
+	CandidateRef & cand, const ast::SymbolTable & symtab, CandidateList & out,
 	std::vector<std::string> & errors
 ) {
@@ -408,5 +408,5 @@
 				// either add successful match or push back next state
 				if ( sat.newNeed.empty() ) {
-					finalizeAssertions( 
+					finalizeAssertions(
 						sat.cand, sat.inferred, thresholds, std::move( sat.costs ), out );
 				} else {
@@ -430,5 +430,5 @@
 				std::vector< CandidateEnvMerger::OutType > compatible = filterCombos(
 					sat.deferred, CandidateEnvMerger{ sat.cand->env, sat.cand->open, sat.symtab } );
-				
+
 				// fail early if no mutually-compatible assertion satisfaction
 				if ( compatible.empty() ) {
@@ -453,5 +453,5 @@
 					// set up next satisfaction state
 					CandidateRef nextCand = std::make_shared<Candidate>(
-						sat.cand->expr, std::move( compat.env ), std::move( compat.open ), 
+						sat.cand->expr, std::move( compat.env ), std::move( compat.open ),
 						ast::AssertionSet{} /* need moved into satisfaction state */,
 						sat.cand->cost, sat.cand->cvtCost );
@@ -459,8 +459,8 @@
 					ast::AssertionSet nextNewNeed{ sat.newNeed };
 					InferCache nextInferred{ sat.inferred };
-					
+
 					CostVec nextCosts{ sat.costs };
 					nextCosts.back() += compat.cost;
-								
+
 					ast::SymbolTable nextSymtab{ sat.symtab };
 
@@ -476,10 +476,10 @@
 					// either add successful match or push back next state
 					if ( nextNewNeed.empty() ) {
-						finalizeAssertions( 
+						finalizeAssertions(
 							nextCand, nextInferred, thresholds, std::move( nextCosts ), out );
 					} else {
-						nextSats.emplace_back( 
-							std::move( nextCand ), std::move( nextNewNeed ), 
-							std::move( nextInferred ), std::move( nextCosts ), 
+						nextSats.emplace_back(
+							std::move( nextCand ), std::move( nextNewNeed ),
+							std::move( nextInferred ), std::move( nextCosts ),
 							std::move( nextSymtab ) );
 					}
@@ -493,5 +493,5 @@
 		nextSats.clear();
 	}
-	
+
 	// exceeded recursion limit if reaches here
 	if ( out.empty() ) {