Index: src/ResolvExpr/AlternativeFinder.cc
===================================================================
--- src/ResolvExpr/AlternativeFinder.cc	(revision f6f0cca3f172613989f420c40761026fe191b651)
+++ src/ResolvExpr/AlternativeFinder.cc	(revision 3ef35bd884d4a41b6dc4f4a4a2243f1e96843a20)
@@ -453,7 +453,7 @@
 	/// Adds type variables to the open variable set and marks their assertions
 	void makeUnifiableVars( Type *type, OpenVarSet &unifiableVars, AssertionSet &needAssertions ) {
-		for ( Type::ForallList::const_iterator tyvar = type->get_forall().begin(); tyvar != type->get_forall().end(); ++tyvar ) {
+		for ( Type::ForallList::const_iterator tyvar = type->forall.begin(); tyvar != type->forall.end(); ++tyvar ) {
 			unifiableVars[ (*tyvar)->get_name() ] = TypeDecl::Data{ *tyvar };
-			for ( std::list< DeclarationWithType* >::iterator assert = (*tyvar)->get_assertions().begin(); assert != (*tyvar)->get_assertions().end(); ++assert ) {
+			for ( std::list< DeclarationWithType* >::iterator assert = (*tyvar)->assertions.begin(); assert != (*tyvar)->assertions.end(); ++assert ) {
 				needAssertions[ *assert ].isUsed = true;
 			}
Index: src/ResolvExpr/AlternativeFinder.h
===================================================================
--- src/ResolvExpr/AlternativeFinder.h	(revision f6f0cca3f172613989f420c40761026fe191b651)
+++ src/ResolvExpr/AlternativeFinder.h	(revision 3ef35bd884d4a41b6dc4f4a4a2243f1e96843a20)
@@ -126,4 +126,7 @@
 	void printAlts( const AltList &list, std::ostream &os, unsigned int indentAmt = 0 );
 
+	/// Adds type variables to the open variable set and marks their assertions
+	void makeUnifiableVars( Type *type, OpenVarSet &unifiableVars, AssertionSet &needAssertions );
+
 	template< typename InputIterator >
 	void simpleCombineEnvironments( InputIterator begin, InputIterator end, TypeEnvironment &result ) {
Index: src/ResolvExpr/Resolver.cc
===================================================================
--- src/ResolvExpr/Resolver.cc	(revision f6f0cca3f172613989f420c40761026fe191b651)
+++ src/ResolvExpr/Resolver.cc	(revision 3ef35bd884d4a41b6dc4f4a4a2243f1e96843a20)
@@ -493,4 +493,8 @@
 			}
 
+			if(clause.target.arguments.empty()) {
+				SemanticError( stmt->location, "Waitfor clause must have at least one mutex parameter");
+			}
+
 			// Find all alternatives for all arguments in canonical form
 			std::vector< AlternativeFinder > argAlternatives;
@@ -541,5 +545,9 @@
 							OpenVarSet openVars;
 							AssertionSet resultNeed, resultHave;
-							TypeEnvironment resultEnv;
+							TypeEnvironment resultEnv( func.env );
+							makeUnifiableVars( function, openVars, resultNeed );
+							// add all type variables as open variables now so that those not used in the parameter
+							// list are still considered open.
+							resultEnv.add( function->forall );
 
 							// Load type variables from arguemnts into one shared space
@@ -557,4 +565,6 @@
 							auto param_end = function->parameters.end();
 
+							int n_mutex_arg = 0;
+
 							// For every arguments of its set, check if it matches one of the parameter
 							// The order is important
@@ -565,15 +575,19 @@
 									// We ran out of parameters but still have arguments
 									// this function doesn't match
-									SemanticError( function, "candidate function not viable: too many mutex arguments\n" );
+									SemanticError( function, toString("candidate function not viable: too many mutex arguments, expected ", n_mutex_arg, "\n" ));
 								}
 
+								n_mutex_arg++;
+
 								// Check if the argument matches the parameter type in the current scope
-								if( ! unify( (*param)->get_type(), arg.expr->get_result(), resultEnv, resultNeed, resultHave, openVars, this->indexer ) ) {
+								if( ! unify( arg.expr->get_result(), (*param)->get_type(), resultEnv, resultNeed, resultHave, openVars, this->indexer ) ) {
 									// Type doesn't match
 									stringstream ss;
 									ss << "candidate function not viable: no known convertion from '";
+									(*param)->get_type()->print( ss );
+									ss << "' to '";
 									arg.expr->get_result()->print( ss );
-									ss << "' to '";
-									(*param)->get_type()->print( ss );
+									ss << "' with env '";
+									resultEnv.print(ss);
 									ss << "'\n";
 									SemanticError( function, ss.str() );
@@ -589,5 +603,5 @@
 								// We ran out of arguments but still have parameters left
 								// this function doesn't match
-								SemanticError( function, "candidate function not viable: too few mutex arguments\n" );
+								SemanticError( function, toString("candidate function not viable: too few mutex arguments, expected ", n_mutex_arg, "\n" ));
 							}