JOURNAL — 16b.2 planning entry (LetRec capture)

Orchestrator-level planning artifact, not an iteration log.
Captures the design space for 16b.2 so the user can review
trade-offs before implementation. Three architectural paths
considered (desugar-only with restrictions, post-typecheck pass,
mini-inference inside desugar); recommends the first as the
incremental path. Lists restrictions for the safe subset
(fn/Lam-param captures only, direct-call only, monomorphic
enclosing fn, single-level LetRec) and queues the lifted
restrictions as 16b.3-16b.7. Adjacent open items (16d chain
terminator, 16e == extension) likewise scoped.

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

docs/JOURNAL.md

@@ -3395,3 +3395,148 @@ capture, unchanged), 17a (per-fn arena, gated on user
 discussion of memory management, unchanged). 16c-aux
 (`std_list::take`/`drop` refactor onto lit patterns) is a
 separate iter, gated on orchestrator decision.
+
+## Iter 16b.2 — planning entry (LetRec capture)
+
+**Status: planning, not implemented.** This entry is orchestrator
+work-product, not an iteration log. It captures the design space
+for 16b.2 so the user can review the trade-offs before
+implementation, and so a future agent has a sharp brief to work
+against.
+
+**Goal (when implemented).** Lift 16b.1's no-capture restriction.
+Support `(let-rec name ...)` whose body references one or more
+names bound in the enclosing lexical scope, by augmenting the
+lifted top-level fn's signature with the captured names as extra
+parameters and rewriting every call site of `name` (in body and
+in_term) to pass the captures positionally.
+
+**Why this is non-trivial.** The lifted fn's signature must
+include the captures' types. Those types are not always
+discoverable at desugar time:
+
+- **Captured fn-param**: type is in `f.ty.params[i]`. Known.
+- **Captured Lam-param**: type is in `param_tys[i]`. Known.
+- **Captured Let-binding**: `Term::Let { name, value, body }`
+  carries no type annotation on `name`. Type is the inferred
+  type of `value`, which the typechecker computes — but the
+  desugar pass runs *before* the typechecker. **Unknown at
+  desugar time.**
+- **Captured Match-arm pattern var**: type is the substituted
+  field type of the matched constructor, requiring an ADT-def
+  lookup plus arg-substitution. Computable in principle, but
+  the desugar pass would need to track the scrutinee's type
+  through the walk — also a small inference engine.
+
+**Architectural choices.** Pick one path before implementing:
+
+1. **Stay at desugar; restrict to fn/Lam-param captures only.**
+   Reject Let-binding and Match-arm captures with a clear
+   error → `16b.3` (Let captures) and `16b.4` (Match captures).
+   Lowest-cost path, covers the most common case (recursive
+   helpers that close over an enclosing fn's input).
+
+2. **Move LetRec elimination to a post-typecheck pass.** By
+   then every `Term` has known types; capture types fall out.
+   Cost: a new pipeline stage, plus updating `DESIGN.md`'s
+   pipeline section. Pays off if the post-pass is also where
+   other future lowerings live (e.g. closure conversion).
+
+3. **Run a lightweight inference inside desugar.** Just enough
+   to resolve `Term::Let`-bound names to their value's type.
+   Effectively a Hindley-Milner pass on a subset of the AST.
+   Cost: significant; basically duplicating part of
+   `ailang-check`. Rejected on principle — one source of truth.
+
+**Recommended path.** (1), shipping incrementally. 16b.2 covers
+fn/Lam-params; 16b.3 lifts Let-bindings via path (2). The
+benefit of (1) first: it surfaces real-world usage and informs
+how often Let-binding capture actually matters.
+
+**Other restrictions for 16b.2 (under path 1).**
+
+- **Direct-call only.** The LetRec name `f` may appear in
+  `body` and `in_term` only as the callee of a `Term::App`,
+  never as a `Term::Var` in any other position (e.g. passed as
+  an argument, bound to a `let`, or stored in an ADT field).
+  Reason: with captures-as-extra-params, every use site needs
+  the extras appended. Treating `f` as a value would require
+  a closure object that bundles `f` and its captures — that's
+  16b.5 / closure conversion.
+- **Monomorphic enclosing fn.** If the enclosing fn is
+  `forall(...). ...`, the captures' types may mention the
+  outer's type vars. Constructing the lifted fn's `Forall` is
+  doable but error-prone; defer to 16b.6.
+- **Single-level LetRec.** A LetRec whose body contains
+  another LetRec that captures the outer's name or params is
+  not supported in 16b.2; reject with a clear error → 16b.7.
+
+**What 16b.2 ships (under the recommended scope).**
+
+- `desugar_term`'s `scope` parameter changes from
+  `&BTreeSet<String>` to `&BTreeMap<String, ScopeEntry>`,
+  where `ScopeEntry` is `KnownType(Type) | LetBound | MatchArm`.
+- Each binder extends the map: fn/Lam-params with `KnownType`,
+  Let-bindings with `LetBound`, Match-arm bindings with
+  `MatchArm`.
+- LetRec arm's capture detection: free-vars ∩ scope-keys.
+  For each capture, look up `ScopeEntry`. If `KnownType(t)`,
+  proceed. If `LetBound` / `MatchArm`, error.
+- Validate: walk body and in_term, assert `name` only appears
+  as `Term::App.callee`. Helper `validate_callee_only_use`.
+- Build augmented fn type: `original.ty` with capture types
+  appended to `params`. Reject if `original.ty` is `Forall`
+  (out of scope per restriction 2 above).
+- Rewrite call sites: `(app f a b)` → `(app f$lr_N a b cap0
+  cap1)`. Use a new helper `subst_call_with_extras` that
+  walks the term, recognizes `Term::App { callee = Var{f} }`
+  patterns, rewrites them, and recurses elsewhere.
+- Substitute `f` → `f$lr_N` everywhere in body (for the
+  recursive self-reference at the lifted level). The existing
+  `subst_var` from 16b.1 handles this, but care needed: it
+  must run **after** `subst_call_with_extras` so that
+  recursive calls get both the rename and the extras.
+- Append the lifted `FnDef` to `Module.defs`.
+
+**Risk.** The most likely failure mode is the typechecker
+rejecting a synthesized augmented fn signature that we believe
+should type-check. Mitigation: implement under restriction 2
+(no Forall) so we never construct a Forall; the augmented type
+is plain `Type::Fn` with monomorphic capture types appended.
+
+**Tests.**
+
+- `examples/local_rec_capture.ailx`: an enclosing fn with one
+  Int param, a LetRec that recurses against that param. e2e
+  asserts an output value derived from that capture.
+- Negative tests at the desugar unit-test level: Let-binding
+  capture errors; Match-arm capture errors; name-as-value
+  errors; nested LetRec mutual-capture errors. All
+  `#[should_panic]` (consistent with 16b.1's panic discipline).
+
+**Adjacent open items.**
+
+- **16d**: chain-machinery's `Unit` terminator forces a
+  trailing `_` arm in matches that are otherwise exhaustive,
+  surfaced by 16c (`categorize_first` fixture). Two design
+  paths: (a) introduce a polymorphic `__unreachable__`
+  builtin that codegen lowers to LLVM `unreachable`, used as
+  the chain default; (b) run an exhaustiveness pre-check in
+  desugar against the scrutinee's ADT and omit the
+  terminator when arms cover all ctors. Path (a) is broader
+  (gives users a primitive for panics/asserts). Path (b) is
+  purer (terminator never appears for exhaustive matches)
+  but needs ADT lookup in desugar.
+- **16e**: extend `==` from Int-only to Int/Bool/Str. Bool
+  comparison is i1-equality (trivial). Str comparison
+  needs a runtime `strcmp`. Surfaced by 16c (`build_eq`
+  produces `(app == ...)` for Bool/Str/Unit but currently
+  fails at typecheck because `==` is not declared for them).
+- **17a**: per-fn arena allocator. Gated on user
+  memory-management discussion (separate stored memory).
+
+**Queue update post-16c.** 16c done. Open: 16b.2 (this entry —
+planning only, awaiting user input on path 1 vs path 2), 16d
+(planning needed — pick path a vs b), 16e (`==` extension),
+17a (gated). All implementation work in this session-arc is
+suspended at this planning checkpoint.