Index: src/Common/FilterCombos.h
===================================================================
--- src/Common/FilterCombos.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
+++ src/Common/FilterCombos.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -0,0 +1,103 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// FilterCombos.h --
+//
+// Author           : Aaron B. Moss
+// Created On       : Mon Jul 23 16:05:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Mon Jul 23 16:05:00 2018
+// Update Count     : 1
+//
+
+#pragma once
+
+#include <vector>
+
+/// Type of index vector for combinations
+typedef std::vector<unsigned> Indices;
+
+/// Combo iterator that simply collects values into a vector, marking all values as valid.
+/// Prefer combos in typeops.h to use of IntoVectorComboIter with filterCombos
+/// @param T	The element type of the vector.
+template<typename T>
+class IntoVectorComboIter {
+	std::vector<T> crnt_combo;
+public:
+	/// Outputs a vector of T
+	using OutType = std::vector<T>;
+
+	/// Adds the element to the current combination, always returning true for valid.
+	bool append( const T& x ) {
+		crnt_combo.push_back( x );
+		return true;
+	}
+
+	/// Removes the last element of the current combination.
+	void backtrack() { crnt_combo.pop_back(); }
+
+	/// Returns a copy of the current combination.
+	OutType finalize() { return crnt_combo; }
+};
+
+/// Filters combinations from qs by the given combo iterator. If the iterator rejects some prefix 
+/// of a combination, it will not accept any combination with that prefix.
+/// qs should not be empty
+template<typename Q, typename ComboIter>
+auto filterCombos( const std::vector<Q>& qs, ComboIter&& iter )
+		-> std::vector<typename ComboIter::OutType> {
+    unsigned n = qs.size();  // number of queues to combine
+
+	std::vector<typename ComboIter::OutType> out;  // filtered output
+	for ( auto& q : qs ) if ( q.empty() ) return out;  // return empty if any empty queue
+
+	Indices inds;
+	inds.reserve( n );
+	inds.push_back( 0 );
+
+	while (true) {
+		unsigned i = inds.size() - 1;
+
+		// iterate or keep successful match
+		if ( iter.append( qs[i][inds.back()] ) ) {
+			if ( i + 1 == n ) {
+				// keep successful match of entire combination and continue iterating final place
+				out.push_back( iter.finalize() );
+				iter.backtrack();
+			} else {
+				// try to extend successful prefix
+				inds.push_back( 0 );
+				continue;
+			}
+		}
+
+		// move to next combo
+		++inds.back();
+		if ( inds.back() < qs[i].size() ) continue;
+		
+		// Otherwise done with the current row.
+		// At this point, an invalid prefix is stored in inds and iter is in a state looking at 
+		// all but the final value in inds. Now backtrack to next prefix:
+		inds.pop_back();
+		while ( ! inds.empty() ) {
+			// try the next value at the previous index
+			++inds.back();
+			iter.backtrack();
+			if ( inds.back() < qs[inds.size()-1].size() ) break;
+			// if the previous index is finished, backtrack out
+			inds.pop_back();
+		}
+
+		// Done if backtracked the entire array
+		if ( inds.empty() ) return out;
+	}
+}
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/Common/utility.h
===================================================================
--- src/Common/utility.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/Common/utility.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -26,4 +26,5 @@
 #include <string>
 #include <type_traits>
+#include <utility>
 
 #include <cassert>
@@ -462,4 +463,38 @@
 std::pair<long long int, bool> eval(Expression * expr);
 
+// -----------------------------------------------------------------------------
+/// Reorders the input range in-place so that the minimal-value elements according to the 
+/// comparator are in front; 
+/// returns the iterator after the last minimal-value element.
+template<typename Iter, typename Compare>
+Iter sort_mins( Iter begin, Iter end, Compare& lt ) {
+	if ( begin == end ) return end;
+	
+	Iter min_pos = begin;
+	for ( Iter i = begin + 1; i != end; ++i ) {
+		if ( lt( *i, *min_pos ) ) {
+			// new minimum cost; swap into first position
+			min_pos = begin;
+			std::iter_swap( min_pos, i );
+		} else if ( ! lt( *min_pos, *i ) ) {
+			// duplicate minimum cost; swap into next minimum position
+			++min_pos;
+			std::iter_swap( min_pos, i );
+		}
+	}
+	return ++min_pos;
+}
+
+template<typename Iter, typename Compare>
+inline Iter sort_mins( Iter begin, Iter end, Compare&& lt ) {
+	return sort_mins( begin, end, lt );
+}
+
+/// sort_mins defaulted to use std::less
+template<typename Iter>
+inline Iter sort_mins( Iter begin, Iter end ) {
+	return sort_mins( begin, end, std::less<typename std::iterator_traits<Iter>::value_type>{} );
+}
+
 // Local Variables: //
 // tab-width: 4 //
Index: src/GenPoly/Box.cc
===================================================================
--- src/GenPoly/Box.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/GenPoly/Box.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -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 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/GenPoly/Specialize.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -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/Makefile.am
===================================================================
--- src/Makefile.am	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/Makefile.am	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -127,6 +127,8 @@
   ResolvExpr/PtrsCastable.cc \
   ResolvExpr/RenameVars.cc \
+  ResolvExpr/ResolveAssertions.cc \
   ResolvExpr/Resolver.cc \
   ResolvExpr/ResolveTypeof.cc \
+  ResolvExpr/SpecCost.cc \
   ResolvExpr/TypeEnvironment.cc \
   ResolvExpr/Unify.cc \
Index: src/Makefile.in
===================================================================
--- src/Makefile.in	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/Makefile.in	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -206,6 +206,9 @@
 	ResolvExpr/PtrsAssignable.$(OBJEXT) \
 	ResolvExpr/PtrsCastable.$(OBJEXT) \
-	ResolvExpr/RenameVars.$(OBJEXT) ResolvExpr/Resolver.$(OBJEXT) \
+	ResolvExpr/RenameVars.$(OBJEXT) \
+	ResolvExpr/ResolveAssertions.$(OBJEXT) \
+	ResolvExpr/Resolver.$(OBJEXT) \
 	ResolvExpr/ResolveTypeof.$(OBJEXT) \
+	ResolvExpr/SpecCost.$(OBJEXT) \
 	ResolvExpr/TypeEnvironment.$(OBJEXT) \
 	ResolvExpr/Unify.$(OBJEXT) SymTab/Autogen.$(OBJEXT) \
@@ -262,11 +265,14 @@
 	ResolvExpr/TypeEnvironment.$(OBJEXT) \
 	ResolvExpr/CurrentObject.$(OBJEXT) \
-	ResolvExpr/ExplodedActual.$(OBJEXT) SymTab/Indexer.$(OBJEXT) \
-	SymTab/Mangler.$(OBJEXT) SymTab/ManglerCommon.$(OBJEXT) \
-	SymTab/Validate.$(OBJEXT) SymTab/FixFunction.$(OBJEXT) \
-	SymTab/Autogen.$(OBJEXT) SynTree/Type.$(OBJEXT) \
-	SynTree/VoidType.$(OBJEXT) SynTree/BasicType.$(OBJEXT) \
-	SynTree/PointerType.$(OBJEXT) SynTree/ArrayType.$(OBJEXT) \
-	SynTree/ReferenceType.$(OBJEXT) SynTree/FunctionType.$(OBJEXT) \
+	ResolvExpr/ExplodedActual.$(OBJEXT) \
+	ResolvExpr/SpecCost.$(OBJEXT) \
+	ResolvExpr/ResolveAssertions.$(OBJEXT) \
+	SymTab/Indexer.$(OBJEXT) SymTab/Mangler.$(OBJEXT) \
+	SymTab/ManglerCommon.$(OBJEXT) SymTab/Validate.$(OBJEXT) \
+	SymTab/FixFunction.$(OBJEXT) SymTab/Autogen.$(OBJEXT) \
+	SynTree/Type.$(OBJEXT) SynTree/VoidType.$(OBJEXT) \
+	SynTree/BasicType.$(OBJEXT) SynTree/PointerType.$(OBJEXT) \
+	SynTree/ArrayType.$(OBJEXT) SynTree/ReferenceType.$(OBJEXT) \
+	SynTree/FunctionType.$(OBJEXT) \
 	SynTree/ReferenceToType.$(OBJEXT) SynTree/TupleType.$(OBJEXT) \
 	SynTree/TypeofType.$(OBJEXT) SynTree/AttrType.$(OBJEXT) \
@@ -589,4 +595,5 @@
 	ResolvExpr/Occurs.cc ResolvExpr/TypeEnvironment.cc \
 	ResolvExpr/CurrentObject.cc ResolvExpr/ExplodedActual.cc \
+	ResolvExpr/SpecCost.cc ResolvExpr/ResolveAssertions.cc \
 	SymTab/Indexer.cc SymTab/Mangler.cc SymTab/ManglerCommon.cc \
 	SymTab/Validate.cc SymTab/FixFunction.cc SymTab/Autogen.cc \
@@ -696,6 +703,8 @@
   ResolvExpr/PtrsCastable.cc \
   ResolvExpr/RenameVars.cc \
+  ResolvExpr/ResolveAssertions.cc \
   ResolvExpr/Resolver.cc \
   ResolvExpr/ResolveTypeof.cc \
+  ResolvExpr/SpecCost.cc \
   ResolvExpr/TypeEnvironment.cc \
   ResolvExpr/Unify.cc \
@@ -946,7 +955,11 @@
 ResolvExpr/RenameVars.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
 	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
+ResolvExpr/ResolveAssertions.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
+	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
 ResolvExpr/Resolver.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
 	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
 ResolvExpr/ResolveTypeof.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
+	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
+ResolvExpr/SpecCost.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
 	ResolvExpr/$(DEPDIR)/$(am__dirstamp)
 ResolvExpr/TypeEnvironment.$(OBJEXT): ResolvExpr/$(am__dirstamp) \
@@ -1207,6 +1220,8 @@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/PtrsCastable.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/RenameVars.Po@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/ResolveAssertions.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/ResolveTypeof.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/Resolver.Po@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/SpecCost.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/TypeEnvironment.Po@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@ResolvExpr/$(DEPDIR)/Unify.Po@am__quote@
Index: src/ResolvExpr/Alternative.cc
===================================================================
--- src/ResolvExpr/Alternative.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/Alternative.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -9,7 +9,7 @@
 // Author           : Richard C. Bilson
 // Created On       : Sat May 16 23:44:23 2015
-// Last Modified By : Peter A. Buhr
-// Last Modified On : Sat May 16 23:54:23 2015
-// Update Count     : 2
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Thu Oct 11 10:55:00 2018
+// Update Count     : 3
 //
 
@@ -20,5 +20,5 @@
 #include <utility>                       // for move
 
-#include "Common/utility.h"              // for maybeClone
+#include "Common/utility.h"              // for cloneAll
 #include "ResolvExpr/Cost.h"             // for Cost, Cost::zero, operator<<
 #include "ResolvExpr/TypeEnvironment.h"  // for TypeEnvironment
@@ -27,14 +27,49 @@
 
 namespace ResolvExpr {
-	Alternative::Alternative() : cost( Cost::zero ), cvtCost( Cost::zero ), expr( nullptr ) {}
+	Alternative::Alternative() 
+	: cost( Cost::zero ), cvtCost( Cost::zero ), expr( nullptr ), env(), openVars(), need() {}
 
-	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, const Cost& cost )
-		: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( env ) {}
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env )
+	: cost( Cost::zero ), cvtCost( Cost::zero ), expr( expr ), env( env ), openVars(), need() {}
+	
+	Alternative::Alternative( const Alternative &o, Expression *expr, const Cost &cost ) 
+	: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( o.env ), openVars( o.openVars ), 
+	  need() { cloneAll( o.need, need ); }
 
-	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, const Cost& cost, const Cost &cvtCost )
-		: cost( cost ), cvtCost( cvtCost ), expr( expr ), env( env ) {}
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, 
+		const OpenVarSet& openVars, const AssertionList& oneed, const Cost& cost )
+	: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( env ), openVars( openVars ), 
+	  need() { cloneAll( oneed, need ); }
 
-	Alternative::Alternative( const Alternative &other ) : cost( other.cost ), cvtCost( other.cvtCost ), expr( maybeClone( other.expr ) ), env( other.env ) {
-	}
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, 
+		const OpenVarSet& openVars, const AssertionList& oneed, const Cost& cost, 
+		const Cost &cvtCost )
+	: cost( cost ), cvtCost( cvtCost ), expr( expr ), env( env ), openVars( openVars ), 
+	  need() { cloneAll( oneed, need ); }
+	
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, 
+		const OpenVarSet &openVars, const AssertionSet &oneed, const Cost &cost)
+	: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( env ), openVars( openVars ), 
+	  need() { cloneAll( oneed, need ); }
+	
+	Alternative::Alternative( Expression *expr, const TypeEnvironment &env, 
+		const OpenVarSet &openVars, const AssertionSet &oneed, const Cost &cost, 
+		const Cost& cvtCost )
+	: cost( cost ), cvtCost( cvtCost ), expr( expr ), env( env ), openVars( openVars ), 
+	  need() { cloneAll( oneed, need ); }
+	
+	Alternative::Alternative( Expression *expr, TypeEnvironment &&env, OpenVarSet &&openVars, 
+		AssertionSet &&needSet, const Cost &cost )
+	: cost( cost ), cvtCost( Cost::zero ), expr( expr ), env( std::move(env) ), 
+	  openVars( std::move(openVars) ), need( needSet.begin(), needSet.end() ) {}
+	
+	Alternative::Alternative( Expression *expr, TypeEnvironment &&env, OpenVarSet &&openVars, 
+		AssertionSet &&needSet, const Cost &cost, const Cost &cvtCost )
+	: cost( cost ), cvtCost( cvtCost ), expr( expr ), env( std::move(env) ), 
+	  openVars( std::move(openVars) ), need( needSet.begin(), needSet.end() ) {}
+
+	Alternative::Alternative( const Alternative &other ) 
+	: cost( other.cost ), cvtCost( other.cvtCost ), expr( maybeClone( other.expr ) ), 
+	  env( other.env ), openVars( other.openVars ), need() { cloneAll( other.need, need ); }
 
 	Alternative &Alternative::operator=( const Alternative &other ) {
@@ -45,10 +80,14 @@
 		expr = maybeClone( other.expr );
 		env = other.env;
+		openVars = other.openVars;
+		need.clear();
+		cloneAll( other.need, need );
 		return *this;
 	}
 
-	Alternative::Alternative( Alternative && other ) : cost( other.cost ), cvtCost( other.cvtCost ), expr( other.expr ), env( std::move( other.env ) ) {
-		other.expr = nullptr;
-	}
+	Alternative::Alternative( Alternative && other ) 
+	: cost( other.cost ), cvtCost( other.cvtCost ), expr( other.expr ), 
+	  env( std::move( other.env ) ), openVars( std::move( other.openVars ) ), 
+	  need( std::move( other.need ) ) { other.expr = nullptr; }
 
 	Alternative & Alternative::operator=( Alternative && other ) {
@@ -59,4 +98,6 @@
 		expr = other.expr;
 		env = std::move( other.env );
+		openVars = std::move( other.openVars );
+		need = std::move( other.need );
 		other.expr = nullptr;
 		return *this;
@@ -64,4 +105,5 @@
 
 	Alternative::~Alternative() {
+		for ( AssertionItem& n : need ) { delete n.decl; }
 		delete expr;
 	}
Index: src/ResolvExpr/Alternative.h
===================================================================
--- src/ResolvExpr/Alternative.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/Alternative.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -9,7 +9,7 @@
 // Author           : Richard C. Bilson
 // Created On       : Sat May 16 23:45:43 2015
-// Last Modified By : Peter A. Buhr
-// Last Modified On : Sat Jul 22 09:36:36 2017
-// Update Count     : 3
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Thu Oct 11 10:55:00 2018
+// Update Count     : 4
 //
 
@@ -20,13 +20,68 @@
 
 #include "Cost.h"             // for Cost
-#include "TypeEnvironment.h"  // for TypeEnvironment
+#include "TypeEnvironment.h"  // for TypeEnvironment, AssertionSetValue
+
+#include "Common/utility.h"   // for maybeClone
 
 class Expression;
 
 namespace ResolvExpr {
+	/// One assertion to resolve
+	struct AssertionItem {
+		DeclarationWithType* decl;
+		AssertionSetValue info;
+		
+		AssertionItem() = default;
+		AssertionItem( DeclarationWithType* decl, const AssertionSetValue& info ) 
+		: decl(decl), info(info) {}
+		AssertionItem( const AssertionSet::value_type& e ) : decl(e.first), info(e.second) {}
+		operator AssertionSet::value_type () const { return { decl, info }; }
+
+		// to support cloneAll
+		AssertionItem clone() const { return { maybeClone(decl), info }; }
+	};
+	/// A list of unresolved assertions
+	using AssertionList = std::vector<AssertionItem>;
+
+	/// Clones an assertion list into an assertion set
+	static inline void cloneAll( const AssertionList& src, AssertionSet& dst ) {
+		for ( const AssertionItem& item : src ) {
+			dst.emplace( maybeClone(item.decl), item.info );
+		}
+	}
+
+	/// Clones an assertion set into an assertion list
+	static inline void cloneAll( const AssertionSet& src, AssertionList& dst ) {
+		dst.reserve( dst.size() + src.size() );
+		for ( const auto& entry : src ) {
+			dst.emplace_back( maybeClone(entry.first), entry.second );
+		}
+	}
+
+	/// Clones an assertion list into an assertion list
+	static inline void cloneAll( const AssertionList& src, AssertionList& dst ) {
+		dst.reserve( dst.size() + src.size() );
+		for ( const AssertionItem& item : src ) {
+			dst.emplace_back( maybeClone(item.decl), item.info );
+		}
+	}
+
+	/// One option for resolution of an expression
 	struct Alternative {
 		Alternative();
-		Alternative( Expression *expr, const TypeEnvironment &env, const Cost &cost );
-		Alternative( Expression *expr, const TypeEnvironment &env, const Cost &cost, const Cost &cvtCost );
+		Alternative( Expression *expr, const TypeEnvironment &env );
+		Alternative( const Alternative &o, Expression *expr, const Cost &cost );
+		Alternative( Expression *expr, const TypeEnvironment &env, const OpenVarSet& openVars, 
+			const AssertionList& need, const Cost &cost );
+		Alternative( Expression *expr, const TypeEnvironment &env, const OpenVarSet& openVars, 
+			const AssertionList& need, const Cost &cost, const Cost &cvtCost );
+		Alternative( Expression *expr, const TypeEnvironment &env, const OpenVarSet &openVars, 
+			const AssertionSet &need, const Cost &cost);
+		Alternative( Expression *expr, const TypeEnvironment &env, const OpenVarSet &openVars, 
+			const AssertionSet &need, const Cost &cost, const Cost& cvtCost );
+		Alternative( Expression *expr, TypeEnvironment &&env, OpenVarSet &&openVars, 
+			AssertionSet &&need, const Cost &cost );
+		Alternative( Expression *expr, TypeEnvironment &&env, OpenVarSet &&openVars, 
+			AssertionSet &&need, const Cost &cost, const Cost &cvtCost );
 		Alternative( const Alternative &other );
 		Alternative &operator=( const Alternative &other );
@@ -44,8 +99,13 @@
 		}
 
-		Cost cost;
-		Cost cvtCost;
-		Expression *expr;
-		TypeEnvironment env;
+		/// Sorts by cost
+		bool operator< ( const Alternative& o ) const { return cost < o.cost; }
+
+		Cost cost;            ///< Cost of the whole expression
+		Cost cvtCost;         ///< Cost of conversions to the satisfying expression
+		Expression *expr;     ///< Satisfying expression
+		TypeEnvironment env;  ///< Containing type environment
+		OpenVarSet openVars;  ///< Open variables for environment
+		AssertionList need;   ///< Assertions which need to be resolved
 	};
 
Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -11,5 +11,5 @@
 // Last Modified By : Peter A. Buhr
 // Last Modified On : Thu Nov  1 21:00:56 2018
-// Update Count     : 34
+// Update Count     : 35
 //
 
@@ -34,4 +34,5 @@
 #include "InitTweak/InitTweak.h"   // for getFunctionName
 #include "RenameVars.h"            // for RenameVars, global_renamer
+#include "ResolveAssertions.h"     // for resolveAssertions
 #include "ResolveTypeof.h"         // for resolveTypeof
 #include "Resolver.h"              // for resolveStmtExpr
@@ -102,7 +103,7 @@
 		void addAnonConversions( const Alternative & alt );
 		/// Adds alternatives for member expressions, given the aggregate, conversion cost for that aggregate, and name of the member
-		template< typename StructOrUnionType > void addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Cost &newCost, const TypeEnvironment & env, const std::string & name );
+		template< typename StructOrUnionType > void addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Alternative &alt, const Cost &newCost, const std::string & name );
 		/// Adds alternatives for member expressions where the left side has tuple type
-		void addTupleMembers( TupleType * tupleType, Expression *expr, const Cost &newCost, const TypeEnvironment & env, Expression * member );
+		void addTupleMembers( TupleType *tupleType, Expression *expr, const Alternative &alt, const Cost &newCost, Expression *member );
 		/// Adds alternatives for offsetof expressions, given the base type and name of the member
 		template< typename StructOrUnionType > void addOffsetof( StructOrUnionType *aggInst, const std::string &name );
@@ -113,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;
@@ -244,8 +245,8 @@
 	}
 
-	void AlternativeFinder::find( Expression *expr, bool adjust, bool prune, bool failFast ) {
+	void AlternativeFinder::find( Expression *expr, ResolvMode mode ) {
 		PassVisitor<Finder> finder( *this );
 		expr->accept( finder );
-		if ( failFast && alternatives.empty() ) {
+		if ( mode.failFast && alternatives.empty() ) {
 			PRINT(
 				std::cerr << "No reasonable alternatives for expression " << expr << std::endl;
@@ -253,5 +254,23 @@
 			SemanticError( expr, "No reasonable alternatives for expression " );
 		}
-		if ( prune ) {
+		if ( mode.resolveAssns || mode.prune ) {
+			// trim candidates just to those where the assertions resolve
+			// - necessary pre-requisite to pruning
+			AltList candidates;
+			for ( unsigned i = 0; i < alternatives.size(); ++i ) {
+				resolveAssertions( alternatives[i], indexer, candidates );
+			}
+			// fail early if none such
+			if ( mode.failFast && candidates.empty() ) {
+				std::ostringstream stream;
+				stream << "No resolvable alternatives for expression " << expr << "\n"
+				       << "Alternatives with failing assertions are:\n";
+				printAlts( alternatives, stream, 1 );
+				SemanticError( expr->location, stream.str() );
+			}
+			// reset alternatives
+			alternatives = std::move( candidates );
+		}
+		if ( mode.prune ) {
 			auto oldsize = alternatives.size();
 			PRINT(
@@ -261,5 +280,5 @@
 			AltList pruned;
 			pruneAlternatives( alternatives.begin(), alternatives.end(), back_inserter( pruned ) );
-			if ( failFast && pruned.empty() ) {
+			if ( mode.failFast && pruned.empty() ) {
 				std::ostringstream stream;
 				AltList winners;
@@ -280,7 +299,7 @@
 		}
 		// adjust types after pruning so that types substituted by pruneAlternatives are correctly adjusted
-		for ( AltList::iterator i = alternatives.begin(); i != alternatives.end(); ++i ) {
-			if ( adjust ) {
-				adjustExprType( i->expr->get_result(), i->env, indexer );
+		if ( mode.adjust ) {
+			for ( Alternative& i : alternatives ) {
+				adjustExprType( i.expr->get_result(), i.env, indexer );
 			}
 		}
@@ -294,13 +313,13 @@
 
 	void AlternativeFinder::findWithAdjustment( Expression *expr ) {
-		find( expr, true );
+		find( expr, ResolvMode::withAdjustment() );
 	}
 
 	void AlternativeFinder::findWithoutPrune( Expression * expr ) {
-		find( expr, true, false );
+		find( expr, ResolvMode::withoutPrune() );
 	}
 
 	void AlternativeFinder::maybeFind( Expression * expr ) {
-		find( expr, true, true, false );
+		find( expr, ResolvMode::withoutFailFast() );
 	}
 
@@ -317,12 +336,12 @@
 
 		if ( StructInstType *structInst = dynamic_cast< StructInstType* >( aggrExpr->result ) ) {
-			addAggMembers( structInst, aggrExpr.get(), alt.cost+Cost::safe, alt.env, "" );
+			addAggMembers( structInst, aggrExpr.get(), alt, alt.cost+Cost::safe, "" );
 		} else if ( UnionInstType *unionInst = dynamic_cast< UnionInstType* >( aggrExpr->result ) ) {
-			addAggMembers( unionInst, aggrExpr.get(), alt.cost+Cost::safe, alt.env, "" );
+			addAggMembers( unionInst, aggrExpr.get(), alt, alt.cost+Cost::safe, "" );
 		} // if
 	}
 
 	template< typename StructOrUnionType >
-	void AlternativeFinder::Finder::addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Cost &newCost, const TypeEnvironment & env, const std::string & name ) {
+	void AlternativeFinder::Finder::addAggMembers( StructOrUnionType *aggInst, Expression *expr, const Alternative& alt, const Cost &newCost, const std::string & name ) {
 		std::list< Declaration* > members;
 		aggInst->lookup( name, members );
@@ -332,5 +351,5 @@
 				// addAnonAlternatives uses vector::push_back, which invalidates references to existing elements, so
 				// can't construct in place and use vector::back
-				Alternative newAlt( new MemberExpr( dwt, expr->clone() ), env, newCost );
+				Alternative newAlt{ alt, new MemberExpr{ dwt, expr->clone() }, newCost };
 				renameTypes( newAlt.expr );
 				addAnonConversions( newAlt ); // add anonymous member interpretations whenever an aggregate value type is seen as a member expression.
@@ -342,5 +361,5 @@
 	}
 
-	void AlternativeFinder::Finder::addTupleMembers( TupleType * tupleType, Expression *expr, const Cost &newCost, const TypeEnvironment & env, Expression * member ) {
+	void AlternativeFinder::Finder::addTupleMembers( TupleType *tupleType, Expression *expr, 			const Alternative &alt, const Cost &newCost, Expression *member ) {
 		if ( ConstantExpr * constantExpr = dynamic_cast< ConstantExpr * >( member ) ) {
 			// get the value of the constant expression as an int, must be between 0 and the length of the tuple type to have meaning
@@ -348,5 +367,6 @@
 			std::string tmp;
 			if ( val >= 0 && (unsigned long long)val < tupleType->size() ) {
-				alternatives.push_back( Alternative( new TupleIndexExpr( expr->clone(), val ), env, newCost ) );
+				alternatives.push_back( Alternative{ 
+					alt, new TupleIndexExpr( expr->clone(), val ), newCost } );
 			} // if
 		} // if
@@ -354,5 +374,5 @@
 
 	void AlternativeFinder::Finder::postvisit( ApplicationExpr *applicationExpr ) {
-		alternatives.push_back( Alternative( applicationExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ applicationExpr->clone(), env } );
 	}
 
@@ -410,26 +430,26 @@
 	Cost computeApplicationConversionCost( Alternative &alt, const SymTab::Indexer &indexer ) {
 		ApplicationExpr *appExpr = strict_dynamic_cast< ApplicationExpr* >( alt.expr );
-		PointerType *pointer = strict_dynamic_cast< PointerType* >( appExpr->get_function()->get_result() );
-		FunctionType *function = strict_dynamic_cast< FunctionType* >( pointer->get_base() );
+		PointerType *pointer = strict_dynamic_cast< PointerType* >( appExpr->function->result );
+		FunctionType *function = strict_dynamic_cast< FunctionType* >( pointer->base );
 
 		Cost convCost = Cost::zero;
-		std::list< DeclarationWithType* >& formals = function->get_parameters();
+		std::list< DeclarationWithType* >& formals = function->parameters;
 		std::list< DeclarationWithType* >::iterator formal = formals.begin();
-		std::list< Expression* >& actuals = appExpr->get_args();
-
-		for ( std::list< Expression* >::iterator actualExpr = actuals.begin(); actualExpr != actuals.end(); ++actualExpr ) {
-			Type * actualType = (*actualExpr)->get_result();
+		std::list< Expression* >& actuals = appExpr->args;
+
+		for ( Expression*& actualExpr : actuals ) {
+			Type * actualType = actualExpr->result;
 			PRINT(
 				std::cerr << "actual expression:" << std::endl;
-				(*actualExpr)->print( std::cerr, 8 );
+				actualExpr->print( std::cerr, 8 );
 				std::cerr << "--- results are" << std::endl;
 				actualType->print( std::cerr, 8 );
 			)
 			if ( formal == formals.end() ) {
-				if ( function->get_isVarArgs() ) {
+				if ( function->isVarArgs ) {
 					convCost.incUnsafe();
 					PRINT( std::cerr << "end of formals with varargs function: inc unsafe: " << convCost << std::endl; ; )
 					// convert reference-typed expressions to value-typed expressions
-					referenceToRvalueConversion( *actualExpr, convCost );
+					referenceToRvalueConversion( actualExpr, convCost );
 					continue;
 				} else {
@@ -437,13 +457,15 @@
 				}
 			}
-			if ( DefaultArgExpr * def = dynamic_cast< DefaultArgExpr * >( *actualExpr ) ) {
+			if ( DefaultArgExpr * def = dynamic_cast< DefaultArgExpr * >( actualExpr ) ) {
 				// default arguments should be free - don't include conversion cost.
 				// Unwrap them here because they are not relevant to the rest of the system.
-				*actualExpr = def->expr;
+				actualExpr = def->expr;
 				++formal;
 				continue;
 			}
+			// mark conversion cost to formal and also specialization cost of formal type
 			Type * formalType = (*formal)->get_type();
-			convCost += computeExpressionConversionCost( *actualExpr, formalType, indexer, alt.env );
+			convCost += computeExpressionConversionCost( actualExpr, formalType, indexer, alt.env );
+			convCost.decSpec( specCost( formalType ) );
 			++formal; // can't be in for-loop update because of the continue
 		}
@@ -452,5 +474,17 @@
 		}
 
-		for ( InferredParams::const_iterator assert = appExpr->get_inferParams().begin(); assert != appExpr->get_inferParams().end(); ++assert ) {
+		// mark specialization cost of return types
+		for ( DeclarationWithType* returnVal : function->returnVals ) {
+			convCost.decSpec( specCost( returnVal->get_type() ) );
+		}
+
+		// mark type variable and specialization cost of forall clause
+		convCost.incVar( function->forall.size() );
+		for ( TypeDecl* td : function->forall ) {
+			convCost.decSpec( td->assertions.size() );
+		}
+
+		// xxx -- replace with new costs in resolver
+		for ( InferredParams::const_iterator assert = appExpr->inferParams.begin(); assert != appExpr->inferParams.end(); ++assert ) {
 			convCost += computeConversionCost( assert->second.actualType, assert->second.formalType, indexer, alt.env );
 		}
@@ -466,149 +500,27 @@
 				needAssertions[ *assert ].isUsed = true;
 			}
-///     needAssertions.insert( needAssertions.end(), (*tyvar)->get_assertions().begin(), (*tyvar)->get_assertions().end() );
-		}
-	}
-
-	static const int recursionLimit = /*10*/ 4;  ///< Limit to depth of recursion satisfaction
-
-	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 );
-			}
-		}
-	}
-
-	template< typename ForwardIterator, typename OutputIterator >
-	void inferRecursive( ForwardIterator begin, ForwardIterator end, const Alternative &newAlt, OpenVarSet &openVars, const SymTab::Indexer &decls, const AssertionSet &newNeed, int level, const SymTab::Indexer &indexer, OutputIterator out ) {
-		if ( newAlt.cost == Cost::infinity ) return; // don't proceed down this dead end
-		if ( begin == end ) {
-			if ( newNeed.empty() ) {
-				PRINT(
-					std::cerr << "all assertions satisfied, output alternative: ";
-					newAlt.print( std::cerr );
-					std::cerr << std::endl;
-				);
-				*out++ = newAlt;
-				return;
-			} else if ( level >= recursionLimit ) {
-				SemanticError( newAlt.expr->location, "Too many recursive assertions" );
-			} else {
-				AssertionSet newerNeed;
-				PRINT(
-					std::cerr << "recursing with new set:" << std::endl;
-					printAssertionSet( newNeed, std::cerr, 8 );
-				)
-				inferRecursive( newNeed.begin(), newNeed.end(), newAlt, openVars, decls, newerNeed, level+1, indexer, out );
-				return;
-			}
-		}
-
-		ForwardIterator cur = begin++;
-		if ( ! cur->second.isUsed ) {
-			inferRecursive( begin, end, newAlt, openVars, decls, newNeed, level, indexer, out );
-			return; // xxx - should this continue? previously this wasn't here, and it looks like it should be
-		}
-		DeclarationWithType *curDecl = cur->first;
-
-		PRINT(
-			std::cerr << "inferRecursive: assertion is ";
-			curDecl->print( std::cerr );
-			std::cerr << std::endl;
-		)
-		std::list< SymTab::Indexer::IdData > candidates;
-		decls.lookupId( curDecl->get_name(), candidates );
-///   if ( candidates.empty() ) { std::cerr << "no candidates!" << std::endl; }
-		for ( const auto & data : candidates ) {
-			DeclarationWithType * candidate = data.id;
-			PRINT(
-				std::cerr << "inferRecursive: candidate is ";
-				candidate->print( std::cerr );
-				std::cerr << std::endl;
-			)
-
-			AssertionSet newHave, newerNeed( newNeed );
-			TypeEnvironment newEnv( newAlt.env );
-			OpenVarSet newOpenVars( openVars );
-			Type *adjType = candidate->get_type()->clone();
-			adjustExprType( adjType, newEnv, indexer );
-			renameTyVars( adjType );
-			PRINT(
-				std::cerr << "unifying ";
-				curDecl->get_type()->print( std::cerr );
-				std::cerr << " with ";
-				adjType->print( std::cerr );
-				std::cerr << std::endl;
-			)
-			if ( unify( curDecl->get_type(), adjType, newEnv, newerNeed, newHave, newOpenVars, indexer ) ) {
-				PRINT(
-					std::cerr << "success!" << std::endl;
-				)
-				SymTab::Indexer newDecls( decls );
-				addToIndexer( newHave, newDecls );
-				Alternative newerAlt( newAlt );
-				newerAlt.env = newEnv;
-				assertf( candidate->get_uniqueId(), "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
-
-				// everything with an empty idChain was pulled in by the current assertion.
-				// add current assertion's idChain + current assertion's ID so that the correct inferParameters can be found.
-				for ( auto & a : newerNeed ) {
-					if ( a.second.idChain.empty() ) {
-						a.second.idChain = cur->second.idChain;
-						a.second.idChain.push_back( curDecl->get_uniqueId() );
-					}
-				}
-
-				Expression *varExpr = data.combine( newerAlt.cvtCost );
-				delete varExpr->get_result();
-				varExpr->set_result( adjType->clone() );
-				PRINT(
-					std::cerr << "satisfying assertion " << curDecl->get_uniqueId() << " ";
-					curDecl->print( std::cerr );
-					std::cerr << " with declaration " << candidate->get_uniqueId() << " ";
-					candidate->print( std::cerr );
-					std::cerr << std::endl;
-				)
-				// 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();
-				for ( UniqueId id : cur->second.idChain ) {
-					inferParameters = (*inferParameters)[ id ].inferParams.get();
-				}
-				// XXX: this is a memory leak, but adjType can't be deleted because it might contain assertions
-				(*inferParameters)[ curDecl->get_uniqueId() ] = ParamEntry( candidate->get_uniqueId(), adjType->clone(), curDecl->get_type()->clone(), varExpr );
-				inferRecursive( begin, end, newerAlt, newOpenVars, newDecls, newerNeed, level, indexer, out );
-			} else {
-				delete adjType;
-			}
-		}
-	}
+		}
+	}
+
+	/// Unique identifier for matching expression resolutions to their requesting expression
+	UniqueId globalResnSlot = 0;
 
 	template< typename OutputIterator >
-	void AlternativeFinder::Finder::inferParameters( const AssertionSet &need, AssertionSet &have, const Alternative &newAlt, OpenVarSet &openVars, OutputIterator out ) {
-//	PRINT(
-//	    std::cerr << "inferParameters: assertions needed are" << std::endl;
-//	    printAll( need, std::cerr, 8 );
-//	    )
-		SymTab::Indexer decls( indexer );
-		// PRINT(
-		// 	std::cerr << "============= original indexer" << std::endl;
-		// 	indexer.print( std::cerr );
-		// 	std::cerr << "============= new indexer" << std::endl;
-		// 	decls.print( std::cerr );
-		// )
-		addToIndexer( have, decls );
-		AssertionSet newNeed;
-		PRINT(
-			std::cerr << "env is: " << std::endl;
-			newAlt.env.print( std::cerr, 0 );
-			std::cerr << std::endl;
-		)
-
-		inferRecursive( need.begin(), need.end(), newAlt, openVars, decls, newNeed, 0, indexer, out );
-//	PRINT(
-//	    std::cerr << "declaration 14 is ";
-//	    Declaration::declFromId
-//	    *out++ = newAlt;
-//	    )
+	void AlternativeFinder::Finder::inferParameters( Alternative &newAlt, OutputIterator out ) {
+		// 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;
 	}
 
@@ -951,5 +863,5 @@
 		}
 		// build and validate new alternative
-		Alternative newAlt( appExpr, result.env, cost );
+		Alternative newAlt{ appExpr, result.env, result.openVars, result.need, cost };
 		PRINT(
 			std::cerr << "instantiate function success: " << appExpr << std::endl;
@@ -957,5 +869,5 @@
 			printAssertionSet( result.need, std::cerr, 8 );
 		)
-		inferParameters( result.need, result.have, newAlt, result.openVars, out );
+		inferParameters( newAlt, out );
 	}
 
@@ -1202,5 +1114,5 @@
 
 		// function may return struct or union value, in which case we need to add alternatives
-		// for implicitconversions to each of the anonymous members, must happen after findMinCost
+		// for implicit conversions to each of the anonymous members, must happen after findMinCost
 		// since anon conversions are never the cheapest expression
 		for ( const Alternative & alt : winners ) {
@@ -1234,5 +1146,5 @@
 			if ( isLvalue( alt.expr ) ) {
 				alternatives.push_back(
-					Alternative{ new AddressExpr( alt.expr->clone() ), alt.env, alt.cost } );
+					Alternative{ alt, new AddressExpr( alt.expr->clone() ), alt.cost } );
 			} // if
 		} // for
@@ -1240,5 +1152,5 @@
 
 	void AlternativeFinder::Finder::postvisit( LabelAddressExpr * expr ) {
-		alternatives.push_back( Alternative{ expr->clone(), env, Cost::zero } );
+		alternatives.push_back( Alternative{ expr->clone(), env } );
 	}
 
@@ -1285,6 +1197,7 @@
 		AltList candidates;
 		for ( Alternative & alt : finder.alternatives ) {
-			AssertionSet needAssertions, haveAssertions;
-			OpenVarSet openVars;
+			AssertionSet needAssertions( alt.need.begin(), alt.need.end() );
+			AssertionSet haveAssertions;
+			OpenVarSet openVars{ alt.openVars };
 
 			alt.env.extractOpenVars( openVars );
@@ -1314,8 +1227,8 @@
 				// count one safe conversion for each value that is thrown away
 				thisCost.incSafe( discardedValues );
-				Alternative newAlt( restructureCast( alt.expr->clone(), toType, castExpr->isGenerated ), alt.env,
-					alt.cost, thisCost );
-				inferParameters( needAssertions, haveAssertions, newAlt, openVars,
-					back_inserter( candidates ) );
+				Alternative newAlt{ 
+					restructureCast( alt.expr->clone(), toType, castExpr->isGenerated ), 
+					alt.env, openVars, needAssertions, alt.cost + thisCost, thisCost };
+				inferParameters( newAlt, back_inserter( candidates ) );
 			} // if
 		} // for
@@ -1330,12 +1243,12 @@
 
 	void AlternativeFinder::Finder::postvisit( VirtualCastExpr * castExpr ) {
-		assertf( castExpr->get_result(), "Implicate virtual cast targets not yet supported." );
+		assertf( castExpr->get_result(), "Implicit virtual cast targets not yet supported." );
 		AlternativeFinder finder( indexer, env );
 		// don't prune here, since it's guaranteed all alternatives will have the same type
 		finder.findWithoutPrune( castExpr->get_arg() );
 		for ( Alternative & alt : finder.alternatives ) {
-			alternatives.push_back( Alternative(
-				new VirtualCastExpr( alt.expr->clone(), castExpr->get_result()->clone() ),
-				alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{
+				alt, new VirtualCastExpr{ alt.expr->clone(), castExpr->get_result()->clone() },
+				alt.cost } );
 		}
 	}
@@ -1365,9 +1278,9 @@
 			// find member of the given type
 			if ( StructInstType *structInst = dynamic_cast< StructInstType* >( aggrExpr->get_result() ) ) {
-				addAggMembers( structInst, aggrExpr, cost, agg->env, get_member_name(memberExpr) );
+				addAggMembers( structInst, aggrExpr, *agg, cost, get_member_name(memberExpr) );
 			} else if ( UnionInstType *unionInst = dynamic_cast< UnionInstType* >( aggrExpr->get_result() ) ) {
-				addAggMembers( unionInst, aggrExpr, cost, agg->env, get_member_name(memberExpr) );
+				addAggMembers( unionInst, aggrExpr, *agg, cost, get_member_name(memberExpr) );
 			} else if ( TupleType * tupleType = dynamic_cast< TupleType * >( aggrExpr->get_result() ) ) {
-				addTupleMembers( tupleType, aggrExpr, cost, agg->env, memberExpr->get_member() );
+				addTupleMembers( tupleType, aggrExpr, *agg, cost, memberExpr->get_member() );
 			} // if
 		} // for
@@ -1375,5 +1288,5 @@
 
 	void AlternativeFinder::Finder::postvisit( MemberExpr *memberExpr ) {
-		alternatives.push_back( Alternative( memberExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ memberExpr->clone(), env } );
 	}
 
@@ -1388,5 +1301,5 @@
 			// addAnonAlternatives uses vector::push_back, which invalidates references to existing elements, so
 			// can't construct in place and use vector::back
-			Alternative newAlt( newExpr, env, Cost::zero, cost );
+			Alternative newAlt{ newExpr, env, OpenVarSet{}, AssertionList{}, Cost::zero, cost };
 			PRINT(
 				std::cerr << "decl is ";
@@ -1406,9 +1319,9 @@
 		// not sufficient to clone here, because variable's type may have changed
 		// since the VariableExpr was originally created.
-		alternatives.push_back( Alternative( new VariableExpr( variableExpr->var ), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ new VariableExpr{ variableExpr->var }, env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( ConstantExpr *constantExpr ) {
-		alternatives.push_back( Alternative( constantExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ constantExpr->clone(), env } );
 	}
 
@@ -1416,5 +1329,6 @@
 		if ( sizeofExpr->get_isType() ) {
 			Type * newType = sizeofExpr->get_type()->clone();
-			alternatives.push_back( Alternative( new SizeofExpr( resolveTypeof( newType, indexer ) ), env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				new SizeofExpr{ resolveTypeof( newType, indexer ) }, env } );
 		} else {
 			// find all alternatives for the argument to sizeof
@@ -1430,5 +1344,6 @@
 			Alternative &choice = winners.front();
 			referenceToRvalueConversion( choice.expr, choice.cost );
-			alternatives.push_back( Alternative( new SizeofExpr( choice.expr->clone() ), choice.env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				choice, new SizeofExpr( choice.expr->clone() ), Cost::zero } );
 		} // if
 	}
@@ -1437,5 +1352,6 @@
 		if ( alignofExpr->get_isType() ) {
 			Type * newType = alignofExpr->get_type()->clone();
-			alternatives.push_back( Alternative( new AlignofExpr( resolveTypeof( newType, indexer ) ), env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				new AlignofExpr{ resolveTypeof( newType, indexer ) }, env } );
 		} else {
 			// find all alternatives for the argument to sizeof
@@ -1451,5 +1367,6 @@
 			Alternative &choice = winners.front();
 			referenceToRvalueConversion( choice.expr, choice.cost );
-			alternatives.push_back( Alternative( new AlignofExpr( choice.expr->clone() ), choice.env, Cost::zero ) );
+			alternatives.push_back( Alternative{ 
+				choice, new AlignofExpr{ choice.expr->clone() }, Cost::zero } );
 		} // if
 	}
@@ -1461,5 +1378,6 @@
 		for ( std::list< Declaration* >::const_iterator i = members.begin(); i != members.end(); ++i ) {
 			if ( DeclarationWithType *dwt = dynamic_cast< DeclarationWithType* >( *i ) ) {
-				alternatives.push_back( Alternative( new OffsetofExpr( aggInst->clone(), dwt ), env, Cost::zero ) );
+				alternatives.push_back( Alternative{ 
+					new OffsetofExpr{ aggInst->clone(), dwt }, env } );
 				renameTypes( alternatives.back().expr );
 			} else {
@@ -1480,9 +1398,9 @@
 
 	void AlternativeFinder::Finder::postvisit( OffsetofExpr *offsetofExpr ) {
-		alternatives.push_back( Alternative( offsetofExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ offsetofExpr->clone(), env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( OffsetPackExpr *offsetPackExpr ) {
-		alternatives.push_back( Alternative( offsetPackExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ offsetPackExpr->clone(), env } );
 	}
 
@@ -1504,5 +1422,7 @@
 				Cost cost = Cost::zero;
 				Expression * newExpr = data.combine( cost );
-				alternatives.push_back( Alternative( new AttrExpr( newExpr, argType->clone() ), env, Cost::zero, cost ) );
+				alternatives.push_back( Alternative{ 
+					new AttrExpr{ newExpr, argType->clone() }, env, OpenVarSet{}, 
+					AssertionList{}, Cost::zero, cost } );
 				for ( DeclarationWithType * retVal : function->returnVals ) {
 					alternatives.back().expr->result = retVal->get_type()->clone();
@@ -1543,5 +1463,6 @@
 				Cost cost = Cost::zero;
 				Expression * newExpr = data.combine( cost );
-				alternatives.push_back( Alternative( newExpr, env, Cost::zero, cost ) );
+				alternatives.push_back( Alternative{ 
+					newExpr, env, OpenVarSet{}, AssertionList{}, Cost::zero, cost } );
 				renameTypes( alternatives.back().expr );
 			} // for
@@ -1558,10 +1479,17 @@
 		for ( const Alternative & first : firstFinder.alternatives ) {
 			for ( const Alternative & second : secondFinder.alternatives ) {
-				TypeEnvironment compositeEnv;
-				compositeEnv.simpleCombine( first.env );
+				TypeEnvironment compositeEnv{ first.env };
 				compositeEnv.simpleCombine( second.env );
-
-				LogicalExpr *newExpr = new LogicalExpr( first.expr->clone(), second.expr->clone(), logicalExpr->get_isAnd() );
-				alternatives.push_back( Alternative( newExpr, compositeEnv, first.cost + second.cost ) );
+				OpenVarSet openVars{ first.openVars };
+				mergeOpenVars( openVars, second.openVars );
+				AssertionSet need;
+				cloneAll( first.need, need );
+				cloneAll( second.need, need );
+
+				LogicalExpr *newExpr = new LogicalExpr{ 
+					first.expr->clone(), second.expr->clone(), logicalExpr->get_isAnd() };
+				alternatives.push_back( Alternative{ 
+					newExpr, std::move(compositeEnv), std::move(openVars), 
+					AssertionList( need.begin(), need.end() ), first.cost + second.cost } );
 			}
 		}
@@ -1584,22 +1512,34 @@
 			for ( const Alternative & second : secondFinder.alternatives ) {
 				for ( const Alternative & third : thirdFinder.alternatives ) {
-					TypeEnvironment compositeEnv;
-					compositeEnv.simpleCombine( first.env );
+					TypeEnvironment compositeEnv{ first.env };
 					compositeEnv.simpleCombine( second.env );
 					compositeEnv.simpleCombine( third.env );
-
+					OpenVarSet openVars{ first.openVars };
+					mergeOpenVars( openVars, second.openVars );
+					mergeOpenVars( openVars, third.openVars );
+					AssertionSet need;
+					cloneAll( first.need, need );
+					cloneAll( second.need, need );
+					cloneAll( third.need, need );
+					AssertionSet have;
+					
 					// unify true and false types, then infer parameters to produce new alternatives
-					OpenVarSet openVars;
-					AssertionSet needAssertions, haveAssertions;
-					Alternative newAlt( 0, compositeEnv, first.cost + second.cost + third.cost );
 					Type* commonType = nullptr;
-					if ( unify( second.expr->result, third.expr->result, newAlt.env, needAssertions, haveAssertions, openVars, indexer, commonType ) ) {
-						ConditionalExpr *newExpr = new ConditionalExpr( first.expr->clone(), second.expr->clone(), third.expr->clone() );
+					if ( unify( second.expr->result, third.expr->result, compositeEnv, 
+							need, have, openVars, indexer, commonType ) ) {
+						ConditionalExpr *newExpr = new ConditionalExpr{ 
+							first.expr->clone(), second.expr->clone(), third.expr->clone() };
 						newExpr->result = commonType ? commonType : second.expr->result->clone();
 						// convert both options to the conditional result type
-						newAlt.cost += computeExpressionConversionCost( newExpr->arg2, newExpr->result, indexer, newAlt.env );
-						newAlt.cost += computeExpressionConversionCost( newExpr->arg3, newExpr->result, indexer, newAlt.env );
-						newAlt.expr = newExpr;
-						inferParameters( needAssertions, haveAssertions, newAlt, openVars, back_inserter( alternatives ) );
+						Cost cost = first.cost + second.cost + third.cost;
+						cost += computeExpressionConversionCost( 
+							newExpr->arg2, newExpr->result, indexer, compositeEnv );
+						cost += computeExpressionConversionCost( 
+							newExpr->arg3, newExpr->result, indexer, compositeEnv );
+						// output alternative
+						Alternative newAlt{ 
+							newExpr, std::move(compositeEnv), std::move(openVars), 
+							AssertionList( need.begin(), need.end() ), cost };
+						inferParameters( newAlt, back_inserter( alternatives ) );
 					} // if
 				} // for
@@ -1614,5 +1554,6 @@
 		secondFinder.findWithAdjustment( commaExpr->get_arg2() );
 		for ( const Alternative & alt : secondFinder.alternatives ) {
-			alternatives.push_back( Alternative( new CommaExpr( newFirstArg->clone(), alt.expr->clone() ), alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{ 
+				alt, new CommaExpr{ newFirstArg->clone(), alt.expr->clone() }, alt.cost } );
 		} // for
 		delete newFirstArg;
@@ -1629,16 +1570,23 @@
 		for ( const Alternative & first : firstFinder.alternatives ) {
 			for ( const Alternative & second : secondFinder.alternatives ) {
-				TypeEnvironment compositeEnv;
-				compositeEnv.simpleCombine( first.env );
+				TypeEnvironment compositeEnv{ first.env };
 				compositeEnv.simpleCombine( second.env );
-				OpenVarSet openVars;
-				AssertionSet needAssertions, haveAssertions;
-				Alternative newAlt( 0, compositeEnv, first.cost + second.cost );
+				OpenVarSet openVars{ first.openVars };
+				mergeOpenVars( openVars, second.openVars );
+				AssertionSet need;
+				cloneAll( first.need, need );
+				cloneAll( second.need, need );
+				AssertionSet have;
+
 				Type* commonType = nullptr;
-				if ( unify( first.expr->result, second.expr->result, newAlt.env, needAssertions, haveAssertions, openVars, indexer, commonType ) ) {
-					RangeExpr * newExpr = new RangeExpr( first.expr->clone(), second.expr->clone() );
+				if ( unify( first.expr->result, second.expr->result, compositeEnv, need, have, 
+						openVars, indexer, commonType ) ) {
+					RangeExpr * newExpr = 
+						new RangeExpr{ first.expr->clone(), second.expr->clone() };
 					newExpr->result = commonType ? commonType : first.expr->result->clone();
-					newAlt.expr = newExpr;
-					inferParameters( needAssertions, haveAssertions, newAlt, openVars, back_inserter( alternatives ) );
+					Alternative newAlt{ 
+						newExpr, std::move(compositeEnv), std::move(openVars), 
+						AssertionList( need.begin(), need.end() ), first.cost + second.cost };
+					inferParameters( newAlt, back_inserter( alternatives ) );
 				} // if
 			} // for
@@ -1658,16 +1606,24 @@
 
 			TypeEnvironment compositeEnv;
-			simpleCombineEnvironments( alts.begin(), alts.end(), compositeEnv );
-			alternatives.push_back(
-				Alternative{ new TupleExpr( exprs ), compositeEnv, sumCost( alts ) } );
+			OpenVarSet openVars;
+			AssertionSet need;
+			for ( const Alternative& alt : alts ) {
+				compositeEnv.simpleCombine( alt.env );
+				mergeOpenVars( openVars, alt.openVars );
+				cloneAll( alt.need, need );
+			}
+			
+			alternatives.push_back( Alternative{ 
+				new TupleExpr{ exprs }, std::move(compositeEnv), std::move(openVars), 
+				AssertionList( need.begin(), need.end() ), sumCost( alts ) } );
 		} // for
 	}
 
 	void AlternativeFinder::Finder::postvisit( TupleExpr *tupleExpr ) {
-		alternatives.push_back( Alternative( tupleExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ tupleExpr->clone(), env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( ImplicitCopyCtorExpr * impCpCtorExpr ) {
-		alternatives.push_back( Alternative( impCpCtorExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ impCpCtorExpr->clone(), env } );
 	}
 
@@ -1678,14 +1634,15 @@
 		finder.findWithoutPrune( ctorExpr->get_callExpr() );
 		for ( Alternative & alt : finder.alternatives ) {
-			alternatives.push_back( Alternative( new ConstructorExpr( alt.expr->clone() ), alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{ 
+				alt, new ConstructorExpr( alt.expr->clone() ), alt.cost } );
 		}
 	}
 
 	void AlternativeFinder::Finder::postvisit( TupleIndexExpr *tupleExpr ) {
-		alternatives.push_back( Alternative( tupleExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ tupleExpr->clone(), env } );
 	}
 
 	void AlternativeFinder::Finder::postvisit( TupleAssignExpr *tupleAssignExpr ) {
-		alternatives.push_back( Alternative( tupleAssignExpr->clone(), env, Cost::zero ) );
+		alternatives.push_back( Alternative{ tupleAssignExpr->clone(), env } );
 	}
 
@@ -1696,5 +1653,5 @@
 			// ensure that the id is passed on to the UniqueExpr alternative so that the expressions are "linked"
 			UniqueExpr * newUnqExpr = new UniqueExpr( alt.expr->clone(), unqExpr->get_id() );
-			alternatives.push_back( Alternative( newUnqExpr, alt.env, alt.cost ) );
+			alternatives.push_back( Alternative{ alt, newUnqExpr, alt.cost } );
 		}
 	}
@@ -1704,5 +1661,5 @@
 		ResolvExpr::resolveStmtExpr( newStmtExpr, indexer );
 		// xxx - this env is almost certainly wrong, and needs to somehow contain the combined environments from all of the statements in the stmtExpr...
-		alternatives.push_back( Alternative( newStmtExpr, env, Cost::zero ) );
+		alternatives.push_back( Alternative{ newStmtExpr, env } );
 	}
 
@@ -1726,19 +1683,27 @@
 			for ( Alternative & alt : finder.get_alternatives() ) {
 				TypeEnvironment newEnv( alt.env );
-				AssertionSet needAssertions, haveAssertions;
-				OpenVarSet openVars;  // find things in env that don't have a "representative type" and claim those are open vars?
+				AssertionSet need;
+				cloneAll( alt.need, need );
+				AssertionSet have;
+				OpenVarSet openVars( alt.openVars );  
+				// xxx - find things in env that don't have a "representative type" and claim 
+				// those are open vars?
 				PRINT(
 					std::cerr << "  @ " << toType << " " << initAlt.designation << std::endl;
 				)
-				// It's possible that a cast can throw away some values in a multiply-valued expression.  (An example is a
-				// cast-to-void, which casts from one value to zero.)  Figure out the prefix of the subexpression results
-				// that are cast directly.  The candidate is invalid if it has fewer results than there are types to cast
-				// to.
+				// It's possible that a cast can throw away some values in a multiply-valued 
+				// expression. (An example is a cast-to-void, which casts from one value to 
+				// zero.)  Figure out the prefix of the subexpression results that are cast 
+				// directly.  The candidate is invalid if it has fewer results than there are 
+				// types to cast to.
 				int discardedValues = alt.expr->result->size() - toType->size();
 				if ( discardedValues < 0 ) continue;
-				// xxx - may need to go into tuple types and extract relevant types and use unifyList. Note that currently, this does not
-				// allow casting a tuple to an atomic type (e.g. (int)([1, 2, 3]))
+				// xxx - may need to go into tuple types and extract relevant types and use 
+				// unifyList. Note that currently, this does not allow casting a tuple to an 
+				// atomic type (e.g. (int)([1, 2, 3]))
+				
 				// unification run for side-effects
-				unify( toType, alt.expr->result, newEnv, needAssertions, haveAssertions, openVars, indexer ); // xxx - do some inspecting on this line... why isn't result bound to initAlt.type??
+				unify( toType, alt.expr->result, newEnv, need, have, openVars, indexer );
+				// xxx - do some inspecting on this line... why isn't result bound to initAlt.type?
 
 				Cost thisCost = castCost( alt.expr->result, toType, indexer, newEnv );
@@ -1746,6 +1711,10 @@
 					// count one safe conversion for each value that is thrown away
 					thisCost.incSafe( discardedValues );
-					Alternative newAlt( new InitExpr( restructureCast( alt.expr->clone(), toType, true ), initAlt.designation->clone() ), newEnv, alt.cost, thisCost );
-					inferParameters( needAssertions, haveAssertions, newAlt, openVars, back_inserter( candidates ) );
+					Alternative newAlt{ 
+						new InitExpr{ 
+							restructureCast( alt.expr->clone(), toType, true ), initAlt.designation->clone() }, 
+						std::move(newEnv), std::move(openVars), 
+						AssertionList( need.begin(), need.end() ), alt.cost, thisCost };
+					inferParameters( newAlt, back_inserter( candidates ) );
 				}
 			}
Index: src/ResolvExpr/AlternativeFinder.h
===================================================================
--- src/ResolvExpr/AlternativeFinder.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/AlternativeFinder.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -9,7 +9,7 @@
 // Author           : Richard C. Bilson
 // Created On       : Sat May 16 23:56:12 2015
-// Last Modified By : Andrew Beach
-// Last Modified On : Wed Jul 26 11:24:00 2017
-// Update Count     : 4
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct -5 10:01:00 2018
+// Update Count     : 5
 //
 
@@ -24,4 +24,5 @@
 #include "ResolvExpr/Cost.h"             // for Cost, Cost::infinity
 #include "ResolvExpr/TypeEnvironment.h"  // for AssertionSet, OpenVarSet
+#include "ResolvMode.h"                  // for ResolvMode
 #include "SynTree/Visitor.h"             // for Visitor
 #include "SynTree/SynTree.h"             // for Visitor Nodes
@@ -68,5 +69,5 @@
 		}
 
-		void find( Expression *expr, bool adjust = false, bool prune = true, bool failFast = true );
+		void find( Expression *expr, ResolvMode mode = ResolvMode{} );
 		/// Calls find with the adjust flag set; adjustment turns array and function types into equivalent pointer types
 		void findWithAdjustment( Expression *expr );
Index: src/ResolvExpr/ConversionCost.cc
===================================================================
--- src/ResolvExpr/ConversionCost.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/ConversionCost.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -28,10 +28,12 @@
 
 namespace ResolvExpr {
-	const Cost Cost::zero =      Cost(  0,  0,  0,  0 );
-	const Cost Cost::infinity =  Cost( -1, -1, -1, -1 );
-	const Cost Cost::unsafe =    Cost(  1,  0,  0,  0 );
-	const Cost Cost::poly =      Cost(  0,  1,  0,  0 );
-	const Cost Cost::safe =      Cost(  0,  0,  1,  0 );
-	const Cost Cost::reference = Cost(  0,  0,  0,  1 );
+	const Cost Cost::zero =      Cost{  0,  0,  0,  0,  0,  0 };
+	const Cost Cost::infinity =  Cost{ -1, -1, -1, -1,  1, -1 };
+	const Cost Cost::unsafe =    Cost{  1,  0,  0,  0,  0,  0 };
+	const Cost Cost::poly =      Cost{  0,  1,  0,  0,  0,  0 };
+	const Cost Cost::safe =      Cost{  0,  0,  1,  0,  0,  0 };
+	const Cost Cost::var =       Cost{  0,  0,  0,  1,  0,  0 };
+	const Cost Cost::spec =      Cost{  0,  0,  0,  0, -1,  0 };
+	const Cost Cost::reference = Cost{  0,  0,  0,  0,  0,  1 };
 
 #if 0
Index: src/ResolvExpr/Cost.h
===================================================================
--- src/ResolvExpr/Cost.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/Cost.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -9,7 +9,7 @@
 // Author           : Richard C. Bilson
 // Created On       : Sun May 17 09:39:50 2015
-// Last Modified By : Peter A. Buhr
-// Last Modified On : Sat Jul 22 09:35:55 2017
-// Update Count     : 5
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 14:32:00 2018
+// Update Count     : 7
 //
 
@@ -21,5 +21,6 @@
 	class Cost {
 	  private:
-		Cost( int unsafeCost, int polyCost, int safeCost, int referenceCost );
+		Cost( int unsafeCost, int polyCost, int safeCost, int varCost, int specCost,
+			int referenceCost );
 
 	  public:
@@ -27,4 +28,6 @@
 		Cost & incPoly( int inc = 1 );
 		Cost & incSafe( int inc = 1 );
+		Cost & incVar( int inc = 1 );
+		Cost & decSpec( int inc = 1 );
 		Cost & incReference( int inc = 1 );
 
@@ -32,4 +35,6 @@
 		int get_polyCost() const { return polyCost; }
 		int get_safeCost() const { return safeCost; }
+		int get_varCost() const { return varCost; }
+		int get_specCost() const { return specCost; }
 		int get_referenceCost() const { return referenceCost; }
 
@@ -41,4 +46,6 @@
 		bool operator!=( const Cost &other ) const;
 		friend std::ostream &operator<<( std::ostream &os, const Cost &cost );
+		// returns negative for *this < other, 0 for *this == other, positive for *this > other
+		int compare( const Cost &other ) const;
 
 		static const Cost zero;
@@ -48,15 +55,21 @@
 		static const Cost poly;
 		static const Cost safe;
+		static const Cost var;
+		static const Cost spec;
 		static const Cost reference;
+
 	  private:
-		int compare( const Cost &other ) const;
-
-		int unsafeCost;
-		int polyCost;
-		int safeCost;
-		int referenceCost;
+		int unsafeCost;     ///< Unsafe (narrowing) conversions
+		int polyCost;       ///< Count of parameters and return values bound to some poly type
+		int safeCost;       ///< Safe (widening) conversions
+		int varCost;        ///< Count of polymorphic type variables
+		int specCost;       ///< Polymorphic type specializations (type assertions), negative cost
+		int referenceCost;  ///< reference conversions
 	};
 
-	inline Cost::Cost( int unsafeCost, int polyCost, int safeCost, int referenceCost ) : unsafeCost( unsafeCost ), polyCost( polyCost ), safeCost( safeCost ), referenceCost( referenceCost ) {}
+	inline Cost::Cost( int unsafeCost, int polyCost, int safeCost, int varCost, int specCost, 
+			int referenceCost ) 
+		: unsafeCost( unsafeCost ), polyCost( polyCost ), safeCost( safeCost ), varCost( varCost ), 
+		  specCost( specCost ), referenceCost( referenceCost ) {}
 
 	inline Cost & Cost::incUnsafe( int inc ) {
@@ -75,4 +88,16 @@
 		if ( *this == infinity ) return *this;
 		safeCost += inc;
+		return *this;
+	}
+
+	inline Cost & Cost::incVar( int inc ) {
+		if ( *this == infinity ) return *this;
+		varCost += inc;
+		return *this;
+	}
+
+	inline Cost& Cost::decSpec( int dec ) {
+		if ( *this == infinity ) return *this;
+		specCost -= dec;
 		return *this;
 	}
@@ -86,10 +111,16 @@
 	inline Cost Cost::operator+( const Cost &other ) const {
 		if ( *this == infinity || other == infinity ) return infinity;
-		return Cost( unsafeCost + other.unsafeCost, polyCost + other.polyCost, safeCost + other.safeCost, referenceCost + other.referenceCost );
+		return Cost{ 
+			unsafeCost + other.unsafeCost, polyCost + other.polyCost, safeCost + other.safeCost, 
+			varCost + other.varCost, specCost + other.specCost, 
+			referenceCost + other.referenceCost };
 	}
 
 	inline Cost Cost::operator-( const Cost &other ) const {
 		if ( *this == infinity || other == infinity ) return infinity;
-		return Cost( unsafeCost - other.unsafeCost, polyCost - other.polyCost, safeCost - other.safeCost, referenceCost - other.referenceCost );
+		return Cost{ 
+			unsafeCost - other.unsafeCost, polyCost - other.polyCost, safeCost - other.safeCost, 
+			varCost - other.varCost, specCost - other.specCost, 
+			referenceCost - other.referenceCost };
 	}
 
@@ -103,4 +134,6 @@
 		polyCost += other.polyCost;
 		safeCost += other.safeCost;
+		varCost += other.varCost;
+		specCost += other.specCost;
 		referenceCost += other.referenceCost;
 		return *this;
@@ -123,4 +156,12 @@
 		} else if ( safeCost < other.safeCost ) {
 			return true;
+		} else if ( varCost > other.varCost ) {
+			return false;
+		} else if ( varCost < other.varCost ) {
+			return true;
+		} else if ( specCost > other.specCost ) {
+			return false;
+		} else if ( specCost > other.specCost ) {
+			return true;
 		} else if ( referenceCost > other.referenceCost ) {
 			return false;
@@ -130,4 +171,16 @@
 			return false;
 		} // if
+	}
+
+	inline int Cost::compare( const Cost &other ) const {
+		if ( *this == infinity ) return +1;
+		if ( other == infinity ) return -1;
+
+		int c = unsafeCost - other.unsafeCost; if ( c ) return c;
+		c = polyCost - other.polyCost; if ( c ) return c;
+		c = safeCost - other.safeCost; if ( c ) return c;
+		c = varCost - other.varCost; if ( c ) return c;
+		c = specCost - other.specCost; if ( c ) return c;
+		return referenceCost - other.referenceCost;
 	}
 
@@ -136,4 +189,6 @@
 			&& polyCost == other.polyCost
 			&& safeCost == other.safeCost
+			&& varCost == other.varCost
+			&& specCost == other.specCost
 			&& referenceCost == other.referenceCost;
 	}
@@ -144,6 +199,7 @@
 
 	inline std::ostream &operator<<( std::ostream &os, const Cost &cost ) {
-		os << "( " << cost.unsafeCost << ", " << cost.polyCost << ", " << cost.safeCost << ", " << cost.referenceCost << " )";
-		return os;
+		return os << "( " << cost.unsafeCost << ", " << cost.polyCost << ", " 
+		          << cost.safeCost << ", " << cost.varCost << ", " << cost.specCost << ", "
+		          << cost.referenceCost << " )";
 	}
 } // namespace ResolvExpr
Index: src/ResolvExpr/ResolvMode.h
===================================================================
--- src/ResolvExpr/ResolvMode.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
+++ src/ResolvExpr/ResolvMode.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -0,0 +1,54 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// ResolvMode.h --
+//
+// Author           : Aaron B. Moss
+// Created On       : Mon Jun 11 13:28:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 13:46:00 2018
+// Update Count     : 2
+//
+
+#pragma once
+
+namespace ResolvExpr {
+	/// Flag set for resolution
+	struct ResolvMode {
+		const bool adjust;			 ///< Adjust array and function types to pointer types? [false]
+		const bool prune;            ///< Prune alternatives to min-cost per return type? [true]
+		const bool failFast;         ///< Fail on no resulting alternatives? [true]
+		const bool resolveAssns;     ///< Resolve assertions? [false]
+
+	private:
+		constexpr ResolvMode(bool a, bool p, bool ff, bool ra) 
+		: adjust(a), prune(p), failFast(ff), resolveAssns(ra) {}
+
+	public:
+		/// Default settings
+		constexpr ResolvMode() : adjust(false), prune(true), failFast(true), resolveAssns(false) {}
+		
+		/// With adjust flag set; turns array and function types into equivalent pointers
+		static constexpr ResolvMode withAdjustment() { return { true, true, true, false }; }
+
+		/// With adjust flag set but prune unset; pruning ensures there is at least one alternative 
+		/// per result type
+		static constexpr ResolvMode withoutPrune() { return { true, false, true, false }; }
+
+		/// With adjust and prune flags set but failFast unset; failFast ensures there is at least 
+		/// one resulting alternative
+		static constexpr ResolvMode withoutFailFast() { return { true, true, false, false }; }
+
+		/// The same mode, but with resolveAssns turned on; for top-level calls
+		ResolvMode atTopLevel() const { return { adjust, prune, failFast, true }; }
+	};
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/ResolveAssertions.cc
===================================================================
--- src/ResolvExpr/ResolveAssertions.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
+++ src/ResolvExpr/ResolveAssertions.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -0,0 +1,444 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// ResolveAssertions.cc --
+//
+// Author           : Aaron B. Moss
+// Created On       : Fri Oct 05 13:46:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 13:46:00 2018
+// Update Count     : 1
+//
+
+#include "ResolveAssertions.h"
+
+#include <algorithm>                // for sort
+#include <cassert>                  // for assertf
+#include <list>                     // for list
+#include <memory>                   // for unique_ptr
+#include <unordered_map>            // for unordered_map, unordered_multimap
+#include <utility>                  // for move
+#include <vector>                   // for vector
+
+#include "Alternative.h"            // for Alternative, AssertionItem, AssertionList
+#include "Common/FilterCombos.h"    // for filterCombos
+#include "Common/utility.h"         // for sort_mins
+#include "ResolvExpr/RenameVars.h"  // for renameTyVars
+#include "SymTab/Indexer.h"         // for Indexer
+#include "SymTab/Mangler.h"         // for Mangler
+#include "SynTree/Expression.h"     // for InferredParams
+#include "TypeEnvironment.h"        // for TypeEnvironment, etc.
+#include "typeops.h"                // for adjustExprType
+#include "Unify.h"                  // for unify
+
+namespace ResolvExpr {
+	/// Unified assertion candidate
+	struct AssnCandidate {
+		SymTab::Indexer::IdData cdata;  ///< Satisfying declaration
+		Type* adjType;                  ///< Satisfying type
+		TypeEnvironment env;            ///< Post-unification environment
+		AssertionSet have;              ///< Post-unification have-set
+		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, UniqueId resnSlot ) 
+		: cdata(cdata), adjType(adjType), env(std::move(env)), have(std::move(have)), 
+			need(std::move(need)), openVars(std::move(openVars)), resnSlot(resnSlot) {}
+	};
+
+	/// List of candidate assertion resolutions
+	using CandidateList = std::vector<AssnCandidate>;
+
+	/// Reference to single deferred item
+	struct DeferRef {
+		const DeclarationWithType* decl;
+		const AssertionSetValue& info;
+		const AssnCandidate& match;
+	};
+
+	/// Wrapper for the deferred items from a single assertion resolution.
+	/// 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] }; }
+	};
+
+	/// List of deferred resolution items
+	using DeferList = std::vector<DeferItem>;
+
+	/// Combo iterator that combines candidates into an output list, merging their environments. 
+	/// Rejects an appended candidate if the environments cannot be merged.
+	class CandidateEnvMerger {
+		/// Current list of merged candidates
+		std::vector<DeferRef> crnt;
+		/// Stack of environments to support backtracking
+		std::vector<TypeEnvironment> envs;
+		/// Stack of open variables to support backtracking
+		std::vector<OpenVarSet> varSets;
+		/// Indexer to use for merges
+		const SymTab::Indexer& indexer;
+	
+	public:
+		/// The merged environment/open variables and the list of candidates
+		struct OutType {
+			TypeEnvironment env;
+			OpenVarSet openVars;
+			std::vector<DeferRef> assns;
+
+			OutType( const TypeEnvironment& env, const OpenVarSet& openVars, 
+				const std::vector<DeferRef>& assns )
+			: env(env), openVars(openVars), assns(assns) {}
+		};
+
+		CandidateEnvMerger( const TypeEnvironment& env, const OpenVarSet& openVars, 
+			const SymTab::Indexer& indexer )
+		: crnt(), envs{ env }, varSets{ openVars }, indexer(indexer) {}
+
+		bool append( DeferRef i ) {
+			TypeEnvironment env = envs.back();
+			OpenVarSet openVars = varSets.back();
+			mergeOpenVars( openVars, i.match.openVars );
+
+			if ( ! env.combine( i.match.env, openVars, indexer ) ) return false;
+
+			crnt.emplace_back( i );
+			envs.emplace_back( env );
+			varSets.emplace_back( openVars );
+			return true;
+		}
+
+		void backtrack() {
+			crnt.pop_back();
+			envs.pop_back();
+			varSets.pop_back();
+		}
+
+		OutType finalize() { return { envs.back(), varSets.back(), crnt }; }
+	};
+
+	/// Comparator for CandidateEnvMerger outputs that sums their costs and caches the stored 
+	/// sums
+	struct CandidateCost {
+		using Element = CandidateEnvMerger::OutType;
+	private:
+		using Memo = std::unordered_map<const Element*, Cost>;
+		mutable Memo cache;              ///< cache of element costs
+		const SymTab::Indexer& indexer;  ///< Indexer for costing
+
+	public:
+		CandidateCost( const SymTab::Indexer& indexer ) : indexer(indexer) {}
+
+		/// reports the cost of an element
+		Cost get( const Element& x ) const {
+			Memo::const_iterator it = cache.find( &x );
+			if ( it == cache.end() ) {
+				Cost k = Cost::zero;
+				for ( const auto& assn : x.assns ) {
+					k += computeConversionCost( 
+						assn.match.adjType, assn.decl->get_type(), indexer, x.env );
+				}
+				it = cache.emplace_hint( it, &x, k );
+			}
+			return it->second;
+		}
+		
+		/// compares elements by cost
+		bool operator() ( const Element& a, const Element& b ) const {
+			return get( a ) < get( b );
+		}
+	};
+
+	/// Set of assertion resolutions, grouped by resolution ID
+	using InferCache = std::unordered_map< UniqueId, InferredParams >;
+
+	/// Flag for state iteration
+	enum IterateFlag { IterateState };
+
+	/// State needed to resolve a set of assertions
+	struct ResnState {
+		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(), inferred(), indexer(indexer) {
+			need.swap( a.need );
+		}
+
+		/// Updated resolution state with new need-list
+		ResnState( ResnState&& o, IterateFlag )
+		: alt(std::move(o.alt)), need(o.newNeed.begin(), o.newNeed.end()), newNeed(), deferred(), 
+		  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, InferCache& inferred ) {
+		
+		DeclarationWithType* candidate = match.cdata.id;
+		assertf( candidate->get_uniqueId(), "Assertion candidate does not have a unique ID: %s", toString( candidate ).c_str() );
+
+		Expression* varExpr = match.cdata.combine( alt.cvtCost );
+		delete varExpr->result;
+		varExpr->result = match.adjType->clone();
+		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->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 );
+			}
+		}
+	}
+
+	// in AlternativeFinder.cc; unique ID for assertion resolutions
+	extern UniqueId globalResnSlot;
+
+	/// Resolve a single assertion, in context
+	bool resolveAssertion( AssertionItem& assn, ResnState& resn ) {
+		// 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;
+					}
+				}
+				// // 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;
+			}
+		}
+
+		// break if no suitable assertion
+		if ( matches.empty() ) return false;
+
+		// defer if too many suitable assertions
+		if ( matches.size() > 1 ) {
+			resn.deferred.emplace_back( assn.decl, assn.info, std::move(matches) );
+			return true;
+		}
+
+		// otherwise bind current match in ongoing scope
+		AssnCandidate& match = matches.front();
+		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);
+
+		bindAssertion( assn.decl, assn.info, resn.alt, match, resn.inferred );
+		return true;
+	}
+
+	/// Associates inferred parameters with an expression
+	struct InferMatcher {
+		InferCache& inferred;
+
+		InferMatcher( InferCache& inferred ) : inferred( inferred ) {}
+
+		Expression* postmutate( Expression* expr ) {
+			// defer missing inferred parameters until they are hopefully found later
+			std::vector<UniqueId> missingSlots;
+			// place inferred parameters into resolution slots
+			for ( UniqueId slot : expr->resnSlots ) {
+				// fail if no matching parameters found
+				auto it = inferred.find( slot );
+				if ( it == inferred.end() ) {
+					missingSlots.push_back( slot );
+					continue;
+				}
+				InferredParams& inferParams = it->second;
+				
+				// 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.swap( missingSlots );
+			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;
+
+	void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out ) {
+		// finish early if no assertions to resolve
+		if ( alt.need.empty() ) {
+			out.emplace_back( alt );
+			return;
+		}
+
+		// build list of possible resolutions
+		using ResnList = std::vector<ResnState>;
+		SymTab::Indexer root_indexer{ indexer };
+		ResnList resns{ ResnState{ alt, root_indexer } };
+		ResnList new_resns{};
+
+		// resolve assertions in breadth-first-order up to a limited number of levels deep
+		for ( unsigned level = 0; level < recursionLimit; ++level ) {
+			// scan over all mutually-compatible resolutions
+			for ( auto& resn : resns ) {
+				// make initial pass at matching assertions
+				for ( auto& assn : resn.need ) {
+					// fail early if any assertion is not resolvable
+					if ( ! resolveAssertion( assn, resn ) ) goto nextResn;
+				}
+
+				if ( resn.deferred.empty() ) {
+					// either add successful match or push back next state
+					if ( resn.newNeed.empty() ) {
+						finalizeAssertions( resn.alt, resn.inferred, out );
+					} else {
+						new_resns.emplace_back( std::move(resn), IterateState );
+					}
+				} else {
+					// resolve deferred assertions by mutual compatibility
+					std::vector<CandidateEnvMerger::OutType> compatible = filterCombos(
+						resn.deferred, 
+						CandidateEnvMerger{ resn.alt.env, resn.alt.openVars, resn.indexer } );
+					// sort by cost
+					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
+					std::unordered_map<std::string, Cost> found;
+					for ( auto& compat : compatible ) {
+						// filter by environment-adjusted result type, keep only cheapest option
+						Type* resType = alt.expr->result->clone();
+						compat.env.apply( resType );
+						// skip if cheaper alternative already processed with same result type
+						Cost resCost = coster.get( compat );
+						auto it = found.emplace( SymTab::Mangler::mangleType( resType ), resCost );
+						delete resType;
+						if ( it.second == false && it.first->second < resCost ) continue;
+
+						// proceed with resolution step
+						ResnState new_resn = resn;
+
+						// add compatible assertions to new resolution state
+						for ( DeferRef r : compat.assns ) {
+							AssnCandidate match = r.match;
+							addToIndexer( match.have, new_resn.indexer );
+							new_resn.newNeed.insert( match.need.begin(), match.need.end() );
+
+							bindAssertion( r.decl, r.info, new_resn.alt, match, new_resn.inferred );
+						}
+
+						// set mutual environment into resolution state
+						new_resn.alt.env = std::move(compat.env);
+						new_resn.alt.openVars = std::move(compat.openVars);
+
+						// either add sucessful match or push back next state
+						if ( new_resn.newNeed.empty() ) {
+							finalizeAssertions( new_resn.alt, new_resn.inferred, out );
+						} else {
+							new_resns.emplace_back( std::move(new_resn), IterateState );
+						}
+					}
+				}
+			nextResn:; }
+
+			// finish or reset for next round
+			if ( new_resns.empty() ) return;
+			resns.swap( new_resns );
+			new_resns.clear();
+		}
+		
+		// exceeded recursion limit if reaches here
+		if ( out.empty() ) {
+			SemanticError( alt.expr->location, "Too many recursive assertions" );
+		}
+	}
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/ResolveAssertions.h
===================================================================
--- src/ResolvExpr/ResolveAssertions.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
+++ src/ResolvExpr/ResolveAssertions.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -0,0 +1,33 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// ResolveAssertions.h --
+//
+// Author           : Aaron B. Moss
+// Created On       : Fri Oct 05 13:46:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 13:46:00 2018
+// Update Count     : 1
+//
+
+#pragma once
+
+#include "Alternative.h"  // for Alternative, AltList
+
+namespace SymTab {
+	class Indexer;
+}
+
+namespace ResolvExpr {
+	/// Recursively resolves all assertions provided in an alternative; returns true iff succeeds
+	void resolveAssertions( Alternative& alt, const SymTab::Indexer& indexer, AltList& out );
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/Resolver.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -9,14 +9,13 @@
 // Author           : Richard C. Bilson
 // Created On       : Sun May 17 12:17:01 2015
-// Last Modified By : Peter A. Buhr
-// Last Modified On : Sat Feb 17 11:19:40 2018
-// Update Count     : 213
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Fri Oct 05 09:43:00 2018
+// Update Count     : 214
 //
 
-#include <stddef.h>                      // for NULL
 #include <cassert>                       // for strict_dynamic_cast, assert
 #include <memory>                        // for allocator, allocator_traits<...
 #include <tuple>                         // for get
-#include <vector>
+#include <vector>                        // for vector
 
 #include "Alternative.h"                 // for Alternative, AltList
@@ -31,4 +30,5 @@
 #include "ResolvExpr/TypeEnvironment.h"  // for TypeEnvironment
 #include "Resolver.h"
+#include "ResolvMode.h"                  // for ResolvMode
 #include "SymTab/Autogen.h"              // for SizeType
 #include "SymTab/Indexer.h"              // for Indexer
@@ -168,9 +168,15 @@
 
 	namespace {
-		void findUnfinishedKindExpression(Expression * untyped, Alternative & alt, const SymTab::Indexer & indexer, const std::string & kindStr, std::function<bool(const Alternative &)> pred, bool adjust = false, bool prune = true, bool failFast = true) {
+		void findUnfinishedKindExpression(Expression * untyped, Alternative & alt, const SymTab::Indexer & indexer, const std::string & kindStr, std::function<bool(const Alternative &)> pred, ResolvMode mode = ResolvMode{} ) {
 			assertf( untyped, "expected a non-null expression." );
+
+			// xxx - this isn't thread-safe, but should work until we parallelize the resolver
+			static unsigned recursion_level = 0;
+
+			++recursion_level;
 			TypeEnvironment env;
 			AlternativeFinder finder( indexer, env );
-			finder.find( untyped, adjust, prune, failFast );
+			finder.find( untyped, recursion_level == 1 ? mode.atTopLevel() : mode );
+			--recursion_level;
 
 			#if 0
@@ -185,4 +191,5 @@
 			#endif
 
+			// produce filtered list of alternatives
 			AltList candidates;
 			for ( Alternative & alt : finder.get_alternatives() ) {
@@ -192,11 +199,43 @@
 			}
 
-			// xxx - if > 1 alternative with same cost, ignore deleted and pick from remaining
-			// choose the lowest cost expression among the candidates
+			// produce invalid error if no candidates
+			if ( candidates.empty() ) {
+				SemanticError( untyped, toString( "No reasonable alternatives for ", kindStr, (kindStr != "" ? " " : ""), "expression: ") );
+			}
+
+			// search for cheapest candidate
 			AltList winners;
-			findMinCost( candidates.begin(), candidates.end(), back_inserter( winners ) );
-			if ( winners.size() == 0 ) {
-				SemanticError( untyped, toString( "No reasonable alternatives for ", kindStr, (kindStr != "" ? " " : ""), "expression: ") );
-			} else if ( winners.size() != 1 ) {
+			bool seen_undeleted = false;
+			for ( unsigned i = 0; i < candidates.size(); ++i ) {
+				int c = winners.empty() ? -1 : candidates[i].cost.compare( winners.front().cost );
+
+				if ( c > 0 ) continue; // skip more expensive than winner
+
+				if ( c < 0 ) {
+					// reset on new cheapest
+					seen_undeleted = ! findDeletedExpr( candidates[i].expr );
+					winners.clear();
+				} else /* if ( c == 0 ) */ {
+					if ( findDeletedExpr( candidates[i].expr ) ) {
+						// skip deleted expression if already seen one equivalent-cost not
+						if ( seen_undeleted ) continue;
+					} else if ( ! seen_undeleted ) {
+						// replace list of equivalent-cost deleted expressions with one non-deleted
+						winners.clear();
+						seen_undeleted = true;
+					}
+				}
+
+				winners.emplace_back( std::move( candidates[i] ) );
+			}
+
+			// promote alternative.cvtCost to .cost
+			// xxx - I don't know why this is done, but I'm keeping the behaviour from findMinCost
+			for ( Alternative& winner : winners ) {
+				winner.cost = winner.cvtCost;
+			}
+			
+			// produce ambiguous errors, if applicable
+			if ( winners.size() != 1 ) {
 				std::ostringstream stream;
 				stream << "Cannot choose between " << winners.size() << " alternatives for " << kindStr << (kindStr != "" ? " " : "") << "expression\n";
@@ -207,17 +246,23 @@
 			}
 
-			// there is one unambiguous interpretation - move the expression into the with statement
-			Alternative & choice = winners.front();
-			if ( findDeletedExpr( choice.expr ) ) {
+			// single selected choice
+			Alternative& choice = winners.front();
+
+			// fail on only expression deleted
+			if ( ! seen_undeleted ) {
 				SemanticError( untyped->location, choice.expr, "Unique best alternative includes deleted identifier in " );
 			}
+
+			// xxx - check for ambiguous expressions
+			
+			// output selected choice
 			alt = std::move( choice );
 		}
 
 		/// resolve `untyped` to the expression whose alternative satisfies `pred` with the lowest cost; kindStr is used for providing better error messages
-		void findKindExpression(Expression *& untyped, const SymTab::Indexer & indexer, const std::string & kindStr, std::function<bool(const Alternative &)> pred, bool adjust = false, bool prune = true, bool failFast = true) {
+		void findKindExpression(Expression *& untyped, const SymTab::Indexer & indexer, const std::string & kindStr, std::function<bool(const Alternative &)> pred, ResolvMode mode = ResolvMode{}) {
 			if ( ! untyped ) return;
 			Alternative choice;
-			findUnfinishedKindExpression( untyped, choice, indexer, kindStr, pred, adjust, prune, failFast );
+			findUnfinishedKindExpression( untyped, choice, indexer, kindStr, pred, mode );
 			finishExpr( choice.expr, choice.env, untyped->env );
 			delete untyped;
@@ -250,5 +295,5 @@
 		untyped.arg = expr;
 		Alternative choice;
-		findUnfinishedKindExpression( &untyped, choice, indexer, "", standardAlternativeFilter, true );
+		findUnfinishedKindExpression( &untyped, choice, indexer, "", standardAlternativeFilter, ResolvMode::withAdjustment() );
 		CastExpr * castExpr = strict_dynamic_cast< CastExpr * >( choice.expr );
 		env = std::move( choice.env );
@@ -357,9 +402,9 @@
 
 	void Resolver::previsit( ObjectDecl *objectDecl ) {
-		// To handle initialization of routine pointers, e.g., int (*fp)(int) = foo(), means that class-variable
-		// initContext is changed multiple time because the LHS is analysed twice. The second analysis changes
-		// initContext because of a function type can contain object declarations in the return and parameter types. So
-		// each value of initContext is retained, so the type on the first analysis is preserved and used for selecting
-		// the RHS.
+		// To handle initialization of routine pointers, e.g., int (*fp)(int) = foo(), means that 
+		// class-variable initContext is changed multiple time because the LHS is analysed twice. 
+		// The second analysis changes initContext because of a function type can contain object 
+		// declarations in the return and parameter types. So each value of initContext is 
+		// retained, so the type on the first analysis is preserved and used for selecting the RHS.
 		GuardValue( currentObject );
 		currentObject = CurrentObject( objectDecl->get_type() );
@@ -397,7 +442,8 @@
 
 	void Resolver::postvisit( FunctionDecl *functionDecl ) {
-		// default value expressions have an environment which shouldn't be there and trips up later passes.
-		// xxx - it might be necessary to somehow keep the information from this environment, but I can't currently
-		// see how it's useful.
+		// default value expressions have an environment which shouldn't be there and trips up 
+		// later passes.
+		// xxx - it might be necessary to somehow keep the information from this environment, but I 
+		// can't currently see how it's useful.
 		for ( Declaration * d : functionDecl->type->parameters ) {
 			if ( ObjectDecl * obj = dynamic_cast< ObjectDecl * >( d ) ) {
@@ -749,10 +795,12 @@
 		initExpr->expr = nullptr;
 		std::swap( initExpr->env, newExpr->env );
-		// InitExpr may have inferParams in the case where the expression specializes a function pointer,
-		// and newExpr may already have inferParams of its own, so a simple swap is not sufficient.
+		// InitExpr may have inferParams in the case where the expression specializes a function 
+		// pointer, and newExpr may already have inferParams of its own, so a simple swap is not 
+		// sufficient.
 		newExpr->spliceInferParams( initExpr );
 		delete initExpr;
 
-		// get the actual object's type (may not exactly match what comes back from the resolver due to conversions)
+		// get the actual object's type (may not exactly match what comes back from the resolver 
+		// due to conversions)
 		Type * initContext = currentObject.getCurrentType();
 
@@ -766,5 +814,6 @@
 					if ( isCharType( pt->get_base() ) ) {
 						if ( CastExpr *ce = dynamic_cast< CastExpr * >( newExpr ) ) {
-							// strip cast if we're initializing a char[] with a char *, e.g.  char x[] = "hello";
+							// strip cast if we're initializing a char[] with a char *, 
+							// e.g.  char x[] = "hello";
 							newExpr = ce->get_arg();
 							ce->set_arg( nullptr );
@@ -788,9 +837,10 @@
 		// move cursor into brace-enclosed initializer-list
 		currentObject.enterListInit();
-		// xxx - fix this so that the list isn't copied, iterator should be used to change current element
+		// xxx - fix this so that the list isn't copied, iterator should be used to change current 
+		// element
 		std::list<Designation *> newDesignations;
 		for ( auto p : group_iterate(listInit->get_designations(), listInit->get_initializers()) ) {
-			// iterate designations and initializers in pairs, moving the cursor to the current designated object and resolving
-			// the initializer against that object.
+			// iterate designations and initializers in pairs, moving the cursor to the current 
+			// designated object and resolving the initializer against that object.
 			Designation * des = std::get<0>(p);
 			Initializer * init = std::get<1>(p);
@@ -822,7 +872,7 @@
 		// fall back on C-style initializer
 		delete ctorInit->get_ctor();
-		ctorInit->set_ctor( NULL );
+		ctorInit->set_ctor( nullptr );
 		delete ctorInit->get_dtor();
-		ctorInit->set_dtor( NULL );
+		ctorInit->set_dtor( nullptr );
 		maybeAccept( ctorInit->get_init(), *visitor );
 	}
@@ -867,9 +917,9 @@
 
 		// xxx - todo -- what about arrays?
-		// if ( dtor == NULL && InitTweak::isIntrinsicCallStmt( ctorInit->get_ctor() ) ) {
+		// if ( dtor == nullptr && InitTweak::isIntrinsicCallStmt( ctorInit->get_ctor() ) ) {
 		// 	// can reduce the constructor down to a SingleInit using the
 		// 	// second argument from the ctor call, since
 		// 	delete ctorInit->get_ctor();
-		// 	ctorInit->set_ctor( NULL );
+		// 	ctorInit->set_ctor( nullptr );
 
 		// 	Expression * arg =
Index: src/ResolvExpr/SpecCost.cc
===================================================================
--- src/ResolvExpr/SpecCost.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
+++ src/ResolvExpr/SpecCost.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -0,0 +1,119 @@
+//
+// Cforall Version 1.0.0 Copyright (C) 2015 University of Waterloo
+//
+// The contents of this file are covered under the licence agreement in the
+// file "LICENCE" distributed with Cforall.
+//
+// SpecCost.cc --
+//
+// Author           : Aaron B. Moss
+// Created On       : Tue Oct 02 15:50:00 2018
+// Last Modified By : Aaron B. Moss
+// Last Modified On : Tue Oct 02 15:50:00 2018
+// Update Count     : 1
+//
+
+#include <limits>
+#include <list>
+
+#include "Common/PassVisitor.h"
+#include "SynTree/Declaration.h"
+#include "SynTree/Expression.h"
+#include "SynTree/Type.h"
+
+namespace ResolvExpr {
+
+	/// Counts specializations in a type
+	class CountSpecs : public WithShortCircuiting, public WithVisitorRef<CountSpecs> {
+		int count = -1;  ///< specialization count (-1 for none)
+
+	public:
+		int get_count() const { return count >= 0 ? count : 0; }
+
+		// mark specialization of base type
+		void postvisit(PointerType*) { if ( count >= 0 ) ++count; }
+
+		// mark specialization of base type
+		void postvisit(ArrayType*) { if ( count >= 0 ) ++count; }
+
+		// mark specialization of base type
+		void postvisit(ReferenceType*) { if ( count >= 0 ) ++count; }
+
+	private:
+		// takes minimum non-negative count over parameter/return list
+		void takeminover( int& mincount, std::list<DeclarationWithType*>& dwts ) {
+			for ( DeclarationWithType* dwt : dwts ) {
+				count = -1;
+				maybeAccept( dwt->get_type(), *visitor );
+				if ( count != -1 && count < mincount ) mincount = count;
+			}
+		}
+
+	public:
+		// take minimal specialization value over ->returnVals and ->parameters
+		void previsit(FunctionType* fty) {
+			int mincount = std::numeric_limits<int>::max();
+			takeminover( mincount, fty->parameters );
+			takeminover( mincount, fty->returnVals );
+			// add another level to mincount if set
+			count = mincount < std::numeric_limits<int>::max() ? mincount + 1 : -1;
+			// already visited children
+			visit_children = false;
+		}
+	
+	private:
+		// returns minimum non-negative count + 1 over type parameters (-1 if none such)
+		int minover( std::list<Expression*>& parms ) {
+			int mincount = std::numeric_limits<int>::max();
+			for ( Expression* parm : parms ) {
+				count = -1;
+				maybeAccept( parm->result, *visitor );
+				if ( count != -1 && count < mincount ) mincount = count;
+			}
+			return mincount < std::numeric_limits<int>::max() ? mincount + 1 : -1;
+		}
+
+	public:
+		// look for polymorphic parameters
+		void previsit(StructInstType* sty) {
+			count = minover( sty->parameters );
+			visit_children = false;
+		}
+		
+		// look for polymorphic parameters
+		void previsit(UnionInstType* uty) {
+			count = minover( uty->parameters );
+			visit_children = false;
+		}
+
+		// note polymorphic type (which may be specialized)
+		// xxx - maybe account for open/closed type variables
+		void postvisit(TypeInstType*) { count = 0; }
+
+		// take minimal specialization over elements
+		// xxx - maybe don't increment, tuple flattening doesn't necessarily specialize
+		void previsit(TupleType* tty) {
+			int mincount = std::numeric_limits<int>::max();
+			for ( Type* ty : tty->types ) {
+				count = -1;
+				maybeAccept( ty, *visitor );
+				if ( count != -1 && count < mincount ) mincount = count;
+			}
+			count = mincount < std::numeric_limits<int>::max() ? mincount + 1 : -1;
+			visit_children = false;
+		}
+	};
+
+	/// Returns the (negated) specialization cost for a given type
+	int specCost( Type* ty ) {
+		PassVisitor<CountSpecs> counter;
+		maybeAccept( ty, *counter.pass.visitor );
+		return counter.pass.get_count();
+	}
+} // namespace ResolvExpr
+
+// Local Variables: //
+// tab-width: 4 //
+// mode: c++ //
+// compile-command: "make install" //
+// End: //
Index: src/ResolvExpr/TypeEnvironment.cc
===================================================================
--- src/ResolvExpr/TypeEnvironment.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/TypeEnvironment.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -120,5 +120,5 @@
 
 	const EqvClass* TypeEnvironment::lookup( const std::string &var ) const {
-		for ( std::list< EqvClass >::const_iterator i = env.begin(); i != env.end(); ++i ) {
+		for ( ClassList::const_iterator i = env.begin(); i != env.end(); ++i ) {
 			if ( i->vars.find( var ) != i->vars.end() ) return &*i;
 		} // for
@@ -168,5 +168,5 @@
 
 	void TypeEnvironment::makeSubstitution( TypeSubstitution &sub ) const {
-		for ( std::list< EqvClass >::const_iterator theClass = env.begin(); theClass != env.end(); ++theClass ) {
+		for ( ClassList::const_iterator theClass = env.begin(); theClass != env.end(); ++theClass ) {
 			for ( std::set< std::string >::const_iterator theVar = theClass->vars.begin(); theVar != theClass->vars.end(); ++theVar ) {
 				if ( theClass->type ) {
@@ -188,6 +188,6 @@
 	}
 
-	std::list< EqvClass >::iterator TypeEnvironment::internal_lookup( const std::string &var ) {
-		for ( std::list< EqvClass >::iterator i = env.begin(); i != env.end(); ++i ) {
+	TypeEnvironment::ClassList::iterator TypeEnvironment::internal_lookup( const std::string &var ) {
+		for ( ClassList::iterator i = env.begin(); i != env.end(); ++i ) {
 			if ( i->vars.count( var ) ) return i;
 		} // for
@@ -199,6 +199,103 @@
 	}
 
+	// xxx -- this should maybe be worrying about iterator invalidation (see resolv-proto)
+	bool TypeEnvironment::mergeBound( EqvClass& to, const EqvClass& from, OpenVarSet& openVars, const SymTab::Indexer& indexer ) {
+		if ( from.type ) {
+			if ( to.type ) {
+				// attempt to unify bound types
+				std::unique_ptr<Type> toType{ to.type->clone() }, fromType{ from.type->clone() };
+				WidenMode widenMode{ to.allowWidening, from.allowWidening };
+				Type* common = nullptr;
+				AssertionSet need, have;
+				if ( unifyInexact( toType.get(), fromType.get(), *this, need, have, openVars, widenMode, indexer, common ) ) {
+					// unifies, set common type if necessary
+					if ( common ) {
+						common->get_qualifiers() = Type::Qualifiers{};
+						to.set_type( common );
+					}
+				} else return false; // cannot unify
+			} else {
+				to.type = from.type->clone();
+			}
+		}
+
+		// unify widening if matches
+		to.allowWidening &= from.allowWidening;
+		return true;
+	}
+
+	// xxx -- this should maybe be worrying about iterator invalidation (see resolv-proto)
+	bool TypeEnvironment::mergeClasses( TypeEnvironment::ClassList::iterator to, TypeEnvironment::ClassList::iterator from, OpenVarSet& openVars, const SymTab::Indexer& indexer ) {
+		EqvClass& r = *to;
+		EqvClass& s = *from;
+
+		// ensure bounds match
+		if ( ! mergeBound( r, s, openVars, indexer ) ) return false;
+
+		// check safely bindable
+		if ( r.type && occursIn( r.type, s.vars.begin(), s.vars.end(), *this ) ) return false;
+		
+		// merge classes in
+		r.vars.insert( s.vars.begin(), s.vars.end() );
+		r.allowWidening &= s.allowWidening;
+		env.erase( from );
+
+		return true;
+	}
+
+	bool TypeEnvironment::combine( const TypeEnvironment& o, OpenVarSet& openVars, const SymTab::Indexer& indexer ) {
+		// short-circuit easy cases
+		if ( o.isEmpty() ) return true;
+		if ( isEmpty() ) {
+			simpleCombine( o );
+			return true;
+		}
+
+		// merge classes
+		for ( auto ct = o.env.begin(); ct != o.env.end(); ++ct ) {
+			const EqvClass& c = *ct;
+
+			// typeclass in local environment bound to c
+			auto rt = env.end();
+
+			// look for first existing bound variable
+			auto vt = c.vars.begin();
+			for ( ; vt != c.vars.end(); ++vt ) {
+				rt = internal_lookup( *vt );
+				if ( rt != env.end() ) break;
+			}
+
+			if ( rt != env.end() ) {  // c needs to be merged into *rt
+				EqvClass& r = *rt;
+				// merge bindings
+				if ( ! mergeBound( r, c, openVars, indexer ) ) return false;
+				// merge previous unbound variables into this class, checking occurs if needed
+				if ( r.type ) for ( auto ut = c.vars.begin(); ut != vt; ++ut ) {
+					if ( occurs( r.type, *ut, *this ) ) return false;
+					r.vars.insert( *ut );
+				} else { r.vars.insert( c.vars.begin(), vt ); }
+				// merge subsequent variables into this class (skipping *vt, already there)
+				while ( ++vt != c.vars.end() ) {
+					auto st = internal_lookup( *vt );
+					if ( st == env.end() ) {
+						// unbound, safe to add if passes occurs
+						if ( r.type && occurs( r.type, *vt, *this ) ) return false;
+						r.vars.insert( *vt );
+					} else if ( st != rt ) {
+						// bound, but not to the same class
+						if ( ! mergeClasses( rt, st, openVars, indexer ) ) return false;
+					}   // ignore bound into the same class
+				}
+			} else {  // no variables in c bound; just copy up
+				env.push_back( c );
+			}
+		}
+
+		// merged all classes
+		return true;
+	}
+
 	void TypeEnvironment::extractOpenVars( OpenVarSet &openVars ) const {
-		for ( std::list< EqvClass >::const_iterator eqvClass = env.begin(); eqvClass != env.end(); ++eqvClass ) {
+		for ( ClassList::const_iterator eqvClass = env.begin(); eqvClass != env.end(); ++eqvClass ) {
 			for ( std::set< std::string >::const_iterator var = eqvClass->vars.begin(); var != eqvClass->vars.end(); ++var ) {
 				openVars[ *var ] = eqvClass->data;
Index: src/ResolvExpr/TypeEnvironment.h
===================================================================
--- src/ResolvExpr/TypeEnvironment.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/TypeEnvironment.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -39,14 +39,16 @@
 	// declarations.
 	//
-	// I've seen a TU go from 54 minutes to 1 minute 34 seconds with the addition of this comparator.
+	// I've seen a TU go from 54 minutes to 1 minute 34 seconds with the addition of this 
+	// comparator.
 	//
 	// Note: since this compares pointers for position, minor changes in the source file that affect
 	// memory layout can alter compilation time in unpredictable ways. For example, the placement
 	// of a line directive can reorder type pointers with respect to each other so that assertions
-	// are seen in different orders, causing a potentially different number of unification calls when
-	// resolving assertions. I've seen a TU go from 36 seconds to 27 seconds by reordering line directives
-	// alone, so it would be nice to fix this comparison so that assertions compare more consistently.
-	// I've tried to modify this to compare on mangle name instead of type as the second comparator, but
-	// this causes some assertions to never be recorded. More investigation is needed.
+	// are seen in different orders, causing a potentially different number of unification calls 
+	// when resolving assertions. I've seen a TU go from 36 seconds to 27 seconds by reordering 
+	// line directives alone, so it would be nice to fix this comparison so that assertions compare 
+	// more consistently. I've tried to modify this to compare on mangle name instead of type as 
+	// the second comparator, but this causes some assertions to never be recorded. More 
+	// investigation is needed.
 	struct AssertCompare {
 		bool operator()( DeclarationWithType * d1, DeclarationWithType * d2 ) const {
@@ -57,12 +59,16 @@
 	};
 	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;
 	typedef std::map< std::string, TypeDecl::Data > OpenVarSet;
+
+	/// merges one set of open vars into another
+	static inline void mergeOpenVars( OpenVarSet& dst, const OpenVarSet& src ) {
+		for ( const auto& entry : src ) { dst[ entry.first ] = entry.second; }
+	}
 
 	void printAssertionSet( const AssertionSet &, std::ostream &, int indent = 0 );
@@ -91,4 +97,5 @@
 
 	class TypeEnvironment {
+		using ClassList = std::list< EqvClass >;
 	  public:
 		const EqvClass* lookup( const std::string &var ) const;
@@ -103,6 +110,20 @@
 		bool isEmpty() const { return env.empty(); }
 		void print( std::ostream &os, Indenter indent = {} ) const;
-		// void combine( const TypeEnvironment &second, Type *(*combineFunc)( Type*, Type* ) );
+		
+		/// Simply concatenate the second environment onto this one; no safety checks performed
 		void simpleCombine( const TypeEnvironment &second );
+
+	  private:
+		/// Unifies the type bound of to with the type bound of from, returning false if fails
+		bool mergeBound( EqvClass& to, const EqvClass& from, OpenVarSet& openVars, const SymTab::Indexer& indexer );
+
+		/// Merges two type classes from local environment, returning false if fails
+		bool mergeClasses( ClassList::iterator to, ClassList::iterator from, OpenVarSet& openVars, const SymTab::Indexer& indexer );
+
+	  public:
+		/// Merges the second environment with this one, checking compatibility.
+		/// Returns false if fails, but does NOT roll back partial changes.
+		bool combine( const TypeEnvironment& second, OpenVarSet& openVars, const SymTab::Indexer& indexer );
+		
 		void extractOpenVars( OpenVarSet &openVars ) const;
 		TypeEnvironment *clone() const { return new TypeEnvironment( *this ); }
@@ -123,12 +144,12 @@
 		void forbidWidening();
 
-		using iterator = std::list< EqvClass >::const_iterator;
+		using iterator = ClassList::const_iterator;
 		iterator begin() const { return env.begin(); }
 		iterator end() const { return env.end(); }
 
 	  private:
-		std::list< EqvClass > env;
+		ClassList env;
 		
-		std::list< EqvClass >::iterator internal_lookup( const std::string &var );
+		ClassList::iterator internal_lookup( const std::string &var );
 	};
 
Index: src/ResolvExpr/module.mk
===================================================================
--- src/ResolvExpr/module.mk	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/module.mk	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -33,3 +33,5 @@
        ResolvExpr/TypeEnvironment.cc \
        ResolvExpr/CurrentObject.cc \
-       ResolvExpr/ExplodedActual.cc
+       ResolvExpr/ExplodedActual.cc \
+       ResolvExpr/SpecCost.cc \
+       ResolvExpr/ResolveAssertions.cc
Index: src/ResolvExpr/typeops.h
===================================================================
--- src/ResolvExpr/typeops.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/ResolvExpr/typeops.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -72,4 +72,8 @@
 	Cost conversionCost( Type *src, Type *dest, const SymTab::Indexer &indexer, const TypeEnvironment &env );
 
+	// in AlternativeFinder.cc
+	Cost computeConversionCost( Type *actualType, Type *formalType, 
+		const SymTab::Indexer &indexer, const TypeEnvironment &env );
+
 	// in PtrsAssignable.cc
 	int ptrsAssignable( Type *src, Type *dest, const TypeEnvironment &env );
@@ -102,6 +106,18 @@
 	int polyCost( Type *type, const TypeEnvironment &env, const SymTab::Indexer &indexer );
 
+	// in SpecCost.cc
+	int specCost( Type *type );
+
 	// in Occurs.cc
 	bool occurs( Type *type, std::string varName, const TypeEnvironment &env );
+
+	template<typename Iter> 
+	bool occursIn( Type* ty, Iter begin, Iter end, const TypeEnvironment &env ) {
+		while ( begin != end ) {
+			if ( occurs( ty, *begin, env ) ) return true;
+			++begin;
+		}
+		return false;
+	}
 
 	// in AlternativeFinder.cc
Index: src/SynTree/ApplicationExpr.cc
===================================================================
--- src/SynTree/ApplicationExpr.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/SynTree/ApplicationExpr.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -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 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/SynTree/Expression.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -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 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/SynTree/Expression.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -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
Index: src/Tuples/Explode.h
===================================================================
--- src/Tuples/Explode.h	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/Tuples/Explode.h	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -44,13 +44,15 @@
 	template<typename OutputIterator>
 	void append( OutputIterator out, Expression* expr, const ResolvExpr::TypeEnvironment& env,
+			const ResolvExpr::OpenVarSet& openVars, const ResolvExpr::AssertionList& need, 
 			const ResolvExpr::Cost& cost, const ResolvExpr::Cost& cvtCost ) {
-		*out++ = ResolvExpr::Alternative{ expr, env, cost, cvtCost };
+		*out++ = ResolvExpr::Alternative{ expr, env, openVars, need, cost, cvtCost };
 	}
 
 	/// Append alternative to an ExplodedActual
 	static inline void append( ResolvExpr::ExplodedActual& ea, Expression* expr,
-			const ResolvExpr::TypeEnvironment&, const ResolvExpr::Cost&, const ResolvExpr::Cost& ) {
+			const ResolvExpr::TypeEnvironment&, const ResolvExpr::OpenVarSet&, 
+			const ResolvExpr::AssertionList&, const ResolvExpr::Cost&, const ResolvExpr::Cost& ) {
 		ea.exprs.emplace_back( expr );
-		/// xxx -- merge environment, cost?
+		/// xxx -- merge environment, openVars, need, cost?
 	}
 
@@ -68,5 +70,5 @@
 					// distribute reference cast over all components
 					append( std::forward<Output>(out), distributeReference( alt.release_expr() ),
-						alt.env, alt.cost, alt.cvtCost );
+						alt.env, alt.openVars, alt.need, alt.cost, alt.cvtCost );
 				}
 				// in tuple assignment, still need to handle the other cases, but only if not already handled here (don't want to output too many alternatives)
@@ -102,5 +104,6 @@
 		} else {
 			// atomic (non-tuple) type - output a clone of the expression in a new alternative
-			append( std::forward<Output>(out), expr->clone(), alt.env, alt.cost, alt.cvtCost );
+			append( std::forward<Output>(out), expr->clone(), alt.env, alt.openVars, alt.need,  
+				alt.cost, alt.cvtCost );
 		}
 	}
Index: src/Tuples/TupleAssignment.cc
===================================================================
--- src/Tuples/TupleAssignment.cc	(revision 07ec1a266e4ed6bb2fdcd15a073ce16d98d5ea51)
+++ src/Tuples/TupleAssignment.cc	(revision fd732488a0c9611e90598dc83b89dfc5bf7e63b4)
@@ -62,9 +62,21 @@
 		struct Matcher {
 		  public:
-			Matcher( TupleAssignSpotter &spotter, const ResolvExpr::AltList& lhs, const
-				ResolvExpr::AltList& rhs );
+			Matcher( TupleAssignSpotter &spotter, const ResolvExpr::AltList& lhs, 
+				const ResolvExpr::AltList& rhs );
 			virtual ~Matcher() {}
+			
 			virtual void match( std::list< Expression * > &out ) = 0;
 			ObjectDecl * newObject( UniqueName & namer, Expression * expr );
+
+			void combineState( const ResolvExpr::Alternative& alt ) {
+				compositeEnv.simpleCombine( alt.env );
+				ResolvExpr::mergeOpenVars( openVars, alt.openVars );
+				cloneAll( alt.need, need );
+			}
+
+			void combineState( const ResolvExpr::AltList& alts ) {
+				for ( const ResolvExpr::Alternative& alt : alts ) { combineState( alt ); }
+			}
+			
 			ResolvExpr::AltList lhs, rhs;
 			TupleAssignSpotter &spotter;
@@ -72,4 +84,6 @@
 			std::list< ObjectDecl * > tmpDecls;
 			ResolvExpr::TypeEnvironment compositeEnv;
+			ResolvExpr::OpenVarSet openVars;
+			ResolvExpr::AssertionSet need;
 		};
 
@@ -245,16 +259,18 @@
 		}
 
-		// extract expressions from the assignment alternatives to produce a list of assignments that
-		// together form a single alternative
+		// extract expressions from the assignment alternatives to produce a list of assignments 
+		// that together form a single alternative
 		std::list< Expression *> solved_assigns;
 		for ( ResolvExpr::Alternative & alt : current ) {
 			solved_assigns.push_back( alt.expr->clone() );
-		}
-		// combine assignment environments into combined expression environment
-		simpleCombineEnvironments( current.begin(), current.end(), matcher->compositeEnv );
+			matcher->combineState( alt );
+		}
+		
 		// xxx -- was push_front
-		currentFinder.get_alternatives().push_back( ResolvExpr::Alternative(
-			new TupleAssignExpr(solved_assigns, matcher->tmpDecls), matcher->compositeEnv,
-			ResolvExpr::sumCost( current ) + matcher->baseCost ) );
+		currentFinder.get_alternatives().push_back( ResolvExpr::Alternative{
+			new TupleAssignExpr{ solved_assigns, matcher->tmpDecls }, matcher->compositeEnv, 
+			matcher->openVars, 
+			ResolvExpr::AssertionList( matcher->need.begin(), matcher->need.end() ), 
+			ResolvExpr::sumCost( current ) + matcher->baseCost } );
 	}
 
@@ -263,6 +279,6 @@
 	: lhs(lhs), rhs(rhs), spotter(spotter),
 	  baseCost( ResolvExpr::sumCost( lhs ) + ResolvExpr::sumCost( rhs ) ) {
-		simpleCombineEnvironments( lhs.begin(), lhs.end(), compositeEnv );
-		simpleCombineEnvironments( rhs.begin(), rhs.end(), compositeEnv );
+		combineState( lhs ); 
+		combineState( rhs );
 	}
 
