diff --git a/libsolidity/analysis/experimental/DebugWarner.cpp b/libsolidity/analysis/experimental/DebugWarner.cpp
index 6bfbc121d..c421a839c 100644
--- a/libsolidity/analysis/experimental/DebugWarner.cpp
+++ b/libsolidity/analysis/experimental/DebugWarner.cpp
@@ -43,10 +43,14 @@ bool DebugWarner::visitNode(ASTNode const& _node)
 	if (typeInferenceAnnotation.type)
 	{
 		Type type = *typeInferenceAnnotation.type;
+		Sort sort = m_analysis.typeSystem().env().sort(type);
+		std::string sortString;
+		if (sort.classes.size() != 1 || *sort.classes.begin() != TypeClass{{BuiltinClass::Type}})
+			sortString = ":" + TypeSystemHelpers{m_analysis.typeSystem()}.sortToString(m_analysis.typeSystem().env().sort(type));
 		m_errorReporter.info(
 			0000_error,
 			_node.location(),
-			"Inferred type: " + m_analysis.typeSystem().env().typeToString(type) + ":" + TypeSystemHelpers{m_analysis.typeSystem()}.sortToString(m_analysis.typeSystem().env().sort(type))
+			"Inferred type: " + TypeEnvironmentHelpers{m_analysis.typeSystem().env()}.typeToString(type) + sortString
 		);
 	}
 	return true;
diff --git a/libsolidity/analysis/experimental/TypeInference.cpp b/libsolidity/analysis/experimental/TypeInference.cpp
index 50f8e20d5..ee76fb82f 100644
--- a/libsolidity/analysis/experimental/TypeInference.cpp
+++ b/libsolidity/analysis/experimental/TypeInference.cpp
@@ -90,7 +90,7 @@ bool TypeInference::visit(FunctionDefinition const& _functionDefinition)
 
 	functionAnnotation.type = functionType;
 
-	m_errorReporter.info(0000_error, _functionDefinition.location(), m_env->typeToString(*functionAnnotation.type));
+	m_errorReporter.info(0000_error, _functionDefinition.location(), TypeEnvironmentHelpers{*m_env}.typeToString(*functionAnnotation.type));
 
 	return false;
 }
@@ -162,7 +162,7 @@ bool TypeInference::visit(TypeClassDefinition const& _typeClassDefinition)
 		solAssert(functionDefinitionType);
 		auto functionType = m_env->fresh(*functionDefinitionType);
 		functionTypes[functionDefinition->name()] = functionType;
-		auto typeVars = TypeSystemHelpers{m_typeSystem}.typeVars(functionType);
+		auto typeVars = TypeEnvironmentHelpers{*m_env}.typeVars(functionType);
 		if(typeVars.size() != 1)
 			m_errorReporter.fatalTypeError(0000_error, functionDefinition->location(), "Function in type class may only depend on the type class variable.");
 		unify(typeVars.front(), typeVar);
@@ -175,9 +175,7 @@ bool TypeInference::visit(TypeClassDefinition const& _typeClassDefinition)
 		m_errorReporter.fatalTypeError(0000_error, _typeClassDefinition.location(), *error);
 
 	solAssert(typeVariableAnnotation.type);
-	TypeSystemHelpers helper{m_typeSystem};
-	unify(*typeVariableAnnotation.type, helper.kindType(m_typeSystem.freshTypeVariable(Sort{{TypeClass{&_typeClassDefinition}}})), _typeClassDefinition.location());
-
+	unify(*typeVariableAnnotation.type, m_typeSystem.freshTypeVariable(Sort{{TypeClass{&_typeClassDefinition}}}), _typeClassDefinition.location());
 	for (auto instantiation: m_analysis.annotation<TypeRegistration>(_typeClassDefinition).instantiations | ranges::views::values)
 		// TODO: recursion-safety?
 		instantiation->accept(*this);
@@ -190,19 +188,30 @@ void TypeInference::unify(Type _a, Type _b, langutil::SourceLocation _location,
 	if (!_env)
 		_env = m_env;
 	for (auto failure: _env->unify(_a, _b))
+	{
+		TypeEnvironmentHelpers helper{*_env};
 		std::visit(util::GenericVisitor{
 			[&](TypeEnvironment::TypeMismatch _typeMismatch) {
-				m_errorReporter.typeError(0000_error, _location, fmt::format("Cannot unify {} and {}.", _env->typeToString(_typeMismatch.a), _env->typeToString(_typeMismatch.b)));
+				m_errorReporter.typeError(
+					0000_error,
+					_location,
+					fmt::format(
+						"Cannot unify {} and {}.",
+						helper.typeToString(_typeMismatch.a),
+						helper.typeToString(_typeMismatch.b))
+				);
 			},
 			[&](TypeEnvironment::SortMismatch _sortMismatch) {
 				m_errorReporter.typeError(0000_error, _location, fmt::format(
 					"{} does not have sort {}",
-					_env->typeToString(_sortMismatch.type),
+					helper.typeToString(_sortMismatch.type),
 					TypeSystemHelpers{m_typeSystem}.sortToString(_sortMismatch.sort)
 				));
 			}
 		}, failure);
 
+	}
+
 }
 bool TypeInference::visit(InlineAssembly const& _inlineAssembly)
 {
@@ -262,29 +271,29 @@ bool TypeInference::visit(ElementaryTypeNameExpression const& _expression)
 	switch(_expression.type().typeName().token())
 	{
 	case Token::Word:
-		expressionAnnotation.type = helper.kindType(m_wordType);
+		expressionAnnotation.type = m_wordType;
 		break;
 	case Token::Void:
-		expressionAnnotation.type = helper.kindType(m_voidType);
+		expressionAnnotation.type = m_voidType;
 		break;
 	case Token::Integer:
-		expressionAnnotation.type = helper.kindType(m_integerType);
+		expressionAnnotation.type = m_integerType;
 		break;
 	case Token::Unit:
-		expressionAnnotation.type = helper.kindType(m_unitType);
+		expressionAnnotation.type = m_unitType;
 		break;
 	case Token::Bool:
-		expressionAnnotation.type = helper.kindType(m_boolType);
+		expressionAnnotation.type = m_boolType;
 		break;
 	case Token::Pair:
 	{
 		auto leftType = m_typeSystem.freshTypeVariable({});
 		auto rightType = m_typeSystem.freshTypeVariable({});
 		expressionAnnotation.type =
-			helper.functionType(
-			helper.kindType(helper.tupleType({leftType, rightType})),
-			helper.kindType(m_typeSystem.type(BuiltinType::Pair, {leftType, rightType}))
-			);
+			helper.typeFunctionType(
+			helper.tupleType({leftType, rightType}),
+			m_typeSystem.type(BuiltinType::Pair, {leftType, rightType})
+		);
 		break;
 	}
 	case Token::Fun:
@@ -292,15 +301,15 @@ bool TypeInference::visit(ElementaryTypeNameExpression const& _expression)
 		auto argType = m_typeSystem.freshTypeVariable({});
 		auto resultType = m_typeSystem.freshTypeVariable({});
 		expressionAnnotation.type =
-			helper.functionType(
-				helper.kindType(helper.tupleType({argType, resultType})),
-				helper.kindType(m_typeSystem.type(BuiltinType::Function, {argType, resultType}))
+			helper.typeFunctionType(
+				helper.tupleType({argType, resultType}),
+				m_typeSystem.type(BuiltinType::Function, {argType, resultType})
 			);
 		break;
 	}
 	default:
 		m_errorReporter.typeError(0000_error, _expression.location(), "Only elementary types are supported.");
-		expressionAnnotation.type = helper.kindType(m_typeSystem.freshTypeVariable({}));
+		expressionAnnotation.type = m_typeSystem.freshTypeVariable({});
 		break;
 	}
 	return false;
@@ -356,29 +365,21 @@ bool TypeInference::visit(BinaryOperation const& _binaryOperation)
 		{
 			_binaryOperation.leftExpression().accept(*this);
 			_binaryOperation.rightExpression().accept(*this);
-			auto getType = [&](std::optional<Type> _type) -> Type {
-				solAssert(_type);
-				if (helper.isKindType(*_type))
-					return helper.destKindType(*_type);
-				else
-				{
-					m_errorReporter.typeError(0000_error, _binaryOperation.leftExpression().location(), "Expected type but got " + m_env->typeToString(*leftAnnotation.type));
-					return m_typeSystem.freshTypeVariable({});
-				}
-			};
-			Type leftType = getType(leftAnnotation.type);
-			Type rightType = getType(rightAnnotation.type);
-			operationAnnotation.type = helper.kindType(helper.functionType(leftType, rightType));
+			solAssert(leftAnnotation.type);
+			solAssert(rightAnnotation.type);
+			Type leftType = *leftAnnotation.type;
+			Type rightType = *rightAnnotation.type;
+			operationAnnotation.type = helper.functionType(leftType, rightType);
 		}
 		else
 		{
 			m_errorReporter.typeError(0000_error, _binaryOperation.location(), "Invalid binary operations in type context.");
-			operationAnnotation.type = helper.kindType(m_typeSystem.freshTypeVariable({}));
+			operationAnnotation.type = m_typeSystem.freshTypeVariable({});
 		}
 		return false;
 	case ExpressionContext::Sort:
 		m_errorReporter.typeError(0000_error, _binaryOperation.location(), "Invalid binary operation in sort context.");
-		operationAnnotation.type = helper.kindType(m_typeSystem.freshTypeVariable({}));
+		operationAnnotation.type = m_typeSystem.freshTypeVariable({});
 		return false;
 	}
 	return false;
@@ -408,7 +409,6 @@ bool TypeInference::visit(VariableDeclaration const& _variableDeclaration)
 	auto& variableAnnotation = annotation(_variableDeclaration);
 	solAssert(!variableAnnotation.type);
 
-	TypeSystemHelpers helper{m_typeSystem};
 	switch (m_expressionContext)
 	{
 	case ExpressionContext::Term:
@@ -418,20 +418,14 @@ bool TypeInference::visit(VariableDeclaration const& _variableDeclaration)
 			_variableDeclaration.typeExpression()->accept(*this);
 			auto& typeExpressionAnnotation = annotation(*_variableDeclaration.typeExpression());
 			solAssert(typeExpressionAnnotation.type);
-			if (helper.isKindType(*typeExpressionAnnotation.type))
-				variableAnnotation.type = helper.destKindType(*typeExpressionAnnotation.type);
-			else
-			{
-				m_errorReporter.typeError(0000_error, _variableDeclaration.typeExpression()->location(), "Expected type, but got " + m_env->typeToString(*typeExpressionAnnotation.type));
-				variableAnnotation.type = m_typeSystem.freshTypeVariable({});
-			}
+			variableAnnotation.type = *typeExpressionAnnotation.type;
 			return false;
 		}
 
 		variableAnnotation.type = m_typeSystem.freshTypeVariable({});
 		return false;
 	case ExpressionContext::Type:
-		variableAnnotation.type = helper.kindType(m_typeSystem.freshTypeVariable({}));
+		variableAnnotation.type = m_typeSystem.freshTypeVariable({});
 		if (_variableDeclaration.typeExpression())
 		{
 			ScopedSaveAndRestore expressionContext{m_expressionContext, ExpressionContext::Sort};
@@ -487,7 +481,6 @@ TypeInference::GlobalAnnotation& TypeInference::annotation()
 
 experimental::Type TypeInference::handleIdentifierByReferencedDeclaration(langutil::SourceLocation _location, Declaration const& _declaration)
 {
-	TypeSystemHelpers helper{m_typeSystem};
 	switch(m_expressionContext)
 	{
 	case ExpressionContext::Term:
@@ -561,12 +554,12 @@ experimental::Type TypeInference::handleIdentifierByReferencedDeclaration(langut
 		{
 			ScopedSaveAndRestore expressionContext{m_expressionContext, ExpressionContext::Term};
 			typeClass->accept(*this);
-			return helper.kindType(m_typeSystem.freshTypeVariable(Sort{{TypeClass{typeClass}}}));
+			return m_typeSystem.freshTypeVariable(Sort{{TypeClass{typeClass}}});
 		}
 		else
 		{
 			m_errorReporter.typeError(0000_error, _location, "Expected type class.");
-			return helper.kindType(m_typeSystem.freshTypeVariable({}));
+			return m_typeSystem.freshTypeVariable({});
 		}
 		break;
 	}
@@ -585,7 +578,6 @@ bool TypeInference::visit(Identifier const& _identifier)
 		return false;
 	}
 
-	TypeSystemHelpers helper{m_typeSystem};
 	switch(m_expressionContext)
 	{
 	case ExpressionContext::Term:
@@ -595,7 +587,7 @@ bool TypeInference::visit(Identifier const& _identifier)
 	case ExpressionContext::Type:
 	{
 		// TODO: register free type variable name!
-		identifierAnnotation.type = helper.kindType(m_typeSystem.freshTypeVariable({}));
+		identifierAnnotation.type = m_typeSystem.freshTypeVariable({});
 		return false;
 	}
 	case ExpressionContext::Sort:
@@ -616,34 +608,17 @@ void TypeInference::endVisit(TupleExpression const& _tupleExpression)
 	auto componentTypes = _tupleExpression.components() | ranges::views::transform([&](auto _expr) -> Type {
 		auto& componentAnnotation = annotation(*_expr);
 		solAssert(componentAnnotation.type);
-		switch(m_expressionContext)
-		{
-		case ExpressionContext::Term:
-			return *componentAnnotation.type;
-		case ExpressionContext::Type:
-			if (helper.isKindType(*componentAnnotation.type))
-				return helper.destKindType(*componentAnnotation.type);
-			else
-			{
-				m_errorReporter.typeError(0000_error, _expr->location(), "Expected type, but got " + m_env->typeToString(*componentAnnotation.type));
-				return m_typeSystem.freshTypeVariable({});
-			}
-		case ExpressionContext::Sort:
-			return *componentAnnotation.type;
-		}
-		solAssert(false);
+		return *componentAnnotation.type;
 	}) | ranges::to<vector<Type>>;
 	switch (m_expressionContext)
 	{
 	case ExpressionContext::Term:
-		expressionAnnotation.type = helper.tupleType(componentTypes);
-		break;
 	case ExpressionContext::Type:
-		expressionAnnotation.type = helper.kindType(helper.tupleType(componentTypes));
+		expressionAnnotation.type = helper.tupleType(componentTypes);
 		break;
 	case ExpressionContext::Sort:
 	{
-		Type type = helper.kindType(m_typeSystem.freshTypeVariable({}));
+		Type type = m_typeSystem.freshTypeVariable({});
 		for (auto componentType: componentTypes)
 			unify(type, componentType, _tupleExpression.location());
 		expressionAnnotation.type = type;
@@ -725,8 +700,6 @@ bool TypeInference::visit(TypeClassInstantiation const& _typeClassInstantiation)
 			auto& argumentSortAnnotation = annotation(*_typeClassInstantiation.argumentSorts());
 			solAssert(argumentSortAnnotation.type);
 			arguments = TypeSystemHelpers{m_typeSystem}.destTupleType(*argumentSortAnnotation.type);
-			for (auto& argument: arguments)
-				argument = TypeSystemHelpers{m_typeSystem}.destKindType(argument);
 			arity.argumentSorts = arguments | ranges::views::transform([&](Type _type) {
 				return m_env->sort(_type);
 			}) | ranges::to<vector<Sort>>;
@@ -743,7 +716,8 @@ bool TypeInference::visit(TypeClassInstantiation const& _typeClassInstantiation)
 		solAssert(functionDefinition);
 		subNode->accept(*this);
 		solAssert(annotation(*functionDefinition).type);
-		functionTypes[functionDefinition->name()] = *annotation(*functionDefinition).type;
+		if (!functionTypes.emplace(functionDefinition->name(), *annotation(*functionDefinition).type).second)
+			m_errorReporter.typeError(0000_error, subNode->location(), "Multiple definitions of function " + functionDefinition->name() + " during type class instantiation.");
 	}
 
 	if (auto error = m_typeSystem.instantiateClass(type, arity, std::move(functionTypes)))
@@ -762,9 +736,6 @@ void TypeInference::endVisit(MemberAccess const& _memberAccess)
 	if (helper.isTypeConstant(*expressionAnnotation.type))
 	{
 		Type expressionType = *expressionAnnotation.type;
-		// TODO: unify this, s.t. this is always or never a kind type.
-		if (helper.isKindType(expressionType))
-			expressionType = helper.destKindType(expressionType);
 		auto constructor = std::get<0>(helper.destTypeConstant(expressionType));
 		if (auto* typeMember = util::valueOrNullptr(annotation().members.at(constructor), _memberAccess.memberName()))
 		{
@@ -807,26 +778,19 @@ bool TypeInference::visit(TypeDefinition const& _typeDefinition)
 		 ScopedSaveAndRestore expressionContext{m_expressionContext, ExpressionContext::Type};
 		 _typeDefinition.typeExpression()->accept(*this);
 		 underlyingType = annotation(*_typeDefinition.typeExpression()).type;
-		 // TODO: settle the kind type mess.
-		 if (underlyingType && helper.isKindType(*underlyingType))
-			underlyingType = helper.destKindType(*underlyingType);
 	}
 
 	vector<Type> arguments;
 	if (_typeDefinition.arguments())
 		 for (size_t i = 0; i < _typeDefinition.arguments()->parameters().size(); ++i)
-			// TODO: GENERALIZE
+			// TODO: GENERALIZE?
 			arguments.emplace_back(m_typeSystem.freshTypeVariable({}));
 
 	Type type = m_typeSystem.type(TypeConstructor{&_typeDefinition}, arguments);
 	if (arguments.empty())
-		 typeDefinitionAnnotation.type = helper.kindType(m_typeSystem.type(TypeConstructor{&_typeDefinition}, arguments));
+		 typeDefinitionAnnotation.type = m_typeSystem.type(TypeConstructor{&_typeDefinition}, arguments);
 	else
-		typeDefinitionAnnotation.type =
-			 helper.functionType(
-				 helper.kindType(helper.tupleType(arguments)),
-				helper.kindType(type)
-			);
+		typeDefinitionAnnotation.type = helper.typeFunctionType(helper.tupleType(arguments), type);
 
 	auto& typeMembers = annotation().members[&_typeDefinition];
 
@@ -859,16 +823,8 @@ void TypeInference::endVisit(FunctionCall const& _functionCall)
 		 switch(m_expressionContext)
 		 {
 		 case ExpressionContext::Term:
-			argTypes.emplace_back(*argAnnotation.type);
-			break;
 		 case ExpressionContext::Type:
-			if (helper.isKindType(*argAnnotation.type))
-				argTypes.emplace_back(helper.destKindType(*argAnnotation.type));
-			else
-			{
-				m_errorReporter.typeError(0000_error, arg->location(), "Expected type, but got " + m_env->typeToString(*argAnnotation.type));
-				argTypes.emplace_back(m_typeSystem.freshTypeVariable({}));
-			}
+			argTypes.emplace_back(*argAnnotation.type);
 			break;
 		 case ExpressionContext::Sort:
 			m_errorReporter.typeError(0000_error, _functionCall.location(), "Function call in sort context.");
@@ -890,11 +846,11 @@ void TypeInference::endVisit(FunctionCall const& _functionCall)
 	}
 	case ExpressionContext::Type:
 	{
-		 Type argTuple = helper.kindType(helper.tupleType(argTypes));
-		 Type genericFunctionType = helper.functionType(argTuple, m_typeSystem.freshKindVariable({}));
+		 Type argTuple = helper.tupleType(argTypes);
+		 Type genericFunctionType = helper.typeFunctionType(argTuple, m_typeSystem.freshKindVariable({}));
 		 unify(functionType, genericFunctionType, _functionCall.location());
 
-		 functionCallAnnotation.type = m_env->resolve(std::get<1>(helper.destFunctionType(m_env->resolve(genericFunctionType))));
+		 functionCallAnnotation.type = m_env->resolve(std::get<1>(helper.destTypeFunctionType(m_env->resolve(genericFunctionType))));
 		 break;
 	}
 	case ExpressionContext::Sort:
diff --git a/libsolidity/ast/experimental/Type.cpp b/libsolidity/ast/experimental/Type.cpp
index 487b97bb5..a06426834 100644
--- a/libsolidity/ast/experimental/Type.cpp
+++ b/libsolidity/ast/experimental/Type.cpp
@@ -69,8 +69,6 @@ string TypeClass::toString() const
 				return "type";
 			case BuiltinClass::Kind:
 				return "kind";
-			case BuiltinClass::Constraint:
-				return "contraint";
 			case BuiltinClass::Integer:
 				return "integer";
 			case BuiltinClass::Mul:
diff --git a/libsolidity/ast/experimental/Type.h b/libsolidity/ast/experimental/Type.h
index 7d76b5f22..1bb831e1d 100644
--- a/libsolidity/ast/experimental/Type.h
+++ b/libsolidity/ast/experimental/Type.h
@@ -44,6 +44,7 @@ enum class BuiltinType
 	Sort,
 	Void,
 	Function,
+	TypeFunction,
 	Unit,
 	Pair,
 	Word,
@@ -73,7 +74,6 @@ enum class BuiltinClass
 {
 	Type,
 	Kind,
-	Constraint,
 	Integer,
 	Mul,
 	Add,
diff --git a/libsolidity/ast/experimental/TypeSystem.cpp b/libsolidity/ast/experimental/TypeSystem.cpp
index 918d6af6c..7146fa44f 100644
--- a/libsolidity/ast/experimental/TypeSystem.cpp
+++ b/libsolidity/ast/experimental/TypeSystem.cpp
@@ -36,151 +36,6 @@ using namespace std;
 using namespace solidity::frontend;
 using namespace solidity::frontend::experimental;
 
-std::string TypeEnvironment::canonicalTypeName(Type _type) const
-{
-	return visit(util::GenericVisitor{
-		[&](TypeConstant const& _type) {
-			std::stringstream stream;
-			auto printTypeArguments = [&]() {
-				if (!_type.arguments.empty())
-				{
-					stream << "$";
-					for (auto type: _type.arguments | ranges::views::drop_last(1))
-						stream << canonicalTypeName(type) << "$";
-					stream << canonicalTypeName(_type.arguments.back());
-					stream << "$";
-				}
-			};
-			std::visit(util::GenericVisitor{
-				[&](Declaration const* _declaration) {
-					printTypeArguments();
-					if (auto const* typeDeclarationAnnotation = dynamic_cast<TypeDeclarationAnnotation const*>(&_declaration->annotation()))
-						stream << *typeDeclarationAnnotation->canonicalName;
-					else
-						// TODO: canonical name
-						stream << _declaration->name();
-				},
-				[&](BuiltinType _builtinType) {
-					printTypeArguments();
-					switch(_builtinType)
-					{
-					case BuiltinType::Type:
-						stream << "type";
-						break;
-					case BuiltinType::Sort:
-						stream << "sort";
-						break;
-					case BuiltinType::Void:
-						stream << "void";
-						break;
-					case BuiltinType::Function:
-						stream << "fun";
-						break;
-					case BuiltinType::Unit:
-						stream << "unit";
-						break;
-					case BuiltinType::Pair:
-						stream << "pair";
-						break;
-					case BuiltinType::Word:
-						stream << "word";
-						break;
-					case BuiltinType::Bool:
-						stream << "bool";
-						break;
-					case BuiltinType::Integer:
-						stream << "integer";
-						break;
-					}
-				}
-			}, _type.constructor);
-			return stream.str();
-		},
-		[](TypeVariable const&)-> string {
-			solAssert(false);
-		},
-	}, resolve(_type));
-}
-
-
-std::string TypeEnvironment::typeToString(Type const& _type) const
-{
-	return std::visit(util::GenericVisitor{
-		[&](TypeConstant const& _type) {
-			std::stringstream stream;
-			auto printTypeArguments = [&]() {
-				if (!_type.arguments.empty())
-				{
-					stream << "(";
-					for (auto type: _type.arguments | ranges::views::drop_last(1))
-						stream << typeToString(type) << ", ";
-					stream << typeToString(_type.arguments.back());
-					stream << ")";
-				}
-			};
-			std::visit(util::GenericVisitor{
-				[&](Declaration const* _declaration) {
-					stream << m_typeSystem.typeName(_declaration);
-					printTypeArguments();
-				},
-				[&](BuiltinType _builtinType) {
-					switch (_builtinType)
-					{
-					case BuiltinType::Function:
-						solAssert(_type.arguments.size() == 2);
-						stream << fmt::format("{} -> {}", typeToString(_type.arguments.front()), typeToString(_type.arguments.back()));
-						break;
-					case BuiltinType::Unit:
-						solAssert(_type.arguments.empty());
-						stream << "()";
-						break;
-					case BuiltinType::Pair:
-					{
-						auto tupleTypes = TypeSystemHelpers{m_typeSystem}.destTupleType(_type);
-						stream << "(";
-						for (auto type: tupleTypes | ranges::views::drop_last(1))
-							stream << typeToString(type) << ", ";
-						stream << typeToString(tupleTypes.back()) << ")";
-						break;
-					}
-					case BuiltinType::Type:
-					{
-						solAssert(_type.arguments.size() == 1);
-						stream << "TYPE(" << typeToString(_type.arguments.front()) << ")";
-						break;
-					}
-					default:
-						stream << m_typeSystem.typeName(_builtinType);
-						printTypeArguments();
-						break;
-					}
-				}
-			}, _type.constructor);
-			return stream.str();
-		},
-		[](TypeVariable const& _type) {
-			std::stringstream stream;
-			stream << "'var" << _type.index();
-			switch (_type.sort().classes.size())
-			{
-			case 0:
-				break;
-			case 1:
-				stream << ":" << _type.sort().classes.begin()->toString();
-				break;
-			default:
-				stream << ":(";
-				for (auto typeClass: _type.sort().classes | ranges::views::drop_last(1))
-					stream << typeClass.toString() << ", ";
-				stream << _type.sort().classes.rbegin()->toString();
-				stream << ")";
-				break;
-			}
-			return stream.str();
-		},
-	}, resolve(_type));
-}
-
 vector<TypeEnvironment::UnificationFailure> TypeEnvironment::unify(Type _a, Type _b)
 {
 	vector<UnificationFailure> failures;
@@ -267,15 +122,10 @@ TypeEnvironment TypeEnvironment::clone() const
 
 TypeSystem::TypeSystem()
 {
-	Sort kindSort{{TypeClass{BuiltinClass::Kind}}};
 	Sort typeSort{{TypeClass{BuiltinClass::Type}}};
-	m_typeConstructors[BuiltinType::Type] = TypeConstructorInfo{
-		"type",
-		{Arity{vector<Sort>{{typeSort}}, TypeClass{BuiltinClass::Kind}}}
-	};
-	m_typeConstructors[BuiltinType::Sort] = TypeConstructorInfo{
-		"constraint",
-		{Arity{vector<Sort>{{kindSort}}, TypeClass{BuiltinClass::Constraint}}}
+	m_typeConstructors[BuiltinType::TypeFunction] = TypeConstructorInfo{
+		"tfun",
+		{Arity{vector<Sort>{{typeSort},{typeSort}}, TypeClass{BuiltinClass::Kind}}}
 	};
 	m_typeConstructors[BuiltinType::Function] = TypeConstructorInfo{
 		"fun",
@@ -392,7 +242,7 @@ std::optional<std::string> TypeSystem::declareTypeClass(TypeClass _class, Type _
 		return "Invalid type variable.";
 	for (auto [functionName, functionType]: _functions)
 	{
-		auto typeVars = TypeSystemHelpers{*this}.typeVars(functionType);
+		auto typeVars = TypeEnvironmentHelpers{m_globalTypeEnvironment}.typeVars(functionType);
 		if (typeVars.empty())
 			return "Function " + functionName + " does not depend on class variable.";
 		if (typeVars.size() > 2)
@@ -479,7 +329,7 @@ std::optional<std::string> TypeSystem::instantiateClass(Type _instanceVariable,
 		_functionTypes.erase(name);
 
 		if (!newEnv.typeEquals(instanceFunctionType, classFunctionType))
-			return "Type mismatch for function " + name + " " + newEnv.typeToString(instanceFunctionType) + " != " + newEnv.typeToString(classFunctionType);
+			return "Type mismatch for function " + name + " " + TypeEnvironmentHelpers{newEnv}.typeToString(instanceFunctionType) + " != " + TypeEnvironmentHelpers{newEnv}.typeToString(classFunctionType);
 	}
 
 	typeConstructorInfo.arities.emplace_back(_arity);
diff --git a/libsolidity/ast/experimental/TypeSystem.h b/libsolidity/ast/experimental/TypeSystem.h
index 232c955ac..3d2e1247c 100644
--- a/libsolidity/ast/experimental/TypeSystem.h
+++ b/libsolidity/ast/experimental/TypeSystem.h
@@ -42,10 +42,10 @@ public:
 	struct SortMismatch { Type type; Sort sort; };
 	using UnificationFailure = std::variant<TypeMismatch, SortMismatch>;
 	[[nodiscard]] std::vector<UnificationFailure> unify(Type _a, Type _b);
-	std::string canonicalTypeName(Type _type) const;
-	std::string typeToString(Type const& _type) const;
 	Sort sort(Type _type) const;
 	bool typeEquals(Type _lhs, Type _rhs) const;
+	TypeSystem& typeSystem() { return m_typeSystem; }
+	TypeSystem const& typeSystem() const { return m_typeSystem; }
 private:
 	TypeEnvironment(TypeEnvironment&& _env): m_typeSystem(_env.m_typeSystem), m_typeVariables(std::move(_env.m_typeVariables)) {}
 	[[nodiscard]] std::vector<TypeEnvironment::UnificationFailure> instantiate(TypeVariable _variable, Type _type);
diff --git a/libsolidity/ast/experimental/TypeSystemHelper.cpp b/libsolidity/ast/experimental/TypeSystemHelper.cpp
index cf0a92bd1..aa4a1c5e5 100644
--- a/libsolidity/ast/experimental/TypeSystemHelper.cpp
+++ b/libsolidity/ast/experimental/TypeSystemHelper.cpp
@@ -26,6 +26,8 @@
 #include <range/v3/view/drop_last.hpp>
 #include <range/v3/view/reverse.hpp>
 
+#include <fmt/format.h>
+
 using namespace std;
 using namespace solidity::langutil;
 using namespace solidity::frontend;
@@ -156,11 +158,6 @@ vector<experimental::Type> TypeSystemHelpers::destTupleType(Type _tupleType) con
 	return result;
 }
 
-experimental::Type TypeSystemHelpers::functionType(experimental::Type _argType, experimental::Type _resultType) const
-{
-	return typeSystem.type(BuiltinType::Function, {_argType, _resultType});
-}
-
 tuple<TypeConstructor, vector<experimental::Type>> TypeSystemHelpers::destTypeConstant(Type _type) const
 {
 	using ResultType = tuple<TypeConstructor, vector<Type>>;
@@ -186,6 +183,11 @@ bool TypeSystemHelpers::isTypeConstant(Type _type) const
 	}, _type);
 }
 
+experimental::Type TypeSystemHelpers::functionType(experimental::Type _argType, experimental::Type _resultType) const
+{
+	return typeSystem.type(BuiltinType::Function, {_argType, _resultType});
+}
+
 tuple<experimental::Type, experimental::Type> TypeSystemHelpers::destFunctionType(Type _functionType) const
 {
 	auto [constructor, arguments] = destTypeConstant(_functionType);
@@ -204,7 +206,30 @@ bool TypeSystemHelpers::isFunctionType(Type _type) const
 	return builtinType && *builtinType == BuiltinType::Function;
 }
 
-vector<experimental::Type> TypeSystemHelpers::typeVars(Type _type) const
+experimental::Type TypeSystemHelpers::typeFunctionType(experimental::Type _argType, experimental::Type _resultType) const
+{
+	return typeSystem.type(BuiltinType::TypeFunction, {_argType, _resultType});
+}
+
+tuple<experimental::Type, experimental::Type> TypeSystemHelpers::destTypeFunctionType(Type _functionType) const
+{
+	auto [constructor, arguments] = destTypeConstant(_functionType);
+	auto const* builtinType = get_if<BuiltinType>(&constructor);
+	solAssert(builtinType && *builtinType == BuiltinType::TypeFunction);
+	solAssert(arguments.size() == 2);
+	return make_tuple(arguments.front(), arguments.back());
+}
+
+bool TypeSystemHelpers::isTypeFunctionType(Type _type) const
+{
+	if (!isTypeConstant(_type))
+		return false;
+	auto constructor = get<0>(destTypeConstant(_type));
+	auto const* builtinType = get_if<BuiltinType>(&constructor);
+	return builtinType && *builtinType == BuiltinType::TypeFunction;
+}
+
+vector<experimental::Type> TypeEnvironmentHelpers::typeVars(Type _type) const
 {
 	set<size_t> indices;
 	vector<Type> typeVars;
@@ -219,33 +244,13 @@ vector<experimental::Type> TypeSystemHelpers::typeVars(Type _type) const
 					typeVars.emplace_back(_var);
 			},
 // TODO: move to env helpers?
-		}, typeSystem.env().resolve(_type));
+		}, env.resolve(_type));
 	};
 	typeVarsImpl(_type, typeVarsImpl);
 	return typeVars;
 
 }
 
-experimental::Type TypeSystemHelpers::kindType(Type _type) const
-{
-	return typeSystem.type(BuiltinType::Type, {_type});
-}
-
-experimental::Type TypeSystemHelpers::destKindType(Type _type) const
-{
-	auto [constructor, arguments] = destTypeConstant(_type);
-	solAssert(constructor == TypeConstructor{BuiltinType::Type});
-	solAssert(arguments.size() == 1);
-	return arguments.front();
-}
-
-bool TypeSystemHelpers::isKindType(Type _type) const
-{
-	if (!isTypeConstant(_type))
-		return false;
-	auto constructor = get<0>(destTypeConstant(_type));
-	return constructor == TypeConstructor{BuiltinType::Type};
-}
 
 std::string TypeSystemHelpers::sortToString(Sort _sort) const
 {
@@ -265,4 +270,151 @@ std::string TypeSystemHelpers::sortToString(Sort _sort) const
 		return stream.str();
 	}
 	}
-}
\ No newline at end of file
+}
+
+std::string TypeEnvironmentHelpers::canonicalTypeName(Type _type) const
+{
+	return visit(util::GenericVisitor{
+		[&](TypeConstant const& _type) {
+			std::stringstream stream;
+			auto printTypeArguments = [&]() {
+				if (!_type.arguments.empty())
+				{
+					stream << "$";
+					for (auto type: _type.arguments | ranges::views::drop_last(1))
+					stream << canonicalTypeName(type) << "$";
+					stream << canonicalTypeName(_type.arguments.back());
+					stream << "$";
+				}
+			};
+			std::visit(util::GenericVisitor{
+				[&](Declaration const* _declaration) {
+					printTypeArguments();
+					if (auto const* typeDeclarationAnnotation = dynamic_cast<TypeDeclarationAnnotation const*>(&_declaration->annotation()))
+						stream << *typeDeclarationAnnotation->canonicalName;
+					else
+					// TODO: canonical name
+						stream << _declaration->name();
+				},
+				[&](BuiltinType _builtinType) {
+					printTypeArguments();
+					switch(_builtinType)
+					{
+					case BuiltinType::Type:
+						stream << "type";
+						break;
+					case BuiltinType::Sort:
+						stream << "sort";
+						break;
+					case BuiltinType::Void:
+						stream << "void";
+						break;
+					case BuiltinType::Function:
+						stream << "fun";
+						break;
+					case BuiltinType::TypeFunction:
+						stream << "tfun";
+						break;
+					case BuiltinType::Unit:
+						stream << "unit";
+						break;
+					case BuiltinType::Pair:
+						stream << "pair";
+						break;
+					case BuiltinType::Word:
+						stream << "word";
+						break;
+					case BuiltinType::Bool:
+						stream << "bool";
+						break;
+					case BuiltinType::Integer:
+						stream << "integer";
+						break;
+					}
+				}
+			}, _type.constructor);
+			return stream.str();
+		},
+		[](TypeVariable const&)-> string {
+			solAssert(false);
+		},
+	}, env.resolve(_type));
+}
+
+std::string TypeEnvironmentHelpers::typeToString(Type const& _type) const
+{
+	return std::visit(util::GenericVisitor{
+		[&](TypeConstant const& _type) {
+			std::stringstream stream;
+			auto printTypeArguments = [&]() {
+				if (!_type.arguments.empty())
+				{
+					stream << "(";
+					for (auto type: _type.arguments | ranges::views::drop_last(1))
+						stream << typeToString(type) << ", ";
+					stream << typeToString(_type.arguments.back());
+					stream << ")";
+				}
+			};
+			std::visit(util::GenericVisitor{
+				[&](Declaration const* _declaration) {
+					stream << env.typeSystem().typeName(_declaration);
+					printTypeArguments();
+				},
+				[&](BuiltinType _builtinType) {
+					switch (_builtinType)
+					{
+					case BuiltinType::Function:
+						solAssert(_type.arguments.size() == 2);
+						stream << fmt::format("{} -> {}", typeToString(_type.arguments.front()), typeToString(_type.arguments.back()));
+						break;
+					case BuiltinType::Unit:
+						solAssert(_type.arguments.empty());
+						stream << "()";
+						break;
+					case BuiltinType::Pair:
+					{
+						auto tupleTypes = TypeSystemHelpers{env.typeSystem()}.destTupleType(_type);
+						stream << "(";
+						for (auto type: tupleTypes | ranges::views::drop_last(1))
+						stream << typeToString(type) << ", ";
+						stream << typeToString(tupleTypes.back()) << ")";
+						break;
+					}
+					case BuiltinType::Type:
+					{
+						solAssert(_type.arguments.size() == 1);
+						stream << "TYPE(" << typeToString(_type.arguments.front()) << ")";
+						break;
+					}
+					default:
+						stream << env.typeSystem().typeName(_builtinType);
+						printTypeArguments();
+						break;
+					}
+				}
+			}, _type.constructor);
+			return stream.str();
+		},
+		[](TypeVariable const& _type) {
+			std::stringstream stream;
+			stream << "'var" << _type.index();
+			switch (_type.sort().classes.size())
+			{
+			case 0:
+				break;
+			case 1:
+				stream << ":" << _type.sort().classes.begin()->toString();
+				break;
+			default:
+				stream << ":(";
+				for (auto typeClass: _type.sort().classes | ranges::views::drop_last(1))
+				stream << typeClass.toString() << ", ";
+				stream << _type.sort().classes.rbegin()->toString();
+				stream << ")";
+				break;
+			}
+			return stream.str();
+		},
+	}, env.resolve(_type));
+}
diff --git a/libsolidity/ast/experimental/TypeSystemHelper.h b/libsolidity/ast/experimental/TypeSystemHelper.h
index 2b282eb68..f1013a01c 100644
--- a/libsolidity/ast/experimental/TypeSystemHelper.h
+++ b/libsolidity/ast/experimental/TypeSystemHelper.h
@@ -39,11 +39,18 @@ struct TypeSystemHelpers
 	Type functionType(Type _argType, Type _resultType) const;
 	std::tuple<Type, Type> destFunctionType(Type _functionType) const;
 	bool isFunctionType(Type _type) const;
-	std::vector<Type> typeVars(Type _type) const;
+	Type typeFunctionType(Type _argType, Type _resultType) const;
+	std::tuple<Type, Type> destTypeFunctionType(Type _functionType) const;
+	bool isTypeFunctionType(Type _type) const;
 	std::string sortToString(Sort _sort) const;
-	Type kindType(Type _type) const;
-	bool isKindType(Type _type) const;
-	Type destKindType(Type _type) const;
+};
+
+struct TypeEnvironmentHelpers
+{
+	TypeEnvironment const& env;
+	std::string typeToString(Type const& _type) const;
+	std::string canonicalTypeName(Type _type) const;
+	std::vector<Type> typeVars(Type _type) const;
 };
 
 }
diff --git a/libsolidity/codegen/experimental/Common.cpp b/libsolidity/codegen/experimental/Common.cpp
index 8da2b1cca..0e655696e 100644
--- a/libsolidity/codegen/experimental/Common.cpp
+++ b/libsolidity/codegen/experimental/Common.cpp
@@ -18,6 +18,7 @@
 
 #include <libsolidity/codegen/experimental/Common.h>
 #include <libsolidity/ast/experimental/TypeSystem.h>
+#include <libsolidity/ast/experimental/TypeSystemHelper.h>
 
 #include <libsolutil/CommonIO.h>
 
@@ -37,7 +38,7 @@ string IRNames::function(TypeEnvironment const& _env, FunctionDefinition const&
 	if (_function.isConstructor())
 		return constructor(*_function.annotation().contract);
 
-	return "fun_" + _function.name() + "_" + to_string(_function.id()) + "$" + _env.canonicalTypeName(_type) + "$";
+	return "fun_" + _function.name() + "_" + to_string(_function.id()) + "$" + TypeEnvironmentHelpers{_env}.canonicalTypeName(_type) + "$";
 }
 
 string IRNames::function(VariableDeclaration const& _varDecl)
diff --git a/libsolidity/codegen/experimental/IRGenerator.cpp b/libsolidity/codegen/experimental/IRGenerator.cpp
index bf9a3bab5..a9e18b483 100644
--- a/libsolidity/codegen/experimental/IRGenerator.cpp
+++ b/libsolidity/codegen/experimental/IRGenerator.cpp
@@ -25,6 +25,7 @@
 #include <libsolidity/analysis/experimental/Analysis.h>
 #include <libsolidity/analysis/experimental/TypeInference.h>
 
+#include <libsolidity/ast/experimental/TypeSystemHelper.h>
 
 #include <libyul/YulStack.h>
 #include <libyul/AsmPrinter.h>
@@ -128,7 +129,8 @@ string IRGenerator::generate(FunctionDefinition const& _function, Type _type)
 	solAssert(type);
 	for (auto err: newEnv.unify(*type, _type))
 	{
-		solAssert(false, newEnv.typeToString(*type) + " <-> " + newEnv.typeToString(_type));
+		TypeEnvironmentHelpers helper{newEnv};
+		solAssert(false, helper.typeToString(*type) + " <-> " + helper.typeToString(_type));
 	}
 	std::stringstream code;
 	code << "function " << IRNames::function(newEnv, _function, _type) << "(";
diff --git a/libsolidity/codegen/experimental/IRGeneratorForStatements.cpp b/libsolidity/codegen/experimental/IRGeneratorForStatements.cpp
index 500ac4a96..00b1d4ec1 100644
--- a/libsolidity/codegen/experimental/IRGeneratorForStatements.cpp
+++ b/libsolidity/codegen/experimental/IRGeneratorForStatements.cpp
@@ -219,7 +219,7 @@ FunctionDefinition const& IRGeneratorForStatements::resolveTypeClassFunction(Typ
 	Type genericFunctionType = typeClassInfo->functions.at(_name);
 
 	TypeEnvironment env = m_context.env->clone();
-	auto typeVars = helper.typeVars(genericFunctionType);
+	auto typeVars = TypeEnvironmentHelpers{env}.typeVars(genericFunctionType);
 	solAssert(typeVars.size() == 1);
 	solAssert(env.unify(genericFunctionType, _type).empty());
 	auto typeClassInstantiation = get<0>(helper.destTypeConstant(env.resolve(typeVars.front())));
@@ -245,9 +245,6 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 {
 	TypeSystemHelpers helper{m_context.analysis.typeSystem()};
 	auto expressionType = type(_memberAccess.expression());
-	// TODO: avoid kind destruction
-	if (helper.isKindType(expressionType))
-		expressionType = helper.destKindType(expressionType);
 	auto constructor = std::get<0>(helper.destTypeConstant(expressionType));
 	auto memberAccessType = type(_memberAccess);
 	std::visit(util::GenericVisitor{