fix bug in unification

README.md

@@ -32,3 +32,4 @@ ruby ./tests/test.rb
 - [ ] disallow Type Names like `Natural` or `let` as labels
 - [ ] more tests and tests for expected failure
 - [ ] "n-1": currently interpreted as label, but should be a subtraction (sometimes)
+- [ ] Warum funktionieren Typannotationen in lets mit verschiedenen Typvariablen?

lib/ast.rb

@@ -426,7 +426,7 @@ module Dhallish
 				type_type = @type.compute_type ctx
 				assert ("Annotated expression not a type") { type_type.is_a? Types::Type }
 				exp_type = type_type.metadata
-				assert ("Expression does not match annotated type. Actual: #{act_type}, expected: #{exp_type}") { act_type == exp_type }
+				assert ("Expression does not match annotated type. Actual: #{act_type}, expected: #{exp_type}") { Types::unification act_type, exp_type }
 				exp_type
 			end
 

lib/types.rb

@@ -149,7 +149,6 @@ module Dhallish
 		module_function :resolve
 
 		def unification(a, b, mapping={})
-			assert("a and b must be types") { is_a_type(a) and is_a_type(b) }
 			case a
 			when Type
 				if b.is_a? Type
@@ -162,7 +161,7 @@ module Dhallish
 					if mapping[a.name] == nil
 						mapping[a.name] = b.name
 						mapping
-					elsif mapping[a.name] != mapping[b.name]
+					elsif mapping[a.name] != b.name
 						nil
 					else
 						mapping