Note on why we stopped

aeon/core/types.py

@@ -150,7 +150,7 @@ class TypePolymorphism(Type):
     name: str  # alpha
     kind: Kind
     body: Type
-    bounded: list[type] = field(default_factory=list)
+    bounded: list[Type] = field(default_factory=list)
 
     def __str__(self):
         return f"forall {self.name}:{self.kind}, {self.body}"

aeon/typechecking/elaboration.py

@@ -157,14 +157,33 @@ def unify(ctx: TypingContext, sub: Type, sup: Type) -> list[Type]:
         unify(ctx, sup.var_type, sub.var_type)
         unify(ctx, sub.type, sup.type)
         return []
-    elif (isinstance(sub, TypeVar) and isinstance(
-            sup,
-            TypeVar,
-    ) and sup.name == sup.name):
+    elif isinstance(sub, TypeVar) and isinstance(
+            sup, TypeVar) and sup.name == sup.name:
         return []
+    elif isinstance(sup, Intersection):
+        for alt in sup.intersected:
+            try:
+                """
+                TODO
+
+                This implementation of unification is mutable.
+                As such, we cannot backtrack if unification fails, leading to a polluted environment.
+
+                The next step is to change the implementation to be pure.
+
+                Source: https://research.cs.queensu.ca/home/jana/papers/intcomp-jfp/Dunfield14_elaboration.pdf
+                """
+
+                unify(ctx, sub, alt)
+                break
+            except UnificationException:
+                pass
+        raise UnificationException(
+            f"Failed to unify {sub} with {sup} ({type(sup)})")
+
     else:
         raise UnificationException(
-            f"Failed to unify {sub} with {sup} ({type(sup)})", )
+            f"Failed to unify {sub} with {sup} ({type(sup)})")
 
 
 def simple_subtype(ctx: TypingContext, a: Type, b: Type) -> bool:
@@ -358,24 +377,13 @@ def elaborate_check(ctx: TypingContext, t: Term, ty: Type) -> Term:
             # Supports multiple nested foralls
             u = UnificationVar(ctx.fresh_var())
             c = TypeApplication(c, u)
-            for v in s.bounded:
-                try:
-                    s1 = type_substitution(s.body, s.name, u)
-                    unify(ctx, s1, ty)
-                except UnificationException:
-                    pass
+            if s.bounded:
+                unify(ctx, u, Intersection(s.bounded))
+            s = type_substitution(s.body, s.name, u)
         unify(ctx, s, ty)
         return c
 
 
-# TODO now:
-
-# I was trying to add intersection types, but I am not sure about the complexity of inference.
-
-# Instead, we could try to lazily translate "+(top) x y" to "smtPlus x y" by peeking into the type of arguments during translation.
-assert False
-
-
 @dataclass
 class Union(Type):
     united: list[Type]
@@ -613,6 +621,7 @@ def elaborate_remove_unification(ctx: TypingContext, t: Term) -> Term:
 
 
 def elaborate(ctx: TypingContext, e: Term, expected_type: Type = top) -> Term:
+
     e2 = elaborate_foralls(e)
     e3 = elaborate_check(ctx, e2, expected_type)
     print("e3", e3)

tests/elaboration_test.py

@@ -91,5 +91,4 @@ def test_bound_type():
         "f", parse_type("forall a:B = Int±Bool, (x:a) -> a"))
 
     t2 = elaborate(ctx, t, Top())
-
     assert t2.fun.type == BaseType("Int")