Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision aeb8f70056004f741c9dcb505f8cb1cecb640ff1)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision 6dbeef78b56e5d179cf0a9d2ee1f991e73dde4a4)
@@ -20,4 +20,5 @@
 #include <list>                     // for list
 #include <memory>                   // for unique_ptr
+#include <string>
 #include <unordered_map>            // for unordered_map, unordered_multimap
 #include <utility>                  // for move
@@ -55,8 +56,26 @@
 	using CandidateList = std::vector<AssnCandidate>;
 
+	/// Unique identifier for a yet-to-be-resolved assertion
+	struct AssnId {
+		DeclarationWithType* decl;  ///< Declaration of assertion
+		AssertionSetValue info;     ///< Information about assertion
+
+		AssnId(DeclarationWithType* decl, const AssertionSetValue& info) : decl(decl), info(info) {}
+	};
+
+	/// Cached assertion items
+	struct AssnCacheItem {
+		CandidateList matches;         ///< Possible matches for this assertion
+		std::vector<AssnId> deferIds;  ///< Deferred assertions which resolve to this item
+
+		AssnCacheItem( CandidateList&& m ) : matches(std::move(m)), deferIds() {}
+	};
+
+	/// Cache of resolved assertions
+	using AssnCache = std::unordered_map<std::string, AssnCacheItem>;
+
 	/// Reference to single deferred item
 	struct DeferRef {
-		const DeclarationWithType* decl;
-		const AssertionSetValue& info;
+		const AssnCacheItem& item;
 		const AssnCandidate& match;
 	};
@@ -65,17 +84,23 @@
 	/// Acts like indexed list of DeferRef
 	struct DeferItem {
-		DeclarationWithType* decl;
-		AssertionSetValue info;
-		CandidateList matches;
-
-		DeferItem( DeclarationWithType* decl, const AssertionSetValue& info, 
-			CandidateList&& matches )
-		: decl(decl), info(info), matches(std::move(matches)) {}
-
-		bool empty() const { return matches.empty(); }
-
-		CandidateList::size_type size() const { return matches.size(); }
-
-		DeferRef operator[] ( unsigned i ) const { return { decl, info, matches[i] }; }
+		const AssnCache* cache;     ///< Cache storing assertion item
+		std::string key;            ///< Key into cache
+		
+		DeferItem( const AssnCache& cache, const std::string& key ) : cache(&cache), key(key) {}
+
+		bool empty() const { return cache->at(key).matches.empty(); }
+
+		CandidateList::size_type size() const { return cache->at(key).matches.size(); }
+
+		DeferRef operator[] ( unsigned i ) const {
+			const AssnCacheItem& item = cache->at(key);
+			return { item, item.matches[i] };
+		}
+
+		// sortable by key
+		// TODO look into optimizing combination process with other sort orders (e.g. by number 
+		// of matches in candidate)
+		bool operator< ( const DeferItem& o ) const { return key < o.key; }
+		bool operator== ( const DeferItem& o ) const { return key == o.key; }
 	};
 
@@ -152,5 +177,6 @@
 				for ( const auto& assn : x.assns ) {
 					k += computeConversionCost( 
-						assn.match.adjType, assn.decl->get_type(), indexer, x.env );
+						assn.match.adjType, assn.item.deferIds[0].decl->get_type(), indexer, 
+						x.env );
 				}
 				it = cache.emplace_hint( it, &x, k );
@@ -208,22 +234,11 @@
 				candidate->get_uniqueId(), match.adjType->clone(), 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 };
 	}
 
 	/// Adds a captured assertion to the symbol table
 	void addToIndexer( AssertionSet &assertSet, SymTab::Indexer &indexer ) {
-		for ( AssertionSet::iterator i = assertSet.begin(); i != assertSet.end(); ++i ) {
-			if ( i->second.isUsed ) {
-				indexer.addId( i->first );
+		for ( auto&  i : assertSet ) {
+			if ( i.second.isUsed ) {
+				indexer.addId( i.first );
 			}
 		}
@@ -234,48 +249,54 @@
 
 	/// Resolve a single assertion, in context
-	bool resolveAssertion( AssertionItem& assn, ResnState& resn ) {
+	bool resolveAssertion( AssertionItem& assn, ResnState& resn, AssnCache& cache ) {
 		// skip unused assertions
 		if ( ! assn.info.isUsed ) return true;
 
-		// lookup candidates for this assertion
-		std::list< SymTab::Indexer::IdData > candidates;
-		resn.indexer.lookupId( assn.decl->name, candidates );
-
-		// find the candidates that unify with the desired type
-		CandidateList matches;
-		for ( const auto& cdata : candidates ) {
-			DeclarationWithType* candidate = cdata.id;
-
-			// build independent unification context for candidate
-			AssertionSet have, newNeed;
-			TypeEnvironment newEnv{ resn.alt.env };
-			OpenVarSet newOpenVars{ resn.alt.openVars };
-			Type* adjType = candidate->get_type()->clone();
-			adjustExprType( adjType, newEnv, resn.indexer );
-			renameTyVars( adjType );
-
-			// keep unifying candidates
-			if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 
-					resn.indexer ) ) {
-				// set up binding slot for recursive assertions
-				UniqueId crntResnSlot = 0;
-				if ( ! newNeed.empty() ) {
-					crntResnSlot = ++globalResnSlot;
-					for ( auto& a : newNeed ) {
-						a.second.resnSlot = crntResnSlot;
+		// check cache for this assertion
+		std::string assnKey = SymTab::Mangler::mangleAssnKey( assn.decl, resn.alt.env );
+		auto it = cache.find( assnKey );
+
+		// attempt to resolve assertion if this is the first time seen
+		if ( it == cache.end() ) {
+			// lookup candidates for this assertion
+			std::list< SymTab::Indexer::IdData > candidates;
+			resn.indexer.lookupId( assn.decl->name, candidates );
+
+			// find the candidates that unify with the desired type
+			CandidateList matches;
+			for ( const auto& cdata : candidates ) {
+				DeclarationWithType* candidate = cdata.id;
+
+				// build independent unification context for candidate
+				AssertionSet have, newNeed;
+				TypeEnvironment newEnv{ resn.alt.env };
+				OpenVarSet newOpenVars{ resn.alt.openVars };
+				Type* adjType = candidate->get_type()->clone();
+				adjustExprType( adjType, newEnv, resn.indexer );
+				renameTyVars( adjType );
+
+				// keep unifying candidates
+				if ( unify( assn.decl->get_type(), adjType, newEnv, newNeed, have, newOpenVars, 
+						resn.indexer ) ) {
+					// 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), crntResnSlot );
-			} else {
-				delete adjType;
+
+					matches.emplace_back( cdata, adjType, std::move(newEnv), std::move(have), 
+						std::move(newNeed), std::move(newOpenVars), crntResnSlot );
+				} else {
+					delete adjType;
+				}
 			}
-		}
+
+			it = cache.emplace_hint( it, assnKey, AssnCacheItem{ std::move(matches) } );
+		}
+
+		CandidateList& matches = it->second.matches;
 
 		// break if no suitable assertion
@@ -284,5 +305,6 @@
 		// defer if too many suitable assertions
 		if ( matches.size() > 1 ) {
-			resn.deferred.emplace_back( assn.decl, assn.info, std::move(matches) );
+			it->second.deferIds.emplace_back( assn.decl, assn.info );
+			resn.deferred.emplace_back( cache, assnKey );
 			return true;
 		}
@@ -292,6 +314,6 @@
 		addToIndexer( match.have, resn.indexer );
 		resn.newNeed.insert( match.need.begin(), match.need.end() );
-		resn.alt.env = std::move(match.env);
-		resn.alt.openVars = std::move(match.openVars);
+		resn.alt.env = match.env;
+		resn.alt.openVars = match.openVars;
 
 		bindAssertion( assn.decl, assn.info, resn.alt, match, resn.inferred );
@@ -354,4 +376,5 @@
 		ResnList resns{ ResnState{ alt, root_indexer } };
 		ResnList new_resns{};
+		AssnCache assnCache;
 
 		// resolve assertions in breadth-first-order up to a limited number of levels deep
@@ -362,5 +385,5 @@
 				for ( auto& assn : resn.need ) {
 					// fail early if any assertion is not resolvable
-					if ( ! resolveAssertion( assn, resn ) ) goto nextResn;
+					if ( ! resolveAssertion( assn, resn, assnCache ) ) goto nextResn;
 				}
 
@@ -373,4 +396,8 @@
 					}
 				} else {
+					// only resolve each deferred assertion once
+					std::sort( resn.deferred.begin(), resn.deferred.end() );
+					auto last = std::unique( resn.deferred.begin(), resn.deferred.end() );
+					resn.deferred.erase( last, resn.deferred.end() );
 					// resolve deferred assertions by mutual compatibility
 					std::vector<CandidateEnvMerger::OutType> compatible = filterCombos(
@@ -380,10 +407,4 @@
 					CandidateCost coster{ resn.indexer };
 					std::sort( compatible.begin(), compatible.end(), coster );
-					// // sort by cost if pruning
-					// if ( pruneAssertions ) {
-					// 	auto lmin = sort_mins( compatible.begin(), compatible.end(), 
-					// 		CandidateCost{resn.indexer} );
-					// 	compatible.erase( lmin, compatible.end() );
-					// }
 
 					// keep map of detected options
@@ -408,5 +429,9 @@
 							new_resn.newNeed.insert( match.need.begin(), match.need.end() );
 
-							bindAssertion( r.decl, r.info, new_resn.alt, match, new_resn.inferred );
+							// for each deferred assertion with the same form
+							for ( AssnId id : r.item.deferIds ) {
+								bindAssertion( 
+									id.decl, id.info, new_resn.alt, match, new_resn.inferred );
+							}
 						}
 
