Equiricursive unification

src/check/test/unify_test.zig

@@ -4425,3 +4425,187 @@ test "recursion_var - does not cause infinite loop during resolution" {
     // Both should resolve to the same root var
     try std.testing.expectEqual(resolved_rec.var_, resolved_structure.var_);
 }
+
+// Equirecursive unification tests
+
+test "recursion_var - unifies with alias" {
+    const gpa = std.testing.allocator;
+
+    var env = try TestEnv.init(gpa);
+    defer env.deinit();
+
+    // Create an alias MyStr = Str
+    const str_var = try env.module_env.types.freshFromContent(Content{ .structure = .str });
+    const alias_content = try env.mkAlias("MyStr", str_var, &[_]Var{});
+    const alias_var = try env.module_env.types.freshFromContent(alias_content);
+
+    // Create a RecursionVar pointing to str
+    const rec_var = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = str_var,
+            .name = null,
+        },
+    });
+
+    // RecursionVar should unify with alias by going through to the backing var
+    const result = try env.unify(rec_var, alias_var);
+    try std.testing.expectEqual(.ok, result);
+}
+
+test "recursion_var - cannot unify with rigid" {
+    const gpa = std.testing.allocator;
+
+    var env = try TestEnv.init(gpa);
+    defer env.deinit();
+
+    // Create a rigid var
+    const rigid_content = try env.mkRigidVar("a");
+    const rigid_var = try env.module_env.types.freshFromContent(rigid_content);
+
+    // Create a RecursionVar
+    const structure_var = try env.module_env.types.freshFromContent(Content{ .structure = .str });
+    const rec_var = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = structure_var,
+            .name = null,
+        },
+    });
+
+    // RecursionVar cannot unify with rigid
+    const result = try env.unify(rec_var, rigid_var);
+    try std.testing.expectEqual(false, result.isOk());
+}
+
+test "recursion_var - two recursion vars with same structure unify" {
+    const gpa = std.testing.allocator;
+
+    var env = try TestEnv.init(gpa);
+    defer env.deinit();
+
+    // Create a shared structure
+    const structure_var = try env.module_env.types.freshFromContent(Content{ .structure = .str });
+
+    // Create two RecursionVars both pointing to the same structure
+    const rec_var_1 = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = structure_var,
+            .name = null,
+        },
+    });
+
+    const rec_var_2 = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = structure_var,
+            .name = null,
+        },
+    });
+
+    // They should unify successfully
+    const result = try env.unify(rec_var_1, rec_var_2);
+    try std.testing.expectEqual(.ok, result);
+}
+
+test "recursion_var - two recursion vars with different structures do not unify" {
+    const gpa = std.testing.allocator;
+
+    var env = try TestEnv.init(gpa);
+    defer env.deinit();
+
+    // Create different structures
+    const str_var = try env.module_env.types.freshFromContent(Content{ .structure = .str });
+    const num_var = try env.module_env.types.freshFromContent(Content{ .structure = .{ .num = Num.int_i32 } });
+
+    // Create two RecursionVars with different structures
+    const rec_var_1 = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = str_var,
+            .name = null,
+        },
+    });
+
+    const rec_var_2 = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = num_var,
+            .name = null,
+        },
+    });
+
+    // They should not unify - different base structures
+    const result = try env.unify(rec_var_1, rec_var_2);
+    try std.testing.expectEqual(false, result.isOk());
+}
+
+test "recursion_var - equirecursive unification with nested structure" {
+    const gpa = std.testing.allocator;
+
+    var env = try TestEnv.init(gpa);
+    defer env.deinit();
+
+    // Create a list structure: List(a) where a is flexible
+    const elem_var = try env.module_env.types.fresh();
+    const list_var = try env.module_env.types.freshFromContent(Content{ .structure = .{ .list = elem_var } });
+
+    // Create a RecursionVar that points to the list
+    const rec_var = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = list_var,
+            .name = null,
+        },
+    });
+
+    // Create another list with the same structure
+    const elem_var_2 = try env.module_env.types.fresh();
+    const list_var_2 = try env.module_env.types.freshFromContent(Content{ .structure = .{ .list = elem_var_2 } });
+
+    // RecursionVar should unify with the list
+    const result = try env.unify(rec_var, list_var_2);
+    try std.testing.expectEqual(.ok, result);
+
+    // The element vars should also have been unified
+    const resolved_elem_1 = env.module_env.types.resolveVar(elem_var);
+    const resolved_elem_2 = env.module_env.types.resolveVar(elem_var_2);
+    try std.testing.expectEqual(resolved_elem_1.var_, resolved_elem_2.var_);
+}
+
+test "recursion_var - unifies with flex preserving constraints" {
+    const gpa = std.testing.allocator;
+
+    var env = try TestEnv.init(gpa);
+    defer env.deinit();
+
+    // Create a flex var with static dispatch constraints
+    const fn_var = try env.module_env.types.freshFromContent(Content{
+        .structure = .{ .fn_pure = .{
+            .args = VarSafeList.Range.empty(),
+            .ret = try env.module_env.types.fresh(),
+            .needs_instantiation = false,
+        } },
+    });
+
+    const constraint = types_mod.StaticDispatchConstraint{
+        .fn_name = try env.module_env.getIdentStore().insert(env.module_env.gpa, Ident.for_text("to_str")),
+        .fn_var = fn_var,
+        .origin = .method_call,
+    };
+
+    const constraints_range = try env.module_env.types.appendStaticDispatchConstraints(&[_]types_mod.StaticDispatchConstraint{constraint});
+    const flex_with_constraints = try env.module_env.types.freshFromContent(Content{
+        .flex = Flex.init().withConstraints(constraints_range),
+    });
+
+    // Create a RecursionVar
+    const structure_var = try env.module_env.types.freshFromContent(Content{ .structure = .str });
+    const rec_var = try env.module_env.types.freshFromContent(Content{
+        .recursion_var = .{
+            .structure = structure_var,
+            .name = null,
+        },
+    });
+
+    // Unify - should defer the constraints
+    const result = try env.unify(rec_var, flex_with_constraints);
+    try std.testing.expectEqual(.ok, result);
+
+    // Should have deferred the constraints
+    try std.testing.expectEqual(@as(usize, 1), env.scratch.deferred_constraints.len());
+}

src/check/unify.zig

@@ -789,9 +789,14 @@ const Unifier = struct {
 
     /// Unify when `a` is a recursion variable
     ///
-    /// Placeholder: This currently just unifies with the structure the recursion
-    /// var points to. This will be enhanced to handle equirecursive unification
-    /// properly and prevent infinite loops.
+    /// Equirecursive unification: Two recursive types unify if they are structurally
+    /// equal up to their recursion points. RecursionVar marks these recursion points
+    /// and prevents infinite expansion during unification.
+    ///
+    /// The key insight: when we encounter a RecursionVar, we unify with the structure
+    /// it points to. The existing cycle detection in unifyGuarded (via checkVarsEquiv)
+    /// ensures we don't infinitely recurse - if we've already unified these exact vars,
+    /// we return early.
     fn unifyRecursionVar(
         self: *Self,
         vars: *const ResolvedVarDescs,
@@ -803,6 +808,7 @@ const Unifier = struct {
 
         switch (b_content) {
             .flex => |b_flex| {
+                // RecursionVar can unify with flex - defer constraints and merge
                 if (b_flex.constraints.len() > 0) {
                     // Record that we need to check constraints later
                     _ = self.scratch.deferred_constraints.append(self.scratch.gpa, DeferredConstraintCheck{
@@ -813,20 +819,24 @@ const Unifier = struct {
                 self.merge(vars, vars.a.desc.content);
             },
             .rigid => {
-                // Recursion var cannot unify with rigid
+                // RecursionVar cannot unify with rigid - rigid types have no structure to recurse into
                 return error.TypeMismatch;
             },
-            .alias => {
-                // TODO: Handle alias case properly in Phase 4
-                return error.TypeMismatch;
+            .alias => |b_alias| {
+                // Unify with the alias backing var to preserve the alias structure
+                // This allows RecursionVar to work through type aliases
+                const backing_var = self.types_store.getAliasBackingVar(b_alias);
+                try self.unifyGuarded(vars.a.var_, backing_var);
             },
             .structure => {
                 // Unify the structure the recursion var points to with b's structure
+                // This is equirecursive unification: unfold one level and continue
                 try self.unifyGuarded(a_rec_var.structure, vars.b.var_);
             },
             .recursion_var => |b_rec_var| {
-                // Both are recursion vars - unify their structures
-                // This is the key to equirecursive unification (will be enhanced in Phase 4)
+                // Both are recursion vars - the heart of equirecursive unification
+                // We unify their structures. If they form a cycle, checkVarsEquiv
+                // in unifyGuarded will detect it and prevent infinite recursion.
                 try self.unifyGuarded(a_rec_var.structure, b_rec_var.structure);
             },
             .err => self.merge(vars, .err),