Different fresh strategy

aeon/typechecking/context.py

@@ -10,6 +10,9 @@
 from aeon.core.types import StarKind
 from aeon.core.types import Type
 
+KEY = "KEY"
+COUNTER: dict[str, int] = {KEY: 0}
+
 
 class Polarity(Enum):
     NEITHER = 1
@@ -100,8 +103,9 @@ def type_constructor_named(self, name: str) -> list[tuple[str, Kind, Polarity]]
             return None
 
     def fresh_var(self):
-        x = len(self.entries)
-        return f"fresh_{x}"
+        y = COUNTER[KEY]
+        COUNTER[KEY] += 1
+        return f"fresh_{y}"
 
     def kind_of(self, ty) -> Kind | None:
         if isinstance(ty, BaseType):

aeon/typechecking/elaboration.py

@@ -4,6 +4,7 @@
 from dataclasses import field
 from functools import reduce
 from itertools import combinations
+from loguru import logger
 
 from aeon.core.instantiation import type_substitution
 from aeon.core.liquid import LiquidHornApplication
@@ -308,12 +309,16 @@ def elaborate_check(ctx: TypingContext, t: Term, ty: Type) -> Term:
 
     elif isinstance(t, Let):
         u = UnificationVar(ctx.fresh_var())
+        if t.var_name == "r":
+            logger.error(f"debug: {u} {t} {ty}")
         nval = elaborate_check(ctx, t.var_value, u)
         nbody = elaborate_check(
             ctx.with_var(t.var_name, u),
             t.body,
             ty,
         )
+        if t.var_name == "r":
+            logger.error(f"debug: {u}")
         return Let(t.var_name, nval, nbody)
 
     elif isinstance(t, Rec):

aeon/verification/sub.py

@@ -112,6 +112,7 @@ def sub(ctx: TypingContext, t1: Type, t2: Type) -> Constraint:
             base_type = BaseType("TypeConstructorPlaceHolder")
         else:
             logger.error(f"Could not subtype: {t1} <: {t2} because of non-refined type.")
+            raise Exception()
             return cfalse
         assert isinstance(base_type, BaseType)
 

tests/horn_test.py

@@ -4,6 +4,7 @@
 from aeon.core.liquid import LiquidHornApplication
 from aeon.core.types import RefinedType
 from aeon.core.types import t_int
+from aeon.typechecking.context import COUNTER, KEY
 from aeon.utils.ctx_helpers import build_context
 from aeon.verification.helpers import get_abs_example
 from aeon.verification.helpers import parse_liquid
@@ -21,13 +22,15 @@ def test_fresh():
     ctx = build_context({"x": t_int})
 
     t = RefinedType("v", t_int, LiquidHornApplication("?"))
+    counter = COUNTER[KEY]
+    name = f"fresh_{counter}"
     r = fresh(ctx, t)
     assert r == RefinedType(
-        "v_fresh_1",
+        f"v_{name}",
         t_int,
         LiquidHornApplication(
-            "fresh_1",
-            [(parse_liquid("x"), "Int"), (parse_liquid("v_fresh_1"), "Int")],
+            name,
+            [(parse_liquid("x"), "Int"), (parse_liquid(f"v_{name}"), "Int")],
         ),
     )
     assert wellformed_horn(r.refinement)
@@ -47,17 +50,18 @@ def test_possible_args2():
 
 def test_base_assignment_helper():
     assign = build_initial_assignment(
-        LiquidConstraint(
-            LiquidHornApplication("k", [(parse_liquid("x"), "Int")])), )
+        LiquidConstraint(LiquidHornApplication("k", [(parse_liquid("x"), "Int")])),
+    )
     assert "k" in assign
     assert len(assign["k"]) == 30
 
 
 def test_base_assignment_helper2():
     assign = build_initial_assignment(
         LiquidConstraint(
-            LiquidHornApplication("k", [(parse_liquid("x"), "Int"),
-                                        (parse_liquid("y"), "Int")]), ), )
+            LiquidHornApplication("k", [(parse_liquid("x"), "Int"), (parse_liquid("y"), "Int")]),
+        ),
+    )
     assert "k" in assign
     assert len(assign["k"]) == 120
 
@@ -72,7 +76,9 @@ def test_merge_assignments():
                     (parse_liquid("y"), "Int"),
                     (parse_liquid("z"), "Bool"),
                 ],
-            ), ), )
+            ),
+        ),
+    )
     t = merge_assignments(assign["k"])
     assert isinstance(t, LiquidApp)