Iter 13c: docs for parameterised ADTs

DESIGN.md: removes "No parameterised ADTs" from the gap list,
adds an entry under "what is supported" that names the per-use-
site substitution scheme and the `llvm_type(Type::Var)` hard-error
defence. Smoke-test list extended with `box.ail.json` and
`maybe_int.ail.json`. Boundary snapshot moved from "end of Iter 12"
to "end of Iter 13".

JOURNAL.md: single Iter 13 entry covering 13a/b/c. Records the
hash-invariant regression test, the architect-flagged debt I
deliberately did not touch (poly-fn-as-value asymmetry, builtins
triple-source, `synth_arg_type` shortcuts on If/Match), the
KISS observation that 13b's "no mono-queue for types" was the
right call, and the process note that this was the first iter
worked strictly through `/agents/` after the role pin in 3df943d.
Plan iteration 14 queued: list_map-as-`List a` rewrite, GC/arena,
poly-fn-as-value.

docs/DESIGN.md

@@ -244,16 +244,11 @@ ail run <module>                 — build + execute (tempdir), passthrough exit
 
 ## What is not (yet) supported
 
-Snapshot of the boundary at the end of Iter 12. Items move out of this list
+Snapshot of the boundary at the end of Iter 13. Items move out of this list
 as iterations land; the JOURNAL records the exact iteration.
 
 - No effect handlers — only the built-in IO and Diverge ops.
 - No refinements / SMT escalation.
-- No parameterised ADTs. `List a` / `Maybe a` aren't expressible —
-  ADTs are concrete (`IntList`, `Maybe_Int`, ...). Polymorphism over
-  primitives and fn-typed values works, but a generic `map :: forall
-  a b. ((a) -> b, List a) -> List b` is blocked on this. Queued
-  next.
 - No HM inference inside bodies. Top-level def types are explicit;
   polymorphism is opt-in via `Type::Forall { vars, body }`. Inside
   a body, lambdas check monomorphically against their declared type.
@@ -295,6 +290,18 @@ What **is** supported (and used as the smoke test for the pipeline):
   demand: each unique instantiation emits a specialised LLVM fn
   mangled `@ail_<m>_<def>__<descriptor>` (e.g. `id__I` for `id` at
   `Int`, `apply__I_I` for `apply` at `(Int, Int)`).
+- **Parameterised ADTs** (Iter 13). `TypeDef.vars: Vec<String>`
+  declares type parameters; `Type::Con.args: Vec<Type>` carries the
+  type arguments at use sites. Both fields default to empty and are
+  skipped during serialization, so canonical-JSON hashes of every
+  pre-13a definition stay bit-identical (regression test in
+  `crates/ailang-core/src/hash.rs`). Ctor and match codegen stay
+  inline at every use site — there is no specialised ADT symbol —
+  but LLVM field types are derived per use site by substituting
+  through `cdef.ail_fields`. The substitution is read off the call's
+  arg types (ctor) or the scrutinee's `Type::Con.args` (match). An
+  unresolved `Type::Var` reaching `llvm_type` is a hard error
+  rather than a silent fallback to `ptr`.
 
 Pipeline regression smoke tests:
 
@@ -310,3 +317,9 @@ Pipeline regression smoke tests:
   identity at `Int` and `Bool`; two specialised fns emitted).
 - `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply`
   with a fn-typed parameter; `apply(succ, 41)`).
+- `examples/box.ail.json` → prints 42 (parameterised ADT round-
+  trip: `MkBox(42)` constructed, then projected by a polymorphic
+  `unbox : forall a. (Box<a>) -> a` and printed).
+- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
+  over `Maybe<Int>`: `or_else(Some(7), 99)` then
+  `or_else(None, 99)`).