Iter 8c: docs (DESIGN.md + JOURNAL.md)

DESIGN.md:
- Term schema: add `ctor`, `match`, `lam` rows. The schema fragment is
  now exhaustive for the supported language; prior versions silently
  dropped Iter 3/Iter 8 additions.
- "What is not (yet) supported": closures-with-capture moves out of
  pending. New positive bullet for anonymous lambdas. Polymorphism
  added as an explicit pending bullet (Forall is parseable but not
  inferred). Smoke-test list extended with closure.ail.json.

JOURNAL: append Iter 8 entry covering both 8a (closure-pair ABI) and
8b (Term::Lam + capture). Includes the rationale for skipping TIR
(KISS won — `synth` already provides enough type info), the closure-
conversion sketch, hash stability check (existing examples produce
the same fn hashes pre vs post Iter 8), and the Iter 9 plan with
two candidates ranked.

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

docs/DESIGN.md

@@ -178,9 +178,20 @@ hashes stay bit-identical.
 { "t": "let", "name": "<id>", "value": Term, "body": Term }
 { "t": "if", "cond": Term, "then": Term, "else": Term }
 { "t": "do", "op": "<eff>/<op>", "args": [Term...] }
+{ "t": "ctor", "type": "<id>", "ctor": "<id>", "args": [Term...] }
+{ "t": "match", "scrutinee": Term, "arms": [Arm...] }
+{ "t": "lam",
+  "params": ["<id>"...],
+  "paramTypes": [Type...],
+  "retType": Type,
+  "effects": ["<id>"...],
+  "body": Term }
 ```
 
 In the MVP, `do` is only a direct call to a built-in effect op (no handler).
+A `lam` term constructs an anonymous function value; free variables of
+its body are captured from the enclosing scope (see Iter 8 closure
+conversion in JOURNAL).
 
 ### Type
 
@@ -229,21 +240,22 @@ ail build <module>               — full pipeline → binary
 
 ## What is not (yet) supported
 
-Snapshot of the boundary at the end of Iter 7. Items move out of this list
+Snapshot of the boundary at the end of Iter 8. Items move out of this list
 as iterations land; the JOURNAL records the exact iteration.
 
-- No closures with capture / no anonymous lambdas. Both will require a
-  typed IR stage (TIR) and closure conversion in lowering. First-class
-  function references (top-level fns as values, fn-typed parameters,
-  indirect calls) **are** supported as of Iter 7 — see below.
 - 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 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
   is reachable; there is no `pub` / `priv`.
-- No GC. The `Ctor` heap layout leaks. Acceptable for current example
-  programs; required before any longer-running program.
+- No GC. ADT boxes, lambda envs, and closure pairs all leak. Acceptable
+  for current example programs; required before any longer-running
+  program.
 
 What **is** supported (and used as the smoke test for the pipeline):
 
@@ -256,13 +268,17 @@ What **is** supported (and used as the smoke test for the pipeline):
 - **Imports + qualified cross-module references** via dotted names
   (Iter 5).
 - **First-class function references** (Iter 7). A top-level fn name (or
-  qualified `prefix.def`) used as a `Term::Var` is a fn-pointer value of
-  AILang type `Type::Fn { ... }` and LLVM type `ptr`. Fn-typed parameters
-  may be called directly as `f(args)`. No capture, no lambdas — the only
-  way to construct a fn-value is to refer to a top-level def.
+  qualified `prefix.def`) used as a `Term::Var` is a fn-value.
+- **Anonymous lambdas with capture** (Iter 8). `Term::Lam` constructs a
+  closure that captures any free variables of its body from the
+  enclosing scope. All fn-values share a single ABI: a `ptr` to a
+  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.
 
 Pipeline regression smoke tests:
 
 - `examples/sum.ail.json` → prints 55 (recursion, arithmetic).
 - `examples/list.ail.json` → prints 42 (ADTs + match).
 - `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call).
+- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var).