Iter 12c: docs for polymorphism

DESIGN.md:
- "What is not (yet) supported" updated for end-of-Iter-12 boundary:
  parameterised ADTs replace HM-inside-bodies as the headline gap;
  polymorphism limitations (direct-call-only, no higher-rank) are
  spelled out so future me doesn't trip over them.
- "What is supported" gains the polymorphism + monomorphisation
  bullet, with the descriptor scheme written out.
- Smoke-test list extended with poly_id and poly_apply.

JOURNAL.md: Iter 12a/b retrospective. Notes the metavar-encoding
choice (Type::Var{name:"$m<n>"} vs new variant) and why the
codegen-side type tracker was preferable to a typechecker
sidetable for now. Architecture self-check confirms the language
is now usable for poly-flavoured programs over primitives. Plan 13:
parameterised ADTs as the natural next step (without them, generic
map remains hand-monomorphised).

Iter 12c was originally to include a polymorphic map rewrite —
dropped because parameterised ADTs are the prerequisite. The two
new examples (poly_id, poly_apply, both already in 12b) cover the
real e2e proof.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

docs/DESIGN.md

@@ -244,15 +244,25 @@ ail run <module>                 — build + execute (tempdir), passthrough exit
 
 ## What is not (yet) supported
 
-Snapshot of the boundary at the end of Iter 8. Items move out of this list
+Snapshot of the boundary at the end of Iter 12. 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 polymorphism in inference. `Type::Forall` is parseable but the
-  typechecker rejects polymorphic uses inside a body (`PolymorphicNot
-  Supported`). Generic functions must be monomorphised by the author
-  via separate top-level defs.
+- 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.
+- Polymorphic fns must be **directly called** at the use site.
+  Passing a polymorphic fn as a value (`let f = id in f(42)`) is
+  not yet supported — it would need one closure-pair global per
+  instantiation, deferred.
+- No higher-rank polymorphism. Passing a polymorphic fn to another
+  polymorphic fn (`apply(id, 42)`) is not supported.
 - No cross-module ADTs. ADTs are local to a module; ctor names must be
   unique within their module but may collide across modules.
 - No visibility rules in imports. Every top-level def of an imported module
@@ -279,6 +289,12 @@ What **is** supported (and used as the smoke test for the pipeline):
   closure pair `{ thunk_ptr, env_ptr }`. Top-level fns get an auto-
   generated adapter and a static closure pair (env = null) so they
   remain passable as values without heap overhead.
+- **Polymorphism via `Type::Forall`** at top-level def types (Iter 12).
+  Use sites instantiate fresh metavars; unification pins them against
+  the concrete types of the call args. Codegen monomorphises on
+  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)`).
 
 Pipeline regression smoke tests:
 
@@ -290,3 +306,7 @@ Pipeline regression smoke tests:
   HOF + IO; the dogfood smoke test).
 - `examples/sort.ail.json` → prints sorted [3,1,4,1,5,9,2,6,5,3,5]
   one-per-line (insertion sort over an 11-element list).
+- `examples/poly_id.ail.json` → prints 42 then "true" (polymorphic
+  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)`).