xfail(reify): typefn identity — Box($T) over reify, two sites one type

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.
This commit is contained in:
agra
2026-06-16 18:47:55 +03:00
parent 04e833a825
commit e4d24476a9
2 changed files with 34 additions and 0 deletions

View File

@@ -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;
}