diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs
index f26d9e4..cdf75b3 100644
--- a/crates/ail/tests/e2e.rs
+++ b/crates/ail/tests/e2e.rs
@@ -1109,9 +1109,31 @@ fn check_json_unbound_var() {
 /// either a wrong result or an `unreachable!` panic depending on
 /// the path. The fixture exercises both sites: `classify` (top-
 /// level lit arms) and `categorize_first` (nested lit-in-Ctor).
+///
+/// Iter 16d update: the trailing `(case _ 0)` arm of
+/// `categorize_first` was removed when the chain machinery's
+/// terminator switched from a `Unit` literal to the polymorphic
+/// `__unreachable__` builtin. Output is unchanged — this test
+/// guards both 16c (lit-pattern desugar) and 16d (no-workaround
+/// chain default).
 #[test]
 fn lit_pat_demo() {
     let stdout = build_and_run("lit_pat.ail.json");
     let lines: Vec<&str> = stdout.lines().collect();
     assert_eq!(lines, vec!["100", "200", "999", "-1", "0", "7"]);
 }
+
+/// Iter 16d: `__unreachable__` as an explicit user-callable
+/// primitive. Property protected: a polymorphic `forall a. a` value
+/// reference (a) typechecks against any expected type at the use
+/// site (here `Int`), and (b) codegen lowers it to LLVM
+/// `unreachable`, with the surrounding `if` correctly forwarding
+/// the live branch's value past the terminated branch. The fixture
+/// only ever hits the live branch, so the binary must succeed and
+/// print the expected outputs.
+#[test]
+fn unreachable_demo() {
+    let stdout = build_and_run("unreachable_demo.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["4", "5"]);
+}
diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs
index d5d71a5..a3cea88 100644
--- a/crates/ailang-check/src/builtins.rs
+++ b/crates/ailang-check/src/builtins.rs
@@ -73,6 +73,20 @@ pub fn install(env: &mut crate::Env) {
         },
     );
 
+    // Iter 16d: `__unreachable__` is the polymorphic bottom value.
+    // Type: `forall a. a`. Used by the desugar pass as the chain
+    // terminator of an exhaustive match, and available to user code as
+    // a primitive panic point. Codegen lowers it to LLVM `unreachable`.
+    // It is a value, not a fn — reference site is `(var __unreachable__)`,
+    // not `(app __unreachable__)`.
+    env.globals.insert(
+        "__unreachable__".into(),
+        Type::Forall {
+            vars: vec!["a".into()],
+            body: Box::new(Type::Var { name: "a".into() }),
+        },
+    );
+
     env.effect_ops.insert(
         "io/print_int".into(),
         EffectOpSig {
@@ -130,6 +144,7 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
         (">", "(Int, Int) -> Bool"),
         (">=", "(Int, Int) -> Bool"),
         ("not", "(Bool) -> Bool"),
+        ("__unreachable__", "forall a. a"),
         ("io/print_int", "(Int) -> Unit !IO  [effect op]"),
         ("io/print_bool", "(Bool) -> Unit !IO  [effect op]"),
         ("io/print_str", "(Str) -> Unit !IO  [effect op]"),
diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs
index 49a7ba9..9be8cc8 100644
--- a/crates/ailang-codegen/src/lib.rs
+++ b/crates/ailang-codegen/src/lib.rs
@@ -863,6 +863,20 @@ impl<'a> Emitter<'a> {
                 Literal::Unit => ("0".into(), "i8".into()),
             }),
             Term::Var { name } => {
+                // Iter 16d: `__unreachable__` is a polymorphic bottom
+                // value (`forall a. a`). At codegen we emit LLVM
+                // `unreachable` as the block terminator and return a
+                // dummy SSA value. The surrounding `if`/`match`/`seq`
+                // already inspects `block_terminated` and forwards the
+                // sibling branch's type, so the type we report here is
+                // not consumed by a phi node — `i8` is a sound
+                // placeholder. Subsequent emissions in this block are
+                // gated by `block_terminated`.
+                if name == "__unreachable__" {
+                    self.body.push_str("  unreachable\n");
+                    self.block_terminated = true;
+                    return Ok(("0".into(), "i8".into()));
+                }
                 if let Some((_, ssa, ty, _)) =
                     self.locals.iter().rev().find(|(n, _, _, _)| n == name)
                 {
@@ -2632,6 +2646,12 @@ fn builtin_ail_type(name: &str) -> Option<Type> {
             ret: Box::new(Type::bool_()),
             effects: vec![],
         },
+        // Iter 16d: `__unreachable__` is the polymorphic bottom value
+        // (`forall a. a`). Mirrors the typechecker's `builtins::install`.
+        "__unreachable__" => Type::Forall {
+            vars: vec!["a".into()],
+            body: Box::new(Type::Var { name: "a".into() }),
+        },
         _ => return None,
     })
 }
diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs
index 263a52f..945275e 100644
--- a/crates/ailang-core/src/desugar.rs
+++ b/crates/ailang-core/src/desugar.rs
@@ -28,10 +28,15 @@
 //! 2. Let-bind the scrutinee to a fresh name `$mp_N` (so that we don't
 //!    re-evaluate effectful scrutinees per arm).
 //! 3. Build a chain of single-level matches via
-//!    `build_chain(s_var, arms, default)` where `default` is a unit
-//!    literal — a placeholder for the unreachable fallthrough. Valid
+//!    `build_chain(s_var, arms, default)` where `default` is the
+//!    polymorphic bottom builtin `__unreachable__` (`forall a. a`,
+//!    Iter 16d) — codegen lowers it to LLVM `unreachable`. Valid
 //!    programs never reach it because the checker requires
 //!    exhaustiveness (the catch-all arm dominates the chain).
+//!    Pre-16d the default was a `Unit` literal, which forced any
+//!    match whose arms returned a non-Unit type to carry a
+//!    synthetic `_` arm dominating the terminator. The polymorphic
+//!    `__unreachable__` removes that workaround.
 //! 4. Each arm is lowered via `desugar_one_arm`:
 //!    - `Pattern::Wild` → arm body (catch-all; later arms are dropped).
 //!    - `Pattern::Var { name }` → `Let { name = scrutinee_var; body }`.
@@ -844,11 +849,14 @@ impl Desugarer {
         }
         let s = self.fresh();
         let s_var = Term::Var { name: s.clone() };
-        // Document: `default` is unreachable for valid programs because
-        // the typechecker requires a catch-all arm (`pat-wild` or
-        // exhaustive ctor coverage). It only exists to give
-        // `build_chain` a well-typed terminator.
-        let default = Term::Lit { lit: Literal::Unit };
+        // Iter 16d: `default` is unreachable for valid programs (the
+        // typechecker requires either a catch-all arm or exhaustive
+        // ctor coverage). Use the polymorphic bottom builtin
+        // `__unreachable__` (`forall a. a`) so the terminator unifies
+        // against any arm result type without forcing a synthetic
+        // `Unit`-typed `_` arm to dominate it. Codegen lowers the
+        // var to LLVM `unreachable`.
+        let default = Term::Var { name: "__unreachable__".into() };
         let chain = self.build_chain(&s_var, &arms, &default);
         Term::Let {
             name: s,
@@ -2652,4 +2660,76 @@ mod tests {
             "Pattern::Lit must be classified as non-flat after 16c"
         );
     }
+
+    /// Iter 16d: the chain machinery's deepest fall-through is the
+    /// polymorphic `__unreachable__` builtin (`forall a. a`), not a
+    /// `Unit` literal. A match with two lit arms and a wildcard
+    /// catches all paths via the wild-arm body, so the deepest
+    /// `else_` of the chain is the `__unreachable__` var.
+    #[test]
+    fn chain_default_is_unreachable_builtin() {
+        // (match n (case (pat-lit 0) 100) (case (pat-lit 1) 200))
+        // Note: no wildcard on purpose — the chain reaches the
+        // synthetic terminator after both lit arms fail.
+        let body_match = Term::Match {
+            scrutinee: Box::new(Term::Var { name: "n".into() }),
+            arms: vec![
+                Arm {
+                    pat: Pattern::Lit {
+                        lit: Literal::Int { value: 0 },
+                    },
+                    body: Term::Lit {
+                        lit: Literal::Int { value: 100 },
+                    },
+                },
+                Arm {
+                    pat: Pattern::Lit {
+                        lit: Literal::Int { value: 1 },
+                    },
+                    body: Term::Lit {
+                        lit: Literal::Int { value: 200 },
+                    },
+                },
+            ],
+        };
+        let m = Module {
+            schema: crate::SCHEMA.to_string(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![Def::Fn(FnDef {
+                name: "f".into(),
+                ty: Type::Fn {
+                    params: vec![Type::int()],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                params: vec!["n".into()],
+                body: body_match,
+                doc: None,
+            })],
+        };
+        let out = desugar_module(&m);
+        let body = match &out.defs[0] {
+            Def::Fn(f) => &f.body,
+            _ => unreachable!(),
+        };
+        // Outer is `let $mp_N = scrutinee in <chain>`. The chain is
+        // `if (== sv 0) then 100 else if (== sv 1) then 200 else __unreachable__`.
+        let chain = match body {
+            Term::Let { body, .. } => body.as_ref(),
+            other => panic!("expected outer Let from chain machinery, got {other:?}"),
+        };
+        let inner_else = match chain {
+            Term::If { else_, .. } => else_.as_ref(),
+            other => panic!("expected outer If, got {other:?}"),
+        };
+        let deepest = match inner_else {
+            Term::If { else_, .. } => else_.as_ref(),
+            other => panic!("expected nested If, got {other:?}"),
+        };
+        assert!(
+            matches!(deepest, Term::Var { name } if name == "__unreachable__"),
+            "deepest chain fall-through must be `__unreachable__`, got {deepest:?}"
+        );
+    }
 }
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index ca9211c..8439bda 100644
--- a/docs/DESIGN.md
+++ b/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
diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md
index b23244f..3d47354 100644
--- a/docs/JOURNAL.md
+++ b/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).
diff --git a/examples/lit_pat.ail.json b/examples/lit_pat.ail.json
index cbadf1b..150fe44 100644
--- a/examples/lit_pat.ail.json
+++ b/examples/lit_pat.ail.json
@@ -1 +1 @@
-{"defs":[{"ctors":[{"fields":[],"name":"Nil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"Cons"}],"kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":100},"t":"lit"},"pat":{"lit":{"kind":"int","value":0},"p":"lit"}},{"body":{"lit":{"kind":"int","value":200},"t":"lit"},"pat":{"lit":{"kind":"int","value":1},"p":"lit"}},{"body":{"lit":{"kind":"int","value":999},"t":"lit"},"pat":{"p":"wild"}}],"scrutinee":{"name":"n","t":"var"},"t":"match"},"doc":"Map 0->100, 1->200, anything else->999.","kind":"fn","name":"classify","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":-1},"t":"lit"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"Cons","fields":[{"lit":{"kind":"int","value":0},"p":"lit"},{"p":"wild"}],"p":"ctor"}},{"body":{"name":"h","t":"var"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"p":"wild"}],"p":"ctor"}},{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"p":"wild"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Empty -> -1; first element 0 -> 0; otherwise return the head.","kind":"fn","name":"categorize_first","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":17},"t":"lit"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"fn":{"name":"categorize_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"fn":{"name":"categorize_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"fn":{"name":"categorize_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive both fns. Expected (per line): 100, 200, 999, -1, 0, 7.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"lit_pat","schema":"ailang/v0"}
+{"defs":[{"ctors":[{"fields":[],"name":"Nil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"Cons"}],"kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":100},"t":"lit"},"pat":{"lit":{"kind":"int","value":0},"p":"lit"}},{"body":{"lit":{"kind":"int","value":200},"t":"lit"},"pat":{"lit":{"kind":"int","value":1},"p":"lit"}},{"body":{"lit":{"kind":"int","value":999},"t":"lit"},"pat":{"p":"wild"}}],"scrutinee":{"name":"n","t":"var"},"t":"match"},"doc":"Map 0->100, 1->200, anything else->999.","kind":"fn","name":"classify","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":-1},"t":"lit"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"Cons","fields":[{"lit":{"kind":"int","value":0},"p":"lit"},{"p":"wild"}],"p":"ctor"}},{"body":{"name":"h","t":"var"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Empty -> -1; first element 0 -> 0; otherwise return the head.","kind":"fn","name":"categorize_first","params":["xs"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":17},"t":"lit"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"fn":{"name":"categorize_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"fn":{"name":"categorize_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"fn":{"name":"categorize_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive both fns. Expected (per line): 100, 200, 999, -1, 0, 7.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"lit_pat","schema":"ailang/v0"}
\ No newline at end of file
diff --git a/examples/lit_pat.ailx b/examples/lit_pat.ailx
index d5acdae..d9d2dc4 100644
--- a/examples/lit_pat.ailx
+++ b/examples/lit_pat.ailx
@@ -5,10 +5,13 @@
 ; inside Pat-Ctor's first field. Both shapes are now handled by the
 ; 16c desugar pass; codegen sees only If/Match-on-Ctor combinations.
 ;
-; The trailing `_` catch-all in `categorize_first` is required by the
-; 16a chain machinery: the chain's terminator is a `Unit` literal,
-; reachable when no arm matches. A `_` arm dominates the chain so the
-; terminator stays unreachable in practice and the match type-checks.
+; Iter 16d update — the chain machinery's terminator is now the
+; polymorphic `__unreachable__` builtin (`forall a. a`, lowered to
+; LLVM `unreachable`) instead of a `Unit` literal. That removed the
+; pre-16d need for a trailing `(case _ 0)` arm in `categorize_first`
+; whose only purpose was to dominate the synthetic `Unit`-typed
+; terminator. The two ctor arms (`Nil` and `Cons h _`) are
+; exhaustive on `IntList`; the chain default is never reached.
 ;
 ; Expected stdout (one per line): 100, 200, 999, -1, 0, 7.
 
@@ -36,8 +39,7 @@
       (match xs
         (case (pat-ctor Nil) -1)
         (case (pat-ctor Cons (pat-lit 0) _) 0)
-        (case (pat-ctor Cons h _) h)
-        (case _ 0))))
+        (case (pat-ctor Cons h _) h))))
 
   (fn main
     (doc "Drive both fns. Expected (per line): 100, 200, 999, -1, 0, 7.")
diff --git a/examples/unreachable_demo.ail.json b/examples/unreachable_demo.ail.json
new file mode 100644
index 0000000..ec59acc
--- /dev/null
+++ b/examples/unreachable_demo.ail.json
@@ -0,0 +1 @@
+{"defs":[{"body":{"cond":{"args":[{"name":"b","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"},"else":{"args":[{"name":"a","t":"var"},{"name":"b","t":"var"}],"fn":{"name":"/","t":"var"},"t":"app"},"t":"if","then":{"name":"__unreachable__","t":"var"}},"doc":"a/b for b != 0; otherwise panic via __unreachable__.","kind":"fn","name":"safe_div","params":["a","b"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":8},"t":"lit"},{"lit":{"kind":"int","value":2},"t":"lit"}],"fn":{"name":"safe_div","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"int","value":15},"t":"lit"},{"lit":{"kind":"int","value":3},"t":"lit"}],"fn":{"name":"safe_div","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"doc":"Drive safe_div with non-zero divisors. Expected: 4, 5.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"unreachable_demo","schema":"ailang/v0"}
\ No newline at end of file
diff --git a/examples/unreachable_demo.ailx b/examples/unreachable_demo.ailx
new file mode 100644
index 0000000..11caf58
--- /dev/null
+++ b/examples/unreachable_demo.ailx
@@ -0,0 +1,35 @@
+; Iter 16d — `__unreachable__` as an explicit user-callable primitive.
+; Type: forall a. a (lowered to LLVM `unreachable`).
+;
+; This fixture exercises `__unreachable__` in a value position that is
+; statically unreachable but still type-checks: the impossible branch
+; of an if. `safe_div(a, b)` returns `a / b` when `b != 0` and panics
+; via `__unreachable__` otherwise. The driver only ever calls it with
+; non-zero divisors, so the panic branch is never executed.
+;
+; The point of the fixture is the type-system + codegen surface:
+; `__unreachable__` unifies against `Int` (the fn's return type) at
+; the typechecker, and codegen lowers it to `unreachable` followed by
+; the rest of the if's join machinery, which is sound because the
+; surrounding if's `block_terminated` flag is honoured.
+;
+; Expected stdout (one per line): 4, 5.
+
+(module unreachable_demo
+
+  (fn safe_div
+    (doc "a/b for b != 0; otherwise panic via __unreachable__.")
+    (type (fn-type (params (con Int) (con Int)) (ret (con Int))))
+    (params a b)
+    (body
+      (if (app == b 0)
+          __unreachable__
+          (app / a b))))
+
+  (fn main
+    (doc "Drive safe_div with non-zero divisors. Expected: 4, 5.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (seq (do io/print_int (app safe_div 8 2))
+           (do io/print_int (app safe_div 15 3))))))