fix: a constructor checks its arguments against the declaration

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

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"]

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

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<a>(x: a): Opt(a) = Yes(x)\n\n\
+             fn keep<a>(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`;

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, &params)),
+                    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 {

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 `#<name>` 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)
             })?;
         }
 

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));