Iter 16b.2 — LetRec captures of fn-params (path-1 safe subset)

Lift 16b.1's no-capture restriction. The desugar pass's `scope`
becomes a `BTreeMap<String, ScopeEntry>` carrying `KnownType` for
fn/Lam-params, sentinels for Let-/Match-bindings. LetRec captures
of `KnownType` names are lifted: the synthetic top-level fn's
signature gets the capture types appended, and every call site of
the LetRec name is rewritten via `subst_call_with_extras` to pass
the captures positionally. Captures from let-bindings, match-arm
patterns, polymorphic enclosing fns, and name-as-value uses are
rejected at desugar with panics pointing at 16b.3-16b.7.

Demo: `sum_below(n)` recurses via `(let-rec loop (params i) ...
(body ... uses n ...) (in (app loop 1)))`. Lifts to
`loop$lr_0(i: Int, n: Int) -> Int` with `(app loop X)` rewritten
to `(app loop$lr_0 X n)`. Outputs 0, 10, 45.

Tests: 103 -> 106 (+1 e2e local_rec_capture_demo, +2 desugar unit;
the 16b.1 capture-panic test was repurposed into the positive
fn-param-capture test).

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

crates/ail/tests/e2e.rs

@@ -450,6 +450,23 @@ fn local_rec_factorial_demo() {
     assert_eq!(lines, vec!["1", "6", "120"]);
 }
 
+/// Iter 16b.2: LetRec capture of a fn-param (path-1 safe subset).
+/// Property protected: the desugar pass lifts a LetRec whose body
+/// captures one or more enclosing-scope names (here: `n` from
+/// `sum_below`'s params) into a synthetic top-level fn whose
+/// signature has the capture types appended, and rewrites every
+/// call site of the LetRec name in body and in_term to pass the
+/// captures positionally as extra args. Without 16b.2, the
+/// 16b.1-era panic ("would capture") would fire and the build
+/// would fail. Three call sites: sum_below(1)=0, sum_below(5)=10,
+/// sum_below(10)=45.
+#[test]
+fn local_rec_capture_demo() {
+    let stdout = build_and_run("local_rec_capture.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["0", "10", "45"]);
+}
+
 /// 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-core/src/desugar.rs

@@ -102,7 +102,36 @@
 //!   bodies that capture from the enclosing scope (queued as 16b.2).
 
 use crate::ast::*;
-use std::collections::BTreeSet;
+use std::collections::{BTreeMap, BTreeSet};
+
+/// Iter 16b.2: per-name scope information used by the LetRec lifter.
+/// `KnownType(t)` is set for fn-params and Lam-params, where the
+/// type is statically declared. Other binder kinds use the
+/// placeholder variants and the LetRec lifter rejects captures of
+/// those names with a clear error pointing at the follow-up iter
+/// that will lift the restriction.
+#[derive(Debug, Clone)]
+enum ScopeEntry {
+    /// Fn-param or Lam-param, type known at this point.
+    KnownType(Type),
+    /// Bound by `Term::Let` — value's type is inferred at
+    /// typecheck, unknown at desugar. Captures error → 16b.3.
+    /// Also used for fn-params of a `Type::Forall`-typed enclosing
+    /// fn, where the param types may mention outer type vars and
+    /// the lifted signature would need a synthesized `Forall` —
+    /// out of scope for 16b.2 (queued for 16b.6).
+    LetBound,
+    /// Bound by a `Term::Match` arm pattern — type would require
+    /// constructor-field substitution from the scrutinee. Not
+    /// computed in this iter. Captures error → 16b.4.
+    MatchArm,
+    /// Bound by a `Term::LetRec` (its own name) — fn-typed, but
+    /// the value flows through a recursive position; supported
+    /// for fn/Lam-param transitivity but not for nested-LetRec
+    /// mutual capture. The LetRec lifter rejects captures of a
+    /// name with this entry → 16b.7.
+    EnclosingLetRec,
+}
 
 /// Rewrite `m` so that every [`Pattern::Ctor`] sub-pattern is a
 /// [`Pattern::Var`] or [`Pattern::Wild`] (i.e. flat) and every
@@ -151,11 +180,41 @@ pub fn desugar_module(m: &Module) -> Module {
     for def in &mut out.defs {
         match def {
             Def::Fn(f) => {
-                let scope: BTreeSet<String> = f.params.iter().cloned().collect();
+                // Iter 16b.2: build initial scope from fn-params with
+                // their declared types (peeled out of `f.ty`). For a
+                // `Type::Forall`-quantified fn, the param types may
+                // mention outer type vars; constructing a lifted
+                // `Forall` signature is out of scope for 16b.2, so
+                // every param of a polymorphic enclosing fn enters
+                // the scope as `LetBound` — captures of those names
+                // by an inner LetRec are rejected at the same site
+                // as let-binding captures.
+                let mut scope: BTreeMap<String, ScopeEntry> = BTreeMap::new();
+                match &f.ty {
+                    Type::Fn { params: ptys, .. } if ptys.len() == f.params.len() => {
+                        for (p, pty) in f.params.iter().zip(ptys.iter()) {
+                            scope.insert(p.clone(), ScopeEntry::KnownType(pty.clone()));
+                        }
+                    }
+                    Type::Forall { .. } => {
+                        for p in &f.params {
+                            scope.insert(p.clone(), ScopeEntry::LetBound);
+                        }
+                    }
+                    _ => {
+                        // Defensive: if the fn type is malformed (e.g.
+                        // arity mismatch, non-Fn). Fall back to LetBound
+                        // for every param so captures are rejected
+                        // cleanly rather than silently mistyped.
+                        for p in &f.params {
+                            scope.insert(p.clone(), ScopeEntry::LetBound);
+                        }
+                    }
+                }
                 f.body = d.desugar_term(&f.body, &scope);
             }
             Def::Const(c) => {
-                let scope: BTreeSet<String> = BTreeSet::new();
+                let scope: BTreeMap<String, ScopeEntry> = BTreeMap::new();
                 c.value = d.desugar_term(&c.value, &scope);
             }
             Def::Type(_) => {}
@@ -309,15 +368,20 @@ impl Desugarer {
     /// Recursively rewrites `t`: descends into every child first
     /// (bottom-up), then dispatches a [`Term::Match`] to
     /// [`desugar_match`](Self::desugar_match) and a [`Term::LetRec`]
-    /// to the 16b.1 lifter.
+    /// to the 16b.1 / 16b.2 lifter.
     ///
-    /// `scope` is the set of names lexically bound at this point —
-    /// initialised at the def boundary (fn params for [`Def::Fn`],
-    /// empty for [`Def::Const`]) and extended locally by every
-    /// binder ([`Term::Let`], [`Term::Lam`], [`Term::Match`] arms,
-    /// [`Term::LetRec`]). Used by the LetRec lifter to detect
-    /// captures.
-    fn desugar_term(&mut self, t: &Term, scope: &BTreeSet<String>) -> Term {
+    /// `scope` maps every name lexically bound at this point to its
+    /// [`ScopeEntry`] — initialised at the def boundary (fn-params
+    /// with `KnownType` for monomorphic enclosing fns; `LetBound`
+    /// for `Type::Forall`-quantified ones; empty for [`Def::Const`])
+    /// and extended locally by every binder ([`Term::Let`] →
+    /// `LetBound`; [`Term::Lam`] → `KnownType`; [`Term::Match`] arm
+    /// pattern bindings → `MatchArm`; [`Term::LetRec`] → its own
+    /// name as `EnclosingLetRec`, params as `KnownType`). Used by
+    /// the LetRec lifter (16b.2) to classify each capture and
+    /// either accept it (KnownType) or reject with a clear error
+    /// pointing at the follow-up iter.
+    fn desugar_term(&mut self, t: &Term, scope: &BTreeMap<String, ScopeEntry>) -> Term {
         match t {
             Term::Lit { .. } | Term::Var { .. } => t.clone(),
             Term::App { callee, args, tail } => Term::App {
@@ -328,7 +392,7 @@ impl Desugarer {
             Term::Let { name, value, body } => {
                 let v = self.desugar_term(value, scope);
                 let mut inner = scope.clone();
-                inner.insert(name.clone());
+                inner.insert(name.clone(), ScopeEntry::LetBound);
                 let b = self.desugar_term(body, &inner);
                 Term::Let {
                     name: name.clone(),
@@ -358,7 +422,11 @@ impl Desugarer {
                     .iter()
                     .map(|a| {
                         let mut inner = scope.clone();
-                        pattern_binds(&a.pat, &mut inner);
+                        let mut pat_binds: BTreeSet<String> = BTreeSet::new();
+                        pattern_binds(&a.pat, &mut pat_binds);
+                        for n in pat_binds {
+                            inner.insert(n, ScopeEntry::MatchArm);
+                        }
                         Arm {
                             pat: a.pat.clone(),
                             body: self.desugar_term(&a.body, &inner),
@@ -375,8 +443,8 @@ impl Desugarer {
                 body,
             } => {
                 let mut inner = scope.clone();
-                for p in params {
-                    inner.insert(p.clone());
+                for (p, pty) in params.iter().zip(param_tys.iter()) {
+                    inner.insert(p.clone(), ScopeEntry::KnownType(pty.clone()));
                 }
                 Term::Lam {
                     params: params.clone(),
@@ -391,26 +459,49 @@ impl Desugarer {
                 rhs: Box::new(self.desugar_term(rhs, scope)),
             },
             Term::LetRec { name, ty, params, body, in_term } => {
-                // Iter 16b.1: lift to a synthetic top-level fn.
-                //
-                // Body's scope: outer ∪ {name} ∪ params (recursive
-                // self-reference is legal; params shadow outer names).
+                // Iter 16b.1: lift to a synthetic top-level fn (no-capture).
+                // Iter 16b.2: extend the lift to the path-1 safe subset —
+                // captures of fn-params / Lam-params (whose types are
+                // known statically). Captures of Let / MatchArm /
+                // EnclosingLetRec names, captures from a polymorphic
+                // enclosing fn, and any non-callee use of `name` are
+                // still rejected at desugar time, with a follow-up
+                // iter pointer in the panic message.
+
+                // Peel `ty` to its inner Fn so we know the LetRec's
+                // own param types (for body-scope) and so we can
+                // detect a Forall LetRec early.
+                let inner_params_tys: Vec<Type> = match peel_forall_to_fn(ty) {
+                    Some(Type::Fn { params: ps, .. }) => ps.clone(),
+                    _ => panic!(
+                        "Iter 16b.2: LetRec `{}` must have a Fn type (or Forall<Fn>); got {:?}",
+                        name, ty
+                    ),
+                };
+                if inner_params_tys.len() != params.len() {
+                    panic!(
+                        "Iter 16b.2: LetRec `{}` param count {} != type's param count {}",
+                        name, params.len(), inner_params_tys.len()
+                    );
+                }
+
+                // Body's scope: outer ∪ {name → EnclosingLetRec} ∪
+                // params with their declared types as KnownType.
                 let mut body_scope = scope.clone();
-                body_scope.insert(name.clone());
-                for p in params {
-                    body_scope.insert(p.clone());
+                body_scope.insert(name.clone(), ScopeEntry::EnclosingLetRec);
+                for (p, pty) in params.iter().zip(inner_params_tys.iter()) {
+                    body_scope.insert(p.clone(), ScopeEntry::KnownType(pty.clone()));
                 }
                 let desugared_body = self.desugar_term(body, &body_scope);
-                // in_term's scope: outer ∪ {name} (params are lambda-
-                // local to the LetRec's body, not visible in `in`).
+                // in_term's scope: outer ∪ {name → EnclosingLetRec}
+                // (params are lambda-local to the LetRec's body,
+                // not visible in `in`).
                 let mut in_scope = scope.clone();
-                in_scope.insert(name.clone());
+                in_scope.insert(name.clone(), ScopeEntry::EnclosingLetRec);
                 let desugared_in = self.desugar_term(in_term, &in_scope);
 
-                // Capture detection: free vars of the desugared body
-                // wrt {name} ∪ params, intersected with the outer
-                // `scope`. Anything in that intersection is a capture
-                // (16b.2 territory).
+                // Capture detection (against the *outer* scope, before
+                // the body-scope extension).
                 let mut local_bound: BTreeSet<String> = BTreeSet::new();
                 local_bound.insert(name.clone());
                 for p in params {
@@ -418,30 +509,125 @@ impl Desugarer {
                 }
                 let mut frees: BTreeSet<String> = BTreeSet::new();
                 free_vars_in_term(&desugared_body, &local_bound, &mut frees);
-                let captures: Vec<String> = frees.intersection(scope).cloned().collect();
-                if !captures.is_empty() {
+                let captures: Vec<String> = frees
+                    .iter()
+                    .filter(|f| scope.contains_key(*f))
+                    .cloned()
+                    .collect();
+
+                // 16b.2: classify each capture's ScopeEntry. KnownType
+                // is supported; everything else errors with a follow-up
+                // iter pointer.
+                let mut capture_types: Vec<(String, Type)> = Vec::new();
+                for c in &captures {
+                    match scope.get(c).expect("capture-in-scope-by-construction") {
+                        ScopeEntry::KnownType(t) => {
+                            capture_types.push((c.clone(), t.clone()));
+                        }
+                        ScopeEntry::LetBound => panic!(
+                            "Iter 16b.2: LetRec `{}` captures `{}` from a let-binding \
+                             (or polymorphic enclosing fn); not supported. Queued for \
+                             16b.3 (let-binding captures with type info from typecheck).",
+                            name, c
+                        ),
+                        ScopeEntry::MatchArm => panic!(
+                            "Iter 16b.2: LetRec `{}` captures `{}` from a match-arm \
+                             pattern binding; not supported. Queued for 16b.4 (match-arm \
+                             captures with constructor-field substitution).",
+                            name, c
+                        ),
+                        ScopeEntry::EnclosingLetRec => panic!(
+                            "Iter 16b.2: LetRec `{}` captures `{}` from an enclosing \
+                             LetRec; nested mutual-capture is not supported. Queued for \
+                             16b.7.",
+                            name, c
+                        ),
+                    }
+                }
+
+                // 16b.2: 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. This guards
+                // against `(let g f ...)` bindings and `(app some_hof
+                // f)` value-passing, which would need closure
+                // conversion.
+                if let Some(violation) = find_non_callee_use(&desugared_body, name) {
                     panic!(
-                        "Iter 16b.1: local recursive `let` `{}` would capture {:?} \
-                         from enclosing scope; capture is queued for 16b.2. Lift \
-                         the helper to top-level for now.",
-                        name, captures
+                        "Iter 16b.2: 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.2: LetRec `{}` is used as a value in the in-clause \
+                         (not as the callee of `app`); not supported. Queued for 16b.5. \
+                         Offending term: {:?}",
+                        name, violation
                     );
                 }
 
-                // Lift: synthesise a fresh top-level def name and
-                // substitute every reference to the local `name`
-                // (in body and in_term) to the lifted name.
+                // Build augmented type: original Fn with capture types
+                // appended to `params`. A Forall LetRec is rejected
+                // (would need synthesised Forall — out of scope).
+                let augmented_ty = match ty {
+                    Type::Fn { params: ps, ret, effects } => {
+                        let mut new_ps = ps.clone();
+                        for (_, t) in &capture_types {
+                            new_ps.push(t.clone());
+                        }
+                        Type::Fn {
+                            params: new_ps,
+                            ret: ret.clone(),
+                            effects: effects.clone(),
+                        }
+                    }
+                    Type::Forall { .. } => panic!(
+                        "Iter 16b.2: LetRec `{}` has a Forall type; captures from a \
+                         polymorphic context are not supported. Queued for 16b.6.",
+                        name
+                    ),
+                    other => panic!(
+                        "Iter 16b.2: LetRec `{}` has non-Fn/Forall type {:?}",
+                        name, other
+                    ),
+                };
+                // Augmented param-name list: original params + capture
+                // names (using the captured variable names directly so
+                // the lifted body's references already resolve
+                // correctly).
+                let mut augmented_params = params.clone();
+                for (cn, _) in &capture_types {
+                    augmented_params.push(cn.clone());
+                }
+
+                // Lift.
                 let lifted_name = self.fresh_lifted(name);
-                let body_lifted = subst_var(&desugared_body, name, &lifted_name);
-                let in_lifted = subst_var(&desugared_in, name, &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).
+                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);
+                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);
+
                 self.lifted.push(Def::Fn(FnDef {
                     name: lifted_name,
-                    ty: ty.clone(),
-                    params: params.clone(),
-                    body: body_lifted,
+                    ty: augmented_ty,
+                    params: augmented_params,
+                    body: body_full,
                     doc: None,
                 }));
-                in_lifted
+                in_full
             }
         }
     }
@@ -844,6 +1030,158 @@ fn subst_var(t: &Term, from: &str, to: &str) -> Term {
     }
 }
 
+/// Iter 16b.2: peel a `Type::Forall { body: Type::Fn { ... } }` to
+/// expose the inner `Type::Fn`. Returns `Some(&Type::Fn)` if the
+/// type is `Fn` or `Forall<Fn>`; `None` otherwise.
+fn peel_forall_to_fn(t: &Type) -> Option<&Type> {
+    match t {
+        Type::Fn { .. } => Some(t),
+        Type::Forall { body, .. } => peel_forall_to_fn(body),
+        _ => None,
+    }
+}
+
+/// Iter 16b.2: walk `t` and rewrite every `Term::App { callee =
+/// Var{name}, args }` to `Term::App { callee = Var{lifted}, args =
+/// args ++ extras_as_vars }`. Recurses into all sub-terms. Does
+/// not touch `Term::Var { name }` in non-callee positions — that's
+/// flagged separately by [`find_non_callee_use`].
+fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[String]) -> Term {
+    match t {
+        Term::Lit { .. } => t.clone(),
+        Term::Var { .. } => t.clone(),
+        Term::App { callee, args, tail } => {
+            let mut new_args: Vec<Term> = args
+                .iter()
+                .map(|a| subst_call_with_extras(a, name, lifted, extras))
+                .collect();
+            let new_callee = match callee.as_ref() {
+                Term::Var { name: n } if n == name => {
+                    // Append extras as Var references — at this site,
+                    // the captured variable names are still in scope
+                    // because the lifted fn appends them as extra
+                    // params with the same names.
+                    for ex in extras {
+                        new_args.push(Term::Var { name: ex.clone() });
+                    }
+                    Box::new(Term::Var { name: lifted.to_string() })
+                }
+                _ => Box::new(subst_call_with_extras(callee, name, lifted, extras)),
+            };
+            Term::App {
+                callee: new_callee,
+                args: new_args,
+                tail: *tail,
+            }
+        }
+        Term::Let { name: n, value, body } => Term::Let {
+            name: n.clone(),
+            value: Box::new(subst_call_with_extras(value, name, lifted, extras)),
+            body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
+        },
+        Term::If { cond, then, else_ } => Term::If {
+            cond: Box::new(subst_call_with_extras(cond, name, lifted, extras)),
+            then: Box::new(subst_call_with_extras(then, name, lifted, extras)),
+            else_: Box::new(subst_call_with_extras(else_, name, lifted, extras)),
+        },
+        Term::Do { op, args, tail } => Term::Do {
+            op: op.clone(),
+            args: args
+                .iter()
+                .map(|a| subst_call_with_extras(a, name, lifted, extras))
+                .collect(),
+            tail: *tail,
+        },
+        Term::Ctor { type_name, ctor, args } => Term::Ctor {
+            type_name: type_name.clone(),
+            ctor: ctor.clone(),
+            args: args
+                .iter()
+                .map(|a| subst_call_with_extras(a, name, lifted, extras))
+                .collect(),
+        },
+        Term::Match { scrutinee, arms } => Term::Match {
+            scrutinee: Box::new(subst_call_with_extras(scrutinee, name, lifted, extras)),
+            arms: arms
+                .iter()
+                .map(|a| Arm {
+                    pat: a.pat.clone(),
+                    body: subst_call_with_extras(&a.body, name, lifted, extras),
+                })
+                .collect(),
+        },
+        Term::Lam {
+            params,
+            param_tys,
+            ret_ty,
+            effects,
+            body,
+        } => Term::Lam {
+            params: params.clone(),
+            param_tys: param_tys.clone(),
+            ret_ty: ret_ty.clone(),
+            effects: effects.clone(),
+            body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
+        },
+        Term::Seq { lhs, rhs } => Term::Seq {
+            lhs: Box::new(subst_call_with_extras(lhs, name, lifted, extras)),
+            rhs: Box::new(subst_call_with_extras(rhs, name, lifted, extras)),
+        },
+        Term::LetRec { name: n, ty, params, body, in_term } => Term::LetRec {
+            name: n.clone(),
+            ty: ty.clone(),
+            params: params.clone(),
+            body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
+            in_term: Box::new(subst_call_with_extras(in_term, name, lifted, extras)),
+        },
+    }
+}
+
+/// Iter 16b.2: returns `Some(t)` if `t` contains a `Term::Var {
+/// name }` reference in a position that is **not** the callee of a
+/// `Term::App`. Returns `None` if every reference is in callee
+/// position. Used by the LetRec lifter to enforce the "direct-call
+/// only" restriction in 16b.2.
+fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
+    match t {
+        Term::Lit { .. } => None,
+        Term::Var { name: n } if n == name => Some(t.clone()),
+        Term::Var { .. } => None,
+        Term::App { callee, args, .. } => {
+            // Allowed: callee = Var{name}. Args are checked normally.
+            // Disallowed: callee != Var{name} but recursing into the
+            // callee surfaces the name as a non-callee position.
+            if !matches!(callee.as_ref(), Term::Var { name: n } if n == name) {
+                if let Some(v) = find_non_callee_use(callee, name) {
+                    return Some(v);
+                }
+            }
+            for a in args {
+                if let Some(v) = find_non_callee_use(a, name) {
+                    return Some(v);
+                }
+            }
+            None
+        }
+        Term::Let { value, body, .. } => {
+            find_non_callee_use(value, name).or_else(|| find_non_callee_use(body, name))
+        }
+        Term::If { cond, then, else_ } => find_non_callee_use(cond, name)
+            .or_else(|| find_non_callee_use(then, name))
+            .or_else(|| find_non_callee_use(else_, name)),
+        Term::Do { args, .. } => args.iter().find_map(|a| find_non_callee_use(a, name)),
+        Term::Ctor { args, .. } => args.iter().find_map(|a| find_non_callee_use(a, name)),
+        Term::Match { scrutinee, arms } => find_non_callee_use(scrutinee, name)
+            .or_else(|| arms.iter().find_map(|a| find_non_callee_use(&a.body, name))),
+        Term::Lam { body, .. } => find_non_callee_use(body, name),
+        Term::Seq { lhs, rhs } => {
+            find_non_callee_use(lhs, name).or_else(|| find_non_callee_use(rhs, name))
+        }
+        Term::LetRec { body, in_term, .. } => find_non_callee_use(body, name)
+            .or_else(|| find_non_callee_use(in_term, name)),
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -1103,25 +1441,30 @@ mod tests {
         }
     }
 
-    /// Iter 16b.1: a LetRec whose body references a var bound in the
-    /// enclosing scope (here, `outer` is a parameter of the
-    /// surrounding fn) panics at desugar time. 16b.2 will lift this.
+    /// Iter 16b.2: a LetRec whose body captures a fn-param of the
+    /// enclosing scope (here, `outer` is a parameter of `main`) is
+    /// **lifted** with the capture appended to the lifted fn's
+    /// signature. The original 16b.1 panic ("would capture") is
+    /// gone for fn-param captures; this test was renamed and
+    /// repurposed to assert the lift succeeds and produces the
+    /// expected augmented signature + call-site rewrite.
     #[test]
-    #[should_panic(expected = "would capture")]
-    fn let_rec_with_capture_panics() {
+    fn let_rec_capture_fn_param_lifts_with_extra_arg() {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
-                name: "main".into(),
+                name: "outer".into(),
                 ty: Type::Fn {
                     params: vec![Type::int()],
                     ret: Box::new(Type::int()),
                     effects: vec![],
                 },
-                params: vec!["outer".into()],
-                // (let-rec helper (params x) ... (body (app + x outer)) ...)
+                params: vec!["n".into()],
+                // (let-rec helper (params x) (type Int -> Int)
+                //   (body (app + x n))     -- captures `n`
+                //   (in (app helper 5)))
                 body: Term::LetRec {
                     name: "helper".into(),
                     ty: Type::Fn {
@@ -1134,19 +1477,188 @@ mod tests {
                         callee: Box::new(Term::Var { name: "+".into() }),
                         args: vec![
                             Term::Var { name: "x".into() },
-                            Term::Var { name: "outer".into() },
+                            Term::Var { name: "n".into() },
                         ],
                         tail: false,
                     }),
                     in_term: Box::new(Term::App {
                         callee: Box::new(Term::Var { name: "helper".into() }),
-                        args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
+                        args: vec![Term::Lit { lit: Literal::Int { value: 5 } }],
                         tail: false,
                     }),
                 },
                 doc: None,
             })],
         };
+        let out = desugar_module(&m);
+        // (a) two defs: original outer + lifted helper.
+        assert_eq!(out.defs.len(), 2, "expected one lifted fn appended");
+        let lifted = match &out.defs[1] {
+            Def::Fn(f) => f,
+            _ => panic!("expected lifted FnDef"),
+        };
+        // (b) lifted ty has the capture type appended.
+        assert_eq!(
+            lifted.ty,
+            Type::Fn {
+                params: vec![Type::int(), Type::int()],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            "lifted fn type should have capture appended; got {:?}",
+            lifted.ty
+        );
+        // (b') param-name list has the capture name appended.
+        assert_eq!(lifted.params, vec!["x".to_string(), "n".to_string()]);
+        // (c) the lifted body is `(app + x n)` — `n` is now a
+        // fn-param of the lifted def, so the body is unchanged.
+        match &lifted.body {
+            Term::App { callee, args, .. } => {
+                match callee.as_ref() {
+                    Term::Var { name } => assert_eq!(name, "+"),
+                    other => panic!("expected `+` callee, got {other:?}"),
+                }
+                assert_eq!(args.len(), 2);
+                match &args[0] {
+                    Term::Var { name } => assert_eq!(name, "x"),
+                    other => panic!("expected x, got {other:?}"),
+                }
+                match &args[1] {
+                    Term::Var { name } => assert_eq!(name, "n"),
+                    other => panic!("expected n, got {other:?}"),
+                }
+            }
+            other => panic!("expected lifted body to be App, got {other:?}"),
+        }
+        // (d) `outer`'s body is now `(app helper$lr_0 5 n)` —
+        // call-site got the capture appended.
+        let outer_body = match &out.defs[0] {
+            Def::Fn(f) => &f.body,
+            _ => unreachable!(),
+        };
+        match outer_body {
+            Term::App { callee, args, .. } => {
+                match callee.as_ref() {
+                    Term::Var { name } => assert_eq!(name, &lifted.name),
+                    other => panic!("expected lifted callee, got {other:?}"),
+                }
+                assert_eq!(args.len(), 2, "expected 2 args (1 original + 1 capture)");
+                match &args[0] {
+                    Term::Lit { lit: Literal::Int { value: 5 } } => {}
+                    other => panic!("expected 5, got {other:?}"),
+                }
+                match &args[1] {
+                    Term::Var { name } => assert_eq!(name, "n"),
+                    other => panic!("expected n, got {other:?}"),
+                }
+            }
+            other => panic!("expected outer body to be App, got {other:?}"),
+        }
+    }
+
+    /// Iter 16b.2: a LetRec whose body captures a `Term::Let`-bound
+    /// name has no statically-known type at desugar time; the
+    /// lifter rejects with a `16b.3` pointer.
+    #[test]
+    #[should_panic(expected = "16b.3")]
+    fn let_rec_capture_let_binding_panics() {
+        // (let y 7 in (let-rec helper (params x) ... (body (app + x y))
+        //                                       (in  (app helper 1))))
+        let letrec = Term::LetRec {
+            name: "helper".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: "+".into() }),
+                args: vec![
+                    Term::Var { name: "x".into() },
+                    Term::Var { name: "y".into() },
+                ],
+                tail: false,
+            }),
+            in_term: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "helper".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: Term::Let {
+                    name: "y".into(),
+                    value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
+                    body: Box::new(letrec),
+                },
+                doc: None,
+            })],
+        };
+        let _ = desugar_module(&m);
+    }
+
+    /// 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.
+    #[test]
+    #[should_panic(expected = "16b.5")]
+    fn let_rec_name_as_value_panics() {
+        // (let-rec f (params x) (type Int->Int)
+        //   (body (let g f (app g x)))   -- f used as a value
+        //   (in   (app f 1)))
+        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::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::Var { name: "x".into() }],
+                    tail: false,
+                }),
+            }),
+            in_term: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "f".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 _ = desugar_module(&m);
     }
 

docs/JOURNAL.md

@@ -3540,3 +3540,160 @@ 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.
+
+## Iter 16b.2 — LetRec captures of fn-params (path-1 safe subset)
+
+**Goal.** Lift 16b.1's no-capture restriction for the **path-1 safe
+subset** described in the 16b.2 planning entry: support a
+`(let-rec ...)` whose body captures one or more names from the
+enclosing scope, **provided every capture comes from a fn-param or
+Lam-param** (whose types are statically declared at desugar time).
+The lifted top-level fn's signature gets the capture types appended
+to `params`; every call site of the LetRec name is rewritten to
+pass the captures positionally as extra args. Anything outside the
+safe subset is rejected at desugar time with a panic that names the
+violation and points at the follow-up iter that will handle it
+(16b.3 / 16b.4 / 16b.5 / 16b.6 / 16b.7).
+
+**Path-1 restrictions in force (rejected at desugar with a
+follow-up-iter pointer).**
+
+- **Let-binding capture** (`Term::Let`-bound name, type unknown at
+  desugar). Queued for **16b.3**.
+- **Match-arm pattern-binding capture** (constructor-field
+  substitution from the scrutinee's ADT not done at desugar).
+  Queued for **16b.4**.
+- **Name-as-value use** (the LetRec name `f` appears anywhere
+  except as the callee of a `Term::App` — e.g. `(let g f ...)` or
+  `(app some_hof f)`). Needs closure conversion. Queued for
+  **16b.5**.
+- **Polymorphic enclosing fn** (`Type::Forall`). Captured fn-param
+  types may mention outer type vars; constructing the lifted
+  signature's `Forall` is error-prone. Encoded as
+  `ScopeEntry::LetBound` for every fn-param of a `Forall`-typed
+  enclosing fn — caught at the same site as let-binding captures.
+  Queued for **16b.6**.
+- **Nested LetRec mutual capture** (an inner LetRec captures the
+  outer LetRec's name or params). Queued for **16b.7**.
+
+**What shipped.**
+
+- `crates/ailang-core/src/desugar.rs` (1341 → 1853 LOC, +512). The
+  hot changes:
+  - New `enum ScopeEntry { KnownType(Type), LetBound, MatchArm,
+    EnclosingLetRec }`. The `scope` parameter threaded through
+    `desugar_term` and helpers became
+    `&BTreeMap<String, ScopeEntry>` (was `&BTreeSet<String>`).
+    Every binder ([`Term::Let`], [`Term::Lam`], [`Term::Match`]
+    arm, [`Term::LetRec`]) inserts the appropriate variant;
+    `desugar_module` seeds fn-param entries from `f.ty` (peeled
+    `Forall`).
+  - `Term::LetRec` arm rewritten end-to-end: peel `ty` to its
+    inner `Type::Fn` to learn the LetRec's own param types,
+    extend body-scope with `EnclosingLetRec` for `name` +
+    `KnownType(_)` for params, recurse on body and in_term, run
+    `free_vars_in_term` against `{name} ∪ params`, intersect
+    with the outer scope's keys, classify each capture's
+    `ScopeEntry` (KnownType → accept; everything else → panic
+    with the follow-up iter pointer), validate via
+    `find_non_callee_use` that `name` only appears as a callee,
+    build the augmented `Type::Fn` with capture types appended,
+    rewrite call sites via `subst_call_with_extras`, then
+    `subst_var` for any non-call references (defensive — none
+    survive the validator), append the lifted `FnDef`.
+  - Two new free helpers (~150 LOC together):
+    `subst_call_with_extras(t, name, lifted, extras)` rewrites
+    every `Term::App { callee = Var{name} }` to
+    `Term::App { callee = Var{lifted}, args ++ extras_as_vars }`,
+    walking through every variant; `find_non_callee_use(t, name)`
+    walks `t` and returns `Some(t)` at the first `Term::Var {
+    name == name }` reference in a non-callee position, `None`
+    otherwise. Plus `peel_forall_to_fn` (one-liner).
+  - The 16b.1 panic is gone for fn-param captures (replaced by
+    the lifter); it persists for every other capture kind, with
+    a sharper message.
+- `crates/ail/tests/e2e.rs` (+18): `local_rec_capture_demo` —
+  e2e count 38 → 39. Asserts that the `local_rec_capture` fixture
+  prints `0\n10\n45\n`.
+- `examples/local_rec_capture.ailx` + `.ail.json` (35 LOC source):
+  `sum_below(n)` returns the sum of integers `1 + ... + (n-1)`.
+  Body uses an inner `(let-rec loop (params i) ... (body ... (app
+  >= i n) ... (app loop (app + i 1))) (in (app loop 1)))`. The
+  helper captures `n` from `sum_below`'s param list; the desugar
+  pass lifts it to `loop$lr_0(i: Int, n: Int) -> Int` and rewrites
+  every `(app loop X)` to `(app loop$lr_0 X n)`. `main` drives
+  `sum_below` at 1, 5, 10 → outputs `0`, `10`, `45`.
+- `crates/ailang-core/src/desugar.rs::tests` (3 new):
+  `let_rec_capture_fn_param_lifts_with_extra_arg` (positive),
+  `let_rec_capture_let_binding_panics`
+  (`#[should_panic(expected = "16b.3")]`),
+  `let_rec_name_as_value_panics`
+  (`#[should_panic(expected = "16b.5")]`). The 16b.1
+  `let_rec_with_capture_panics` test was repurposed into the
+  positive `let_rec_capture_fn_param_lifts_with_extra_arg`: its
+  fixture (a fn-param capture) is now legal and produces the
+  expected augmented signature.
+
+**The augmented-signature mechanism.** Given
+`(let-rec f (params p1..pk) (type Fn(t1..tk) -> tr) (body B) (in I))`
+inside a fn whose scope contains
+`{c1: T1, ..., cm: Tm}` (KnownType entries) used as free vars in
+`B`:
+
+- Lifted signature: `f$lr_N : Fn(t1..tk, T1..Tm) -> tr` with the
+  same `effects` set as the original.
+- Lifted param-name list: `p1..pk, c1..cm` (capture names appended
+  unchanged so the lifted body's references resolve directly).
+- Body rewrite: every `(app f a1..an)` in `B` → `(app f$lr_N
+  a1..an c1..cm)`. The `c1..cm` are `Term::Var` references that
+  resolve, in the lifted body, to the appended params with the
+  same names. Free uses of `f` in non-callee position are
+  pre-rejected by `find_non_callee_use`.
+- In-term rewrite: every `(app f a1..an)` in `I` → `(app f$lr_N
+  a1..an c1..cm)`. The `c1..cm` are `Term::Var` references that
+  resolve, in the in-term's enclosing fn, to the captured names
+  themselves (still in scope).
+
+The rewrite is order-sensitive: `subst_call_with_extras` runs
+**before** `subst_var`, so a recursive self-call inside `B` first
+becomes `(app f$lr_N ... c1..cm)`, then any leftover bare `Var{f}`
+(none in 16b.2 — pre-rejected) gets renamed to `Var{f$lr_N}`. The
+second pass is defensive.
+
+**Tests: 102 → 106 (+4).**
+
+- e2e: 38 → 39 (`local_rec_capture_demo`).
+- `ailang-core::desugar::tests`: 6 → 9. Net +3 because the
+  16b.1-era `let_rec_with_capture_panics` test was repurposed
+  rather than removed (its fn-param-capture fixture is now a
+  positive lift), and two pure-negative tests were added.
+- All other crates unchanged.
+
+**Cumulative state, post-16b.2.**
+
+- Stdlib unchanged (5 modules, 29 combinators).
+- `Term` enum: 11 variants (unchanged; LetRec is still
+  desugar-eliminated, no schema impact). All pre-16b.2 fixtures
+  hash bit-identically.
+- 16a desugar pass now does three jobs: nested-ctor-pattern
+  flattening (16a), literal-pattern lowering (16c), and LetRec
+  lift (16b.1 → 16b.2 path-1). Single AST→AST hop between
+  `load_module` and typecheck.
+- The `unreachable!("Term::LetRec eliminated by desugar")` arms
+  in `ailang-check` × 2 and `ailang-codegen` × 4 remain correct
+  — every LetRec is still gone before either stage runs.
+
+**Queue update post-16b.2 path-1.** 16b.2 path-1 done. Open:
+**16b.3** (LetRec captures of `Term::Let`-bound names — would
+need a post-typecheck re-run of the lift, or a small inference
+on the let-value's type), **16b.4** (LetRec captures of match-arm
+pattern bindings — needs ADT-def lookup + constructor-field
+substitution), **16b.5** (closure conversion — lifts the
+"name-as-value-only" restriction for both LetRec and Lam),
+**16b.6** (LetRec inside a `Type::Forall`-quantified fn — needs
+synthesised `Forall` for the lifted signature), **16b.7**
+(nested LetRec mutual capture — generalised lifting that
+accumulates captures across nesting). 16d (chain-machinery
+exhaustiveness or `__unreachable__` — planning needed), 16e
+(`==` extension to Bool/Str/Unit), 17a (per-fn arena, gated)
+unchanged.

examples/local_rec_capture.ail.json

@@ -0,0 +1 @@
+{"defs":[{"body":{"body":{"cond":{"args":[{"name":"i","t":"var"},{"name":"n","t":"var"}],"fn":{"name":">=","t":"var"},"t":"app"},"else":{"args":[{"name":"i","t":"var"},{"args":[{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"}],"fn":{"name":"loop","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"t":"if","then":{"lit":{"kind":"int","value":0},"t":"lit"}},"in":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"loop","t":"var"},"t":"app"},"name":"loop","params":["i"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},"doc":"Sum 1 + 2 + ... + (n-1). Helper captures n from the enclosing scope.","kind":"fn","name":"sum_below","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"sum_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"sum_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"sum_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"doc":"Drive sum_below at 1, 5, 10. Expected (per line): 0, 10, 45.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"local_rec_capture","schema":"ailang/v0"}

examples/local_rec_capture.ailx

@@ -0,0 +1,35 @@
+; Iter 16b.2 — LetRec captures of fn-params (path-1 safe subset).
+; `sum_below(n)` returns the sum of integers from 1 up to but not
+; including n. The recursive helper `loop` captures the upper
+; bound `n` from `sum_below`'s param list and recurses on its own
+; counter `i`. The 16b.2 desugar pass lifts `loop` to a synthetic
+; top-level fn `loop$lr_0(i: Int, n: Int) -> Int` (capture appended)
+; and rewrites every `(app loop ARGS)` to `(app loop$lr_0 ARGS n)`.
+;
+; Expected stdout (one per line): 0 (sum below 1), 10 (1+2+3+4),
+; 45 (1+2+...+9).
+
+(module local_rec_capture
+
+  (fn sum_below
+    (doc "Sum 1 + 2 + ... + (n-1). Helper captures n from the enclosing scope.")
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params n)
+    (body
+      (let-rec loop
+        (params i)
+        (type (fn-type (params (con Int)) (ret (con Int))))
+        (body
+          (if (app >= i n)
+            0
+            (app + i (app loop (app + i 1)))))
+        (in (app loop 1)))))
+
+  (fn main
+    (doc "Drive sum_below at 1, 5, 10. Expected (per line): 0, 10, 45.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (seq (do io/print_int (app sum_below 1))
+      (seq (do io/print_int (app sum_below 5))
+           (do io/print_int (app sum_below 10)))))))