Iter 16b.1 — local recursive let (no-capture)

Add `(let-rec NAME (params ...) (type ...) (body ...) (in ...))`
as a form-A surface and a `Term::LetRec` AST variant. The 16a
desugar pass lifts each LetRec whose body has no captures from
the enclosing scope to a synthetic top-level fn `<hint>$lr_N`
and substitutes the original name; typecheck and codegen never
see LetRec. Capture detection panics at desugar time, queued
for 16b.2.

Tests: 95 → 99 (+1 e2e local_rec_factorial_demo, +2 desugar
unit, +1 parse unit). The new fixture `examples/local_rec_demo`
runs `fact` at n=1, 3, 5 → prints 1, 6, 120.

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

crates/ail/src/main.rs

@@ -931,6 +931,28 @@ fn walk_term(
             walk_term(lhs, out, builtins, scope);
             walk_term(rhs, out, builtins, scope);
         }
+        Term::LetRec { name, params, body, in_term, .. } => {
+            // Iter 16b.1: `deps` walks the on-disk module before the
+            // desugar pass, so a `Term::LetRec` is reachable here.
+            // Treat it like a fn def for dependency purposes:
+            // `name` shadows for both body and in_term; params shadow
+            // inside the body.
+            let inserted_name = scope.insert(name.clone());
+            let mut newly = Vec::new();
+            for p in params {
+                if scope.insert(p.clone()) {
+                    newly.push(p.clone());
+                }
+            }
+            walk_term(body, out, builtins, scope);
+            for p in newly {
+                scope.remove(&p);
+            }
+            walk_term(in_term, out, builtins, scope);
+            if inserted_name {
+                scope.remove(name);
+            }
+        }
     }
 }
 

crates/ail/tests/e2e.rs

@@ -432,6 +432,24 @@ fn std_list_more_demo() {
     assert_eq!(lines, vec!["0", "3", "5", "5", "3", "0"]);
 }
 
+/// Iter 16b.1: local recursive `let`. Property protected: a
+/// `(let-rec ...)` term in a fn body whose recursive body has no
+/// captures from the enclosing scope is lifted by the 16a desugar
+/// pass to a synthetic top-level fn (`<name>$lr_N`), and the
+/// resulting module type-checks and runs identically to a
+/// hand-written top-level recursive fn. The fixture exercises
+/// `fact` at n=1 (base case), n=3, n=5 — outputs 1, 6, 120.
+/// If the desugar lift regressed (e.g. failed to substitute call
+/// sites in the in-term, or generated a colliding lifted name),
+/// the build would fail at typecheck or the binary would print
+/// wrong values.
+#[test]
+fn local_rec_factorial_demo() {
+    let stdout = build_and_run("local_rec_demo.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["1", "6", "120"]);
+}
+
 /// 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/lib.rs

@@ -1083,6 +1083,11 @@ 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")
+        }
     }
 }
 
@@ -1483,6 +1488,11 @@ 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")
+        }
     }
 }
 

crates/ailang-codegen/src/lib.rs

@@ -1039,6 +1039,12 @@ impl<'a> Emitter<'a> {
                 let _ = self.lower_term(lhs)?;
                 self.lower_term(rhs)
             }
+            Term::LetRec { .. } => {
+                // Iter 16b.1: `Term::LetRec` is eliminated by the
+                // desugar pass before codegen runs, so reaching it
+                // here is a bug.
+                unreachable!("Term::LetRec eliminated by desugar")
+            }
         }
     }
 
@@ -2122,6 +2128,10 @@ impl<'a> Emitter<'a> {
                 Self::collect_captures(lhs, bound, captures, captures_set, builtins, top_level);
                 Self::collect_captures(rhs, bound, captures, captures_set, builtins, top_level);
             }
+            Term::LetRec { .. } => {
+                // Iter 16b.1: eliminated by desugar before codegen.
+                unreachable!("Term::LetRec eliminated by desugar")
+            }
         }
     }
 
@@ -2548,6 +2558,10 @@ impl<'a> Emitter<'a> {
                 }
             }
             Term::Seq { rhs, .. } => self.synth_with_extras(rhs, extras),
+            Term::LetRec { .. } => {
+                // Iter 16b.1: eliminated by desugar before codegen.
+                unreachable!("Term::LetRec eliminated by desugar")
+            }
         }
     }
 }
@@ -2898,6 +2912,11 @@ fn apply_subst_to_term(t: &Term, subst: &BTreeMap<String, Type>) -> Term {
             lhs: Box::new(apply_subst_to_term(lhs, subst)),
             rhs: Box::new(apply_subst_to_term(rhs, subst)),
         },
+        Term::LetRec { .. } => {
+            // Iter 16b.1: eliminated by desugar before any
+            // monomorphisation pass runs.
+            unreachable!("Term::LetRec eliminated by desugar")
+        }
     }
 }
 

crates/ailang-core/src/ast.rs

@@ -219,6 +219,22 @@ pub enum Term {
         value: Box<Term>,
         body: Box<Term>,
     },
+    /// Local recursive let-binding (Iter 16b.1). Always fn-shaped:
+    /// the bound name `name` is recursively visible inside `body`.
+    /// Eliminated by `crate::desugar` before typecheck — lifted to a
+    /// synthetic top-level fn when `body` does not capture any name
+    /// from the enclosing lexical scope. The on-disk schema gains the
+    /// `"t": "letrec"` tag; pre-existing fixtures hash bit-identically
+    /// because the variant is additive.
+    LetRec {
+        name: String,
+        #[serde(rename = "type")]
+        ty: Type,
+        params: Vec<String>,
+        body: Box<Term>,
+        #[serde(rename = "in")]
+        in_term: Box<Term>,
+    },
     /// If-expression. Both branches must have the same type.
     If {
         cond: Box<Term>,

crates/ailang-core/src/desugar.rs

@@ -65,6 +65,29 @@
 //! module and bumps the counter until it lands on a name not in that
 //! set.
 //!
+//! ## Iter 16b.1: local recursive `let` (no-capture)
+//!
+//! [`Term::LetRec`] is a surface-only AST node introduced in 16b.1. The
+//! desugar pass eliminates it before typecheck/codegen by **lifting**
+//! the LetRec to a synthetic top-level fn in the same module. The
+//! lifted name has the form `<hint>$lr_N`, fresh against both the
+//! existing module-top-level def names and the [`Desugarer::used`] set.
+//! Inside the LetRec's `body` and `in_term`, every reference to the
+//! original local name is rewritten via [`subst_var`] to the lifted
+//! name. The lifted [`FnDef`] is appended to the module's `defs` so
+//! the typechecker / codegen see it as if it had been written
+//! top-level by hand.
+//!
+//! Capture is **not** supported in 16b.1: if the LetRec's body's free
+//! variables (excluding `{name} ∪ params`) intersect the enclosing
+//! lexical scope (params of the surrounding fn, let-bound names, or
+//! pattern-bound names), the desugar pass panics with a diagnostic
+//! that points the author at 16b.2 (closure conversion). Free vars
+//! that resolve to module-top-level def names, qualified import names
+//! (containing `.`), effect-op names (containing `/`), and builtin
+//! operators are all ignored — those reach a lifted top-level fn
+//! through the same path they reach any other top-level fn.
+//!
 //! ## What this module deliberately does not do
 //!
 //! - It does not alter [`crate::ast::Pattern`] or [`crate::ast::Term`].
@@ -72,34 +95,75 @@
 //! - It does not implement Maranget-style decision trees; the rewrite
 //!   is a literal-translation chain that the existing single-level
 //!   match codegen already handles.
+//! - It does not implement closure conversion for [`Term::LetRec`]
+//!   bodies that capture from the enclosing scope (queued as 16b.2).
 
 use crate::ast::*;
 use std::collections::BTreeSet;
 
 /// Rewrite `m` so that every [`Pattern::Ctor`] sub-pattern is a
-/// [`Pattern::Var`] or [`Pattern::Wild`] (i.e. flat).
+/// [`Pattern::Var`] or [`Pattern::Wild`] (i.e. flat) and every
+/// [`Term::LetRec`] is replaced by a reference to a synthetic
+/// top-level fn.
 ///
 /// Pure / total: returns a new [`Module`]; does not mutate `m`.
-/// Idempotent: a module that is already flat is returned as-is
-/// modulo cloning.
+/// Idempotent: a module that is already flat and LetRec-free is
+/// returned as-is modulo cloning.
 pub fn desugar_module(m: &Module) -> Module {
     let mut used: BTreeSet<String> = BTreeSet::new();
     for def in &m.defs {
         match def {
-            Def::Fn(f) => collect_used_in_term(&f.body, &mut used),
-            Def::Const(c) => collect_used_in_term(&c.value, &mut used),
-            Def::Type(_) => {}
+            Def::Fn(f) => {
+                used.insert(f.name.clone());
+                for p in &f.params {
+                    used.insert(p.clone());
+                }
+                collect_used_in_term(&f.body, &mut used);
+            }
+            Def::Const(c) => {
+                used.insert(c.name.clone());
+                collect_used_in_term(&c.value, &mut used);
+            }
+            Def::Type(td) => {
+                used.insert(td.name.clone());
+            }
         }
     }
-    let mut d = Desugarer { counter: 0, used };
+    // Iter 16b.1: pre-collect every top-level def name. The LetRec
+    // lifter consults this set to (a) know whether a free var of a
+    // LetRec body resolves to a top-level def (no capture) and
+    // (b) keep its fresh-name generator from colliding with an
+    // existing def — including ones lifted earlier in the same pass.
+    let mut module_top_names: BTreeSet<String> = BTreeSet::new();
+    for def in &m.defs {
+        module_top_names.insert(def.name().to_string());
+    }
+    let mut d = Desugarer {
+        counter: 0,
+        used,
+        lifted: Vec::new(),
+        module_top_names,
+    };
     let mut out = m.clone();
     for def in &mut out.defs {
         match def {
-            Def::Fn(f) => f.body = d.desugar_term(&f.body),
-            Def::Const(c) => c.value = d.desugar_term(&c.value),
+            Def::Fn(f) => {
+                let scope: BTreeSet<String> = f.params.iter().cloned().collect();
+                f.body = d.desugar_term(&f.body, &scope);
+            }
+            Def::Const(c) => {
+                let scope: BTreeSet<String> = BTreeSet::new();
+                c.value = d.desugar_term(&c.value, &scope);
+            }
             Def::Type(_) => {}
         }
     }
+    // Iter 16b.1: append every lifted fn to the desugared module.
+    // Order: original defs first, then lifts in the order they were
+    // produced by the bottom-up walk. Typecheck/codegen are order-
+    // insensitive at the def list level (they index by name), so this
+    // is purely cosmetic.
+    out.defs.extend(d.lifted.into_iter());
     out
 }
 
@@ -156,6 +220,14 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
             collect_used_in_term(lhs, used);
             collect_used_in_term(rhs, used);
         }
+        Term::LetRec { name, params, body, in_term, .. } => {
+            used.insert(name.clone());
+            for p in params {
+                used.insert(p.clone());
+            }
+            collect_used_in_term(body, used);
+            collect_used_in_term(in_term, used);
+        }
     }
 }
 
@@ -180,9 +252,21 @@ fn collect_used_in_pattern(p: &Pattern, used: &mut BTreeSet<String>) {
 /// `counter` is incremented for every fresh-name request; `used`
 /// contains every source-level identifier (var-bind or var-reference)
 /// in the module so that [`fresh`](Self::fresh) cannot shadow one.
+///
+/// Iter 16b.1 fields:
+/// - `lifted` accumulates synthetic top-level fns produced by
+///   [`Term::LetRec`] desugaring. Appended to `Module.defs` once the
+///   per-def walk finishes.
+/// - `module_top_names` mirrors every name reachable as a top-level
+///   def at this point in the pass (originals + already-lifted). The
+///   capture analyser uses it to classify free vars; the fresh-name
+///   generator [`fresh_lifted`](Self::fresh_lifted) consults it so
+///   later lifts cannot collide with earlier ones.
 struct Desugarer {
     counter: u64,
     used: BTreeSet<String>,
+    lifted: Vec<Def>,
+    module_top_names: BTreeSet<String>,
 }
 
 impl Desugarer {
@@ -201,45 +285,81 @@ impl Desugarer {
         }
     }
 
+    /// Iter 16b.1: returns a name of the form `<hint>$lr_N` not in
+    /// `used` and not in `module_top_names`. Bumps both sets so a
+    /// later lift cannot collide. The `hint` is the source-level
+    /// LetRec name; it makes lifted bindings traceable through the
+    /// pipeline (typecheck errors / IR mangling / panic messages).
+    fn fresh_lifted(&mut self, hint: &str) -> String {
+        let mut n = 0u64;
+        loop {
+            let candidate = format!("{hint}$lr_{n}");
+            n += 1;
+            if !self.used.contains(&candidate) && !self.module_top_names.contains(&candidate) {
+                self.used.insert(candidate.clone());
+                self.module_top_names.insert(candidate.clone());
+                return candidate;
+            }
+        }
+    }
+
     /// Recursively rewrites `t`: descends into every child first
     /// (bottom-up), then dispatches a [`Term::Match`] to
-    /// [`desugar_match`](Self::desugar_match).
-    fn desugar_term(&mut self, t: &Term) -> Term {
+    /// [`desugar_match`](Self::desugar_match) and a [`Term::LetRec`]
+    /// to the 16b.1 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 {
         match t {
             Term::Lit { .. } | Term::Var { .. } => t.clone(),
             Term::App { callee, args, tail } => Term::App {
-                callee: Box::new(self.desugar_term(callee)),
-                args: args.iter().map(|a| self.desugar_term(a)).collect(),
+                callee: Box::new(self.desugar_term(callee, scope)),
+                args: args.iter().map(|a| self.desugar_term(a, scope)).collect(),
                 tail: *tail,
             },
-            Term::Let { name, value, body } => Term::Let {
-                name: name.clone(),
-                value: Box::new(self.desugar_term(value)),
-                body: Box::new(self.desugar_term(body)),
-            },
+            Term::Let { name, value, body } => {
+                let v = self.desugar_term(value, scope);
+                let mut inner = scope.clone();
+                inner.insert(name.clone());
+                let b = self.desugar_term(body, &inner);
+                Term::Let {
+                    name: name.clone(),
+                    value: Box::new(v),
+                    body: Box::new(b),
+                }
+            }
             Term::If { cond, then, else_ } => Term::If {
-                cond: Box::new(self.desugar_term(cond)),
-                then: Box::new(self.desugar_term(then)),
-                else_: Box::new(self.desugar_term(else_)),
+                cond: Box::new(self.desugar_term(cond, scope)),
+                then: Box::new(self.desugar_term(then, scope)),
+                else_: Box::new(self.desugar_term(else_, scope)),
             },
             Term::Do { op, args, tail } => Term::Do {
                 op: op.clone(),
-                args: args.iter().map(|a| self.desugar_term(a)).collect(),
+                args: args.iter().map(|a| self.desugar_term(a, scope)).collect(),
                 tail: *tail,
             },
             Term::Ctor { type_name, ctor, args } => Term::Ctor {
                 type_name: type_name.clone(),
                 ctor: ctor.clone(),
-                args: args.iter().map(|a| self.desugar_term(a)).collect(),
+                args: args.iter().map(|a| self.desugar_term(a, scope)).collect(),
             },
             Term::Match { scrutinee, arms } => {
                 // Recurse into children first (bottom-up).
-                let scrutinee = self.desugar_term(scrutinee);
+                let scrutinee = self.desugar_term(scrutinee, scope);
                 let arms: Vec<Arm> = arms
                     .iter()
-                    .map(|a| Arm {
-                        pat: a.pat.clone(),
-                        body: self.desugar_term(&a.body),
+                    .map(|a| {
+                        let mut inner = scope.clone();
+                        pattern_binds(&a.pat, &mut inner);
+                        Arm {
+                            pat: a.pat.clone(),
+                            body: self.desugar_term(&a.body, &inner),
+                        }
                     })
                     .collect();
                 self.desugar_match(scrutinee, arms)
@@ -250,17 +370,76 @@ impl Desugarer {
                 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(self.desugar_term(body)),
-            },
+            } => {
+                let mut inner = scope.clone();
+                for p in params {
+                    inner.insert(p.clone());
+                }
+                Term::Lam {
+                    params: params.clone(),
+                    param_tys: param_tys.clone(),
+                    ret_ty: ret_ty.clone(),
+                    effects: effects.clone(),
+                    body: Box::new(self.desugar_term(body, &inner)),
+                }
+            }
             Term::Seq { lhs, rhs } => Term::Seq {
-                lhs: Box::new(self.desugar_term(lhs)),
-                rhs: Box::new(self.desugar_term(rhs)),
+                lhs: Box::new(self.desugar_term(lhs, scope)),
+                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).
+                let mut body_scope = scope.clone();
+                body_scope.insert(name.clone());
+                for p in params {
+                    body_scope.insert(p.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`).
+                let mut in_scope = scope.clone();
+                in_scope.insert(name.clone());
+                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).
+                let mut local_bound: BTreeSet<String> = BTreeSet::new();
+                local_bound.insert(name.clone());
+                for p in params {
+                    local_bound.insert(p.clone());
+                }
+                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() {
+                    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
+                    );
+                }
+
+                // 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.
+                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);
+                self.lifted.push(Def::Fn(FnDef {
+                    name: lifted_name,
+                    ty: ty.clone(),
+                    params: params.clone(),
+                    body: body_lifted,
+                    doc: None,
+                }));
+                in_lifted
+            }
         }
     }
 
@@ -412,6 +591,213 @@ fn is_flat(p: &Pattern) -> bool {
     }
 }
 
+/// Iter 16b.1: collect free variable names of `t`, with `bound` being
+/// the set of names lexically bound at this point. A
+/// [`Term::Var`] `{ name }` is "free" iff `name` is not in `bound`.
+/// Compound binders ([`Term::Let`], [`Term::Lam`], [`Term::Match`]
+/// arms, [`Term::LetRec`]) extend `bound` for the sub-walk.
+///
+/// Used by the [`Term::LetRec`] desugar to decide whether a local
+/// recursive let would capture any name from the enclosing scope
+/// (16b.2 has not shipped yet, so capture is a panic at desugar time).
+fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<String>) {
+    match t {
+        Term::Lit { .. } => {}
+        Term::Var { name } => {
+            if !bound.contains(name) {
+                out.insert(name.clone());
+            }
+        }
+        Term::App { callee, args, .. } => {
+            free_vars_in_term(callee, bound, out);
+            for a in args {
+                free_vars_in_term(a, bound, out);
+            }
+        }
+        Term::Let { name, value, body } => {
+            free_vars_in_term(value, bound, out);
+            let mut b = bound.clone();
+            b.insert(name.clone());
+            free_vars_in_term(body, &b, out);
+        }
+        Term::If { cond, then, else_ } => {
+            free_vars_in_term(cond, bound, out);
+            free_vars_in_term(then, bound, out);
+            free_vars_in_term(else_, bound, out);
+        }
+        Term::Do { args, .. } => {
+            for a in args {
+                free_vars_in_term(a, bound, out);
+            }
+        }
+        Term::Ctor { args, .. } => {
+            for a in args {
+                free_vars_in_term(a, bound, out);
+            }
+        }
+        Term::Match { scrutinee, arms } => {
+            free_vars_in_term(scrutinee, bound, out);
+            for arm in arms {
+                let mut b = bound.clone();
+                pattern_binds(&arm.pat, &mut b);
+                free_vars_in_term(&arm.body, &b, out);
+            }
+        }
+        Term::Lam { params, body, .. } => {
+            let mut b = bound.clone();
+            for p in params {
+                b.insert(p.clone());
+            }
+            free_vars_in_term(body, &b, out);
+        }
+        Term::Seq { lhs, rhs } => {
+            free_vars_in_term(lhs, bound, out);
+            free_vars_in_term(rhs, bound, out);
+        }
+        Term::LetRec { name, params, body, in_term, .. } => {
+            // Inside body: name + params are bound.
+            let mut b_body = bound.clone();
+            b_body.insert(name.clone());
+            for p in params {
+                b_body.insert(p.clone());
+            }
+            free_vars_in_term(body, &b_body, out);
+            // Inside in_term: only name is bound.
+            let mut b_in = bound.clone();
+            b_in.insert(name.clone());
+            free_vars_in_term(in_term, &b_in, out);
+        }
+    }
+}
+
+/// Iter 16b.1: collect every name a pattern binds into `out`. Mirrors
+/// `Pattern::pattern_bound_names` in `ailang-codegen`; duplicated here
+/// because `ailang-core` cannot depend on the codegen crate.
+fn pattern_binds(p: &Pattern, out: &mut BTreeSet<String>) {
+    match p {
+        Pattern::Wild | Pattern::Lit { .. } => {}
+        Pattern::Var { name } => {
+            out.insert(name.clone());
+        }
+        Pattern::Ctor { fields, .. } => {
+            for sub in fields {
+                pattern_binds(sub, out);
+            }
+        }
+    }
+}
+
+/// Iter 16b.1: rewrite every free [`Term::Var`] `{ name == from }`
+/// reference in `t` to [`Term::Var`] `{ name = to }`. Respects
+/// shadowing: if a binder rebinds `from`, occurrences inside that
+/// binder's scope stop being free and are left alone.
+///
+/// Used after lifting a [`Term::LetRec`] body to a synthetic top-level
+/// fn — every recursive self-call site in the lifted body and every
+/// reference in the in-term needs to point at the new global name.
+fn subst_var(t: &Term, from: &str, to: &str) -> Term {
+    match t {
+        Term::Lit { .. } => t.clone(),
+        Term::Var { name } => {
+            if name == from {
+                Term::Var { name: to.to_string() }
+            } else {
+                t.clone()
+            }
+        }
+        Term::App { callee, args, tail } => Term::App {
+            callee: Box::new(subst_var(callee, from, to)),
+            args: args.iter().map(|a| subst_var(a, from, to)).collect(),
+            tail: *tail,
+        },
+        Term::Let { name, value, body } => {
+            let v = subst_var(value, from, to);
+            // If this `let` rebinds `from`, leave its body alone.
+            let b = if name == from {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            Term::Let {
+                name: name.clone(),
+                value: Box::new(v),
+                body: Box::new(b),
+            }
+        }
+        Term::If { cond, then, else_ } => Term::If {
+            cond: Box::new(subst_var(cond, from, to)),
+            then: Box::new(subst_var(then, from, to)),
+            else_: Box::new(subst_var(else_, from, to)),
+        },
+        Term::Do { op, args, tail } => Term::Do {
+            op: op.clone(),
+            args: args.iter().map(|a| subst_var(a, from, to)).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_var(a, from, to)).collect(),
+        },
+        Term::Match { scrutinee, arms } => Term::Match {
+            scrutinee: Box::new(subst_var(scrutinee, from, to)),
+            arms: arms
+                .iter()
+                .map(|a| {
+                    // Pattern-bound vars shadow `from` inside the arm.
+                    let mut binds: BTreeSet<String> = BTreeSet::new();
+                    pattern_binds(&a.pat, &mut binds);
+                    let body = if binds.contains(from) {
+                        a.body.clone()
+                    } else {
+                        subst_var(&a.body, from, to)
+                    };
+                    Arm { pat: a.pat.clone(), body }
+                })
+                .collect(),
+        },
+        Term::Lam { params, param_tys, ret_ty, effects, body } => {
+            let body = if params.iter().any(|p| p == from) {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            Term::Lam {
+                params: params.clone(),
+                param_tys: param_tys.clone(),
+                ret_ty: ret_ty.clone(),
+                effects: effects.clone(),
+                body: Box::new(body),
+            }
+        }
+        Term::Seq { lhs, rhs } => Term::Seq {
+            lhs: Box::new(subst_var(lhs, from, to)),
+            rhs: Box::new(subst_var(rhs, from, to)),
+        },
+        Term::LetRec { name, ty, params, body, in_term } => {
+            let body_shadowed = name == from || params.iter().any(|p| p == from);
+            let body_rw = if body_shadowed {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            let in_shadowed = name == from;
+            let in_rw = if in_shadowed {
+                (**in_term).clone()
+            } else {
+                subst_var(in_term, from, to)
+            };
+            Term::LetRec {
+                name: name.clone(),
+                ty: ty.clone(),
+                params: params.clone(),
+                body: Box::new(body_rw),
+                in_term: Box::new(in_rw),
+            }
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -446,6 +832,32 @@ mod tests {
             }
             Term::Lam { body, .. } => any_nested_ctor(body),
             Term::Seq { lhs, rhs } => any_nested_ctor(lhs) || any_nested_ctor(rhs),
+            Term::LetRec { body, in_term, .. } => {
+                any_nested_ctor(body) || any_nested_ctor(in_term)
+            }
+        }
+    }
+
+    /// Helper: walk a term, return true iff any [`Term::LetRec`] is
+    /// reachable. After 16b.1 desugaring this should be `false`.
+    fn any_let_rec(t: &Term) -> bool {
+        match t {
+            Term::Lit { .. } | Term::Var { .. } => false,
+            Term::App { callee, args, .. } => {
+                any_let_rec(callee) || args.iter().any(any_let_rec)
+            }
+            Term::Let { value, body, .. } => any_let_rec(value) || any_let_rec(body),
+            Term::If { cond, then, else_ } => {
+                any_let_rec(cond) || any_let_rec(then) || any_let_rec(else_)
+            }
+            Term::Do { args, .. } => args.iter().any(any_let_rec),
+            Term::Ctor { args, .. } => args.iter().any(any_let_rec),
+            Term::Match { scrutinee, arms } => {
+                any_let_rec(scrutinee) || arms.iter().any(|a| any_let_rec(&a.body))
+            }
+            Term::Lam { body, .. } => any_let_rec(body),
+            Term::Seq { lhs, rhs } => any_let_rec(lhs) || any_let_rec(rhs),
+            Term::LetRec { .. } => true,
         }
     }
 
@@ -568,4 +980,127 @@ mod tests {
         // at the top level (no Let-wrap).
         assert!(matches!(body, Term::Match { .. }));
     }
+
+    /// Iter 16b.1: a [`Term::LetRec`] whose body has no captures from
+    /// the enclosing scope is lifted to a synthetic top-level fn. The
+    /// resulting module's `defs` grows by one and the original LetRec
+    /// is gone from the term tree.
+    fn fact_letrec_term() -> Term {
+        // (let-rec fact (params n) (type ...) (body ...) (in (app fact 5)))
+        // Body just returns `n` so the test doesn't depend on `<=`/etc.
+        Term::LetRec {
+            name: "fact".into(),
+            ty: Type::Fn {
+                params: vec![Type::int()],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            params: vec!["n".into()],
+            body: Box::new(Term::Var { name: "n".into() }),
+            in_term: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "fact".into() }),
+                args: vec![Term::Lit { lit: Literal::Int { value: 5 } }],
+                tail: false,
+            }),
+        }
+    }
+
+    #[test]
+    fn let_rec_no_capture_lifts_to_top_level() {
+        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: fact_letrec_term(),
+                doc: None,
+            })],
+        };
+        let out = desugar_module(&m);
+        // One original + one lifted = two defs.
+        assert_eq!(out.defs.len(), 2, "expected one lifted fn appended");
+        // The new def is a fn whose name starts with the LetRec hint.
+        let lifted = match &out.defs[1] {
+            Def::Fn(f) => f,
+            _ => panic!("expected a lifted FnDef"),
+        };
+        assert!(
+            lifted.name.starts_with("fact$lr_"),
+            "lifted name `{}` should start with `fact$lr_`",
+            lifted.name
+        );
+        assert_eq!(lifted.params, vec!["n".to_string()]);
+        // The original main's body must no longer contain a LetRec.
+        let main_body = match &out.defs[0] {
+            Def::Fn(f) => &f.body,
+            _ => unreachable!(),
+        };
+        assert!(
+            !any_let_rec(main_body),
+            "desugarer must remove every Term::LetRec from the term tree; got: {main_body:#?}"
+        );
+        // The in-term of the LetRec was `(app fact 5)`; after the lift
+        // it should be `(app <lifted_name> 5)`.
+        match main_body {
+            Term::App { callee, .. } => match callee.as_ref() {
+                Term::Var { name } => assert_eq!(name, &lifted.name),
+                other => panic!("expected lifted Var as callee, got {other:?}"),
+            },
+            other => panic!("expected App in main body, got {other:?}"),
+        }
+    }
+
+    /// 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.
+    #[test]
+    #[should_panic(expected = "would capture")]
+    fn let_rec_with_capture_panics() {
+        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![Type::int()],
+                    ret: Box::new(Type::int()),
+                    effects: vec![],
+                },
+                params: vec!["outer".into()],
+                // (let-rec helper (params x) ... (body (app + x outer)) ...)
+                body: 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: "outer".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,
+                    }),
+                },
+                doc: None,
+            })],
+        };
+        let _ = desugar_module(&m);
+    }
 }

crates/ailang-surface/src/parse.rs

@@ -36,7 +36,7 @@
 //! term        ::= var-ref | int-lit | str-lit | bool-lit | unit-lit
 //!               | app-term | tail-app-term | match-term | ctor-term
 //!               | do-term | tail-do-term | seq-term | lam-term | if-term
-//!               | let-term
+//!               | let-term | let-rec-term
 //! var-ref     ::= ident                  ; reserved: true/false → bool-lit
 //! int-lit     ::= integer                ; numeric atom
 //! str-lit     ::= string                 ; string atom
@@ -56,6 +56,11 @@
 //! typed-param ::= "(" "typed" ident type ")"
 //! if-term     ::= "(" "if" term term term ")"
 //! let-term    ::= "(" "let" ident term term ")"
+//! let-rec-term ::= "(" "let-rec" ident
+//!                      "(" "params" ident* ")"
+//!                      type-attr
+//!                      body-attr
+//!                      "(" "in" term ")" ")"
 //!
 //! pattern  ::= pat-var | pat-ctor | pat-lit | pat-wild
 //! pat-var  ::= ident
@@ -690,13 +695,14 @@ impl<'a> Parser<'a> {
                     "lam" => self.parse_lam(),
                     "if" => self.parse_if(),
                     "let" => self.parse_let(),
+                    "let-rec" => self.parse_let_rec(),
                     other => {
                         let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
                         Err(ParseError::Production {
                             production: "term",
                             message: format!(
                                 "unknown term head `{other}`; expected one of \
-                                `app`, `tail-app`, `lam`, `let`, `if`, `match`, `do`, \
+                                `app`, `tail-app`, `lam`, `let`, `let-rec`, `if`, `match`, `do`, \
                                 `tail-do`, `seq`, `term-ctor`, `lit-unit`"
                             ),
                             pos,
@@ -943,6 +949,34 @@ impl<'a> Parser<'a> {
         })
     }
 
+    /// Iter 16b.1: `(let-rec NAME (params PARAM*) (type T) (body TERM)
+    /// (in TERM))` — local recursive fn-shaped binding. Eliminated by
+    /// the desugar pass (lifted to a synthetic top-level fn) before
+    /// typecheck. The body's recursive references to `NAME` are
+    /// rewritten to the lifted name; the `in`-clause becomes the term
+    /// that replaces the LetRec.
+    fn parse_let_rec(&mut self) -> Result<Term, ParseError> {
+        self.expect_lparen("let-rec-term")?;
+        self.expect_keyword("let-rec")?;
+        let name = self.expect_ident("let-rec name")?;
+        let params = self.parse_params_attr()?;
+        let ty = self.parse_type_attr()?;
+        let body = self.parse_body_attr()?;
+        // (in TERM)
+        self.expect_lparen("let-rec in-clause")?;
+        self.expect_keyword("in")?;
+        let in_term = self.parse_term()?;
+        self.expect_rparen("let-rec in-clause")?;
+        self.expect_rparen("let-rec-term")?;
+        Ok(Term::LetRec {
+            name,
+            ty,
+            params,
+            body: Box::new(body),
+            in_term: Box::new(in_term),
+        })
+    }
+
     // ---- patterns -------------------------------------------------------
 
     fn parse_pattern(&mut self) -> Result<Pattern, ParseError> {
@@ -1081,4 +1115,45 @@ mod tests {
         .unwrap();
         assert!(matches!(m.defs.len(), 1));
     }
+
+    /// Iter 16b.1: minimal `(let-rec ...)` round-trips through the
+    /// parser into a `Term::LetRec` whose `name`, `params`, `body` and
+    /// `in_term` line up with the source.
+    #[test]
+    fn parses_minimal_let_rec() {
+        let m = parse(
+            r#"
+            (module m
+              (fn main
+                (type (fn-type (params) (ret (con Int))))
+                (params)
+                (body
+                  (let-rec f
+                    (params x)
+                    (type (fn-type (params (con Int)) (ret (con Int))))
+                    (body x)
+                    (in (app f 1))))))
+            "#,
+        )
+        .unwrap();
+        let body = match &m.defs[0] {
+            Def::Fn(fd) => &fd.body,
+            _ => panic!("expected fn"),
+        };
+        match body {
+            Term::LetRec { name, params, body, in_term, .. } => {
+                assert_eq!(name, "f");
+                assert_eq!(params, &vec!["x".to_string()]);
+                assert!(matches!(body.as_ref(), Term::Var { name } if name == "x"));
+                match in_term.as_ref() {
+                    Term::App { callee, args, .. } => {
+                        assert!(matches!(callee.as_ref(), Term::Var { name } if name == "f"));
+                        assert_eq!(args.len(), 1);
+                    }
+                    other => panic!("expected App in in-clause, got {other:?}"),
+                }
+            }
+            other => panic!("expected LetRec, got {other:?}"),
+        }
+    }
 }

crates/ailang-surface/src/print.rs

@@ -245,6 +245,22 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             write_term(out, body, level);
             out.push(')');
         }
+        Term::LetRec { name, ty, params, body, in_term } => {
+            out.push_str("(let-rec ");
+            out.push_str(name);
+            out.push_str(" (params");
+            for p in params {
+                out.push(' ');
+                out.push_str(p);
+            }
+            out.push_str(") (type ");
+            write_type(out, ty);
+            out.push_str(") (body ");
+            write_term(out, body, level);
+            out.push_str(") (in ");
+            write_term(out, in_term, level);
+            out.push_str("))");
+        }
         Term::If { cond, then, else_ } => {
             out.push_str("(if ");
             write_term(out, cond, level);