Tweak unification algorithm.

spec/integration_spec.cr

@@ -173,6 +173,7 @@ describe HM do
 
   expect_normalized("Function(value: a, context: Test.Context(b), Test.Context(c))", "Function(value: a, context: Test.Context(b), Test.Context(c))")
 
+  expect_not_unify("Function(Maybe(value), Maybe(value))", "Function(value: value, Maybe(value))")
   expect_not_unify("Function(String,Number)", "Function(Number,Number)")
   expect_not_unify("Array(x)", "Array(x,y)")
   expect_not_unify("Array(x,y)", "Array(x)")

src/types.cr

@@ -32,6 +32,11 @@ module HM
     def empty?
       true
     end
+
+    # Returns whether this type includes (equals) the other type or variable.
+    def includes?(other : Checkable)
+      self == other
+    end
   end
 
   # Represents a type which has a name and can have many fields.
@@ -80,6 +85,11 @@ module HM
     def empty?
       fields.empty?
     end
+
+    # Returns whether this type includes the other type or variable.
+    def includes?(other : Checkable)
+      self == other || fields.any? { |field| field.item.includes?(other) }
+    end
   end
 
   # Represents a definition of a type.

src/unifier.cr

@@ -18,49 +18,33 @@ module HM
       mapping =
         {} of Variable => Checkable
 
-      result =
-        unify(normalize(a), normalize(b), mapping)
-
-      substitue(result, mapping) if result
+      unify(normalize(a), normalize(b), mapping).try do |result|
+        substitue(result, mapping) if result
+      end
     end
 
     # This method tries to unify the given types by traversing it's parameters
-    # and producing a mapping of variables to types (Variable => Checkable) which
-    # later on we can use to substitue to one of the types and create a unified
-    # type.
+    # and producing a mapping of variables to types (Variable => Checkable)
+    # which later on we can use to substitue to one of the types and create a
+    # unified type.
     #
     # It is important that this method assumes that both of the types were
     # normalized before, since normalization orders the fields, so as an
     # optimization we don't normalize the types here.
     private def unify(a : Checkable, b : Checkable, mapping : Hash(Variable, Checkable))
       case {a, b}
       in {Variable, Variable}
-        # If there are two variables we need to check if they already have
-        # assigned types, if they do we need to test if they are equal, if not
-        # we cannot unify, otherwise we can just point them to each other
-        # (depending if they have instances or not).
-        instanceA = mapping[a]?
-        instanceB = mapping[b]?
-
-        if instanceA && instanceB
-          unify(instanceA, instanceB)
-        elsif instanceA && instanceA != b
-          mapping[b] = a
+        # If the mapped type contains the varaible it would result in a circular
+        # substitution so it's not unifiable.
+        return nil if mapping[b]?.try(&.includes?(a))
+
+        if mapping[a]?
+          unify(b, a)
         else
-          mapping[a] = b
+          a.tap { mapping[a] = b }
         end
       in {Variable, Type}
-        # If we have a variable and a type we need to check if the variable
-        # already points to the same type, if not, we cannot unify, otherwise
-        # we can just point the variable to the type.
-        instance = mapping[a]?
-
-        # This check is important since the variables can point to each other.
-        if instance && instance.is_a?(Type)
-          unify(instance, b)
-        else
-          mapping[a] = b
-        end
+        a.tap { mapping[a] = b }
       in {Type, Variable}
         # In this branch we just call unify for the case above.
         unify(b, a, mapping)