Iter 16b.5: LetRec name as value (in_term only) via eta-Lam wrapper

Drops the direct-call-only restriction on the LetRec name when it
appears in `in_term`. No new ABI: the lift wraps the in-term in
`(let f (lam P (app f$lr_N P CAPTURES)) in_term')` so codegen's
existing Iter-8b closure-pair machinery handles it. Body-position
name-as-value still rejected (deferred — eta-of-self is harder).

- desugar.rs / lift.rs: split find_non_callee_use into body
  (panic) and in_term (wrap).
- examples/local_rec_as_value.{ailx,ail.json}: no-capture path
  (factorial passed to apply5 → 120).
- examples/local_rec_as_value_capture.{ailx,ail.json}: capture
  path; lifted fn has captures, eta-Lam picks them up via 8b.
- e2e + desugar tests: 113 → 116 (+3).

Codegen Lam machinery handled the wrapped form on the first try.

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

crates/ail/tests/e2e.rs

@@ -505,6 +505,38 @@ fn local_rec_match_capture_demo() {
     assert_eq!(lines, vec!["0", "5", "9"]);
 }
 
+/// Iter 16b.5: LetRec name as a value in the in-clause (no capture).
+/// Property protected: the desugar pass detects a non-callee use of
+/// the LetRec name in `in_term` and wraps the rewritten in-term in
+/// `(let factorial (lam ...) ...)` whose lam eta-expands the lifted
+/// fn. The LetRec name then resolves to a closure-pair value usable
+/// anywhere a `Fn(Int) -> Int` is expected (here: passed to a HOF
+/// `apply5`). Without 16b.5, the desugar would panic with the
+/// "name-as-value not supported" message and the build would fail.
+/// Expected stdout: 120 (= apply5 factorial = factorial 5).
+#[test]
+fn local_rec_as_value_demo() {
+    let stdout = build_and_run("local_rec_as_value.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["120"]);
+}
+
+/// Iter 16b.5: LetRec name as a value in the in-clause WITH capture.
+/// Property protected: the eta-Lam wrap composes correctly with the
+/// 16b.2 capture-augmentation. The lifted fn has signature
+/// `factorial_plus$lr_N(n: Int, base: Int) -> Int`; the eta-Lam
+/// wrap binds `factorial_plus` to a `(lam (n) (app
+/// factorial_plus$lr_N n base))` whose free var `base` becomes a
+/// standard 8b closure-env capture. This is the dynamic-env path:
+/// the lifted fn has extra params, the eta-Lam captures them.
+/// Expected stdout: 1320 (= 5*4*3*2*(1+10)), 12120 (= 5*4*3*2*(1+100)).
+#[test]
+fn local_rec_as_value_capture_demo() {
+    let stdout = build_and_run("local_rec_as_value_capture.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["1320", "12120"]);
+}
+
 /// Guards `ail diff`: a modified body changes the hash of `sum`, while
 /// `main` stays unchanged. Expects exit code 1, `changed` contains exactly
 /// `sum`, `unchanged` contains `main`, `added`/`removed` empty.

crates/ailang-check/src/lift.rs

@@ -379,23 +379,19 @@ impl<'a> Lifter<'a> {
                     }
                 }
 
-                // Defensive non-callee-use check (the desugar pass
-                // already ran this on the original LetRec, but
-                // post-lifting of inner LetRecs may have rewritten
-                // sub-terms — we re-run on the lifted body/in_term to
-                // be safe).
+                // 16b.5: name-as-value INSIDE the body remains rejected
+                // (would require an eta-Lam that calls the unlifted name —
+                // chicken-and-egg with the call-site rewrite).
                 if find_non_callee_use(&lifted_body, name).is_some() {
                     panic!(
-                        "Iter 16b.3 invariant: LetRec `{name}` used as a value in its own \
-                         body after sub-term lift; should have been rejected at desugar"
-                    );
-                }
-                if find_non_callee_use(&lifted_in, name).is_some() {
-                    panic!(
-                        "Iter 16b.3 invariant: LetRec `{name}` used as a value in its \
-                         in-clause after sub-term lift; should have been rejected at desugar"
+                        "Iter 16b.5: LetRec `{name}` appears as a value INSIDE its own \
+                         body; name-as-value of a LetRec inside its own body is not yet \
+                         supported."
                     );
                 }
+                // 16b.5: name-as-value in in_term IS supported. The wrap
+                // is built below after we know `lifted_name` and `extras`.
+                let in_has_value_use = find_non_callee_use(&lifted_in, name).is_some();
 
                 // Recompute captures of the lifted body against the
                 // current `locals` (deterministic order via BTreeSet).
@@ -465,10 +461,51 @@ impl<'a> Lifter<'a> {
                     subst_call_with_extras(&lifted_body, name, &lifted_name, &extras);
                 let body_full = subst_var(&body_call_rw, name, &lifted_name);
 
-                // In-clause rewrite: same shape.
+                // In-clause: rewrite call sites, but skip subst_var so that
+                // bare `Var{name}` references (16b.5: name-as-value uses)
+                // can resolve to the eta-Lam binding we wrap below.
                 let in_call_rw =
                     subst_call_with_extras(&lifted_in, name, &lifted_name, &extras);
-                let in_full = subst_var(&in_call_rw, name, &lifted_name);
+
+                // 16b.5: extract effects, param types, ret type from the
+                // LetRec's declared type to mirror them on the eta-Lam.
+                let (orig_param_tys, orig_ret_ty, lr_effects): (Vec<Type>, Type, Vec<String>) =
+                    match ty {
+                        Type::Fn { params: ps, ret, effects } => {
+                            (ps.clone(), (**ret).clone(), effects.clone())
+                        }
+                        Type::Forall { .. } => unreachable!("rejected above"),
+                        _ => unreachable!("rejected above"),
+                    };
+
+                let in_full = if in_has_value_use {
+                    let lam_args: Vec<Term> = params
+                        .iter()
+                        .map(|p| Term::Var { name: p.clone() })
+                        .chain(extras.iter().map(|c| Term::Var { name: c.clone() }))
+                        .collect();
+                    let lam_body = Term::App {
+                        callee: Box::new(Term::Var { name: lifted_name.clone() }),
+                        args: lam_args,
+                        tail: false,
+                    };
+                    let eta_lam = Term::Lam {
+                        params: params.clone(),
+                        param_tys: orig_param_tys,
+                        ret_ty: Box::new(orig_ret_ty),
+                        effects: lr_effects,
+                        body: Box::new(lam_body),
+                    };
+                    Term::Let {
+                        name: name.clone(),
+                        value: Box::new(eta_lam),
+                        body: Box::new(in_call_rw),
+                    }
+                } else {
+                    // No name-as-value uses: defensive subst_var keeps
+                    // the historical zero-capture symmetry intact.
+                    subst_var(&in_call_rw, name, &lifted_name)
+                };
 
                 // Append the lifted FnDef. The doc string makes
                 // post-mortem debugging easier — anything containing

crates/ailang-core/src/desugar.rs

@@ -529,28 +529,32 @@ impl Desugarer {
                 in_scope.insert(name.clone(), ScopeEntry::EnclosingLetRec);
                 let desugared_in = self.desugar_term(in_term, &in_scope);
 
-                // 16b.2/16b.5: validate that `name` is only ever used as
-                // the callee of a Term::App in body and in_term — never
-                // as a Term::Var in any value position. Run BEFORE
-                // capture classification so the diagnostic fires
-                // regardless of whether we end up lifting here or
-                // deferring to the post-typecheck pass.
+                // 16b.2: validate that `name` is only ever used as the
+                // callee of a Term::App in `body` — never as a value.
+                // Body-side name-as-value would require an eta-Lam inside
+                // the body that references the LetRec's own pre-lift name;
+                // that's a non-trivial extension (the Lam's body would need
+                // to call the unlifted name, which by then is already
+                // rewritten to the lifted callee — chicken-and-egg). Stays
+                // rejected.
+                //
+                // 16b.5: in_term-side name-as-value is now SUPPORTED. We
+                // detect it here but DO NOT panic; instead, the lift logic
+                // below wraps `in_term'` in a `Let { f, lam(...), in_term' }`
+                // whose lam eta-expands the lifted fn, supplying the
+                // captures positionally. Bare-`f` references in `in_term'`
+                // then resolve to the let-bound lam value. Callee-position
+                // references in `in_term'` go directly to the lifted fn
+                // (efficient; no closure indirection).
                 if let Some(violation) = find_non_callee_use(&desugared_body, name) {
                     panic!(
-                        "Iter 16b.3: LetRec `{}` is used as a value in its own body \
-                         (not as the callee of `app`); not supported. Queued for 16b.5 \
-                         (closure conversion). Offending term: {:?}",
-                        name, violation
-                    );
-                }
-                if let Some(violation) = find_non_callee_use(&desugared_in, name) {
-                    panic!(
-                        "Iter 16b.3: LetRec `{}` is used as a value in the in-clause \
-                         (not as the callee of `app`); not supported. Queued for 16b.5. \
-                         Offending term: {:?}",
+                        "Iter 16b.5: LetRec `{}` appears as a value INSIDE its own body \
+                         (not as the callee of `app`); name-as-value of a LetRec inside \
+                         its own body is not yet supported. Offending term: {:?}",
                         name, violation
                     );
                 }
+                let in_has_value_use = find_non_callee_use(&desugared_in, name).is_some();
 
                 // Capture detection (against the *outer* scope, before
                 // the body-scope extension).
@@ -666,19 +670,75 @@ impl Desugarer {
                 let lifted_name = self.fresh_lifted(name);
 
                 // Rewrite (app name args) to (app lifted_name args... cap0
-                // cap1 ...) FIRST, then substitute name -> lifted_name
-                // everywhere (handles non-call references, but in 16b.2
-                // those are now ruled out by `find_non_callee_use` —
-                // the second pass remains for symmetry with 16b.1 and
-                // for the case where there are zero captures).
+                // cap1 ...) FIRST in body, then substitute name ->
+                // lifted_name everywhere (handles non-call references,
+                // but body name-as-value is rejected above so this is
+                // a defensive belt-and-braces pass).
                 let extras: Vec<String> =
                     capture_types.iter().map(|(n, _)| n.clone()).collect();
                 let body_call_rw =
                     subst_call_with_extras(&desugared_body, name, &lifted_name, &extras);
                 let body_full = subst_var(&body_call_rw, name, &lifted_name);
+
+                // 16b.5: rewrite call sites in `in_term` to the lifted
+                // name with captures appended. Do NOT run `subst_var` on
+                // `in_term` if there's a name-as-value use — we want
+                // those bare `Var{name}` references to resolve to the
+                // eta-Lam binding we add below. If there is no
+                // name-as-value use, we still skip subst_var (no leftover
+                // bare references exist after subst_call_with_extras).
                 let in_call_rw =
                     subst_call_with_extras(&desugared_in, name, &lifted_name, &extras);
-                let in_full = subst_var(&in_call_rw, name, &lifted_name);
+
+                // Effects on the LetRec's declared type — the eta-Lam
+                // inherits them so its body can call the lifted fn (which
+                // carries the same effects).
+                let lr_effects: Vec<String> = match peel_forall_to_fn(ty) {
+                    Some(Type::Fn { effects: es, .. }) => es.clone(),
+                    _ => vec![],
+                };
+
+                // Original LetRec param types and ret type — the eta-Lam's
+                // signature mirrors the LetRec's declared type so a value
+                // bound by `(let f (lam ...) ...)` has type Fn(t1..tk) -> tr.
+                let (orig_param_tys, orig_ret_ty): (Vec<Type>, Type) =
+                    match peel_forall_to_fn(ty) {
+                        Some(Type::Fn { params: ps, ret, .. }) => {
+                            (ps.clone(), (**ret).clone())
+                        }
+                        _ => unreachable!("ty shape validated above"),
+                    };
+
+                let in_full = if in_has_value_use {
+                    // Build the eta-Lam: `(lam (params P1..Pk -> RT) [effects]
+                    //   (app f$lr_N P1..Pk c1..cm))`. Param names reuse the
+                    // LetRec's original param names — fine because they
+                    // shadow only inside the Lam body.
+                    let lam_args: Vec<Term> = params
+                        .iter()
+                        .map(|p| Term::Var { name: p.clone() })
+                        .chain(extras.iter().map(|c| Term::Var { name: c.clone() }))
+                        .collect();
+                    let lam_body = Term::App {
+                        callee: Box::new(Term::Var { name: lifted_name.clone() }),
+                        args: lam_args,
+                        tail: false,
+                    };
+                    let eta_lam = Term::Lam {
+                        params: params.clone(),
+                        param_tys: orig_param_tys,
+                        ret_ty: Box::new(orig_ret_ty),
+                        effects: lr_effects,
+                        body: Box::new(lam_body),
+                    };
+                    Term::Let {
+                        name: name.clone(),
+                        value: Box::new(eta_lam),
+                        body: Box::new(in_call_rw),
+                    }
+                } else {
+                    in_call_rw
+                };
 
                 self.lifted.push(Def::Fn(FnDef {
                     name: lifted_name,
@@ -1818,16 +1878,16 @@ mod tests {
         );
     }
 
-    /// Iter 16b.2: if the LetRec name is used as a value (not as
-    /// the callee of an `app`), the lifter rejects with a `16b.5`
-    /// pointer (closure conversion). Here `(let g f ...)` binds the
-    /// LetRec name `f` to a let-bound name `g`, which is a value
-    /// position — not a callee.
+    /// Iter 16b.5: name-as-value INSIDE the LetRec's own body is
+    /// still rejected (would require an eta-Lam that calls the
+    /// pre-lift name — chicken-and-egg with the call-site rewrite).
+    /// Here `(let g f ...)` binds the LetRec name `f` to a let-bound
+    /// name `g`, which is a value position — not a callee.
     #[test]
     #[should_panic(expected = "16b.5")]
-    fn let_rec_name_as_value_panics() {
+    fn let_rec_name_as_value_in_body_panics() {
         // (let-rec f (params x) (type Int->Int)
-        //   (body (let g f (app g x)))   -- f used as a value
+        //   (body (let g f (app g x)))   -- f used as a value INSIDE body
         //   (in   (app f 1)))
         let letrec = Term::LetRec {
             name: "f".into(),
@@ -1871,6 +1931,105 @@ mod tests {
         let _ = desugar_module(&m);
     }
 
+    /// Iter 16b.5: name-as-value in the in-clause is now SUPPORTED.
+    /// The desugar pass lifts the LetRec to a synthetic top-level fn
+    /// AND wraps the rewritten in-term in `(let f (lam ...) ...)`
+    /// whose lam eta-expands the lifted fn. After desugar, the
+    /// surviving term tree contains:
+    ///   - one lifted fn `f$lr_N`
+    ///   - inside `main`, a `Term::Let { name: "f", value: Term::Lam,
+    ///     body: <rewritten in_term> }` where the Lam's body calls
+    ///     `f$lr_N` positionally.
+    #[test]
+    fn let_rec_name_as_value_in_in_term_wraps_to_eta_lam() {
+        // (let-rec f (params x) (type Int->Int)
+        //   (body (app f x))         -- only callee uses (legal)
+        //   (in   (let g f (app g 1))))   -- f used as a value
+        let letrec = Term::LetRec {
+            name: "f".into(),
+            ty: Type::Fn {
+                params: vec![Type::int()],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            params: vec!["x".into()],
+            body: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "f".into() }),
+                args: vec![Term::Var { name: "x".into() }],
+                tail: false,
+            }),
+            in_term: Box::new(Term::Let {
+                name: "g".into(),
+                value: Box::new(Term::Var { name: "f".into() }),
+                body: Box::new(Term::App {
+                    callee: Box::new(Term::Var { name: "g".into() }),
+                    args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
+                    tail: false,
+                }),
+            }),
+        };
+        let m = Module {
+            schema: crate::SCHEMA.to_string(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![Def::Fn(FnDef {
+                name: "main".into(),
+                ty: Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                params: vec![],
+                body: letrec,
+                doc: None,
+            })],
+        };
+        let out = desugar_module(&m);
+        // Two defs: original `main` + lifted `f$lr_0`.
+        assert_eq!(
+            out.defs.len(),
+            2,
+            "expected one lifted fn appended; got {:?}",
+            out.defs.iter().map(|d| d.name()).collect::<Vec<_>>()
+        );
+        let lifted_name = out.defs[1].name().to_string();
+        assert!(
+            lifted_name.starts_with("f$lr_"),
+            "unexpected lifted-name shape: {lifted_name}"
+        );
+        // main's body must be wrapped in `Let { name: "f", value: Lam, ... }`.
+        let main_body = match &out.defs[0] {
+            Def::Fn(fd) => &fd.body,
+            _ => unreachable!(),
+        };
+        match main_body {
+            Term::Let { name, value, .. } => {
+                assert_eq!(name, "f", "wrap name must be the original LetRec name");
+                match value.as_ref() {
+                    Term::Lam { params, body, .. } => {
+                        assert_eq!(params, &vec!["x".to_string()]);
+                        // The lam's body is `(app f$lr_0 x)` (no captures
+                        // here, so just original-params).
+                        match body.as_ref() {
+                            Term::App { callee, args, .. } => {
+                                match callee.as_ref() {
+                                    Term::Var { name: cn } => {
+                                        assert_eq!(cn, &lifted_name);
+                                    }
+                                    other => panic!("expected callee Var, got {other:?}"),
+                                }
+                                assert_eq!(args.len(), 1, "no captures expected");
+                            }
+                            other => panic!("expected lam body App, got {other:?}"),
+                        }
+                    }
+                    other => panic!("expected wrap value Lam, got {other:?}"),
+                }
+            }
+            other => panic!("expected wrap Let at main body, got {other:?}"),
+        }
+    }
+
     /// Iter 16c: walks a term, returns true iff any [`Pattern::Lit`] is
     /// reachable in any [`Term::Match`] arm. After 16c desugaring, the
     /// invariant is `false` for every desugared output — `Pattern::Lit`

docs/JOURNAL.md

@@ -4005,3 +4005,161 @@ strictly-nested non-mutual case but the mutual case needs joint
 lifting). 16d (chain-machinery exhaustiveness or
 `__unreachable__`), 16e (`==` extension to Bool/Str/Unit),
 17a (per-fn arena, gated) unchanged.
+
+## Iter 16b.5 — LetRec name as value (in_term only) via eta-Lam wrapper
+
+**Goal.** Lift the "callee-only use of the LetRec name" restriction
+for the **in-clause** of a `(let-rec ...)`. After this iter, the
+LetRec name `f` may appear in `in_term` as a value (e.g. passed to
+a higher-order combinator, bound to another `let`, stored in an ADT
+field). References to `f` as a value INSIDE the LetRec's own body
+remain rejected — that case has a chicken-and-egg with the call-site
+rewrite (the body's bare `f` references would need to call a name
+that doesn't exist before the lift) and is queued as a non-trivial
+extension.
+
+**Architectural choice (no new ABI).** Reuse the closure-pair
+machinery from Iter 8b (`lower_lambda` in `ailang-codegen`). After
+the existing 16b.2/16b.3 capture rewrite produces the lifted fn
+`f$lr_N(p1..pk, c1..cm) -> rt` and rewrites every `(app f a..)` →
+`(app f$lr_N a.. c1..cm)`, the lifter detects whether `in_term`
+contains any non-callee use of `f`. If yes, it WRAPS the rewritten
+in-term in
+
+```
+(let f
+   (lam (params p1..pk) (ret rt) (effects E)
+        (app f$lr_N p1..pk c1..cm))
+   <rewritten in_term>)
+```
+
+The Lam's free variables (the captures `c1..cm`) are picked up
+automatically by the existing 8b capture analysis in
+`lower_lambda`. The Lam's signature mirrors the LetRec's declared
+type, so any non-callee `Var{f}` in `in_term` resolves to a
+`Fn(t1..tk) -> rt ![E]` value — usable wherever the typechecker
+expects that type. Callee-position references in `in_term` are
+already rewritten to `f$lr_N` (no closure indirection at the call
+site; the wrap only affects value-position uses).
+
+The reduction is satisfying: 16b.5 reduces a problem that looked
+like it needed a new ABI to a problem already solved by Iter 8b.
+No closure ABI changes, no codegen plumbing, no LLVM IR change.
+
+**Where the wrap happens.** Two sites — both fast paths can
+encounter LetRecs with non-callee uses in in_term:
+
+1. **`crates/ailang-core/src/desugar.rs`** (~+50 LOC inside the
+   existing `Term::LetRec` arm). The body-side `find_non_callee_use`
+   panic was kept (now points at the body-only restriction rather
+   than the generic 16b.5 deferral). The in_term-side check no
+   longer panics; instead it sets a flag `in_has_value_use`. After
+   the standard call-site rewrite, when `in_has_value_use` is true,
+   the in-term is wrapped in a `Term::Let { name: f, value: Term::Lam,
+   body: <rewritten in_term> }`. The Lam's `effects` come from
+   `peel_forall_to_fn(ty)`. The defensive `subst_var` on `in_term`
+   is dropped — bare `Var{f}` references must reach the new
+   let-binding unchanged.
+
+2. **`crates/ailang-check/src/lift.rs`** (~+50 LOC inside the
+   existing post-typecheck LetRec arm). Symmetric to (1). The
+   wrap is identical in shape. The lift's effects come straight
+   from `ty` (already known to be `Type::Fn` at this point —
+   Forall is rejected upstream).
+
+**What stays rejected.**
+- `find_non_callee_use(body, name)` returns Some → panic with the
+  16b.5 body-only message: "name-as-value of a LetRec inside its
+  own body is not yet supported." Both sites.
+- `EnclosingLetRec` capture (16b.7) — unchanged.
+- Forall-typed LetRec (16b.6) — unchanged.
+
+**Did the codegen Lam machinery handle the wrapped form on the
+first try?** Yes. The eta-Lam is a perfectly ordinary `Term::Lam`
+whose body happens to be a single `Term::App` to a top-level
+synthetic fn with the lam's params + free-var captures appended.
+8b's `collect_captures` walks the Lam body, sees `f$lr_N` in
+top-level fns (it's been pushed to `module.defs` already), sees
+`p1..pk` in `bound`, and classifies the remaining `c1..cm` as
+captures — exactly right. No AST massaging was needed. The
+non-capture variant (no extras) reduces to the simplest possible
+Lam (params-only body), which 8b also handles trivially. End-to-end
+ran on first attempt for both fixtures.
+
+**What shipped.**
+
+- `crates/ailang-core/src/desugar.rs`: split `find_non_callee_use`
+  into body-only (panic) and in_term-only (sets a flag, then wraps
+  below). Drop the post-rewrite `subst_var` on the in-term — it
+  would otherwise rename the very `Var{f}` references that need to
+  resolve to the eta-Lam binding. Updated docstring on the
+  pre-existing panic test (`let_rec_name_as_value_panics` →
+  `let_rec_name_as_value_in_body_panics`) and added a new positive
+  unit test `let_rec_name_as_value_in_in_term_wraps_to_eta_lam`
+  that constructs an in_term-side value use and asserts the
+  resulting AST shape (lifted FnDef appended; main's body is
+  `Let { f, Lam{x -> App f$lr_0 x}, <rewritten body> }`).
+- `crates/ailang-check/src/lift.rs`: same split. Drop the
+  defensive `subst_var` on `in_term` when there's a value use;
+  keep it as no-op when there isn't (zero-capture symmetry).
+- `examples/local_rec_as_value.ailx` + `.ail.json`: factorial
+  bound by `(let-rec ...)` inside main, then in the in-clause
+  passed as a VALUE to a higher-order combinator
+  `apply5 : (Fn(Int) -> Int) -> Int`. No captures. Expected
+  stdout: `120` (= apply5(factorial) = factorial(5)).
+- `examples/local_rec_as_value_capture.ailx` + `.ail.json`:
+  variant with capture. `run_with_base(base)` builds a recursive
+  `factorial_plus` that uses `base` in its base case, then passes
+  the helper as a VALUE to `apply5`. The lifted fn is
+  `factorial_plus$lr_0(n: Int, base: Int) -> Int`; the eta-Lam
+  binds `factorial_plus` to a `(lam (n) (app
+  factorial_plus$lr_0 n base))` whose free var `base` becomes a
+  standard 8b closure-env capture. Expected stdout: `1320`
+  (= 5*4*3*2*(1+10)) and `12120` (= 5*4*3*2*(1+100)).
+- `crates/ail/tests/e2e.rs`: `local_rec_as_value_demo` and
+  `local_rec_as_value_capture_demo` (e2e count 41 → 43).
+- `crates/ailang-core/src/desugar.rs::tests`:
+  `let_rec_name_as_value_in_body_panics` (renamed from the
+  16b.2-era panic test; same fixture) and the new positive test
+  `let_rec_name_as_value_in_in_term_wraps_to_eta_lam` (desugar
+  count 10 → 11; net +1).
+
+**Cross-iter regression check.** All five existing LetRec/lit_pat
+fixtures (`local_rec_demo`, `local_rec_capture`,
+`local_rec_let_capture`, `local_rec_match_capture`, `lit_pat`)
+build, run, and produce identical stdout. Their on-disk hashes
+(reported via `ail manifest`) are unchanged because the desugar
+pass runs after `load_module` and never touches canonical bytes.
+
+**Tests: 113 → 116 (+3).**
+
+- e2e: 41 → 43 (`local_rec_as_value_demo`,
+  `local_rec_as_value_capture_demo`).
+- `ailang-core::desugar::tests`: 10 → 11 (one rename + one new
+  positive test). Net +1.
+
+**Cumulative state, post-16b.5.**
+
+- Stdlib unchanged (5 modules, 29 combinators).
+- `Term` enum: 11 variants (unchanged). All pre-16b.5 fixture
+  hashes bit-identical.
+- Compiler stages: load → desugar → typecheck → lift_letrecs →
+  codegen (unchanged from 16b.3).
+- The four `unreachable!("Term::LetRec eliminated by desugar")`
+  arms in `ailang-codegen` are still correct — by the time
+  codegen runs, no LetRec survives. The eta-Lam is a `Term::Lam`,
+  which has its own well-trodden codegen path.
+- DESIGN.md unchanged. Pipeline is unchanged.
+- Compiler bugs surfaced and fixed in dogfood since 14a: 5/5
+  (unchanged).
+
+**Queue update post-16b.5.** 16b.5 done for the in_term-only
+slice. Open: **16b.5-body** (informal — not formally numbered;
+"non-trivial extension" per the orchestrator's brief), where the
+LetRec name is used as a value INSIDE its own body. Solving that
+needs either eta-conversion-of-self (the body's `f` would resolve
+to a fresh Lam built around the lifted callee, but constructing it
+inside the body before the lift completes is order-sensitive) or
+a true closure conversion that doesn't lift to a top-level fn at
+all. **16b.6** (Forall-typed LetRec), **16b.7** (nested mutual
+LetRec capture), 16d, 16e, 17a unchanged.

examples/local_rec_as_value.ail.json

@@ -0,0 +1 @@
+{"defs":[{"body":{"args":[{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"f","t":"var"},"t":"app"},"doc":"Higher-order: applies its fn argument to 5.","kind":"fn","name":"apply5","params":["f"],"type":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"cond":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"<=","t":"var"},"t":"app"},"else":{"args":[{"name":"n","t":"var"},{"args":[{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"}],"fn":{"name":"factorial","t":"var"},"t":"app"}],"fn":{"name":"*","t":"var"},"t":"app"},"t":"if","then":{"lit":{"kind":"int","value":1},"t":"lit"}},"in":{"args":[{"args":[{"name":"factorial","t":"var"}],"fn":{"name":"apply5","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"name":"factorial","params":["n"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},"doc":"Iter 16b.5: pass a let-rec'd factorial as a value to apply5. Expected stdout: 120.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"local_rec_as_value","schema":"ailang/v0"}

examples/local_rec_as_value.ailx

@@ -0,0 +1,33 @@
+; Iter 16b.5 — LetRec name as value (in_term, no capture).
+; A recursive `factorial` is bound by `(let-rec ...)` inside `main`,
+; then in the in-clause it is passed as a VALUE to a higher-order
+; combinator `apply5` (which expects `Fn(Int) -> Int`). Without
+; 16b.5, the desugar pass would panic with the "name-as-value not
+; supported" message. With 16b.5 it wraps the in-term in
+; `(let factorial (lam ...) ...)` whose lam eta-expands the lifted
+; top-level fn — so `factorial` reaches `apply5` as a closure-pair
+; value just like any other fn-value (Iter 7/8b ABI).
+;
+; Expected stdout: 120 (= apply5 factorial = factorial 5).
+
+(module local_rec_as_value
+
+  (fn apply5
+    (doc "Higher-order: applies its fn argument to 5.")
+    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int)))) (ret (con Int))))
+    (params f)
+    (body (app f 5)))
+
+  (fn main
+    (doc "Iter 16b.5: pass a let-rec'd factorial as a value to apply5. Expected stdout: 120.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let-rec factorial
+        (params n)
+        (type (fn-type (params (con Int)) (ret (con Int))))
+        (body
+          (if (app <= n 1)
+            1
+            (app * n (app factorial (app - n 1)))))
+        (in (do io/print_int (app apply5 factorial)))))))

examples/local_rec_as_value_capture.ail.json

@@ -0,0 +1 @@
+{"defs":[{"body":{"args":[{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"f","t":"var"},"t":"app"},"doc":"Higher-order: applies its fn argument to 5.","kind":"fn","name":"apply5","params":["f"],"type":{"effects":[],"k":"fn","params":[{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"cond":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"<=","t":"var"},"t":"app"},"else":{"args":[{"name":"n","t":"var"},{"args":[{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"}],"fn":{"name":"factorial_plus","t":"var"},"t":"app"}],"fn":{"name":"*","t":"var"},"t":"app"},"t":"if","then":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"},{"name":"base","t":"var"}],"fn":{"name":"+","t":"var"},"t":"app"}},"in":{"args":[{"name":"factorial_plus","t":"var"}],"fn":{"name":"apply5","t":"var"},"t":"app"},"name":"factorial_plus","params":["n"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},"doc":"Build a recursive helper that captures `base` and pass it as a value to apply5.","kind":"fn","name":"run_with_base","params":["base"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"run_with_base","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"int","value":100},"t":"lit"}],"fn":{"name":"run_with_base","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"doc":"Iter 16b.5: pass a capturing let-rec helper as a value. Expected stdout: 1320, 12120.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"local_rec_as_value_capture","schema":"ailang/v0"}

examples/local_rec_as_value_capture.ailx

@@ -0,0 +1,43 @@
+; Iter 16b.5 — LetRec name as value, with capture. A recursive
+; helper `factorial_plus` captures the outer fn-param `base` and is
+; passed as a VALUE to a higher-order combinator. The lifted fn has
+; signature `factorial_plus$lr_N(n: Int, base: Int) -> Int`. The
+; eta-Lam wrap binds `factorial_plus` in the in-clause to a
+; `(lam (n) (app factorial_plus$lr_N n base))` — the Lam's free var
+; `base` becomes a closure-env capture under the standard 8b ABI.
+; This exercises the dynamic-env path (lifted fn has extra params,
+; the eta-Lam captures them).
+;
+; Expected stdout (one per line):
+;   apply5(factorial_plus[base=10])  = 5*4*3*2*(1+10)  = 1320
+;   apply5(factorial_plus[base=100]) = 5*4*3*2*(1+100) = 12120
+
+(module local_rec_as_value_capture
+
+  (fn apply5
+    (doc "Higher-order: applies its fn argument to 5.")
+    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int)))) (ret (con Int))))
+    (params f)
+    (body (app f 5)))
+
+  (fn run_with_base
+    (doc "Build a recursive helper that captures `base` and pass it as a value to apply5.")
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params base)
+    (body
+      (let-rec factorial_plus
+        (params n)
+        (type (fn-type (params (con Int)) (ret (con Int))))
+        (body
+          (if (app <= n 1)
+            (app + 1 base)
+            (app * n (app factorial_plus (app - n 1)))))
+        (in (app apply5 factorial_plus)))))
+
+  (fn main
+    (doc "Iter 16b.5: pass a capturing let-rec helper as a value. Expected stdout: 1320, 12120.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (seq (do io/print_int (app run_with_base 10))
+           (do io/print_int (app run_with_base 100))))))