Index: src/GenPoly/Box.cc
===================================================================
--- src/GenPoly/Box.cc	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/GenPoly/Box.cc	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -798,6 +798,6 @@
 			for ( Type::ForallList::iterator tyVar = functionType->get_forall().begin(); tyVar != functionType->get_forall().end(); ++tyVar ) {
 				for ( std::list< DeclarationWithType *>::iterator assert = (*tyVar)->assertions.begin(); assert != (*tyVar)->assertions.end(); ++assert ) {
-					InferredParams::const_iterator inferParam = appExpr->get_inferParams().find( (*assert)->get_uniqueId() );
-					assertf( inferParam != appExpr->get_inferParams().end(), "addInferredParams missing inferred parameter: %s in: %s", toString( *assert ).c_str(), toString( appExpr ).c_str() );
+					InferredParams::const_iterator inferParam = appExpr->inferParams.find( (*assert)->get_uniqueId() );
+					assertf( inferParam != appExpr->inferParams.end(), "addInferredParams missing inferred parameter: %s in: %s", toString( *assert ).c_str(), toString( appExpr ).c_str() );
 					Expression *newExpr = inferParam->second.expr->clone();
 					addCast( newExpr, (*assert)->get_type(), tyVars );
Index: src/GenPoly/Specialize.cc
===================================================================
--- src/GenPoly/Specialize.cc	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/GenPoly/Specialize.cc	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -245,5 +245,5 @@
 		appExpr->env = TypeSubstitution::newFromExpr( appExpr, env );
 		if ( inferParams ) {
-			appExpr->get_inferParams() = *inferParams;
+			appExpr->inferParams = *inferParams;
 		} // if
 
@@ -284,5 +284,5 @@
 		std::list< Expression* >::iterator actual;
 		for ( formal = function->get_parameters().begin(), actual = appExpr->get_args().begin(); formal != function->get_parameters().end() && actual != appExpr->get_args().end(); ++formal, ++actual ) {
-			*actual = doSpecialization( (*formal)->get_type(), *actual, &appExpr->get_inferParams() );
+			*actual = doSpecialization( (*formal)->get_type(), *actual, &appExpr->inferParams );
 		}
 	}
@@ -295,6 +295,6 @@
 			// alternatively, if order starts to matter then copy appExpr's inferParams and pass them to handleExplicitParams.
 			handleExplicitParams( appExpr );
-			for ( InferredParams::iterator inferParam = appExpr->get_inferParams().begin(); inferParam != appExpr->get_inferParams().end(); ++inferParam ) {
-				inferParam->second.expr = doSpecialization( inferParam->second.formalType, inferParam->second.expr, inferParam->second.inferParams.get() );
+			for ( InferredParams::iterator inferParam = appExpr->inferParams.begin(); inferParam != appExpr->inferParams.end(); ++inferParam ) {
+				inferParam->second.expr = doSpecialization( inferParam->second.formalType, inferParam->second.expr, &inferParam->second.expr->inferParams );
 			}
 		}
Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -114,7 +114,7 @@
 		template<typename OutputIterator>
 		void makeFunctionAlternatives( const Alternative &func, FunctionType *funcType, const ExplodedArgs& args, OutputIterator out );
-		/// Checks if assertion parameters match for a new alternative
+		/// Sets up parameter inference for an output alternative
 		template< typename OutputIterator >
-		void inferParameters( const AssertionSet &need, AssertionSet &have, const Alternative &newAlt, OpenVarSet &openVars, OutputIterator out );
+		void inferParameters( Alternative &newAlt, OutputIterator out );
 	private:
 		AlternativeFinder & altFinder;
@@ -486,5 +486,5 @@
 
 		// xxx -- replace with new costs in resolver
-		for ( InferredParams::const_iterator assert = appExpr->get_inferParams().begin(); assert != appExpr->get_inferParams().end(); ++assert ) {
+		for ( InferredParams::const_iterator assert = appExpr->inferParams.begin(); assert != appExpr->inferParams.end(); ++assert ) {
 			convCost += computeConversionCost( assert->second.actualType, assert->second.formalType, indexer, alt.env );
 		}
@@ -595,5 +595,5 @@
 // 				)
 // 				// follow the current assertion's ID chain to find the correct set of inferred parameters to add the candidate to (i.e. the set of inferred parameters belonging to the entity which requested the assertion parameter).
-// 				InferredParams * inferParameters = &newerAlt.expr->get_inferParams();
+// 				InferredParams * inferParameters = &newerAlt.expr->inferParams;
 // 				for ( UniqueId id : cur->second.idChain ) {
 // 					inferParameters = (*inferParameters)[ id ].inferParams.get();
@@ -608,6 +608,9 @@
 // 	}
 
+	/// Unique identifier for matching expression resolutions to their requesting expression
+	UniqueId globalResnSlot = 0;
+
 	template< typename OutputIterator >
-	void AlternativeFinder::Finder::inferParameters( const AssertionSet &, AssertionSet &, const Alternative &newAlt, OpenVarSet &, OutputIterator out ) {
+	void AlternativeFinder::Finder::inferParameters( Alternative &newAlt, OutputIterator out ) {
 		// SymTab::Indexer decls( indexer );
 		// addToIndexer( have, decls );
@@ -621,5 +624,18 @@
 		// inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, 0, indexer, out );
 
-		// add to output list, assertion resolution is defered
+		// Set need bindings for any unbound assertions
+		UniqueId crntResnSlot = 0;  // matching ID for this expression's assertions
+		for ( auto& assn : newAlt.need ) {
+			// skip already-matched assertions
+			if ( assn.info.resnSlot != 0 ) continue;
+			// assign slot for expression if needed
+			if ( crntResnSlot == 0 ) { crntResnSlot = ++globalResnSlot; }
+			// fix slot to assertion
+			assn.info.resnSlot = crntResnSlot;
+		}
+		// pair slot to expression
+		if ( crntResnSlot != 0 ) { newAlt.expr->resnSlots.push_back( crntResnSlot ); }
+
+		// add to output list, assertion resolution is deferred
 		*out++ = newAlt;
 	}
@@ -969,5 +985,5 @@
 			printAssertionSet( result.need, std::cerr, 8 );
 		)
-		inferParameters( result.need, result.have, newAlt, result.openVars, out );
+		inferParameters( newAlt, out );
 	}
 
@@ -1330,6 +1346,5 @@
 					restructureCast( alt.expr->clone(), toType, castExpr->isGenerated ), 
 					alt.env, openVars, needAssertions, alt.cost, thisCost };
-				inferParameters( needAssertions, haveAssertions, newAlt, openVars,
-					back_inserter( candidates ) );
+				inferParameters( newAlt, back_inserter( candidates ) );
 			} // if
 		} // for
@@ -1639,5 +1654,5 @@
 							newExpr, std::move(compositeEnv), std::move(openVars), 
 							AssertionList( need.begin(), need.end() ), cost };
-						inferParameters( need, have, newAlt, openVars, back_inserter( alternatives ) );
+						inferParameters( newAlt, back_inserter( alternatives ) );
 					} // if
 				} // for
@@ -1686,5 +1701,5 @@
 						newExpr, std::move(compositeEnv), std::move(openVars), 
 						AssertionList( need.begin(), need.end() ), first.cost + second.cost };
-					inferParameters( need, have, newAlt, openVars, back_inserter( alternatives ) );
+					inferParameters( newAlt, back_inserter( alternatives ) );
 				} // if
 			} // for
@@ -1814,5 +1829,5 @@
 						std::move(newEnv), std::move(openVars), 
 						AssertionList( need.begin(), need.end() ), alt.cost, thisCost };
-					inferParameters( need, have, newAlt, openVars, back_inserter( candidates ) );
+					inferParameters( newAlt, back_inserter( candidates ) );
 				}
 			}
Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -18,12 +18,13 @@
 #include <cassert>                // for assertf
 #include <list>                   // for list
-#include <unordered_map>          // for unordered_map
+#include <unordered_map>          // for unordered_map, unordered_multimap
 #include <utility>                // for move
 #include <vector>                 // for vector
 
-#include "Alternative.h"          // for Alternative, AssertionItem
+#include "Alternative.h"          // for Alternative, AssertionItem, AssertionList
 #include "Common/FilterCombos.h"  // for filterCombos
 #include "Common/utility.h"       // for sort_mins
 #include "SymTab/Indexer.h"       // for Indexer
+#include "SynTree/Expression.h"   // for InferredParams
 #include "TypeEnvironment.h"      // for TypeEnvironment, etc.
 #include "typeops.h"              // for adjustExprType
@@ -39,9 +40,10 @@
 		AssertionSet need;              ///< Post-unification need-set
 		OpenVarSet openVars;            ///< Post-unification open-var set
+		UniqueId resnSlot;              ///< Slot for any recursive assertion IDs
 
 		AssnCandidate( const SymTab::Indexer::IdData& cdata, Type* adjType, TypeEnvironment&& env, 
-			AssertionSet&& have, AssertionSet&& need, OpenVarSet&& openVars ) 
+			AssertionSet&& have, AssertionSet&& need, OpenVarSet&& openVars, UniqueId resnSlot ) 
 		: cdata(cdata), adjType(adjType), env(std::move(env)), have(std::move(have)), 
-			need(std::move(need)), openVars(std::move(openVars)) {}
+			need(std::move(need)), openVars(std::move(openVars)), resnSlot(resnSlot) {}
 	};
 
@@ -159,4 +161,7 @@
 	};
 
+	/// Set of assertion resolutions, grouped by resolution ID
+	using InferCache = std::unordered_map< UniqueId, InferredParams >;
+
 	/// Flag for state iteration
 	enum IterateFlag { IterateState };
@@ -164,13 +169,14 @@
 	/// State needed to resolve a set of assertions
 	struct ResnState {
-		Alternative alt;                  ///< Alternative assertion is rooted on
-		std::vector<AssertionItem> need;  ///< Assertions to find
-		AssertionSet newNeed;             ///< New assertions for current resolutions
-		DeferList deferred;               ///< Deferred matches
-		SymTab::Indexer& indexer;         ///< Name lookup (depends on previous assertions)
+		Alternative alt;           ///< Alternative assertion is rooted on
+		AssertionList need;        ///< Assertions to find
+		AssertionSet newNeed;      ///< New assertions for current resolutions
+		DeferList deferred;        ///< Deferred matches
+		InferCache inferred;       ///< Cache of already-inferred parameters
+		SymTab::Indexer& indexer;  ///< Name lookup (depends on previous assertions)
 
 		/// Initial resolution state for an alternative
 		ResnState( Alternative& a, SymTab::Indexer& indexer )
-		: alt(a), need(), newNeed(), deferred(), indexer(indexer) {
+		: alt(a), need(), newNeed(), deferred(), inferred(), indexer(indexer) {
 			need.swap( a.need );
 		}
@@ -179,10 +185,10 @@
 		ResnState( ResnState&& o, IterateFlag )
 		: alt(std::move(o.alt)), need(o.newNeed.begin(), o.newNeed.end()), newNeed(), deferred(), 
-		  indexer(o.indexer) {}
+		  inferred(std::move(o.inferred)), indexer(o.indexer) {}
 	};
 
 	/// Binds a single assertion, updating resolution state
 	void bindAssertion( const DeclarationWithType* decl, AssertionSetValue info, Alternative& alt, 
-			AssnCandidate& match ) {
+			AssnCandidate& match, InferCache& inferred ) {
 		
 		DeclarationWithType* candidate = match.cdata.id;
@@ -192,15 +198,20 @@
 		delete varExpr->result;
 		varExpr->result = match.adjType->clone();
-
-		// follow the current assertion's ID chain to find the correct set of inferred parameters 
-		// to add the candidate o (i.e. the set of inferred parameters belonging to the entity 
-		// which requested the assertion parameter)
-		InferredParams* inferParams = &alt.expr->inferParams;
-		for ( UniqueId id : info.idChain ) {
-			inferParams = (*inferParams)[ id ].inferParams.get();
-		}
-
-		(*inferParams)[ decl->get_uniqueId() ] = ParamEntry{
+		if ( match.resnSlot ) { varExpr->resnSlots.push_back( match.resnSlot ); }
+
+		// place newly-inferred assertion in proper place in cache
+		inferred[ info.resnSlot ][ decl->get_uniqueId() ] = ParamEntry{
 				candidate->get_uniqueId(), match.adjType, decl->get_type()->clone(), varExpr };
+
+		// // follow the current assertion's ID chain to find the correct set of inferred parameters 
+		// // to add the candidate o (i.e. the set of inferred parameters belonging to the entity 
+		// // which requested the assertion parameter)
+		// InferredParams* inferParams = &alt.expr->inferParams;
+		// for ( UniqueId id : info.idChain ) {
+		// 	inferParams = (*inferParams)[ id ].inferParams.get();
+		// }
+
+		// (*inferParams)[ decl->get_uniqueId() ] = ParamEntry{
+		// 		candidate->get_uniqueId(), match.adjType, decl->get_type()->clone(), varExpr };
 	}
 
@@ -214,4 +225,7 @@
 	}
 
+	// in AlternativeFinder.cc; unique ID for assertion resolutions
+	extern UniqueId globalResnSlot;
+
 	/// Resolve a single assertion, in context
 	bool resolveAssertion( AssertionItem& assn, ResnState& resn ) {
@@ -238,12 +252,20 @@
 			if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 
 					resn.indexer ) ) {
-				// set up idChain on new assertions
-				for ( auto& a : newNeed ) {
-					a.second.idChain = assn.info.idChain;
-					a.second.idChain.push_back( assn.decl->get_uniqueId() );
+				// set up binding slot for recursive assertions
+				UniqueId crntResnSlot = 0;
+				if ( ! newNeed.empty() ) {
+					crntResnSlot = ++globalResnSlot;
+					for ( auto& a : newNeed ) {
+						a.second.resnSlot = crntResnSlot;
+					}
 				}
+				// // set up idChain on new assertions
+				// for ( auto& a : newNeed ) {
+				// 	a.second.idChain = assn.info.idChain;
+				// 	a.second.idChain.push_back( assn.decl->get_uniqueId() );
+				// }
 
 				matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 
-					std::move(newNeed), std::move(newOpenVars) );
+					std::move(newNeed), std::move(newOpenVars), crntResnSlot );
 			} else {
 				delete adjType;
@@ -267,9 +289,42 @@
 		resn.alt.openVars = std::move(match.openVars);
 
-		bindAssertion( assn.decl, assn.info, resn.alt, match );
+		bindAssertion( assn.decl, assn.info, resn.alt, match, resn.inferred );
 		return true;
 	}
 
-	///< Limit to depth of recursion of assertion satisfaction
+	/// Associates inferred parameters with an expression
+	struct InferMatcher {
+		InferCache& inferred;
+
+		InferMatcher( InferCache& inferred ) : inferred( inferred ) {}
+
+		Expression* postmutate( Expression* expr ) {
+			// place inferred parameters into resolution slots
+			for ( UniqueId slot : expr->resnSlots ) {
+				// fail if no matching parameters found
+				InferredParams& inferParams = inferred.at( slot );
+				
+				// place inferred parameters into proper place in expression
+				for ( auto& entry : inferParams ) {
+					// recurse on inferParams of resolved expressions
+					entry.second.expr = postmutate( entry.second.expr );
+					// xxx - look at entry.second.inferParams?
+					expr->inferParams[ entry.first ] = entry.second;
+				}
+			}
+
+			// clear resolution slots and return
+			expr->resnSlots.clear();
+			return expr;
+		}
+	};
+
+	void finalizeAssertions( Alternative& alt, InferCache& inferred, AltList& out ) {
+		PassVisitor<InferMatcher> matcher{ inferred };
+		alt.expr = alt.expr->acceptMutator( matcher );
+		out.emplace_back( alt );
+	}
+
+	/// Limit to depth of recursion of assertion satisfaction
 	static const int recursionLimit = /* 10 */ 4;
 
@@ -300,5 +355,5 @@
 					// either add successful match or push back next state
 					if ( resn.newNeed.empty() ) {
-						out.emplace_back( resn.alt );
+						finalizeAssertions( resn.alt, resn.inferred, out );
 					} else {
 						new_resns.emplace_back( std::move(resn), IterateState );
@@ -322,5 +377,5 @@
 							new_resn.newNeed.insert( match.need.begin(), match.need.end() );
 
-							bindAssertion( r.decl, r.info, new_resn.alt, match );
+							bindAssertion( r.decl, r.info, new_resn.alt, match, new_resn.inferred );
 						}
 
@@ -331,5 +386,5 @@
 						// either add sucessful match or push back next state
 						if ( new_resn.newNeed.empty() ) {
-							out.emplace_back( new_resn.alt );
+							finalizeAssertions( new_resn.alt, new_resn.inferred, out );
 						} else {
 							new_resns.emplace_back( std::move(new_resn), IterateState );
Index: src/ResolvExpr/TypeEnvironment.h
===================================================================
--- src/ResolvExpr/TypeEnvironment.h	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/ResolvExpr/TypeEnvironment.h	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -59,10 +59,8 @@
 	};
 	struct AssertionSetValue {
-		bool isUsed;
-		// chain of Unique IDs of the assertion declarations. The first ID in the chain is the ID 
-		// of an assertion on the current type, with each successive ID being the ID of an 
-		// assertion pulled in by the previous ID. The last ID in the chain is the ID of the 
-		// assertion that pulled in the current assertion.
-		std::list< UniqueId > idChain;
+		bool isUsed;        ///< True if assertion needs to be resolved
+		UniqueId resnSlot;  ///< ID of slot assertion belongs to
+
+		AssertionSetValue() : isUsed(false), resnSlot(0) {}
 	};
 	typedef std::map< DeclarationWithType*, AssertionSetValue, AssertCompare > AssertionSet;
Index: src/SynTree/ApplicationExpr.cc
===================================================================
--- src/SynTree/ApplicationExpr.cc	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/SynTree/ApplicationExpr.cc	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -29,5 +29,5 @@
 
 ParamEntry::ParamEntry( const ParamEntry &other ) :
-		decl( other.decl ), actualType( maybeClone( other.actualType ) ), formalType( maybeClone( other.formalType ) ), expr( maybeClone( other.expr ) ), inferParams( new InferredParams( *other.inferParams ) ) {
+		decl( other.decl ), actualType( maybeClone( other.actualType ) ), formalType( maybeClone( other.formalType ) ), expr( maybeClone( other.expr ) )/*, inferParams( new InferredParams( *other.inferParams ) )*/ {
 }
 
@@ -39,5 +39,5 @@
 	formalType = maybeClone( other.formalType );
 	expr = maybeClone( other.expr );
-	*inferParams = *other.inferParams;
+	// *inferParams = *other.inferParams;
 	return *this;
 }
@@ -50,5 +50,5 @@
 
 ParamEntry::ParamEntry( ParamEntry && other ) :
-		decl( other.decl ), actualType( other.actualType ), formalType( other.formalType ), expr( other.expr ), inferParams( std::move( other.inferParams ) ) {
+		decl( other.decl ), actualType( other.actualType ), formalType( other.formalType ), expr( other.expr )/*, inferParams( std::move( other.inferParams ) )*/ {
 	other.actualType = nullptr;
 	other.formalType = nullptr;
@@ -68,5 +68,5 @@
 	other.formalType = nullptr;
 	other.expr = nullptr;
-	inferParams = std::move( other.inferParams );
+	// inferParams = std::move( other.inferParams );
 	return *this;
 }
Index: src/SynTree/Expression.cc
===================================================================
--- src/SynTree/Expression.cc	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/SynTree/Expression.cc	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -40,5 +40,5 @@
 			Declaration::declFromId( i->second.decl )->printShort( os, indent+1 );
 			os << std::endl;
-			printInferParams( *i->second.inferParams, os, indent+1, level+1 );
+			printInferParams( i->second.expr->inferParams, os, indent+1, level+1 );
 		} // for
 	} // if
@@ -47,6 +47,5 @@
 Expression::Expression() : result( 0 ), env( 0 ) {}
 
-Expression::Expression( const Expression &other ) : BaseSyntaxNode( other ), result( maybeClone( other.result ) ), env( maybeClone( other.env ) ), extension( other.extension ), inferParams( other.inferParams ) {
-}
+Expression::Expression( const Expression &other ) : BaseSyntaxNode( other ), result( maybeClone( other.result ) ), env( maybeClone( other.env ) ), extension( other.extension ), inferParams( other.inferParams ), resnSlots( other.resnSlots ) {}
 
 void Expression::spliceInferParams( Expression * other ) {
@@ -55,4 +54,5 @@
 		inferParams[p.first] = std::move( p.second );
 	}
+	resnSlots.insert( resnSlots.end(), other->resnSlots.begin(), other->resnSlots.end() );
 }
 
Index: src/SynTree/Expression.h
===================================================================
--- src/SynTree/Expression.h	(revision 2fd9f248cb5343ac6498428e655f30a1222c5ede)
+++ src/SynTree/Expression.h	(revision 0b00df0b8a3e78119f146bb3d5894465fb9f24d4)
@@ -21,4 +21,5 @@
 #include <memory>                 // for allocator, unique_ptr
 #include <string>                 // for string
+#include <vector>                 // for vector
 
 #include "BaseSyntaxNode.h"       // for BaseSyntaxNode
@@ -38,6 +39,6 @@
 /// but subject to decay-to-pointer and type parameter renaming
 struct ParamEntry {
-	ParamEntry(): decl( 0 ), actualType( 0 ), formalType( 0 ), expr( 0 ), inferParams( new InferredParams ) {}
-	ParamEntry( UniqueId decl, Type * actualType, Type * formalType, Expression* expr ): decl( decl ), actualType( actualType ), formalType( formalType ), expr( expr ), inferParams( new InferredParams ) {}
+	ParamEntry(): decl( 0 ), actualType( 0 ), formalType( 0 ), expr( 0 )/*, inferParams( new InferredParams )*/ {}
+	ParamEntry( UniqueId decl, Type * actualType, Type * formalType, Expression* expr ): decl( decl ), actualType( actualType ), formalType( formalType ), expr( expr )/*, inferParams( new InferredParams )*/ {}
 	ParamEntry( const ParamEntry & other );
 	ParamEntry( ParamEntry && other );
@@ -50,5 +51,5 @@
 	Type * formalType;
 	Expression * expr;
-	std::unique_ptr< InferredParams > inferParams;
+	// std::unique_ptr< InferredParams > inferParams;
 };
 
@@ -59,5 +60,8 @@
 	TypeSubstitution * env;
 	bool extension = false;
-	InferredParams inferParams;
+	InferredParams inferParams;       ///< Post-resolution inferred parameter slots
+	std::vector<UniqueId> resnSlots;  ///< Pre-resolution inferred parameter slots
+	
+	// xxx - should turn inferParams+resnSlots into a union to save some memory
 
 	Expression();
@@ -73,6 +77,4 @@
 	bool get_extension() const { return extension; }
 	Expression * set_extension( bool exten ) { extension = exten; return this; }
-
-	InferredParams & get_inferParams() { return inferParams; }
 
 	// move other's inferParams to this
