Iter 16b.3: post-typecheck lift for LetRec with Let-bound captures

Adds path-2 from the 16b.2 planning entry. Desugar now defers
LetRecs whose captures include Term::Let-bound names; a new
ailang-check::lift_letrecs pass runs after typecheck and uses the
elaborated env to resolve capture types. ailang-check learns a real
Term::LetRec typing rule in synth and verify_tail_positions.

- desugar: Term::LetRec arm gains a defer-arm; helpers promoted to
  pub for reuse by the lift pass; find_non_callee_use moved before
  classification.
- ailang-check::synth/verify_tail_positions: real LetRec rules
  (effect-subset, locals install, recursive name in body+in_term).
- ailang-check::lift.rs (new, 720 LOC): post-typecheck lift with
  post-order traversal, env-walk for capture-type resolution,
  fast-path skip when no LetRec is present.
- ail::main.rs: build path now does load → check → desugar →
  lift_letrecs → codegen.
- examples/local_rec_let_capture.{ailx,ail.json}: new fixture
  capturing a let-bound `threshold` in a recursive helper.
- e2e + check unit tests: 106 → 110 (+4).

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

crates/ailang-check/src/lib.rs

@@ -239,8 +239,10 @@ fn unify(a: &Type, b: &Type, subst: &mut Subst) -> Result<()> {
 
 pub mod builtins;
 pub mod diagnostic;
+pub mod lift;
 
 pub use diagnostic::{Diagnostic, Severity};
+pub use lift::lift_letrecs;
 
 /// Internal error type produced by the typechecker.
 ///
@@ -419,7 +421,7 @@ pub enum CheckError {
     },
 }
 
-type Result<T> = std::result::Result<T, CheckError>;
+pub(crate) type Result<T> = std::result::Result<T, CheckError>;
 
 impl CheckError {
     /// Stable kebab-case code for machine consumption (`ail check --json`).
@@ -687,6 +689,31 @@ pub fn check(m: &Module) -> Result<CheckedModule> {
     Ok(CheckedModule { symbols })
 }
 
+/// Iter 16b.3: typecheck `m` and return both the [`CheckedModule`]
+/// (for tooling that wants the original on-disk symbol identities)
+/// AND the lifted module ready for codegen — i.e. the desugared
+/// module with every surviving `Term::LetRec` replaced by a
+/// synthetic top-level `Def::Fn`.
+///
+/// The check phase runs unchanged: same desugar, same typecheck,
+/// same `CheckedModule.symbols` (built from the original `m`'s
+/// defs). On success, the desugared module is fed through
+/// [`lift_letrecs`] and the result is returned alongside.
+///
+/// `build` / `run` go through this entry; the `check` subcommand
+/// stays on the legacy [`check`] entry (no lift needed for
+/// type-checking only).
+pub fn check_and_lift(m: &Module) -> Result<(CheckedModule, Module)> {
+    let cm = check(m)?;
+    // Run desugar exactly as `check` does. The `check` call already
+    // ran desugar internally, but its result is discarded (only the
+    // CheckedModule survives), so we have to re-run it here to get
+    // the post-desugar form for the lift.
+    let desugared = ailang_core::desugar::desugar_module(m);
+    let lifted = lift_letrecs(&desugared)?;
+    Ok((cm, lifted))
+}
+
 /// Iter 15a: builds the ADT type-def table per module. Sibling of
 /// [`build_module_globals`]: gives the body checker O(1) lookup of any
 /// type declared anywhere in the workspace, keyed by module name.
@@ -1083,10 +1110,16 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
             // Entering a Lam body opens a fresh tail scope.
             verify_tail_positions(body, true)
         }
-        Term::LetRec { .. } => {
-            // Iter 16b.1: `Term::LetRec` is eliminated by the desugar
-            // pass before `check` runs, so reaching it here is a bug.
-            unreachable!("Term::LetRec eliminated by desugar")
+        Term::LetRec { body, in_term, .. } => {
+            // Iter 16b.3: `Term::LetRec` may now survive the desugar
+            // pass (when it captures `Term::Let`-bound names whose
+            // types are only known after typecheck). The body is the
+            // body of a fn-typed binding; the recursive name is what
+            // gets tail-called, so `body` is NOT in tail position. The
+            // in-clause IS in tail position iff the enclosing context
+            // is — same propagation rule as `Term::Let.body`.
+            verify_tail_positions(body, false)?;
+            verify_tail_positions(in_term, is_tail)
         }
     }
 }
@@ -1112,7 +1145,7 @@ fn check_const(c: &ConstDef, env: &Env) -> Result<()> {
     Ok(())
 }
 
-fn synth(
+pub(crate) fn synth(
     t: &Term,
     env: &Env,
     locals: &mut IndexMap<String, Type>,
@@ -1488,10 +1521,104 @@ fn synth(
                 effects: lam_effects.clone(),
             })
         }
-        Term::LetRec { .. } => {
-            // Iter 16b.1: `Term::LetRec` is eliminated by the desugar
-            // pass before `synth` runs, so reaching it here is a bug.
-            unreachable!("Term::LetRec eliminated by desugar")
+        Term::LetRec { name, ty, params, body, in_term } => {
+            // Iter 16b.3: a `Term::LetRec` reaches `synth` only when
+            // the desugar pass deferred it (some capture is
+            // `Term::Let`-bound and its type is only knowable here).
+            // We synthesize it as if it were a recursive fn-typed
+            // local binding:
+            //   1. Peel any `Forall` defensively (16b.6 still rejects
+            //      Forall-typed LetRecs at desugar — this is just for
+            //      shape uniformity with `check_fn`).
+            //   2. Validate that `params.len() == ty.params.len()`.
+            //   3. Extend `locals` with `name: ty` for the body
+            //      (recursive self-reference) and each
+            //      `params[i]: ty.params[i]`.
+            //   4. Synth the body, unify against `ty.ret`, check
+            //      effects-subset against `ty.effects`.
+            //   5. Restore locals; extend with `name: ty`; synth
+            //      `in_term`. Restore. Return `in_term`'s type.
+            let inner_ty = match ty {
+                Type::Forall { body, .. } => (**body).clone(),
+                other => other.clone(),
+            };
+            let (param_tys, ret_ty, declared_effs) = match &inner_ty {
+                Type::Fn { params: ps, ret, effects } => {
+                    (ps.clone(), (**ret).clone(), effects.clone())
+                }
+                other => {
+                    return Err(CheckError::FnTypeRequired(
+                        name.clone(),
+                        ailang_core::pretty::type_to_string(other),
+                    ));
+                }
+            };
+            if param_tys.len() != params.len() {
+                return Err(CheckError::ParamCountMismatch {
+                    name: name.clone(),
+                    ty_count: param_tys.len(),
+                    param_count: params.len(),
+                });
+            }
+
+            // Validate the LetRec's declared param/ret types against
+            // the type env (catches malformed types like ADT arity
+            // mismatches before they leak into the body).
+            for p in &param_tys {
+                check_type_well_formed(p, env)?;
+            }
+            check_type_well_formed(&ret_ty, env)?;
+
+            // Save and extend locals: name + params for the body's scope.
+            let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
+            let prev_name = locals.insert(name.clone(), ty.clone());
+            pushed.push((name.clone(), prev_name));
+            for (n, t) in params.iter().zip(param_tys.iter()) {
+                let prev = locals.insert(n.clone(), t.clone());
+                pushed.push((n.clone(), prev));
+            }
+
+            // Body effects are tracked separately so we can check the
+            // subset rule against `declared_effs` — exactly like
+            // `Term::Lam`.
+            let mut body_effects: BTreeSet<String> = BTreeSet::new();
+            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter);
+
+            // Restore body-scope locals (params + name).
+            for (n, prev) in pushed.into_iter().rev() {
+                match prev {
+                    Some(p) => {
+                        locals.insert(n, p);
+                    }
+                    None => {
+                        locals.shift_remove(&n);
+                    }
+                }
+            }
+            let body_ty = body_ty?;
+            unify(&ret_ty, &body_ty, subst)?;
+
+            let declared: BTreeSet<String> = declared_effs.into_iter().collect();
+            for e in &body_effects {
+                if !declared.contains(e) {
+                    return Err(CheckError::UndeclaredEffect(e.clone()));
+                }
+            }
+
+            // Now extend locals with `name: ty` for the in-clause's
+            // scope (params are not visible here; only the recursive
+            // binding is).
+            let prev_in = locals.insert(name.clone(), ty.clone());
+            let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter);
+            match prev_in {
+                Some(p) => {
+                    locals.insert(name.clone(), p);
+                }
+                None => {
+                    locals.shift_remove(name);
+                }
+            }
+            in_ty
         }
     }
 }
@@ -1794,7 +1921,7 @@ pub struct CtorRef {
 }
 
 impl Env {
-    fn new() -> Self {
+    pub(crate) fn new() -> Self {
         Self::default()
     }
 }
@@ -2884,4 +3011,271 @@ mod tests {
         };
         check(&m).expect("tail-call in tail position should typecheck");
     }
+
+    /// Iter 16b.3: a `Term::LetRec` that captures a `Term::Let`-bound
+    /// name (whose type is known only after typecheck) reaches `synth`
+    /// because the desugar pass leaves it in place. The new typing
+    /// rule for `Term::LetRec` accepts it: extends locals with `name`
+    /// and the params, synths the body, unifies against the declared
+    /// return type, then synths the in-clause.
+    #[test]
+    fn letrec_with_let_binding_capture_typechecks() {
+        // fn outer : (Int) -> Int = \n.
+        //   let threshold = + 5 5
+        //   in let-rec loop : (Int) -> Int = \i.
+        //        if (>= i threshold) then 0 else loop (+ i 1)
+        //      in loop 0
+        let body = Term::Let {
+            name: "threshold".into(),
+            value: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "+".into() }),
+                args: vec![
+                    Term::Lit { lit: Literal::Int { value: 5 } },
+                    Term::Lit { lit: Literal::Int { value: 5 } },
+                ],
+                tail: false,
+            }),
+            body: Box::new(Term::LetRec {
+                name: "loop".into(),
+                ty: Type::Fn {
+                    params: vec![Type::int()],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                params: vec!["i".into()],
+                body: Box::new(Term::If {
+                    cond: Box::new(Term::App {
+                        callee: Box::new(Term::Var { name: ">=".into() }),
+                        args: vec![
+                            Term::Var { name: "i".into() },
+                            Term::Var { name: "threshold".into() },
+                        ],
+                        tail: false,
+                    }),
+                    then: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
+                    else_: Box::new(Term::App {
+                        callee: Box::new(Term::Var { name: "loop".into() }),
+                        args: vec![Term::App {
+                            callee: Box::new(Term::Var { name: "+".into() }),
+                            args: vec![
+                                Term::Var { name: "i".into() },
+                                Term::Lit { lit: Literal::Int { value: 1 } },
+                            ],
+                            tail: false,
+                        }],
+                        tail: false,
+                    }),
+                }),
+                in_term: Box::new(Term::App {
+                    callee: Box::new(Term::Var { name: "loop".into() }),
+                    args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
+                    tail: false,
+                }),
+            }),
+        };
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_def(
+                "outer",
+                Type::Fn {
+                    params: vec![Type::int()],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                vec!["n"],
+                body,
+            )],
+        };
+        check(&m).expect("LetRec with Let-binding capture should typecheck");
+    }
+
+    /// Iter 16b.3: a LetRec whose body returns the wrong type (Bool
+    /// instead of the declared Int) is caught by the new typing rule.
+    /// Property protected: the new arm in `synth` for `Term::LetRec`
+    /// runs `unify(&ret_ty, &body_ty, subst)` just like `Term::Lam`
+    /// and `check_fn`.
+    #[test]
+    fn letrec_body_wrong_return_type_is_rejected() {
+        // (let-rec wrong (params x) (type (Int) -> Int) (body true)
+        //                                            (in  (app wrong 0)))
+        let letrec = Term::LetRec {
+            name: "wrong".into(),
+            ty: Type::Fn {
+                params: vec![Type::int()],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            params: vec!["x".into()],
+            body: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
+            in_term: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "wrong".into() }),
+                args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
+                tail: false,
+            }),
+        };
+        // Wrap in a Let so the desugar pass defers the LetRec (its
+        // body would otherwise lift cleanly with no captures, since
+        // `true` doesn't reference `x`).
+        let body = Term::Let {
+            name: "y".into(),
+            value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
+            // Reference `y` inside the LetRec body so it captures.
+            body: Box::new(Term::LetRec {
+                name: "wrong".into(),
+                ty: Type::Fn {
+                    params: vec![Type::int()],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                params: vec!["x".into()],
+                body: Box::new(Term::Seq {
+                    // Use `y` so the LetRec captures it (forces deferral).
+                    lhs: Box::new(Term::Lit { lit: Literal::Unit }),
+                    rhs: Box::new(Term::App {
+                        callee: Box::new(Term::Var { name: "+".into() }),
+                        args: vec![
+                            Term::Var { name: "y".into() },
+                            Term::Lit { lit: Literal::Bool { value: true } },
+                        ],
+                        tail: false,
+                    }),
+                }),
+                in_term: Box::new(Term::App {
+                    callee: Box::new(Term::Var { name: "wrong".into() }),
+                    args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
+                    tail: false,
+                }),
+            }),
+        };
+        // (Suppress dead-code warning on the unused unwrapped letrec.)
+        let _ = letrec;
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_def(
+                "outer",
+                Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                vec![],
+                body,
+            )],
+        };
+        let err = check(&m).expect_err("LetRec body returning Bool but declared Int must error");
+        let msg = format!("{err}");
+        assert!(
+            msg.contains("type mismatch"),
+            "expected a type-mismatch diagnostic, got: {msg}"
+        );
+    }
+
+    /// Iter 16b.3: `lift_letrecs` on a module containing a deferred
+    /// LetRec produces a module whose defs include a synthetic
+    /// `<hint>$lr_N` FnDef and whose original fn body has rewritten
+    /// call sites.
+    #[test]
+    fn lift_letrecs_on_let_capture_produces_synthetic_fn() {
+        // fn outer : () -> Int = \.
+        //   let y = 7
+        //   in let-rec helper : (Int) -> Int = \x. + x y
+        //      in helper 1
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_def(
+                "outer",
+                Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                vec![],
+                Term::Let {
+                    name: "y".into(),
+                    value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
+                    body: Box::new(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,
+                        }),
+                    }),
+                },
+            )],
+        };
+        // Typecheck must succeed (the new LetRec rule accepts this).
+        check(&m).expect("typecheck before lift");
+        let desugared = ailang_core::desugar::desugar_module(&m);
+        // After desugar the LetRec is still present (Let-binding capture).
+        // After lift_letrecs it must be gone, replaced by a synthetic
+        // top-level fn with the capture appended to its signature.
+        let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
+        assert_eq!(lifted.defs.len(), 2, "expected one synthetic fn appended");
+        let synth = match &lifted.defs[1] {
+            Def::Fn(f) => f,
+            _ => panic!("expected synthetic FnDef"),
+        };
+        assert!(
+            synth.name.starts_with("helper$lr_"),
+            "lifted name `{}` should start with `helper$lr_`",
+            synth.name
+        );
+        assert_eq!(
+            synth.ty,
+            Type::Fn {
+                params: vec![Type::int(), Type::int()],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            "lifted ty should have capture appended; got {:?}",
+            synth.ty
+        );
+        assert_eq!(synth.params, vec!["x".to_string(), "y".to_string()]);
+        // `outer`'s body must have the `(app helper 1)` rewritten to
+        // `(app helper$lr_0 1 y)`. The body is now
+        // `let y = 7 in (app helper$lr_0 1 y)`.
+        let outer_body = match &lifted.defs[0] {
+            Def::Fn(f) => &f.body,
+            _ => unreachable!(),
+        };
+        let inner = match outer_body {
+            Term::Let { body, .. } => body.as_ref(),
+            other => panic!("expected outer Let, got {other:?}"),
+        };
+        match inner {
+            Term::App { callee, args, .. } => {
+                match callee.as_ref() {
+                    Term::Var { name } => assert_eq!(name, &synth.name),
+                    other => panic!("expected lifted callee, got {other:?}"),
+                }
+                assert_eq!(args.len(), 2, "expected 2 args (1 original + 1 capture)");
+                match &args[1] {
+                    Term::Var { name } => assert_eq!(name, "y"),
+                    other => panic!("expected y as second arg, got {other:?}"),
+                }
+            }
+            other => panic!("expected App after Let, got {other:?}"),
+        }
+    }
 }