Index: src/ResolvExpr/TypeEnvironment.cc
===================================================================
--- src/ResolvExpr/TypeEnvironment.cc	(revision dd05e12d91f94668b101255655342bfd9b8f4486)
+++ src/ResolvExpr/TypeEnvironment.cc	(revision e2c70abaacda28a5de17564ffc349fdaeb8b9ab3)
@@ -118,4 +118,18 @@
 			env.push_back( newClass );
 		} // for
+	}
+
+	void TypeEnvironment::add( const TypeSubstitution & sub ) {
+		EqvClass newClass;
+		for ( auto p : sub ) {
+			newClass.vars.insert( p.first );
+			newClass.type = p.second->clone();
+			newClass.allowWidening = false;
+			// Minimal assumptions. Not technically correct, but might be good enough, and
+			// is the best we can do at the moment since information is lost in the
+			// transition to TypeSubstitution
+			newClass.data = TypeDecl::Data{ TypeDecl::Dtype, false };
+			add( newClass );
+		}
 	}
 
Index: src/ResolvExpr/TypeEnvironment.h
===================================================================
--- src/ResolvExpr/TypeEnvironment.h	(revision dd05e12d91f94668b101255655342bfd9b8f4486)
+++ src/ResolvExpr/TypeEnvironment.h	(revision e2c70abaacda28a5de17564ffc349fdaeb8b9ab3)
@@ -76,4 +76,5 @@
 		void add( const EqvClass &eqvClass );
 		void add( const Type::ForallList &tyDecls );
+		void add( const TypeSubstitution & sub );
 		template< typename SynTreeClass > int apply( SynTreeClass *&type ) const;
 		template< typename SynTreeClass > int applyFree( SynTreeClass *&type ) const;