diff --git a/lib/ast.rb b/lib/ast.rb
index e4a5e354a8fb69c41267f117fa776e844f74dedd..106e9401ddd06da6b4e0b50b639c1733c2d8fd1c 100644
--- a/lib/ast.rb
+++ b/lib/ast.rb
@@ -208,9 +208,8 @@ module Dhallish
 
 				unres = nil
 				if argtype.is_a? Types::Type
-					assert("DEBUG: wann passiert sowas? #{argtype.inspect}") { argtype.metadata.nil? }
-					argtype = Types::Type.new(Types::Unresolved.new(@argname))
-					unres = @argname
+					unres = Types::Unresolved.new(@argname)
+					argtype = Types::Type.new(unres)
 				end
 
 				newctx = Context.new ctx
@@ -582,8 +581,8 @@ module Dhallish
 				type_var = nil
 				if !@type_var.nil? and lhs_type.is_a? Types::Type
 					new_ctx = Context.new ctx
-					lhs_type = new_ctx[@type_var] = Types::Type.new (Types::Unresolved.new @type_var)
-					type_var = @type_var
+					type_var = Types::Unresolved.new @type_var
+					lhs_type = new_ctx[@type_var] = Types::Type.new (type_var)
 				end
 				rhs_type = @rhs.compute_type new_ctx
 				assert ("Expression for result type not a type") { rhs_type.is_a? Types::Type }
@@ -598,11 +597,12 @@ module Dhallish
 					new_ctx = Context.new(ctx)
 					new_ctx[type_var] = Types::Unresolved.new(type_var)
 					rhs = @rhs.evaluate(new_ctx)
+					Types::Function.new(lhs, rhs, new_ctx[type_var])
 				else
 					rhs = @rhs.evaluate(ctx)
+					Types::Function.new(lhs, rhs)
 				end
 
-				Types::Function.new(lhs, rhs, type_var)
 			end
 		end
 
diff --git a/lib/stdlib.rb b/lib/stdlib.rb
index 48a05057b39ffb91fc4f8d1a62306066559471f1..4ff0caf9a30136db1c84de4e51a57e2af470ec79 100644
--- a/lib/stdlib.rb
+++ b/lib/stdlib.rb
@@ -2,21 +2,19 @@ require_relative './types.rb'
 require_relative './utils.rb'
 
 module Dhallish
-
 	# Utility function to create dhallish function types:
-	# Use [:name] to introduce a new unresolved type and write
-	# :name to use it. Look at `fill_context` for examples.
+	# - args shall be an array of types corresponding to the argument types
+	# - a newly introduced type-varialble shall be represented by a type-object whose
+	#   metadata is an Unresolved-object, which was uniquely created for this type-variable
+	# - See stdlib-functions below for examples (List/fold has an explanation)
 	def make_fn_type(*args, rettype)
 		if Types::not_a_type?(rettype); rettype = Types::Unresolved.new(rettype) end
 		args.reverse.reduce(rettype) { |rettype, arg|
-			argtype = arg
-			name = nil
-			if arg.is_a? Array
-				name = arg[0]
-				argtype = Types::Type.new(Types::Unresolved.new(name))
+			unres = nil
+			if arg.is_a? Types::Type and arg.metadata.is_a? Types::Unresolved
+				unres = arg.metadata
 			end
-			if Types::not_a_type?(argtype); argtype = Types::Unresolved.new(argtype) end
-			Types::Function.new(argtype, rettype, name)
+			Types::Function.new(arg, rettype, unres)
 		}
 	end
 	module_function :make_fn_type
@@ -81,9 +79,11 @@ module Dhallish
 
 		# Lists:
 		globalctx["List"] = BuiltinFunction.new { |a| Types::List.new(a) }
-		types["List"] = make_fn_type([:list_a], Types::Type.new(Types::List.new(Types::Unresolved.new(:list_a))))
+		unres_a = Types::Unresolved.new "a"
+		types["List"] = make_fn_type((Types::Type.new unres_a), Types::Type.new(Types::List.new(unres_a)))
 
-		list_length_type = make_fn_type([:list_len_a], Types::List.new(Types::Unresolved.new(:list_len_a)), Types::Natural)
+		unres_a = Types::Unresolved.new "a"
+		list_length_type = make_fn_type((Types::Type.new unres_a), Types::List.new(unres_a), Types::Natural)
 		globalctx["List/length"] = BuiltinFunction.new{ |a|
 			BuiltinFunction.new { |list|
 				list.length
@@ -91,12 +91,22 @@ module Dhallish
 		}
 		types["List/length"] = list_length_type
 
+		# List/fold introduces two type-variables a and b.
+		# for each of those type-variables, only one unique object shall be created,
+		# because we use references instead of names to check two Unresolved-objects
+		# for equality. This avoids name clashes.
+		unres_a = Types::Unresolved.new "a"
+		unres_b = Types::Unresolved.new "b"
 		list_fold_type = make_fn_type(
-			[:list_fold_a],
-			Types::List.new(Types::Unresolved.new(:list_fold_a)),
-			[:list_fold_b],
-			make_fn_type(:list_fold_a, :list_fold_b, :list_fold_b),
-			:list_fold_b, :list_fold_b)
+			Types::Type.new(unres_a),
+			# ^ This is where List/fold introduces a type-variable a, hence we create
+			# a Type-object with unres_a as its metadata
+			Types::List.new(unres_a),
+			Types::Type.new(unres_b),
+			make_fn_type(unres_a, unres_b, unres_b),
+			unres_b, unres_b)
+			# ^ Here the type-variable "b" is merely used, not introduced. Therefore we
+			# can use unres_b directly, without a Type-object around it
 		globalctx["List/fold"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				BuiltinFunction.new { |b|
@@ -112,10 +122,11 @@ module Dhallish
 		}
 		types["List/fold"] = list_fold_type
 
+		unres_a = Types::Unresolved.new "a"
 		list_head_type = make_fn_type(
-			[:list_head_a],
-			Types::List.new(Types::Unresolved.new(:list_head_a)),
-			Types::Optional.new(Types::Unresolved.new(:list_head_a)))
+			Types::Type.new(unres_a),
+			Types::List.new(unres_a),
+			Types::Optional.new(unres_a))
 		globalctx["List/head"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				list.first
@@ -123,10 +134,11 @@ module Dhallish
 		}
 		types["List/head"] = list_head_type
 
+		unres_a = Types::Unresolved.new "a"
 		list_last_type = make_fn_type(
-			[:list_last_a],
-			Types::List.new(Types::Unresolved.new(:list_last_a)),
-			Types::Optional.new(Types::Unresolved.new(:list_last_a)))
+			Types::Type.new(unres_a),
+			Types::List.new(unres_a),
+			Types::Optional.new(unres_a))
 		globalctx["List/last"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				list.last
@@ -134,10 +146,11 @@ module Dhallish
 		}
 		types["List/last"] = list_last_type
 
+		unres_a = Types::Unresolved.new "a"
 		list_tail_type = make_fn_type(
-			[:list_tail_a],
-			Types::List.new(Types::Unresolved.new(:list_tail_a)),
-			Types::List.new(Types::Unresolved.new(:list_tail_a)))
+			Types::Type.new(unres_a),
+			Types::List.new(unres_a),
+			Types::List.new(unres_a))
 		globalctx["List/tail"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				if list.empty?
@@ -149,20 +162,23 @@ module Dhallish
 		}
 		types["List/tail"] = list_tail_type
 
+		unres_a = Types::Unresolved.new "a"
 		types["List/reverse"] = make_fn_type(
-			[:list_reverse_a],
-			Types::List.new(Types::Unresolved.new(:list_reverse_a)),
-			Types::List.new(Types::Unresolved.new(:list_reverse_a)))
+			Types::Type.new(unres_a),
+			Types::List.new(unres_a),
+			Types::List.new(unres_a))
 		globalctx["List/reverse"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list| list.reverse }
 		}
 
+		unres_a = Types::Unresolved.new "a"
+		unres_b = Types::Unresolved.new "b"
 		types["List/build"] = make_fn_type(
-			[:list_build_a],
+			Types::Type.new(unres_a),
 			make_fn_type(
-				[:list_build_b],
-				make_fn_type(:list_build_a, :list_build_b, :list_build_b), :list_build_b, :list_build_b),
-			Types::List.new(Types::Unresolved.new(:list_build_a)))
+				Types::Type.new(unres_b),
+				make_fn_type(unres_a, unres_b, unres_b), unres_b, unres_b),
+			Types::List.new(unres_a))
 		globalctx["List/build"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |f|
 				cons = BuiltinFunction.new { |x|
@@ -172,12 +188,13 @@ module Dhallish
 			}
 		}
 
+		unres_a = Types::Unresolved.new "a"
 		types["List/indexed"] = make_fn_type(
-			[:list_indexed_a],
-			Types::List.new(Types::Unresolved.new(:list_indexed_a)),
+			Types::Type.new(unres_a),
+			Types::List.new(unres_a),
 			Types::List.new(Types::Record.new({
 				"index" => Types::Natural,
-				"value" => Types::Unresolved.new(:list_indexed_a)})))
+				"value" => unres_a})))
 		globalctx["List/indexed"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |list|
 				list.map.with_index { |val, idx|
@@ -186,18 +203,21 @@ module Dhallish
 			}
 		}
 
+		unres_a = Types::Unresolved.new "a"
 		# Optionals:
 		globalctx["Optional"] = BuiltinFunction.new { |a|
 			Types::Optional.new(a)
 		}
-		types["Optional"] = make_fn_type([:opt_a], Types::Type.new(Types::Optional.new(Types::Unresolved.new(:opt_a))))
+		types["Optional"] = make_fn_type(Types::Type.new(unres_a), Types::Type.new(Types::Optional.new(unres_a)))
 
+		unres_a = Types::Unresolved.new "a"
+		unres_b = Types::Unresolved.new "b"
 		optional_fold_type = make_fn_type(
-			[:opt_fold_a],
-			Types::Optional.new(Types::Unresolved.new(:opt_fold_a)),
-			[:opt_fold_b],
-			make_fn_type(:opt_fold_a, :opt_fold_b),
-			:opt_fold_b, :opt_fold_b)
+			Types::Type.new(unres_a),
+			Types::Optional.new(unres_a),
+			Types::Type.new(unres_b),
+			make_fn_type(unres_a, unres_b),
+			unres_b, unres_b)
 		globalctx["Optional/fold"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |opt|
 				BuiltinFunction.new { |b|
@@ -215,11 +235,13 @@ module Dhallish
 		}
 		types["Optional/fold"] = optional_fold_type
 
+		unres_a = Types::Unresolved.new "a"
+		unres_b = Types::Unresolved.new "b"
 		types["Optional/build"] = make_fn_type(
-			[:opt_build_a],
-			make_fn_type([:opt_build_b],
-				make_fn_type(:opt_build_a, :opt_build_b), :opt_build_b, :opt_build_b),
-			Types::Optional.new(Types::Unresolved.new(:opt_build_a)))
+			Types::Type.new(unres_a),
+			make_fn_type(Types::Type.new(unres_b),
+				make_fn_type(unres_a, unres_b), unres_b, unres_b),
+			Types::Optional.new(unres_a))
 		globalctx["Optional/build"] = BuiltinFunction.new { |a|
 			BuiltinFunction.new { |f|
 				just = BuiltinFunction.new { |x| x }
@@ -229,11 +251,12 @@ module Dhallish
 
 
 		# Naturals:
+		unres_a = Types::Unresolved.new "a"
 		natural_fold_type = make_fn_type(
 			Types::Natural,
-			[:nat_fold_a],
-			make_fn_type(:nat_fold_a, :nat_fold_a),
-			:nat_fold_a, :nat_fold_a)
+			Types::Type.new(unres_a),
+			make_fn_type(unres_a, unres_a),
+			unres_a, unres_a)
 		globalctx["Natural/fold"] = BuiltinFunction.new { |n|
 			BuiltinFunction.new { |a|
 				BuiltinFunction.new { |succ|
@@ -261,7 +284,8 @@ module Dhallish
 			succ = BuiltinFunction.new { |n| n + 1 }
 			f.call(Types::Natural).call(succ).call(zero)
 		}
-		types["Natural/build"] = make_fn_type(make_fn_type([:nat_build_a], make_fn_type(:nat_build_a, :nat_build_a), :nat_build_a, :nat_build_a), Types::Natural)
+		unres_a = Types::Unresolved.new "a"
+		types["Natural/build"] = make_fn_type(make_fn_type(Types::Type.new(unres_a), make_fn_type(unres_a, unres_a), unres_a, unres_a), Types::Natural)
 
 	end
 	module_function :fill_context
diff --git a/lib/types.rb b/lib/types.rb
index 1e6bbee26f4eacf1214c09402f6369345a34d9c5..daeeab6b4e690b87f22d26223409593a3d1d4e50 100644
--- a/lib/types.rb
+++ b/lib/types.rb
@@ -86,15 +86,7 @@ module Dhallish
 			def initialize(argtype, restype, unres=nil)
 				@argtype = argtype
 				@restype = restype
-				if !unres.nil?
-					if !unres.is_a? Symbol
-						@unres = unres.to_sym
-					else
-						@unres = unres
-					end
-				else
-					@unres = nil
-				end
+				@unres = unres
 			end
 
 			def ==(otype)
@@ -122,7 +114,6 @@ module Dhallish
 			def initialize(name)
 				@name = name.to_sym
 			end
-			def ==(otype) otype.is_a? Unresolved and otype.name == @name end
 			def to_s() "#{@name}" end
 		end
 		class Union
@@ -154,7 +145,7 @@ module Dhallish
 			when Type
 				Type.new(resolve(orgtype.metadata, name, newtype))
 			when Unresolved
-				if name == orgtype.name
+				if name == orgtype
 					newtype
 				else
 					orgtype
@@ -195,10 +186,10 @@ module Dhallish
 				end
 			when Unresolved
 				if b.is_a? Unresolved
-					if mapping[a.name] == nil
-						mapping[a.name] = b.name
+					if mapping[a] == nil
+						mapping[a] = b
 						mapping
-					elsif mapping[a.name] != b.name
+					elsif mapping[a] != b
 						nil
 					else
 						mapping