From b6bad20a78aa8b798eed0a1f08e195bda745a529 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 21:54:15 +0000 Subject: [PATCH] fix: a constructor checks its arguments against the declaration A constructor of a `data` type that is not recursive left no core node that carries the declared type. `MkBox(true)` passed for `data Box = MkBox(I32)` until a use of the value as a `Box`. The desugarer now emits `let #: T = in #`. `T` is the declared type and binds the type parameters of the `data` type. The type checker instantiates the annotation, and a mismatch is the new error `ConstructorMismatch`, which names the constructor. The check is on the full value, so the arguments of 1 constructor fix the type parameters for the other constructors also. Wasm codegen reads the type of such a `let` from the type table, because the annotation binds type parameters. Owner decisions 2026-11-10: the annotated `let` is the interim form; decision D14 in the plan document records the type ascription for the P4 core, to be decided with `TMu`, `fold` and `unfold`. A constructor of a recursive type has the check from its `fold`, as before. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --- TEST-NEEDS.adoc | 6 +- .../EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc | 37 ++++++++ src/ephapax-cli/tests/recursive_types.rs | 18 ++-- src/ephapax-cli/tests/run_wasm.rs | 85 +++++++++++++++++++ src/ephapax-desugar/src/lib.rs | 41 +++++++-- src/ephapax-typing/src/lib.rs | 31 +++++-- src/ephapax-wasm/src/lib.rs | 3 + 7 files changed, 200 insertions(+), 21 deletions(-) diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 7fb9c35..7b382eb 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: *639 tests* (`+cargo test --workspace --all-targets+`); +* Total: *640 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 639 +* Documented all-target tests: 640 === 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 — 639 pass, 0 fail +* [x] cargo test –workspace –all-targets — 640 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/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc index fb4f994..0a2e77c 100644 --- a/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc +++ b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc @@ -1175,6 +1175,7 @@ Engineering tracks inside each wave run in parallel with the proof tracks. The o |D10 |W1 (T1a) |layout-profile note / E5 (W2), then E9, E8, E10, E18 |D12 |W5 (T5g) |erasure notes / E16, P21 (W6) |D13 (added 2026-11-09) |W1 (T1a) |the 2026-11-09 classification ruling / P4 and every later P-rung +|D14 (added 2026-11-10) |W1 (T1a), before P4 |the constructor check of 2026-11-10 (interim: annotated `let`) / P4 |=== A rung whose dependency has not completed (for example E8 while the typed-wasm fix is unmerged) carries over to the next wave together with every rung that depends on it (E9 completion, E10, E14, P18, the W5 gate-acceptance exit). It is never declared done against a missing dependency. @@ -1563,6 +1564,42 @@ Follows the owner ruling of 2026-11-09 that the soundness statements are theory, |PROOF-POLICY §2 prefers transport. Coq → Dedukti → Agda is the reverse of the policy's direction and depends on exporters the estate has not pinned; worth an X-experiment before relying on it. |=== +=== D14 — A type ascription in the core (added 2026-11-10) + +A constructor of a `data` type that is not recursive left no core node that carries the declared type: `MkBox(true)` passed for `data Box = MkBox(I32)` until a use of the value as a `Box`. A constructor of a recursive type has the check from its `fold` (D7). This decision is the core form that carries the check for the other `data` types. + +*Interim (owner, 2026-11-10):* the desugarer emits `let #C: T = v in #C`. `T` is the declared type and binds the type parameters of the `data` type. The calculus has this term already (`ELet v (EVar 0)`; its `let` has no annotation), so no proof file changes. Gate: `a_constructor_checks_its_arguments_against_the_declaration` in `src/ephapax-cli/tests/run_wasm.rs`. The decision stays open until the owner decides the nominal or the bidirectional design. It is taken with the P4 core, where `TMu`, `fold` and `unfold` enter the calculus, so that the core is extended 1 time. + +An ascription `EAscribe T e` needs these parts in the P4 core: + +* 1 expression former, and 1 case in each function over expressions; +* 2 step rules: `EAscribe T v` steps to `v`, and the congruence rule. The form is not a value, so each canonical forms lemma keeps 1 case for each type; +* 1 typing rule with 1 premise, which passes the region environment and the context through. It has no sibling, so it needs no side condition; +* 1 case in each proof by induction on an expression, a step or a typing derivation; +* the instantiated type as the annotation, because the calculus has no type variables (`inl` and `inr` have this gap already); +* the same former in the Agda source (D13) and in the Idris2 copy of the IR. + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended:* an ascription former in the P4 core, added with `TMu`, `fold` and `unfold` +|4 |4 +|The standard switch from type synthesis to type checking. It can later make the annotations of `inl` and `inr` unnecessary. It does not make `Box` different from `I32`. + +|Keep the annotated `let` +|3 |5 +|No new former and no proof work. Each constructor costs 1 administrative step and 1 wasm local, and the name of the binder carries the name of the constructor. + +|An ascription in the Rust core only, removed before the calculus +|3 |4 +|No extra step or local. The calculus does not change, and the Coq to Rust bridge gets 1 more erased form. + +|Unconventional: a nominal constructor form (each `data` type is a named type) +|4 |4 +|Also closes the case that this decision leaves open: a value that no constructor made passes as the `data` type (`f(5)` for `fn f(b: Box)`). It is the nominal option of D7, which was not ratified, so it needs the branch table of D7. +|=== + == Risks and kill criteria [cols="3,3,3",options="header"] diff --git a/src/ephapax-cli/tests/recursive_types.rs b/src/ephapax-cli/tests/recursive_types.rs index 3fa34bc..38cd5bc 100644 --- a/src/ephapax-cli/tests/recursive_types.rs +++ b/src/ephapax-cli/tests/recursive_types.rs @@ -529,22 +529,24 @@ fn data_types_that_refer_to_each_other_run() { ); } // A `Tree` is not a `Forest`, and a `Forest` is not a `Tree`: in a - // constructor of the folded type, and as an argument of a function. + // constructor of the folded type (`FCons`), and in a constructor of + // the type that is not folded (`Node`). let forest = "data Tree = Leaf | Node(I32, Forest)\n\n\ data Forest = FNil | FCons(Tree, Forest)\n\n\ fn size(t: Tree): I32 = match t of | Leaf => 0 | Node(v, kids) => v end\n\n"; - for (name, main) in [ + for (name, main, want) in [ ( "forest_as_tree", "match FCons(FNil, FNil) of | FNil => 0 | FCons(t, rest) => 1 end", + "Type mismatch", + ), + ( + "tree_as_forest", + "size(Node(1, Leaf))", + "constructor `Node`", ), - ("tree_as_forest", "size(Node(1, Leaf))"), ] { - check_refuses( - name, - &format!("{forest}fn main(): I32 = {main}\n"), - "Type mismatch", - ); + check_refuses(name, &format!("{forest}fn main(): I32 = {main}\n"), want); } } diff --git a/src/ephapax-cli/tests/run_wasm.rs b/src/ephapax-cli/tests/run_wasm.rs index 58314f9..4481d60 100644 --- a/src/ephapax-cli/tests/run_wasm.rs +++ b/src/ephapax-cli/tests/run_wasm.rs @@ -624,6 +624,91 @@ fn a_constructor_gets_its_type_arguments_from_its_use() { ); } +/// A constructor of a `data` type that is not recursive has the type that +/// the declaration gives. The check was missing: `MkBox(true)` passed for +/// `data Box = MkBox(I32)` until a use of the value as a `Box`. (A +/// constructor of a recursive type has the check from its `fold`.) +#[test] +fn a_constructor_checks_its_arguments_against_the_declaration() { + let tmp = tempfile::tempdir().expect("tempdir"); + let write = + |name: &str, text: &str| std::fs::write(tmp.path().join(name), text).expect("write module"); + let p = "data P(a) = P2(a, a) | Q(a)\n\n"; + + // (declarations, `main` body, text of the error) + for (decls, main, want) in [ + // 1 constructor: the value is the argument itself. + ( + "data Box = MkBox(I32)\n\n", + "match MkBox(true) of | MkBox(x) => if x then 1 else 2 end", + "constructor `MkBox`: the declaration gives Base(I32), \ + but the arguments give Base(Bool)", + ), + // 2 constructors: the argument of the first one. + ( + "data T = A(I32) | B(Bool)\n\n", + "match A(true) of | A(x) => if x then 1 else 2 | B(y) => 3 end", + "constructor `A`", + ), + // 1 type parameter in 2 fields: the 2 arguments have 1 type. + ( + p, + "match P2(1, true) of | P2(x, y) => x | Q(z) => 3 end", + "constructor `P2`", + ), + // The arguments of `P2` fix the type parameter for `Q` also. + ( + p, + "match P2(1, 2) of | P2(x, y) => x | Q(z) => if z then 1 else 0 end", + "Type mismatch", + ), + ] { + write( + "bad.eph", + &format!("module bad\n\n{decls}fn main(): I32 = {main}\n"), + ); + let out = ephapax(tmp.path(), &["check", "bad.eph"]); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + !out.status.success() && stderr.contains(want), + "{main}: exit {:?}, stderr:\n{stderr}", + out.status.code() + ); + } + + // Correct arguments run. (declarations, `main` type and body, output) + for (decls, main, want) in [ + // A generic function whose type parameter has the name of the + // parameter of the `data` type, and a value that is 64 bits wide. + ( + "data Opt(a) = No | Yes(a)\n\ndata W(a) = MkW(a)\n\n\ + fn wrap(x: a): Opt(a) = Yes(x)\n\n\ + fn keep(x: a): (a, Opt(I64)) = (x, No)\n\n\ + fn get(o: Opt(I64)): I64 =\n \ + match o of | No => 5000000000 - 5000000000 | Yes(n) => n end\n\n", + "I64 =\n let (b, o) = keep(true) in\n \ + match MkW(5000000000) of | MkW(v) => v + get(wrap(5000000000)) + get(o) end", + "10000000000i64", + ), + // A linear argument: the string is consumed 1 time. + ( + "data SBox = MkS(String@r) | Empty\n\n\ + fn len(b: SBox): I32 =\n match b of\n | Empty => 0\n \ + | MkS(s) => String.len(&s) + (let _ = drop(s) in 0)\n end\n\n", + "I32 = region r { len(MkS(String.new@r(\"hello\"))) + len(Empty) }", + "5", + ), + ] { + write( + "app.eph", + &format!("module app\n\n{decls}fn main(): {main}\n"), + ); + for args in [&["run", "app.eph"][..], &["run", "--interp", "app.eph"]] { + assert_eq!(stdout_of(tmp.path(), args), want, "{main} under {args:?}"); + } + } +} + /// 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 5fa8018..0ead134 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -1388,7 +1388,22 @@ impl Desugarer { span, ) } else { - value + // snip: an annotated `let` carries the check, because the core + // has no type ascription; upgrade to that core form when the + // calculus gets it (plan decision D14). + // The annotation is the declared type, so the type checker + // compares the arguments with the declaration. The binder + // names the constructor for the text of the error. + let name = SmolStr::new(format!("#{ctor}")); + Expr::new( + ExprKind::Let { + name: name.clone(), + ty: Some(quantify(ty, ¶ms)), + value: Box::new(value), + body: Box::new(Expr::new(ExprKind::Var(name), span)), + }, + span, + ) }) } @@ -2140,6 +2155,22 @@ mod tests { // --- Constructor desugaring --- + /// The injections of the constructor `ctor`: the value of the `let` + /// that carries the declared type ([`Desugarer::desugar_construct`]). + fn injections<'a>(core: &'a Expr, ctor: &str) -> &'a ExprKind { + let ExprKind::Let { + name, + ty: Some(_), + value, + .. + } = &core.kind + else { + panic!("expected a `let` with a type, got {:?}", core.kind); + }; + assert_eq!(name.as_str(), format!("#{ctor}")); + &value.kind + } + #[test] fn desugar_none_constructor() { let mut ds = Desugarer::new(); @@ -2152,7 +2183,7 @@ mod tests { let core = ds.desugar_expr(&expr).unwrap(); // None → inl(()) - assert!(matches!(core.kind, ExprKind::Inl { .. })); + assert!(matches!(injections(&core, "None"), ExprKind::Inl { .. })); } #[test] @@ -2167,7 +2198,7 @@ mod tests { let core = ds.desugar_expr(&expr).unwrap(); // Some(42) → inr(42) - assert!(matches!(core.kind, ExprKind::Inr { .. })); + assert!(matches!(injections(&core, "Some"), ExprKind::Inr { .. })); } #[test] @@ -2182,7 +2213,7 @@ mod tests { let core = ds.desugar_expr(&expr).unwrap(); // Green → inr(inl(())) - if let ExprKind::Inr { value, .. } = &core.kind { + if let ExprKind::Inr { value, .. } = injections(&core, "Green") { assert!(matches!(value.kind, ExprKind::Inl { .. })); } else { panic!("expected inr"); @@ -2201,7 +2232,7 @@ mod tests { let core = ds.desugar_expr(&expr).unwrap(); // Blue → inr(inr(())) - if let ExprKind::Inr { value, .. } = &core.kind { + if let ExprKind::Inr { value, .. } = injections(&core, "Blue") { if let ExprKind::Inr { .. } = &value.kind { // Correct: inr(inr(...)) } else { diff --git a/src/ephapax-typing/src/lib.rs b/src/ephapax-typing/src/lib.rs index e55c7f9..e8d21ab 100644 --- a/src/ephapax-typing/src/lib.rs +++ b/src/ephapax-typing/src/lib.rs @@ -80,6 +80,17 @@ pub enum TypeError { #[error("Type annotation mismatch: declared {declared:?}, but value has type {actual:?}")] AnnotationMismatch { declared: Ty, actual: Ty }, + /// The arguments of a constructor do not give the type that the + /// declaration of its `data` type gives. + #[error( + "constructor `{ctor}`: the declaration gives {declared:?}, but the arguments give {actual:?}" + )] + ConstructorMismatch { + ctor: String, + declared: Ty, + actual: Ty, + }, + #[error("Not yet supported in the core type checker: {0}. Use the surface (parse_surface_module → desugar) path instead.")] NotYetSupportedInCore(&'static str), @@ -1421,17 +1432,27 @@ impl TypeChecker { let value_ty = self.check(value)?; if let Some(declared) = ty_ann { + // The desugarer gives a constructor the binder `#` and + // the declared type of its `data` type, which binds the type + // parameters. A written annotation binds none. + let declared = &self.instantiate(declared.clone()).0; self.unify(s, declared, &value_ty).map_err(|error| { if matches!(error.error, TypeError::LinearPatternDiscard(_)) { return error; } - self.at( - s, - TypeError::AnnotationMismatch { + let actual = self.resolve(&value_ty); + let error = match name.strip_prefix('#') { + Some(ctor) => TypeError::ConstructorMismatch { + ctor: ctor.into(), + declared: self.resolve(declared), + actual, + }, + None => TypeError::AnnotationMismatch { declared: declared.clone(), - actual: self.resolve(&value_ty), + actual, }, - ) + }; + self.at(s, error) })?; } diff --git a/src/ephapax-wasm/src/lib.rs b/src/ephapax-wasm/src/lib.rs index 3d46b27..f8ddaff 100644 --- a/src/ephapax-wasm/src/lib.rs +++ b/src/ephapax-wasm/src/lib.rs @@ -2531,7 +2531,10 @@ impl Codegen { body: &Expr, is_linear: bool, ) { + // The annotation of a constructor binds type parameters + // (`forall`): the type table has the type of its value. let local_ty = ty + .filter(|ty| !matches!(ty, Ty::ForAll { .. })) .map(ty_to_valtype) .unwrap_or_else(|| self.valtype_of(value));