From e4d24476a98dabc3c7eaa92caae614a3ed1a9295 Mon Sep 17 00:00:00 2001
From: agra <alex@swipelab.co>
Date: Tue, 16 Jun 2026 18:47:55 +0300
Subject: [PATCH] =?UTF-8?q?xfail(reify):=20typefn=20identity=20=E2=80=94?=
 =?UTF-8?q?=20Box($T)=20over=20reify,=20two=20sites=20one=20type?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

REIFY Phase 1.0. Add examples/0615: a type-fn `Box :: ($T)->Type {
return reify(...) }` used at two independent sites (a return type and a
parameter type); consume(build()) typechecks only if both sites resolve
to ONE TypeId. RED by design — reify in a type-fn body still bails
("only supported in a :: binding"). Phase 1.1 routes a reify-returning
type-fn body through reifyType under the mangled instantiation name so
identity holds, turning this green.
---
 .../0615-comptime-reify-typefn-identity.sx    | 34 +++++++++++++++++++
 .../0615-comptime-reify-typefn-identity.exit  |  0
 2 files changed, 34 insertions(+)
 create mode 100644 examples/0615-comptime-reify-typefn-identity.sx
 create mode 100644 examples/expected/0615-comptime-reify-typefn-identity.exit

diff --git a/examples/0615-comptime-reify-typefn-identity.sx b/examples/0615-comptime-reify-typefn-identity.sx
new file mode 100644
index 00000000..3877ba70
--- /dev/null
+++ b/examples/0615-comptime-reify-typefn-identity.sx
@@ -0,0 +1,34 @@
+// REIFY Phase 1: a type-fn that RETURNS `reify(...)` must memoize by the
+// instantiation's mangled name, so `Box(i64)` resolved at two INDEPENDENT sites
+// (here: a return type and a parameter type) is ONE `TypeId`. A value built at
+// one site is therefore assignable / matchable at the other — nominal identity
+// (Contract 1). If the reify result were not registered under the mangled
+// instantiation name, the two sites would mint distinct types and
+// `consume(build())` would be a type error.
+#import "modules/std.sx";
+#import "modules/std/meta.sx";
+
+Box :: ($T: Type) -> Type {
+    return reify(.enum(.{ variants = .[
+        EnumVariant.{ name = "some", payload = T    },
+        EnumVariant.{ name = "none", payload = void },
+    ] }));
+}
+
+build :: () -> Box(i64) {            // site A resolves Box(i64)
+    return Box(i64).some(7);
+}
+
+consume :: (b: Box(i64)) {           // site B resolves Box(i64) independently
+    if b == {
+        case .some: (n) { print("some {}\n", n); }
+        case .none: { print("none\n"); }
+    }
+}
+
+main :: () -> i32 {
+    consume(build());                // typechecks ONLY if site A == site B
+    b : Box(i64) = .none;
+    consume(b);
+    return 0;
+}
diff --git a/examples/expected/0615-comptime-reify-typefn-identity.exit b/examples/expected/0615-comptime-reify-typefn-identity.exit
new file mode 100644
index 00000000..e69de29b