From 352456f5e315ce13f93d2a8f60fa22fd971a89db Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 19:57:05 +0000 Subject: [PATCH] fix(desugar): a constructor gets its type arguments from its use A constructor of a `data` type with type parameters did not check when the other side of its sum had a type parameter: `None` was not an `Option(I32)`, and `L(1)` was not an `Either(I32, Bool)`. The annotation of the injection had the type parameter itself, which is no type at the constructor. It checked only when a generic function gave its own type parameter the same name. The annotation now binds the type parameters of the `data` type, for each `data` type with type parameters. #438 did this for a `data` type that refers to itself. The checker gives each bound parameter a type from the use of the value. Each annotation gets its own type: an injection has each type on its other side. A use at another type is a type error, as before. No program of the corpus changed. New test: a_constructor_gets_its_type_arguments_from_its_use (7 programs, as wasm and in the interpreter). 637 tests pass; the all-target count is 634. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --- TEST-NEEDS.adoc | 6 +- src/ephapax-cli/tests/run_wasm.rs | 101 ++++++++++++++++++++++++++++++ src/ephapax-desugar/src/lib.rs | 43 +++++++------ src/ephapax-typing/src/lib.rs | 6 +- 4 files changed, 129 insertions(+), 27 deletions(-) diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index d441664..c126f77 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *633 tests* (`+cargo test --workspace --all-targets+`); +* Total: *634 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 633 +* Documented all-target tests: 634 === CRG Testing Taxonomy — Status @@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) ==== Build & Execution * [x] cargo build — compiles -* [x] cargo test –workspace –all-targets — 633 pass, 0 fail +* [x] cargo test –workspace –all-targets — 634 pass, 0 fail * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays diff --git a/src/ephapax-cli/tests/run_wasm.rs b/src/ephapax-cli/tests/run_wasm.rs index 0c53800..f32d799 100644 --- a/src/ephapax-cli/tests/run_wasm.rs +++ b/src/ephapax-cli/tests/run_wasm.rs @@ -508,6 +508,107 @@ fn a_module_names_a_data_type_only_through_a_pub_import() { } } +/// A constructor of a `data` type with type parameters gets its type +/// arguments from the use of the value. The annotation of the injection +/// had the type parameter itself, which is no type at the constructor: +/// `None` was not an `Option(I32)`, and `L(1)` was not an +/// `Either(I32, Bool)`. +#[test] +fn a_constructor_gets_its_type_arguments_from_its_use() { + let tmp = tempfile::tempdir().expect("tempdir"); + let write = + |name: &str, text: &str| std::fs::write(tmp.path().join(name), text).expect("write module"); + let option = "data Option(a) = None | Some(a)\n\n"; + let either = "data Either(a, b) = L(a) | R(b)\n\n"; + let three = "data T(a) = A(a) | B(a) | C(a)\n\n"; + let or = "fn or(o: Option(I32), d: I32): I32 = match o of | None => d | Some(n) => n end\n\n"; + + // (declarations, `main` type, `main` body, output) + for (decls, ty, main, want) in [ + // As a result, as an argument, and with no annotation. + ( + format!("{option}{or}fn none(): Option(I32) = None\n\n"), + "I32", + "or(none(), 40) + or(None, 2)", + "42", + ), + ( + option.to_string(), + "I32", + "let o = None in match o of | None => 42 | Some(n) => n end", + "42", + ), + // The 2 branches of an `if` give the 2 sides of the sum. + ( + format!("{option}{or}"), + "I32", + "or(if true then None else Some(1), 42)", + "42", + ), + // In a generic function, with a type parameter of another name. + ( + format!( + "{option}{or}fn none(): Option(T) = None\n\n\ + fn is(o: Option(Bool)): Bool = match o of | None => true | Some(b) => b end\n\n" + ), + "I32", + "if is(none()) then or(none(), 42) else 0", + "42", + ), + // A constructor in a constructor. + ( + format!( + "{option}fn deep(o: Option(Option(I32))): I32 =\n match o of\n | None => 1\n \ + | Some(i) => match i of | None => 2 | Some(n) => n end\n end\n\n" + ), + "I32", + "deep(None) + deep(Some(None)) + deep(Some(Some(39)))", + "42", + ), + // 2 type parameters, each side at its width. + ( + format!( + "{either}fn pick(e: Either(I64, F64)): I64 =\n \ + match e of | L(n) => n | R(x) => 5000000000 - 4999999999 end\n\n" + ), + "I64", + "pick(L(5000000000)) + pick(R(1.5))", + "5000000001i64", + ), + // 3 constructors: each annotation of the chain. + ( + format!( + "{three}fn f(t: T(I32)): I32 =\n \ + match t of | A(n) => n | B(n) => n + 1 | C(n) => n + 2 end\n\n" + ), + "I32", + "f(A(10)) + f(B(10)) + f(C(9))", + "32", + ), + ] { + write( + "app.eph", + &format!("module app\n\n{decls}fn main(): {ty} = {main}\n"), + ); + for args in [&["run", "app.eph"][..], &["run", "--interp", "app.eph"]] { + assert_eq!(stdout_of(tmp.path(), args), want, "{main} under {args:?}"); + } + } + + // A use at another type is a type error, as before. + write( + "bad.eph", + &format!("module bad\n\n{three}fn g(t: T(Bool)): I32 = 0\n\nfn main(): I32 = g(B(1))\n"), + ); + let out = ephapax(tmp.path(), &["check", "bad.eph"]); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + !out.status.success() && stderr.contains("Type mismatch"), + "exit {:?}, stderr:\n{stderr}", + out.status.code() + ); +} + /// A `type` alias and an extern type follow the rule of data types (owner /// decision 2026-11-10): a module names one when it declares it, or when /// it imports the module that declares it. An alias must also be `pub`; diff --git a/src/ephapax-desugar/src/lib.rs b/src/ephapax-desugar/src/lib.rs index 3dd66f5..b3cb112 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -1159,13 +1159,11 @@ impl Desugarer { }) } - /// The recursive type of the `data` type of the constructor `info`, - /// or `None` if that `data` type does not refer to itself. The type - /// parameters of the `data` type are type variables in the result. - fn recursive_ty( - &self, - info: &ConstructorInfo, - ) -> Result, Ty)>, DesugarError> { + /// The type parameters of the `data` type of the constructor `info`, + /// and the type of that `data` type with them as type variables. The + /// type is a recursive type (`Ty::Mu`) if the `data` type refers to + /// itself. + fn data_ty(&self, info: &ConstructorInfo) -> Result<(Vec, Ty), DesugarError> { let params = match self.registry.get_type(&info.home, &info.data_name) { Some(TypeInfo { def: TypeDef::Data { params, .. }, @@ -1181,7 +1179,7 @@ impl Desugarer { let ty = self.in_scope(&info.home, |this| { this.desugar_named_type(&info.data_name, &args) })?; - Ok(matches!(ty, Ty::Mu { .. }).then_some((params, ty))) + Ok((params, ty)) } /// Build the right-nested binary sum type for a list of constructors. @@ -1258,27 +1256,28 @@ impl Desugarer { let ctors = self.ctors_of(&info)?; - // A value of a recursive type is folded (v2 plan rung E9). The - // type parameters of the `data` type are bound in each annotation: - // the type checker finds a type for each one at this constructor, - // and the fold makes the annotations of the injections agree. - let recursive = self.recursive_ty(&info)?; - let params: &[SmolStr] = recursive.as_ref().map_or(&[], |(params, _)| params); + // The type parameters of the `data` type are bound in each + // annotation: the type checker finds a type for each one from the + // use of the value. (An annotation had the parameter itself, which + // is no type at the constructor: `None` was not an `Option(I32)`.) + let (params, ty) = self.data_ty(&info)?; // Wrap in inl/inr chain based on index. The types of the other // constructors are names of the module that declares the type. let value = self.in_scope(&info.home, |this| { - this.wrap_injection(payload, info.index, &ctors, params, span) + this.wrap_injection(payload, info.index, &ctors, ¶ms, span) })?; - Ok(match &recursive { - None => value, - Some((params, ty)) => Expr::new( + // A value of a recursive type is folded (v2 plan rung E9). The + // fold makes the annotations of the injections agree. + Ok(match ty { + Ty::Mu { .. } => Expr::new( ExprKind::Fold { - ty: quantify(ty.clone(), params), + ty: quantify(ty, ¶ms), value: Box::new(value), }, span, ), + _ => value, }) } @@ -1462,9 +1461,9 @@ impl Desugarer { let ctors = self.ctors_of(info)?; // A value of a recursive type is unfolded before its sum is read // (v2 plan rung E9). - let core_scrutinee = match self.recursive_ty(info)? { - Some(_) => Expr::new(ExprKind::Unfold(Box::new(core_scrutinee)), span), - None => core_scrutinee, + let core_scrutinee = match self.data_ty(info)?.1 { + Ty::Mu { .. } => Expr::new(ExprKind::Unfold(Box::new(core_scrutinee)), span), + _ => core_scrutinee, }; // The constructor index of each arm; `None` for an arm that takes diff --git a/src/ephapax-typing/src/lib.rs b/src/ephapax-typing/src/lib.rs index eed55a8..35891c1 100644 --- a/src/ephapax-typing/src/lib.rs +++ b/src/ephapax-typing/src/lib.rs @@ -1765,8 +1765,10 @@ impl TypeChecker { /// `inl[ty](value)`: `ty` is the type of the other side of the sum. A /// type parameter that the annotation binds (`forall a. T`, from a - /// constructor of a recursive `data` type) gets a type from the use - /// of the value: the `fold` around the injection. + /// constructor of a `data` type with type parameters) gets a type + /// from the use of the value. Each annotation gets its own: an + /// injection has each type on its other side. The `fold` of a + /// recursive type makes the annotations under it agree. fn check_inl(&mut self, _s: Span, ty: &Ty, value: &Expr) -> Result { let value_ty = self.check(value)?; let (ty, _) = self.instantiate(ty.clone());