Iter 13a: parameterised ADT schema + checker

Adds type parameters to ADTs. `TypeDef` gets a `vars: Vec<String>` and
`Type::Con` gets an `args: Vec<Type>`, both `skip_serializing_if =
"Vec::is_empty"` so canonical-JSON hashes of every pre-13a definition
stay bit-identical (regression test in `hash::tests`).

Checker:
- `check_type_def` installs `td.vars` as rigid vars while validating
  ctor field types — `Cons(a, List a)` now resolves both occurrences
  of `a` and the recursive `List a` use.
- `check_type_well_formed` accepts `Type::Con { name, args }` only
  when the type is in scope and `args.len()` matches its declared
  arity; primitives stay zero-arg.
- `Term::Ctor` synth instantiates `td.vars` with fresh metavars, so
  `MkBox(42)` synthesises to `Box<$m0>` and unifies field types
  through the surrounding context.
- `type_check_pattern` substitutes the scrutinee's concrete type-args
  through ctor field types, so a `MkBox(x)` arm against a `Box<Int>`
  scrutinee binds `x : Int`.
- `check_fn` validates declared param/return types via
  `check_type_well_formed` so arity mismatches on parameterised
  ADTs surface before the body is checked.

`unify`, `occurs`, `Subst::apply`, `substitute_rigids`, and codegen's
`unify_for_subst` / `apply_subst_to_type` recurse into `args`.

Pretty-print:
- `type_to_string` renders `Box<Int>` for parameterised cons.
- `def_block`/`manifest` carry the `[a b ...]` vars list.

Three new check unit tests cover ctor instantiation at a concrete
arg, the polymorphic-`unbox` round trip at two distinct
instantiations, and arity mismatch on `Box<Int, Bool>`. All 62 tests
green; clippy clean (two pre-existing warnings untouched). Hashes
db33f57cb329935e (sum) and b082192bd0c99202 (IntList) verified
unchanged.

Codegen still synthesises `Type::Con` with `args: vec![]` from
`Term::Ctor` — full ADT monomorphisation lands in 13b.

crates/ailang-codegen/src/lib.rs

@@ -217,7 +217,7 @@ fn main_is_void(t: &Type) -> bool {
     match t {
         Type::Fn { params, ret, .. } => {
             params.is_empty()
-                && matches!(ret.as_ref(), Type::Con { name } if name == "Unit")
+                && matches!(ret.as_ref(), Type::Con { name, .. } if name == "Unit")
         }
         _ => false,
     }
@@ -1881,6 +1881,7 @@ impl<'a> Emitter<'a> {
             }),
             Term::Ctor { type_name, .. } => Ok(Type::Con {
                 name: type_name.clone(),
+                args: vec![],
             }),
             Term::Match { arms, .. } => {
                 if let Some(first) = arms.first() {
@@ -1898,7 +1899,7 @@ impl<'a> Emitter<'a> {
 
 fn llvm_type(t: &Type) -> Result<String> {
     match t {
-        Type::Con { name } => match name.as_str() {
+        Type::Con { name, .. } => match name.as_str() {
             "Int" => Ok("i64".into()),
             "Bool" => Ok("i1".into()),
             "Unit" => Ok("i8".into()),
@@ -2031,7 +2032,15 @@ fn unify_for_subst(
             subst.insert(name.clone(), arg.clone());
             Ok(())
         }
-        (Type::Con { name: pn }, Type::Con { name: an }) if pn == an => Ok(()),
+        (
+            Type::Con { name: pn, args: pa },
+            Type::Con { name: an, args: aa },
+        ) if pn == an && pa.len() == aa.len() => {
+            for (p, a) in pa.iter().zip(aa.iter()) {
+                unify_for_subst(p, a, vars, subst)?;
+            }
+            Ok(())
+        }
         (
             Type::Fn { params: pp, ret: pr, .. },
             Type::Fn { params: ap, ret: ar, .. },
@@ -2061,7 +2070,10 @@ fn unify_for_subst(
 fn apply_subst_to_type(t: &Type, subst: &BTreeMap<String, Type>) -> Type {
     match t {
         Type::Var { name } => subst.get(name).cloned().unwrap_or_else(|| t.clone()),
-        Type::Con { .. } => t.clone(),
+        Type::Con { name, args } => Type::Con {
+            name: name.clone(),
+            args: args.iter().map(|a| apply_subst_to_type(a, subst)).collect(),
+        },
         Type::Fn { params, ret, effects } => Type::Fn {
             params: params.iter().map(|p| apply_subst_to_type(p, subst)).collect(),
             ret: Box::new(apply_subst_to_type(ret, subst)),
@@ -2159,13 +2171,27 @@ fn descriptor_for_subst(vars: &[String], subst: &BTreeMap<String, Type>) -> Stri
 /// the MVP are non-recursive at the type level).
 fn type_descriptor(t: &Type) -> String {
     match t {
-        Type::Con { name } => match name.as_str() {
-            "Int" => "I".into(),
-            "Bool" => "B".into(),
-            "Unit" => "U".into(),
-            "Str" => "S".into(),
-            other => format!("F{other}"),
-        },
+        Type::Con { name, args } => {
+            let head = match name.as_str() {
+                "Int" => "I".into(),
+                "Bool" => "B".into(),
+                "Unit" => "U".into(),
+                "Str" => "S".into(),
+                other => format!("F{other}"),
+            };
+            if args.is_empty() {
+                head
+            } else {
+                // Iter 13a: parameterised ADTs get their type-arg
+                // descriptors appended, e.g. `FBox` of `Int` → `FBox_I`.
+                let mut s = head;
+                for a in args {
+                    s.push('_');
+                    s.push_str(&type_descriptor(a));
+                }
+                s
+            }
+        }
         Type::Fn { params, ret, .. } => {
             let mut s = String::from("Fn");
             for p in params {