Iter 13b: codegen for parameterised ADTs

Closes the gap between Iter 13a (parameterised ADTs in the
checker) and end-to-end execution. ADT ctor code stays inlined at
every use site — no mono-queue for types, no new symbols — but
LLVM field types are now derived per use site via substitution.

`CtorRef` gains `type_vars: Vec<String>` so use sites can identify
which fields reference rigid vars. `cref.fields` (precomputed
LLVM strings) is documented as monomorphic-only and read past for
parameterised ADTs.

`lower_ctor`: derives a `BTreeMap<String, Type>` substitution from
`synth_arg_type` of each arg via `unify_for_subst`, then maps every
`ail_field` through `apply_subst_to_type` + `llvm_type` for the
per-store types. Monomorphic ADTs hit the original fast path.

`lower_match`: builds `arm_subst` from `s_ail.args` ↔ `cref.type_vars`,
substitutes through each `cref.ail_fields[idx]`, and uses the
substituted type both for the LLVM `load` AND as the AILang slot
of the local — so a downstream `unbox(b)` sees `b: Int`, not
`b: a`.

`synth_arg_type` for `Term::Ctor`: returns concrete type-args
derived from the ctor's term-args. Vars left unpinned (e.g. `None`
for `Maybe a`) fall back to `Type::unit()`.

`llvm_type(Type::Var)` now hard-errors. Earlier this silently
fell through to `ptr` (the ADT-via-ptr fallback), producing
garbage IR. Failing loudly here surfaces missed substitutions in
the test suite.

Two e2e tests (`box.ail.json`, `maybe_int.ail.json`) cover ctor
lower with substituted field types and match-arm field
substitution. 64 tests green; clippy clean (two pre-existing
warnings untouched). Hash invariant holds.

Out of scope per agent assignment: poly-fn-as-value, higher-rank
polymorphism, DESIGN/JOURNAL updates (deferred to 13c).

crates/ail/tests/e2e.rs

@@ -128,6 +128,29 @@ fn polymorphic_apply_with_fn_param() {
     assert_eq!(stdout.trim(), "42");
 }
 
+/// Iter 13b: round-trip a primitive through a parameterised ADT and a
+/// polymorphic-fn boundary. `type Box[a] = MkBox(a)` plus
+/// `unbox : forall a. (Box<a>) -> a` plus `print_int(unbox(MkBox(42)))`.
+/// Guards: ctor lower with substituted LLVM field types,
+/// match-arm field bindings carrying the substituted AILang type
+/// down into a polymorphic fn body.
+#[test]
+fn parameterised_box_round_trip() {
+    let stdout = build_and_run("box.ail.json");
+    assert_eq!(stdout.trim(), "42");
+}
+
+/// Iter 13b: pattern-match on `Maybe<Int>`. `or_else(Some(7), 99) == 7`
+/// then `or_else(None, 99) == 99`. Guards: match-arm field
+/// substitution at a parameterised ctor (the `Some(x)` arm must bind
+/// `x : Int`, not `x : a`).
+#[test]
+fn parameterised_maybe_match() {
+    let stdout = build_and_run("maybe_int.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["7", "99"]);
+}
+
 /// Guards `ail diff`: a modified body changes the hash of `sum`, while
 /// `main` stays unchanged. Expects exit code 1, `changed` contains exactly
 /// `sum`, `unchanged` contains `main`, `added`/`removed` empty.

crates/ailang-codegen/src/lib.rs

@@ -296,10 +296,24 @@ struct CtorInfo {
 struct CtorRef {
     type_name: String,
     tag: u32,
+    /// Precomputed LLVM field types. Valid only for monomorphic ADTs
+    /// (`type_vars.is_empty()`). For parameterised ADTs the entries are
+    /// meaningless (free `Type::Var` lowers via the `_ => ptr` fallback)
+    /// and must be re-derived per use site after substituting through
+    /// `ail_fields`.
     fields: Vec<String>,
-    /// AILang-level field types (parallel to `fields`). Needed for
-    /// codegen-side type tracking — match field bindings inherit these.
+    /// AILang-level field types (parallel to `fields`). Carries
+    /// `Type::Var` references for parameterised ADTs (Iter 13b); these
+    /// are substituted at every ctor / match-arm use site.
     ail_fields: Vec<Type>,
+    /// Iter 13b: type parameters of the owning TypeDef, in declaration
+    /// order. Empty for monomorphic ADTs (`type IntList = ...`); non-
+    /// empty for parameterised ADTs (`type Box[a] = MkBox(a)` →
+    /// `["a"]`). Used as the var-set for `unify_for_subst` when deriving
+    /// substitutions at a use site, and to map type-args
+    /// (`Type::Con.args[i]`) back to the right var when lowering match
+    /// arms against a parameterised scrutinee.
+    type_vars: Vec<String>,
 }
 
 #[derive(Debug, Clone)]
@@ -323,10 +337,19 @@ impl<'a> Emitter<'a> {
             if let Def::Type(td) = def {
                 let mut infos = Vec::new();
                 for (i, c) in td.ctors.iter().enumerate() {
+                    // Iter 13b: precomputed LLVM field types are only
+                    // meaningful for monomorphic ADTs. For parameterised
+                    // ADTs the field types reference free `Type::Var`s
+                    // and must be derived per use site after
+                    // substituting; we still populate the slot with
+                    // `i64`/`ptr` placeholders so the index shape stays
+                    // uniform, but neither `lower_ctor` nor
+                    // `lower_match` reads from it when `type_vars` is
+                    // non-empty.
                     let fields: Vec<String> = c
                         .fields
                         .iter()
-                        .map(|t| llvm_type(t).unwrap_or_else(|_| "i64".into()))
+                        .map(|t| llvm_type(t).unwrap_or_else(|_| "ptr".into()))
                         .collect();
                     infos.push(CtorInfo {
                         name: c.name.clone(),
@@ -339,6 +362,7 @@ impl<'a> Emitter<'a> {
                             tag: i as u32,
                             fields,
                             ail_fields: c.fields.clone(),
+                            type_vars: td.vars.clone(),
                         },
                     );
                 }
@@ -813,15 +837,39 @@ impl<'a> Emitter<'a> {
                 cref.type_name
             )));
         }
-        if args.len() != cref.fields.len() {
+        if args.len() != cref.ail_fields.len() {
             return Err(CodegenError::Internal(format!(
                 "ctor `{type_name}/{ctor_name}` arity"
             )));
         }
+        // Iter 13b: for parameterised ADTs the precomputed `cref.fields`
+        // is meaningless because field types reference rigid type vars.
+        // Derive a per-use-site substitution from the arg types and
+        // re-lower each field type. Monomorphic ADTs hit the fast path
+        // (no var-set, substitution is empty, ail_fields lower exactly
+        // like cref.fields).
+        let expected_llvm_tys: Vec<String> = if cref.type_vars.is_empty() {
+            cref.fields.clone()
+        } else {
+            let arg_ail_tys: Vec<Type> = args
+                .iter()
+                .map(|a| self.synth_arg_type(a))
+                .collect::<Result<_>>()?;
+            let var_set: BTreeSet<&str> =
+                cref.type_vars.iter().map(|s| s.as_str()).collect();
+            let mut subst: BTreeMap<String, Type> = BTreeMap::new();
+            for (exp, actual) in cref.ail_fields.iter().zip(arg_ail_tys.iter()) {
+                unify_for_subst(exp, actual, &var_set, &mut subst)?;
+            }
+            cref.ail_fields
+                .iter()
+                .map(|f| llvm_type(&apply_subst_to_type(f, &subst)))
+                .collect::<Result<_>>()?
+        };
         // Evaluate arguments up front so allocation and store stay close
         // together.
         let mut compiled = Vec::new();
-        for (a, exp) in args.iter().zip(cref.fields.iter()) {
+        for (a, exp) in args.iter().zip(expected_llvm_tys.iter()) {
             let (v, vty) = self.lower_term(a)?;
             if &vty != exp {
                 return Err(CodegenError::Internal(format!(
@@ -935,12 +983,45 @@ impl<'a> Emitter<'a> {
 
         for (i, (cref, arm, bindings)) in ctor_arms.iter().enumerate() {
             self.start_block(&arm_labels[i]);
+            // Iter 13b: derive substitution for parameterised ADTs from
+            // the scrutinee's concrete type-args. Map `cref.type_vars[i]`
+            // → `s_ail.args[i]`. For monomorphic ADTs the mapping is
+            // empty and substitution is a no-op. The substituted AILang
+            // types are used both for the LLVM `load` instruction and as
+            // the AILang-type slot of the local — without the latter, a
+            // downstream `unbox(b)` would see `b: a` (rigid var) instead
+            // of `b: Int`.
+            let arm_subst: BTreeMap<String, Type> = if cref.type_vars.is_empty() {
+                BTreeMap::new()
+            } else {
+                match &s_ail {
+                    Type::Con { args, .. } if args.len() == cref.type_vars.len() => cref
+                        .type_vars
+                        .iter()
+                        .cloned()
+                        .zip(args.iter().cloned())
+                        .collect(),
+                    _ => {
+                        return Err(CodegenError::Internal(format!(
+                            "match: scrutinee type `{}` not aligned with ctor `{}`'s {} type vars",
+                            ailang_core::pretty::type_to_string(&s_ail),
+                            cref.type_name,
+                            cref.type_vars.len(),
+                        )));
+                    }
+                }
+            };
             // Load fields and bind as locals.
             let mut pushed = 0usize;
-            for (idx, (binding, fty)) in
-                bindings.iter().zip(cref.fields.iter()).enumerate()
-            {
+            for (idx, binding) in bindings.iter().enumerate() {
                 if let Some(bname) = binding {
+                    let raw_ail = cref.ail_fields.get(idx).cloned().unwrap_or(Type::unit());
+                    let bind_ail = if arm_subst.is_empty() {
+                        raw_ail
+                    } else {
+                        apply_subst_to_type(&raw_ail, &arm_subst)
+                    };
+                    let fty = llvm_type(&bind_ail)?;
                     let off = 8 + idx as i64 * 8;
                     let addr = self.fresh_ssa();
                     self.body.push_str(&format!(
@@ -950,9 +1031,7 @@ impl<'a> Emitter<'a> {
                     self.body.push_str(&format!(
                         "  {v} = load {fty}, ptr {addr}, align 8\n"
                     ));
-                    let fail_ail = cref.ail_fields.get(idx).cloned().unwrap_or(Type::unit());
-                    self.locals
-                        .push((bname.clone(), v, fty.clone(), fail_ail));
+                    self.locals.push((bname.clone(), v, fty, bind_ail));
                     pushed += 1;
                 }
             }
@@ -1879,10 +1958,51 @@ impl<'a> Emitter<'a> {
                     "synth_arg_type: unknown effect op `{op}`"
                 ))
             }),
-            Term::Ctor { type_name, .. } => Ok(Type::Con {
-                name: type_name.clone(),
-                args: vec![],
-            }),
+            Term::Ctor { type_name, ctor, args } => {
+                // Iter 13b: derive concrete type-args of a parameterised
+                // ADT instance from the recursively-synthesised arg
+                // types. For monomorphic ADTs (`type_vars.is_empty()`)
+                // we keep the pre-13b shape `Type::Con { args: vec![] }`
+                // — matching what the typechecker produces.
+                let cref = self.ctor_index.get(ctor).cloned().ok_or_else(|| {
+                    CodegenError::Internal(format!(
+                        "synth_arg_type: unknown ctor `{ctor}`"
+                    ))
+                })?;
+                if cref.type_vars.is_empty() {
+                    return Ok(Type::Con {
+                        name: type_name.clone(),
+                        args: vec![],
+                    });
+                }
+                let arg_tys: Vec<Type> = args
+                    .iter()
+                    .map(|a| self.synth_with_extras(a, extras))
+                    .collect::<Result<_>>()?;
+                let var_set: BTreeSet<&str> =
+                    cref.type_vars.iter().map(|s| s.as_str()).collect();
+                let mut subst: BTreeMap<String, Type> = BTreeMap::new();
+                for (exp, actual) in cref.ail_fields.iter().zip(arg_tys.iter()) {
+                    unify_for_subst(exp, actual, &var_set, &mut subst)?;
+                }
+                // Vars not pinned by ctor args (e.g. `None` for
+                // `Maybe a`) are filled with `Type::unit()` as a
+                // placeholder. That's harmless for monomorphic call
+                // sites — codegen never instantiates a polymorphic fn
+                // off this un-pinned shape because the typechecker
+                // would have rejected an under-determined call —
+                // and keeps the function total for the well-formed
+                // ones (e.g. `Some(7)` pins `a` from the arg).
+                let resolved: Vec<Type> = cref
+                    .type_vars
+                    .iter()
+                    .map(|v| subst.get(v).cloned().unwrap_or_else(Type::unit))
+                    .collect();
+                Ok(Type::Con {
+                    name: type_name.clone(),
+                    args: resolved,
+                })
+            }
             Term::Match { arms, .. } => {
                 if let Some(first) = arms.first() {
                     self.synth_with_extras(&first.body, extras)
@@ -1913,6 +2033,13 @@ fn llvm_type(t: &Type) -> Result<String> {
         // at the LLVM level. The actual signature travels via the
         // emitter's `ssa_fn_sigs` sidetable.
         Type::Fn { .. } => Ok("ptr".into()),
+        // Iter 13b: an unresolved rigid `Type::Var` reaching codegen is
+        // a substitution bug. Earlier this silently lowered as `ptr`
+        // (via the ADT fallback) and produced garbage IR; failing loudly
+        // here surfaces the bug in the test suite.
+        Type::Var { name } => Err(CodegenError::UnsupportedType(format!(
+            "unresolved type var `{name}` in codegen"
+        ))),
         other => Err(CodegenError::UnsupportedType(
             ailang_core::pretty::type_to_string(other),
         )),

examples/box.ail.json

@@ -0,0 +1,87 @@
+{
+  "schema": "ailang/v0",
+  "name": "box",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "type",
+      "name": "Box",
+      "vars": ["a"],
+      "doc": "A unary box around a polymorphic value.",
+      "ctors": [
+        {
+          "name": "MkBox",
+          "fields": [{ "k": "var", "name": "a" }]
+        }
+      ]
+    },
+    {
+      "kind": "fn",
+      "name": "unbox",
+      "type": {
+        "k": "forall",
+        "vars": ["a"],
+        "body": {
+          "k": "fn",
+          "params": [
+            {
+              "k": "con",
+              "name": "Box",
+              "args": [{ "k": "var", "name": "a" }]
+            }
+          ],
+          "ret": { "k": "var", "name": "a" },
+          "effects": []
+        }
+      },
+      "params": ["b"],
+      "doc": "Polymorphic projection out of a Box.",
+      "body": {
+        "t": "match",
+        "scrutinee": { "t": "var", "name": "b" },
+        "arms": [
+          {
+            "pat": {
+              "p": "ctor",
+              "ctor": "MkBox",
+              "fields": [{ "p": "var", "name": "x" }]
+            },
+            "body": { "t": "var", "name": "x" }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "doc": "Round-trip 42 through MkBox + unbox.",
+      "body": {
+        "t": "do",
+        "op": "io/print_int",
+        "args": [
+          {
+            "t": "app",
+            "fn": { "t": "var", "name": "unbox" },
+            "args": [
+              {
+                "t": "ctor",
+                "type": "Box",
+                "ctor": "MkBox",
+                "args": [
+                  { "t": "lit", "lit": { "kind": "int", "value": 42 } }
+                ]
+              }
+            ]
+          }
+        ]
+      }
+    }
+  ]
+}

examples/maybe_int.ail.json

@@ -0,0 +1,112 @@
+{
+  "schema": "ailang/v0",
+  "name": "maybe_int",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "type",
+      "name": "Maybe",
+      "vars": ["a"],
+      "doc": "Optional value with a polymorphic payload.",
+      "ctors": [
+        { "name": "None", "fields": [] },
+        {
+          "name": "Some",
+          "fields": [{ "k": "var", "name": "a" }]
+        }
+      ]
+    },
+    {
+      "kind": "fn",
+      "name": "or_else",
+      "type": {
+        "k": "fn",
+        "params": [
+          {
+            "k": "con",
+            "name": "Maybe",
+            "args": [{ "k": "con", "name": "Int" }]
+          },
+          { "k": "con", "name": "Int" }
+        ],
+        "ret": { "k": "con", "name": "Int" },
+        "effects": []
+      },
+      "params": ["m", "d"],
+      "doc": "Returns the wrapped Int for Some(x) and the default d for None.",
+      "body": {
+        "t": "match",
+        "scrutinee": { "t": "var", "name": "m" },
+        "arms": [
+          {
+            "pat": { "p": "ctor", "ctor": "None", "fields": [] },
+            "body": { "t": "var", "name": "d" }
+          },
+          {
+            "pat": {
+              "p": "ctor",
+              "ctor": "Some",
+              "fields": [{ "p": "var", "name": "x" }]
+            },
+            "body": { "t": "var", "name": "x" }
+          }
+        ]
+      }
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Unit" },
+        "effects": ["IO"]
+      },
+      "params": [],
+      "doc": "Print or_else for both arms; expected 7 then 99.",
+      "body": {
+        "t": "seq",
+        "lhs": {
+          "t": "do",
+          "op": "io/print_int",
+          "args": [
+            {
+              "t": "app",
+              "fn": { "t": "var", "name": "or_else" },
+              "args": [
+                {
+                  "t": "ctor",
+                  "type": "Maybe",
+                  "ctor": "Some",
+                  "args": [
+                    { "t": "lit", "lit": { "kind": "int", "value": 7 } }
+                  ]
+                },
+                { "t": "lit", "lit": { "kind": "int", "value": 99 } }
+              ]
+            }
+          ]
+        },
+        "rhs": {
+          "t": "do",
+          "op": "io/print_int",
+          "args": [
+            {
+              "t": "app",
+              "fn": { "t": "var", "name": "or_else" },
+              "args": [
+                {
+                  "t": "ctor",
+                  "type": "Maybe",
+                  "ctor": "None",
+                  "args": []
+                },
+                { "t": "lit", "lit": { "kind": "int", "value": 99 } }
+              ]
+            }
+          ]
+        }
+      }
+    }
+  ]
+}