fix(desugar): a constructor gets its type arguments from its use

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

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<T>(): 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`;

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<Option<(Vec<SmolStr>, 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<SmolStr>, 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, &params, 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, &params),
                     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

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<Ty, SpannedTypeError> {
         let value_ty = self.check(value)?;
         let (ty, _) = self.instantiate(ty.clone());