Iter 16d: chain-terminator via __unreachable__ builtin

Eliminates the Unit-typed chain default that 16c left in place.
Adds __unreachable__ : forall a. a — codegen lowers to LLVM
unreachable. The 16a/16c chain machinery now uses it as the
deepest fall-through, so exhaustive matches with non-Unit arms
no longer need a (case _ ...) workaround.

- check/builtins.rs: register __unreachable__ as Forall(a, a).
- codegen: Term::Var "__unreachable__" emits LLVM unreachable
  and sets block_terminated; If/Match/fn-body gate downstream
  work on that flag.
- desugar: chain default switched from Lit{Unit} to Var.
- examples/lit_pat: categorize_first's trailing _ arm removed.
  Hash changes from c4faec3abc2ed388 to 644de0c0ec15fc17.
- examples/unreachable_demo: positive fixture using safe_div
  with __unreachable__ in the impossible branch.
- e2e + desugar tests: 122 → 124 (+2).

Path-a from 16b.2 planning: real primitive over a desugar-time
exhaustiveness pre-check (which would need cross-module type
registry access from desugar).

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

docs/DESIGN.md

@@ -798,6 +798,19 @@ What **is** supported (and used as the smoke test for the pipeline):
 - `if`, `let`, function calls, recursion.
 - Effects on function signatures, with `do op(args)` for direct effect
   ops (`io/print_int`, `io/print_bool`, `io/print_str`).
+- **Builtins.** Arithmetic and comparison operators (`+`, `-`, `*`,
+  `/`, `%`, `==`, `!=`, `<`, `<=`, `>`, `>=`) of type
+  `(Int, Int) -> Int` / `Bool`; logical `not : (Bool) -> Bool`; the
+  IO effect ops listed above; and **`__unreachable__ : forall a. a`**
+  (Iter 16d). The latter is a polymorphic bottom value: a use of
+  `__unreachable__` typechecks against any expected type at the use
+  site and codegens to the LLVM `unreachable` instruction (UB if
+  ever executed). It is the chain machinery's deepest fall-through
+  for matches that the typechecker proved exhaustive, and it is
+  available to user code as an explicit panic primitive
+  (`(if cond __unreachable__ ...)` for assertions or impossible
+  branches). Reference site is `Term::Var { name = "__unreachable__" }`
+  / form-A bare `__unreachable__`.
 - **ADTs + pattern matching** (Iter 3, extended in Iter 16a/16c).
   Sub-patterns of a Ctor pattern may be `Var`, `Wild`, another `Ctor`
   (Iter 16a), or a literal (Iter 16c). The desugar pass flattens

docs/JOURNAL.md

@@ -4495,3 +4495,154 @@ polymorphic enclosing fn; needs polymorphic closure
 pairs). 16d (chain-machinery exhaustiveness or
 `__unreachable__`), 16e (`==` extension to
 Bool/Str/Unit), 17a (per-fn arena, gated) unchanged.
+
+## Iter 16d — chain-terminator via `__unreachable__` builtin
+
+**Goal.** Eliminate the synthetic `Unit`-typed chain terminator
+that 16a/16c emitted for matches whose arms have non-Unit return
+types. Pre-16d, the desugar pass's `desugar_match` used
+`Term::Lit { lit: Literal::Unit }` as the deepest fall-through of
+the let-bind + chain rewrite. That terminator unifies against
+`Unit` only, so any match returning (say) `Int` had to carry a
+trailing `(case _ <int>)` arm whose sole purpose was to dominate
+the terminator with a same-type value. Surfaced by 16c's
+`categorize_first` fixture, where `IntList`'s two ctors (`Nil`,
+`Cons`) are exhaustive on their own but the trailing `(case _ 0)`
+was load-bearing for the chain machinery rather than for the
+program's semantics.
+
+**Architectural decision (path a, by the orchestrator).** Two
+paths were on the table per the 16c entry's "Adjacent open items":
+**(a)** introduce a polymorphic `__unreachable__` builtin used as
+the chain default; **(b)** run an exhaustiveness pre-check in
+desugar against the scrutinee's ADT and omit the terminator
+entirely for exhaustive matches. Path (b) is purer (terminator
+never appears for exhaustive matches) but needs ADT lookup at
+desugar time, which today runs single-module and would require
+threading workspace type-registry access through the pass — a
+non-trivial pipeline change. Path (a) is broader: besides
+unblocking 16c's fixture, it gives users a real bottom primitive
+for asserts, impossible branches, and panics. Path (a) chosen.
+
+**The new builtin.** `__unreachable__` is registered as a
+**polymorphic value** (not a zero-arg fn) typed
+`Type::Forall { vars: ["a"], body: Type::Var { name: "a" } }` —
+i.e. `forall a. a`, the textbook bottom type. Reference site is
+plain `(var __unreachable__)` (form-A bare ident
+`__unreachable__`). The value-form was preferred over the
+zero-arg-fn form because the obvious authoring shape (a name in
+expression position) is then the right shape — `(app
+__unreachable__)` would have rejected the natural use as a value
+and added paren noise. Chosen the same way as how the
+typechecker already treats every `Forall`-typed global: the
+`Term::Var` resolver (`maybe_instantiate`) substitutes the
+forall var with a fresh metavar at every use site, and
+unification with the surrounding context's expected type pins
+that metavar.
+
+**Codegen lowering.** `Term::Var { name = "__unreachable__" }` in
+`lower_term` emits a single `unreachable\n` line, sets
+`block_terminated = true`, and returns a dummy
+`("0", "i8")` SSA + LLVM-type pair. The dummy type is sound
+because the existing `Term::If`, `Term::Match`, and top-level
+fn-body code paths all gate downstream emission on
+`block_terminated`: the terminated branch's value/type is never
+fed into a phi node. In an `if`, the live branch's value flows
+through to the join unchanged (existing 14e behaviour). In a
+`Term::Match` default block, the arm contributes nothing to
+`phi_inputs` and the join collapses to whatever non-terminated
+arms produced. No alternative lowering (e.g. `abort`/`trap`)
+because LLVM `unreachable` lets the optimizer aggressively prune
+the unreachable region.
+
+**What shipped.**
+
+- `crates/ailang-check/src/builtins.rs` (+12, of which ~7 are
+  doc): registers `__unreachable__` in `env.globals` with type
+  `forall a. a`; adds it to `list()` (consumed by the
+  `ail builtins` CLI subcommand and `value_names()`). Mirrors
+  how operators like `+` / `==` are installed.
+- `crates/ailang-codegen/src/lib.rs` (+15, of which ~10 are
+  doc): special-cases `Term::Var { name = "__unreachable__" }`
+  in `lower_term` to emit `unreachable` + mark
+  `block_terminated`; adds the same `forall a. a` entry to
+  `builtin_ail_type` so `synth_arg_type` resolves it during
+  monomorphisation walks.
+- `crates/ailang-core/src/desugar.rs` (+3 net): one-line
+  swap of the chain default from `Term::Lit { Unit }` to
+  `Term::Var { name: "__unreachable__".into() }` in
+  `desugar_match`; module-level doc updated to reflect the new
+  contract; one new unit test
+  (`chain_default_is_unreachable_builtin`) that walks the
+  desugared output for a two-lit-arm match and asserts the
+  deepest `else_` is `Term::Var { name = "__unreachable__" }`.
+- `examples/lit_pat.ailx` + `examples/lit_pat.ail.json`: the
+  trailing `(case _ 0)` workaround on `categorize_first` is
+  removed. The remaining match (`Nil` arm + `Cons (pat-lit 0)
+  _` arm + `Cons h _` arm) is exhaustive on `IntList`; the
+  chain default is unreached. Header comment rewritten to
+  describe 16d's role. Output unchanged: `100, 200, 999, -1,
+  0, 7`.
+- `examples/unreachable_demo.ailx` + `.ail.json`: new fixture.
+  `safe_div(a, b)` returns `a / b` when `b != 0` and panics via
+  `__unreachable__` otherwise. Driver uses non-zero divisors
+  only, so the panic branch is never executed. Output: `4, 5`.
+  Exercises the typechecker's `forall a. a` instantiation
+  against `Int` and codegen's `unreachable` emission inside an
+  `if`'s then-branch.
+- `crates/ail/tests/e2e.rs` (+18): `unreachable_demo` test;
+  `lit_pat_demo`'s doc updated to mention the 16d simplification.
+- `docs/DESIGN.md`: new "Builtins" bullet under "What is
+  supported", listing every builtin (operators, `not`, IO ops)
+  and calling out `__unreachable__ : forall a. a` with its UB
+  semantics.
+
+**Hash determinism.** Of the 36 fixture defs across all
+`examples/*.ail.json`, exactly one hash changed: the
+`categorize_first` def of `lit_pat` (`c4faec3abc2ed388` →
+`644de0c0ec15fc17`), because that's the only def whose source
+text changed. All other defs — including `lit_pat`'s other
+three (`IntList`, `classify`, `main`) — are bit-identical to
+their pre-16d forms. The new `unreachable_demo` fixture has
+two new hashes (`safe_div`, `main`) which obviously didn't
+exist before. Verified by stash-diff of `ail manifest` output
+on `sum`, `list`, `maybe_int`, and `lit_pat`.
+
+**Other fixtures that benefited.** Just `lit_pat` —
+`categorize_first` was the only place in the shipped corpus
+where a `(case _ ...)` arm existed solely to dominate the
+chain terminator. The `(case _ 0)` arms in `nested_pat` and
+`std_either_list` are semantically required (they handle
+`Nil` and partial-coverage cases that the preceding nested
+ctor patterns don't reach), not workarounds; they stay.
+`std_list::take` / `drop` use a different workaround (base-
+case-via-arm-body / `if (== n 0) Nil ...`) which 16c-aux
+addresses, not 16d.
+
+**Tests: 122 → 124 (+2).**
+
+- e2e: 45 → 46 (`unreachable_demo`).
+- `ailang-core::desugar::tests`: 25 → 26
+  (`chain_default_is_unreachable_builtin`).
+- All other crates unchanged.
+
+**Cumulative state, post-16d.**
+
+- Stdlib unchanged (5 modules, 29 combinators).
+- `Term`/`Pattern`/`Literal` enums unchanged. The new builtin
+  is purely a name-level addition (`env.globals` + a codegen
+  lowering branch); no AST shape changed and no schema bump.
+- 16a desugar pass now does four jobs: nested-ctor flattening
+  (16a), LetRec lift (16b.1–16b.7), lit-pattern → If rewrite
+  (16c), and `__unreachable__` chain default (16d). Pass
+  remains the single AST-→-AST hop between `load_module` and
+  typecheck.
+- Compiler bugs surfaced and fixed in dogfood since 14a: 5/5
+  (unchanged).
+
+**Queue update post-16d.** 16d done. Open: `closure-of-self`
+(informally 16b.5-body — unchanged); `closure-poly`
+(informally 16b.5b — unchanged); 16e (`==` extension to
+Bool/Str/Unit — surfaced by 16c, unchanged); 17a (per-fn
+arena, gated — unchanged); 16c-aux (`std_list::take`/`drop`
+refactor onto lit patterns — unchanged).