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