Iter 16b.6: LetRec inside polymorphic enclosing fn

Lifts the monomorphic-only restriction. Lifted top-level fn now
becomes Forall(α..., Fn(t..., T...) -> tr) when the enclosing fn
is polymorphic; capture types may mention outer type vars and
the existing mono pipeline (Iter 12b/14a) specializes them
correctly at call sites.

- desugar.rs / lift.rs: scope-building unified — Forall fn-params
  are now KnownType, not LetBound. Lift wraps augmented_ty in
  Forall mirroring the enclosing fn.
- Name-as-value-in-in-term in a polymorphic enclosing fn is
  rejected (eta-Lam wrap from 16b.5 has no Forall). Queued
  separately as closure-conversion-with-polymorphism.
- examples/poly_rec_capture.{ailx,ail.json}: apply_n_times :
  Forall(a). drives at Int and Bool to exercise two mono
  instantiations.
- e2e + check + desugar tests: 116 → 120 (+4).

Codegen pipeline untouched — apply_subst_to_type substitutes
through Fn.params uniformly (original params + appended captures).

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

crates/ail/tests/e2e.rs

@@ -537,6 +537,34 @@ fn local_rec_as_value_capture_demo() {
     assert_eq!(lines, vec!["1320", "12120"]);
 }
 
+/// Iter 16b.6: LetRec inside a polymorphic enclosing fn.
+/// Property protected: when the enclosing fn is `Forall(a). Fn(...)`,
+/// the desugar/lift pipeline now (a) enters fn-params as `KnownType`
+/// (not `LetBound`) so a LetRec inside CAN capture them, and (b)
+/// builds the synthetic lifted fn's signature as
+/// `Forall(a). Fn(t1..tk, T1..Tm) -> tr`, mirroring the enclosing
+/// fn's type vars. Capture types `T1..Tm` may mention `a`; the
+/// outer Forall binds them. Codegen's mono pipeline (Iter 12b/14a)
+/// then specialises `loop$lr_0` at every call with the same type
+/// args as the enclosing `apply_n_times`.
+///
+/// `main` drives `apply_n_times` at TWO distinct instantiations
+/// (`Int` with `succ`, `Bool` with `flip`) so the mono path is
+/// exercised twice, producing both `loop$lr_0__I` and
+/// `loop$lr_0__B` in the IR. Without 16b.6 the desugar pass would
+/// have rejected the LetRec capture as a `LetBound`-style failure
+/// (the 16b.2-era `Type::Forall` fallback marked all fn-params as
+/// `LetBound`).
+///
+/// Expected stdout: 5 (succ applied 5 times to 0), false (flip
+/// applied 4 times to false — even count of flips ⇒ false).
+#[test]
+fn poly_rec_capture_demo() {
+    let stdout = build_and_run("poly_rec_capture.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(lines, vec!["5", "false"]);
+}
+
 /// 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

@@ -3394,4 +3394,166 @@ mod tests {
         );
         assert_eq!(synth.params, vec!["z".to_string(), "x".to_string()]);
     }
+
+    /// Iter 16b.6: post-typecheck `lift_letrecs` lifts a deferred
+    /// LetRec inside a polymorphic enclosing fn into a `Forall`-typed
+    /// synthetic top-level fn, mirroring the enclosing fn's type
+    /// vars. Property protected:
+    ///
+    /// 1. The fast-path desugar lift handles the `KnownType`-only
+    ///    case end-to-end (see desugar's
+    ///    `let_rec_capture_under_polymorphic_enclosing_fn_lifts_to_forall_fn`).
+    /// 2. The defer path (some capture is `Term::Let`-bound) goes
+    ///    through `lift_letrecs`. This test forces that path by
+    ///    introducing a `Term::Let { z = 7 }` inside the body and
+    ///    capturing `z`. The lifted fn must still be `Forall(a). Fn(...)`,
+    ///    even though the lift happens post-typecheck rather than
+    ///    in desugar.
+    ///
+    /// Without 16b.6, lift_letrecs would have panicked on the
+    /// `Type::Forall` match arm at lift-construction time.
+    #[test]
+    fn lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn() {
+        // fn outer : Forall(a). (a) -> a = \x.
+        //   let z = 7
+        //   in let-rec helper : (Int) -> a = \k. if k == 0 then x else helper(k-1) + z (impossible — types don't match)
+        //
+        // Simpler shape: capture z (Let-bound, Int) in a polymorphic
+        // enclosing fn, with a body that returns x (the polymorphic
+        // capture).
+        //
+        // fn outer : Forall(a). (a) -> a = \x.
+        //   let z = 7
+        //   in let-rec helper : (Int) -> a = \k.
+        //     if k == 0 then x else helper(k - z)
+        //   in helper 1
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_def(
+                "outer",
+                Type::Forall {
+                    vars: vec!["a".into()],
+                    body: Box::new(Type::Fn {
+                        params: vec![Type::Var { name: "a".into() }],
+                        ret: Box::new(Type::Var { name: "a".into() }),
+                        effects: vec![],
+                    }),
+                },
+                vec!["x".into()],
+                Term::Let {
+                    name: "z".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::Var { name: "a".into() }),
+                            effects: vec![],
+                        },
+                        params: vec!["k".into()],
+                        body: Box::new(Term::If {
+                            cond: Box::new(Term::App {
+                                callee: Box::new(Term::Var { name: "==".into() }),
+                                args: vec![
+                                    Term::Var { name: "k".into() },
+                                    Term::Lit { lit: Literal::Int { value: 0 } },
+                                ],
+                                tail: false,
+                            }),
+                            then: Box::new(Term::Var { name: "x".into() }),
+                            else_: Box::new(Term::App {
+                                callee: Box::new(Term::Var { name: "helper".into() }),
+                                args: vec![Term::App {
+                                    callee: Box::new(Term::Var { name: "-".into() }),
+                                    args: vec![
+                                        Term::Var { name: "k".into() },
+                                        Term::Var { name: "z".into() },
+                                    ],
+                                    tail: false,
+                                }],
+                                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 succeeds.
+        check(&m).expect("typecheck before lift");
+        let desugared = ailang_core::desugar::desugar_module(&m);
+        // After desugar the LetRec should still be present (the
+        // capture set is `{x: KnownType, z: LetBound}` and any
+        // LetBound forces deferral).
+        let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
+        assert_eq!(
+            lifted.defs.len(),
+            2,
+            "expected one synthetic fn appended; got {:?}",
+            lifted.defs.iter().map(|d| d.name()).collect::<Vec<_>>()
+        );
+        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
+        );
+        // Lifted ty must be Forall(a). Fn(Int, a, Int) -> a.
+        // Original LetRec params: [Int]; captures (BTreeSet order):
+        // x: a then z: Int (alphabetical). Ret: a.
+        match &synth.ty {
+            Type::Forall { vars, body } => {
+                assert_eq!(
+                    vars,
+                    &vec!["a".to_string()],
+                    "Forall vars must mirror enclosing fn's vars; got {:?}",
+                    vars
+                );
+                match body.as_ref() {
+                    Type::Fn { params, ret, .. } => {
+                        assert_eq!(params.len(), 3, "expected k + x + z params");
+                        assert!(
+                            matches!(&params[0], Type::Con { name, .. } if name == "Int"),
+                            "first param: original k:Int; got {:?}",
+                            params[0]
+                        );
+                        // Captures are in BTreeSet order, so x (a-typed) comes before z (Int).
+                        assert!(
+                            matches!(&params[1], Type::Var { name } if name == "a"),
+                            "second param: x: a; got {:?}",
+                            params[1]
+                        );
+                        assert!(
+                            matches!(&params[2], Type::Con { name, .. } if name == "Int"),
+                            "third param: z: Int; got {:?}",
+                            params[2]
+                        );
+                        assert!(
+                            matches!(ret.as_ref(), Type::Var { name } if name == "a"),
+                            "ret: a; got {:?}",
+                            ret
+                        );
+                    }
+                    other => panic!("Forall body must be Fn; got {:?}", other),
+                }
+            }
+            other => panic!(
+                "lifted type must be Forall (mirroring enclosing); got {:?}",
+                other
+            ),
+        }
+        assert_eq!(
+            synth.params,
+            vec!["k".to_string(), "x".to_string(), "z".to_string()]
+        );
+    }
 }

crates/ailang-check/src/lift.rs

@@ -130,6 +130,7 @@ pub fn lift_letrecs(m: &Module) -> Result<Module> {
         counter,
         module_names: &mut module_names,
         lifted: Vec::new(),
+        current_def_forall_vars: Vec::new(),
     };
     let _ = &mut counter; // counter lives in lifter from here on
 
@@ -164,7 +165,17 @@ pub fn lift_letrecs(m: &Module) -> Result<Module> {
                         }
                     }
                 }
+                // Iter 16b.6: stash the enclosing fn's Forall.vars (or
+                // empty for a monomorphic enclosing fn) for the LetRec
+                // arm. Save and restore so it never leaks across defs.
+                let saved_forall_vars =
+                    std::mem::take(&mut lifter.current_def_forall_vars);
+                lifter.current_def_forall_vars = match &f.ty {
+                    Type::Forall { vars, .. } => vars.clone(),
+                    _ => Vec::new(),
+                };
                 f.body = lifter.lift_in_term(&f.body, &mut locals, &f.name)?;
+                lifter.current_def_forall_vars = saved_forall_vars;
                 for v in rigids_added {
                     lifter.env.rigid_vars.remove(&v);
                 }
@@ -184,11 +195,22 @@ pub fn lift_letrecs(m: &Module) -> Result<Module> {
 /// State for a single-module lift pass. Mirrors `Desugarer` in
 /// `ailang-core::desugar` but resolves capture types via `synth`
 /// instead of relying on a `ScopeEntry` map.
+///
+/// Iter 16b.6 field:
+/// - `current_def_forall_vars` carries the enclosing fn's
+///   `Type::Forall.vars` while lifting its body. Empty for monomorphic
+///   enclosing fns. Read by the LetRec arm to wrap the synthetic
+///   lifted fn's signature in `Type::Forall` mirroring the enclosing
+///   fn — the lifted fn enters codegen's monomorphisation queue at
+///   every call site, specialising at the same type args as its host.
 struct Lifter<'a> {
     env: Env,
     counter: u64,
     module_names: &'a mut BTreeSet<String>,
     lifted: Vec<Def>,
+    /// Iter 16b.6: enclosing fn's Forall.vars (or empty if mono).
+    /// Reset on entry to each `Def::Fn`.
+    current_def_forall_vars: Vec<String>,
 }
 
 impl<'a> Lifter<'a> {
@@ -393,6 +415,22 @@ impl<'a> Lifter<'a> {
                 // is built below after we know `lifted_name` and `extras`.
                 let in_has_value_use = find_non_callee_use(&lifted_in, name).is_some();
 
+                // Iter 16b.6: reject name-as-value in `in_term` when the
+                // enclosing fn is polymorphic — the eta-Lam wrap would
+                // need to be `Forall`-quantified, but `Term::Lam` has no
+                // such slot. Closure conversion with polymorphism is the
+                // proper fix; queued as `closure-poly` (informally
+                // 16b.5b). Mono enclosing fn + name-as-value-in-in-term
+                // continues to work via the eta-Lam wrap.
+                if in_has_value_use && !self.current_def_forall_vars.is_empty() {
+                    panic!(
+                        "Iter 16b.6: name-as-value of LetRec `{name}` is not yet \
+                         supported in a polymorphic enclosing fn — closure conversion \
+                         with polymorphism would be required. Queued separately as \
+                         `closure-poly` (informally 16b.5b)."
+                    );
+                }
+
                 // Recompute captures of the lifted body against the
                 // current `locals` (deterministic order via BTreeSet).
                 let mut local_bound: BTreeSet<String> = BTreeSet::new();
@@ -422,7 +460,19 @@ impl<'a> Lifter<'a> {
                 }
 
                 // Build the lifted FnDef.
-                let augmented_ty = match ty {
+                //
+                // Iter 16b.6: when the enclosing fn is polymorphic, wrap
+                // the augmented Fn in a `Type::Forall` mirroring the
+                // enclosing fn's type vars (`current_def_forall_vars`).
+                // The capture types may mention any of those vars; the
+                // Forall binds them. Codegen's mono pipeline (Iter
+                // 12b/14a) specialises `f$lr_N` at every call site with
+                // the same type args as the enclosing fn's current
+                // mono — see `apply_subst_to_type`, which substitutes
+                // through both the original params and the appended
+                // capture types uniformly because they're all `Type::Fn`
+                // params at the AST level.
+                let inner_augmented_ty = match ty {
                     Type::Fn { params: ps, ret, effects } => {
                         let mut new_ps = ps.clone();
                         for (_, t) in &capture_types {
@@ -435,14 +485,22 @@ impl<'a> Lifter<'a> {
                         }
                     }
                     Type::Forall { .. } => panic!(
-                        "Iter 16b.3 invariant: LetRec `{name}` has Forall type at lift; \
-                         desugar should have rejected (queued for 16b.6)"
+                        "Iter 16b.6 invariant: LetRec `{name}` has its OWN Forall type at \
+                         lift; LetRec doesn't quantify, only the enclosing fn does"
                     ),
                     other => panic!(
                         "Iter 16b.3 invariant: LetRec `{name}` non-Fn/Forall type {:?}",
                         other
                     ),
                 };
+                let augmented_ty = if self.current_def_forall_vars.is_empty() {
+                    inner_augmented_ty
+                } else {
+                    Type::Forall {
+                        vars: self.current_def_forall_vars.clone(),
+                        body: Box::new(inner_augmented_ty),
+                    }
+                };
                 let mut augmented_params = params.clone();
                 for (cn, _) in &capture_types {
                     augmented_params.push(cn.clone());

crates/ailang-core/src/desugar.rs

@@ -180,43 +180,63 @@ pub fn desugar_module(m: &Module) -> Module {
         used,
         lifted: Vec::new(),
         module_top_names,
+        current_def_forall_vars: Vec::new(),
     };
     let mut out = m.clone();
     for def in &mut out.defs {
         match def {
             Def::Fn(f) => {
-                // 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.
+                // Iter 16b.2 / 16b.6: build initial scope from fn-params
+                // with their declared types (peeled out of `f.ty`).
+                //
+                // 16b.6: a `Type::Forall { vars, body: Fn(ptys, ...) }`
+                // enclosing fn is now supported. Its param types may
+                // mention `vars` — that's fine, the lifted fn becomes
+                // `Forall(vars, Fn(ptys ++ capture_tys, ...))` so the
+                // type vars are still bound at the lift site. Fn-params
+                // of a Forall enclosing fn therefore enter the scope as
+                // `KnownType`, not `LetBound` (the 16b.2 fallback was
+                // overly conservative). The enclosing fn's `Forall.vars`
+                // are stashed in `Desugarer.current_def_forall_vars` for
+                // the LetRec arm to read.
                 let mut scope: BTreeMap<String, ScopeEntry> = BTreeMap::new();
-                match &f.ty {
-                    Type::Fn { params: ptys, .. } if ptys.len() == f.params.len() => {
+                let inner_fn_ty: Option<&Type> = match &f.ty {
+                    Type::Fn { .. } => Some(&f.ty),
+                    Type::Forall { body, .. } => match body.as_ref() {
+                        Type::Fn { .. } => Some(body.as_ref()),
+                        _ => None,
+                    },
+                    _ => None,
+                };
+                let inner_fn_params: Option<&[Type]> = inner_fn_ty.and_then(|t| match t {
+                    Type::Fn { params, .. } => Some(params.as_slice()),
+                    _ => None,
+                });
+                match inner_fn_params {
+                    Some(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.
+                        // Defensive: malformed fn type (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);
                         }
                     }
                 }
+                // Iter 16b.6: stash the enclosing fn's Forall.vars (or
+                // empty for a mono enclosing fn) for the LetRec arm.
+                let saved = std::mem::take(&mut d.current_def_forall_vars);
+                d.current_def_forall_vars = match &f.ty {
+                    Type::Forall { vars, .. } => vars.clone(),
+                    _ => Vec::new(),
+                };
                 f.body = d.desugar_term(&f.body, &scope);
+                d.current_def_forall_vars = saved;
             }
             Def::Const(c) => {
                 let scope: BTreeMap<String, ScopeEntry> = BTreeMap::new();
@@ -329,11 +349,23 @@ fn collect_used_in_pattern(p: &Pattern, used: &mut BTreeSet<String>) {
 ///   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.
+///
+/// Iter 16b.6 field:
+/// - `current_def_forall_vars` carries the enclosing fn's
+///   `Type::Forall.vars` while desugaring its body. Empty for
+///   monomorphic enclosing fns. Read by the LetRec lifter to wrap
+///   the synthetic lifted fn's signature in `Type::Forall` mirroring
+///   the enclosing fn — so the lifted fn enters codegen's
+///   monomorphisation queue at every call site of the enclosing fn,
+///   specialising at the same type args as its host.
 struct Desugarer {
     counter: u64,
     used: BTreeSet<String>,
     lifted: Vec<Def>,
     module_top_names: BTreeSet<String>,
+    /// Iter 16b.6: the enclosing fn's Forall.vars (or empty if mono).
+    /// Reset on entry to each `Def::Fn`.
+    current_def_forall_vars: Vec<String>,
 }
 
 impl Desugarer {
@@ -556,6 +588,25 @@ impl Desugarer {
                 }
                 let in_has_value_use = find_non_callee_use(&desugared_in, name).is_some();
 
+                // Iter 16b.6: reject name-as-value in `in_term` when the
+                // enclosing fn is polymorphic. The 16b.5 wrap synthesises
+                // a `Term::Lam` whose AST has no `Forall` slot, so
+                // wrapping a polymorphic lifted fn into a monomorphic Lam
+                // would lose the type vars. Solving this needs closure
+                // conversion with polymorphism (queue tag `closure-poly`
+                // / informally `16b.5b`). Other 16b.5 use cases — name-
+                // as-value in a MONOMORPHIC enclosing fn — continue to
+                // work via the eta-Lam wrap.
+                if in_has_value_use && !self.current_def_forall_vars.is_empty() {
+                    panic!(
+                        "Iter 16b.6: name-as-value of LetRec `{}` is not yet supported in \
+                         a polymorphic enclosing fn — closure conversion with \
+                         polymorphism would be required. Queued separately as \
+                         `closure-poly` (informally 16b.5b).",
+                        name
+                    );
+                }
+
                 // Capture detection (against the *outer* scope, before
                 // the body-scope extension).
                 let mut local_bound: BTreeSet<String> = BTreeSet::new();
@@ -633,9 +684,22 @@ impl Desugarer {
                     .collect();
 
                 // 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 {
+                // appended to `params`.
+                //
+                // Iter 16b.6: when the ENCLOSING fn is polymorphic
+                // (`current_def_forall_vars` non-empty), wrap the
+                // augmented Fn in a `Type::Forall` mirroring the
+                // enclosing fn's type vars. The capture types may
+                // mention any of those vars; that's fine — the Forall
+                // binds them. At every call site of the LetRec name
+                // inside the enclosing fn's body, codegen's Iter
+                // 12b/14a monomorphisation specialises `f$lr_N` at the
+                // same type args as the enclosing fn's current mono.
+                //
+                // The LetRec's own `ty` (`Type::Fn` — never `Forall`,
+                // since LetRec itself doesn't quantify) is the inner
+                // type.
+                let inner_augmented_ty = match ty {
                     Type::Fn { params: ps, ret, effects } => {
                         let mut new_ps = ps.clone();
                         for (_, t) in &capture_types {
@@ -648,8 +712,9 @@ impl Desugarer {
                         }
                     }
                     Type::Forall { .. } => panic!(
-                        "Iter 16b.3: LetRec `{}` has a Forall type; captures from a \
-                         polymorphic context are not supported. Queued for 16b.6.",
+                        "Iter 16b.6 invariant: LetRec `{}` has a Forall type at its \
+                         own declaration; LetRec doesn't quantify, only the enclosing \
+                         fn does",
                         name
                     ),
                     other => panic!(
@@ -657,6 +722,14 @@ impl Desugarer {
                         name, other
                     ),
                 };
+                let augmented_ty = if self.current_def_forall_vars.is_empty() {
+                    inner_augmented_ty
+                } else {
+                    Type::Forall {
+                        vars: self.current_def_forall_vars.clone(),
+                        body: Box::new(inner_augmented_ty),
+                    }
+                };
                 // Augmented param-name list: original params + capture
                 // names (using the captured variable names directly so
                 // the lifted body's references already resolve
@@ -2030,6 +2103,192 @@ mod tests {
         }
     }
 
+    /// Iter 16b.6: a LetRec inside a polymorphic enclosing fn gets its
+    /// fn-param captures lifted with a `Forall(vars, Fn(...))` augmented
+    /// signature, mirroring the enclosing fn's type vars. Without 16b.6,
+    /// the desugar pass would have classified the fn-params as
+    /// `LetBound` (16b.2 fallback) and deferred to `lift_letrecs`; with
+    /// 16b.6, the fn-params are `KnownType` and the fast-path lift fires
+    /// here, producing a `Forall`-typed synthetic FnDef.
+    #[test]
+    fn let_rec_capture_under_polymorphic_enclosing_fn_lifts_to_forall_fn() {
+        // (fn id_n_times : Forall(a). Fn(Int, a) -> a
+        //   (params n x)
+        //   (body
+        //     (let-rec loop : Fn(Int, a) -> a (params k acc)
+        //       (body (if (== k 0) acc (app loop (- k 1) acc)))
+        //       (in (app loop n x)))))
+        // Captures: none (all references inside the body are to params
+        // of `loop` itself or top-level builtins). To force a capture
+        // of an `a`-typed param, use the simpler shape:
+        //
+        // (fn rec_id : Forall(a). Fn(a) -> a
+        //   (params x)
+        //   (body
+        //     (let-rec loop : Fn(Int) -> a (params k)
+        //       (body (if (== k 0) x (app loop (- k 1))))
+        //       (in (app loop 1)))))
+        //
+        // Here `loop` captures `x: a` from the enclosing fn's params.
+        // Without 16b.6, `x` would be ScopeEntry::LetBound (because the
+        // enclosing fn is Forall) and the LetRec would defer; with
+        // 16b.6, `x` is KnownType and the lift fires here.
+        let letrec = Term::LetRec {
+            name: "loop".into(),
+            ty: Type::Fn {
+                params: vec![Type::int()],
+                ret: Box::new(Type::Var { name: "a".into() }),
+                effects: vec![],
+            },
+            params: vec!["k".into()],
+            body: Box::new(Term::If {
+                cond: Box::new(Term::App {
+                    callee: Box::new(Term::Var { name: "==".into() }),
+                    args: vec![
+                        Term::Var { name: "k".into() },
+                        Term::Lit { lit: Literal::Int { value: 0 } },
+                    ],
+                    tail: false,
+                }),
+                then: Box::new(Term::Var { name: "x".into() }),
+                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: "k".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: 1 } }],
+                tail: false,
+            }),
+        };
+        let m = Module {
+            schema: crate::SCHEMA.to_string(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![Def::Fn(FnDef {
+                name: "rec_id".into(),
+                ty: Type::Forall {
+                    vars: vec!["a".into()],
+                    body: Box::new(Type::Fn {
+                        params: vec![Type::Var { name: "a".into() }],
+                        ret: Box::new(Type::Var { name: "a".into() }),
+                        effects: vec![],
+                    }),
+                },
+                params: vec!["x".into()],
+                body: letrec,
+                doc: None,
+            })],
+        };
+        let out = desugar_module(&m);
+        assert_eq!(
+            out.defs.len(),
+            2,
+            "expected one lifted fn appended; got {:?}",
+            out.defs.iter().map(|d| d.name()).collect::<Vec<_>>()
+        );
+        let lifted = match &out.defs[1] {
+            Def::Fn(fd) => fd,
+            _ => unreachable!(),
+        };
+        assert!(
+            lifted.name.starts_with("loop$lr_"),
+            "unexpected lifted-name shape: {}",
+            lifted.name
+        );
+        // Lifted type must be Forall(a). Fn(Int, a) -> a (k + x capture).
+        match &lifted.ty {
+            Type::Forall { vars, body } => {
+                assert_eq!(vars, &vec!["a".to_string()], "Forall vars must mirror enclosing");
+                match body.as_ref() {
+                    Type::Fn { params, ret, .. } => {
+                        assert_eq!(params.len(), 2, "expected Int + a-typed capture");
+                        assert!(
+                            matches!(&params[0], Type::Con { name, .. } if name == "Int"),
+                            "first param must be Int (loop's own k); got {:?}",
+                            params[0]
+                        );
+                        assert!(
+                            matches!(&params[1], Type::Var { name } if name == "a"),
+                            "second param must be the captured `x: a`; got {:?}",
+                            params[1]
+                        );
+                        assert!(
+                            matches!(ret.as_ref(), Type::Var { name } if name == "a"),
+                            "ret must be `a`; got {:?}",
+                            ret
+                        );
+                    }
+                    other => panic!("Forall body must be Fn; got {:?}", other),
+                }
+            }
+            other => panic!("lifted type must be Forall; got {:?}", other),
+        }
+        // Lifted params: original "k" + captured "x".
+        assert_eq!(lifted.params, vec!["k".to_string(), "x".to_string()]);
+    }
+
+    /// Iter 16b.6: a LetRec inside a polymorphic enclosing fn whose
+    /// `in_term` uses the LetRec name as a value (not as a callee) is
+    /// rejected. The 16b.5 eta-Lam wrap can't quantify `Forall.vars`
+    /// because `Term::Lam` has no Forall slot — wrapping a polymorphic
+    /// lifted fn into a monomorphic Lam loses the type vars. Queued
+    /// separately as `closure-poly` (informally 16b.5b).
+    #[test]
+    #[should_panic(expected = "16b.6")]
+    fn let_rec_name_as_value_in_polymorphic_enclosing_fn_panics() {
+        // Same shape as `let_rec_name_as_value_in_in_term_wraps_to_eta_lam`
+        // but the enclosing fn is Forall-quantified.
+        let letrec = Term::LetRec {
+            name: "f".into(),
+            ty: Type::Fn {
+                params: vec![Type::int()],
+                ret: Box::new(Type::Var { name: "a".into() }),
+                effects: vec![],
+            },
+            params: vec!["k".into()],
+            body: Box::new(Term::Var { name: "x".into() }),
+            in_term: Box::new(Term::Let {
+                name: "g".into(),
+                value: Box::new(Term::Var { name: "f".into() }), // value-position f
+                body: Box::new(Term::App {
+                    callee: Box::new(Term::Var { name: "g".into() }),
+                    args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
+                    tail: false,
+                }),
+            }),
+        };
+        let m = Module {
+            schema: crate::SCHEMA.to_string(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![Def::Fn(FnDef {
+                name: "outer".into(),
+                ty: Type::Forall {
+                    vars: vec!["a".into()],
+                    body: Box::new(Type::Fn {
+                        params: vec![Type::Var { name: "a".into() }],
+                        ret: Box::new(Type::Var { name: "a".into() }),
+                        effects: vec![],
+                    }),
+                },
+                params: vec!["x".into()],
+                body: letrec,
+                doc: None,
+            })],
+        };
+        let _ = desugar_module(&m);
+    }
+
     /// Iter 16c: walks a term, returns true iff any [`Pattern::Lit`] is
     /// reachable in any [`Term::Match`] arm. After 16c desugaring, the
     /// invariant is `false` for every desugared output — `Pattern::Lit`

docs/JOURNAL.md

@@ -4163,3 +4163,182 @@ inside the body before the lift completes is order-sensitive) or
 a true closure conversion that doesn't lift to a top-level fn at
 all. **16b.6** (Forall-typed LetRec), **16b.7** (nested mutual
 LetRec capture), 16d, 16e, 17a unchanged.
+
+## Iter 16b.6 — LetRec inside polymorphic enclosing fn
+
+**Goal.** Lift the "monomorphic enclosing fn only" restriction
+that 16b.2 introduced. A `(let-rec ...)` inside a fn whose
+declared type is `Forall(α1..αn, Fn(...))` is now supported,
+provided (a) the LetRec name is callee-only (any non-callee use
+in `body` was already rejected by 16b.5; non-callee use in
+`in_term` is rejected for the polymorphic case here — see
+"closure-poly" below), and (b) other 16b.x restrictions still
+apply (no nested LetRec mutual capture → 16b.7).
+
+**Architectural choice.** The lifted top-level fn is built as
+`Forall(α1..αn, Fn(t1..tk, T1..Tm) → tr)` where `α1..αn` are
+exactly the enclosing fn's type vars. Capture types `T1..Tm`
+may mention any of those vars; the outer `Forall` binds them
+back. Inside the enclosing fn's body every call site of the
+lifted fn is monomorphic relative to the enclosing fn's current
+instantiation, so codegen's existing Iter-12b/14a
+monomorphisation machinery picks up `f$lr_N` from the
+`mono_queue`, substitutes type args into both the original
+params and the appended capture types (a single
+`apply_subst_to_type` traversal handles both — captures live
+in the same `Type::Fn.params` list as originals), and emits
+specialised `f$lr_N__I`, `f$lr_N__B`, … per instantiation.
+**No codegen changes were needed**: the lifted fn becomes an
+ordinary `Forall` top-level fn and flows through the same
+pipeline as a user-written polymorphic def.
+
+**Scope-building change.** 16b.2 entered fn-params of a
+`Forall`-typed enclosing fn as `ScopeEntry::LetBound` —
+defensive, because the param types could mention outer type
+vars and the lift had no way to bind them. With the
+`Forall(vars, Fn(t1..tk, T1..Tm) → tr)` synthesis above, that
+bind site now exists. Fn-params of a polymorphic enclosing fn
+therefore enter the scope as `ScopeEntry::KnownType(t)`
+(matching the monomorphic case). The `LetBound` fallback is
+reserved for `Term::Let`-bound names and for malformed fn
+types (arity mismatch, non-Fn). Both `Desugarer` and `Lifter`
+gained a `current_def_forall_vars: Vec<String>` field that's
+populated on entry to each `Def::Fn` and read by the LetRec
+arm to decide whether to wrap the augmented type in a
+`Forall`.
+
+**Why name-as-value-in-in-term is excluded for the polymorphic
+case.** The 16b.5 wrap synthesises a `Term::Lam` whose body
+calls the lifted fn positionally. `Term::Lam` has no
+`Forall`-quantification slot — wrapping a polymorphic lifted
+fn into a monomorphic Lam would lose the type vars. The
+proper fix is closure conversion with polymorphism (a closure
+pair generic over `α1..αn`); that's a separate, harder iter.
+Both desugar and lift now panic with a clear message
+referencing queue tag `closure-poly` (informally `16b.5b`)
+when this combination is detected. Name-as-value-in-in-term
+in a MONOMORPHIC enclosing fn continues to work via the
+16b.5 eta-Lam wrap.
+
+**What shipped.**
+
+- `crates/ailang-core/src/desugar.rs`
+  (1931 → 1939 LOC + tests; +50/+135 net of test additions).
+  - New `Desugarer.current_def_forall_vars` field. Populated
+    on entry to each `Def::Fn` (cloned from `f.ty`'s
+    `Forall.vars`, or empty for monomorphic), restored on
+    exit.
+  - `desugar_module`'s per-def loop unified: instead of
+    branching `Type::Fn` vs `Type::Forall`, it peels the
+    inner `Type::Fn` once and treats both shapes uniformly
+    for fn-param scope-building. The defensive `LetBound`
+    fallback now fires only on a malformed fn type
+    (arity mismatch or non-Fn).
+  - `Term::LetRec` arm: when
+    `!current_def_forall_vars.is_empty() && in_has_value_use`,
+    panic with the new `Iter 16b.6` / `closure-poly` message.
+    When the fast-path lift fires, the `augmented_ty` is
+    `Type::Forall { vars: current_def_forall_vars.clone(),
+    body: Box::new(Type::Fn { ... }) }` if `vars` is non-
+    empty, else the bare `Type::Fn` as before.
+- `crates/ailang-check/src/lift.rs`
+  (757 → 791 LOC; +34). Symmetric changes to `Lifter`:
+  new `current_def_forall_vars` field, populated alongside
+  the existing `rigid_vars` install in the per-def loop;
+  same Forall-wrap on `augmented_ty`; same `closure-poly`
+  panic for the polymorphic + name-as-value-in-in-term
+  combination. The lift's `synth_type` and
+  `type_check_pattern_for_lift` were unchanged — capture
+  types containing type vars flow through verbatim because
+  the typechecker installs the same rigid vars on entry.
+- `examples/poly_rec_capture.ailx` + `.ail.json` (49 LOC
+  source). `apply_n_times : Forall(a). Fn(Int, a, Fn(a) -> a) -> a`
+  applies `f` to `x` exactly `n` times. The recursive helper
+  `loop` captures `f` from the enclosing fn's params. `f`'s
+  type is `Fn(a) -> a`, mentioning `a`. The lift produces
+  `loop$lr_0 : Forall(a). Fn(Int, a, Fn(a) -> a) -> a`.
+  `main` drives `apply_n_times` at TWO instantiations
+  (`a = Int` with `succ` to compute `succ` applied 5x to 0
+  → 5; `a = Bool` with `flip` (a top-level wrapper around
+  `not`, since `not` is a builtin without a value-position
+  adapter) to compute `flip` applied 4x to false → false).
+  Codegen specialises `loop$lr_0` twice, emitting
+  `loop$lr_0__I` and `loop$lr_0__B` — confirmed in the
+  generated IR. The `flip` indirection is incidental (it
+  works around an unrelated builtin-as-value gap, not a
+  16b.6 limitation).
+- `crates/ail/tests/e2e.rs::poly_rec_capture_demo` (+25):
+  e2e count 43 → 44.
+- `crates/ailang-core/src/desugar.rs::tests` (+2):
+  `let_rec_capture_under_polymorphic_enclosing_fn_lifts_to_forall_fn`
+  (positive — asserts the lifted FnDef's type is
+  `Forall(a, Fn(Int, a) -> a)` with the `a`-typed capture
+  appended), and
+  `let_rec_name_as_value_in_polymorphic_enclosing_fn_panics`
+  (`#[should_panic(expected = "16b.6")]`).
+- `crates/ailang-check/src/lib.rs::tests` (+1):
+  `lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn`
+  exercises the post-typecheck lift path (a `Term::Let`-
+  bound capture forces deferral to `lift_letrecs`); asserts
+  the lifted ty is `Forall(a, Fn(Int, a, Int) -> a)`.
+
+**Codegen integration: did anything need to change?** No.
+Verified end-to-end: the lifted `Forall` fn is registered in
+`module_polymorphic_fns` by `lower_workspace`'s pass-1 (no
+distinction between user-written and synthetic Forall fns —
+both are `FnDef`s with `Type::Forall` types). At each call
+site inside the enclosing fn, `lower_polymorphic_call`
+derives the substitution from the actual arg types,
+specialises through `apply_subst_to_type` (which substitutes
+through `Type::Fn.params` uniformly — original params and
+appended captures share the same list), and queues a
+specialisation. `emit_specialised_fn` consumes the queue,
+substitutes type vars in both the body and the type, and
+emits the LLVM fn. `poly_rec_capture` produces
+`loop$lr_0__I` and `loop$lr_0__B` in the IR, both correctly
+typed (capture `f: ptr` carries through unchanged because
+`Fn(_) -> _` is `ptr` at the LLVM level).
+
+**Cross-iter regression check.** All seven prior fixtures
+(`local_rec_demo`, `lit_pat`, `local_rec_capture`,
+`local_rec_let_capture`, `local_rec_match_capture`,
+`local_rec_as_value`, `local_rec_as_value_capture`) build,
+run, and produce identical stdout. Their on-disk hashes
+(`ail manifest`) are bit-identical: hashes flow from
+canonical JSON, untouched by 16b.6's desugar/lift changes.
+
+**Tests: 116 → 120 (+4).**
+- e2e: 43 → 44 (`poly_rec_capture_demo`).
+- `ailang-check::tests`: 28 → 29
+  (`lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn`).
+- `ailang-core::desugar::tests`: 21 → 23 (positive lift +
+  negative panic). Net +2.
+
+**Cumulative state, post-16b.6.**
+
+- Stdlib unchanged (5 modules, 29 combinators).
+- `Term` enum: 11 variants (unchanged). All pre-16b.6
+  fixture hashes bit-identical.
+- Compiler stages: load → desugar → typecheck →
+  lift_letrecs → codegen (unchanged pipeline; only the
+  per-stage logic at the LetRec arm changed).
+- The four `unreachable!("Term::LetRec eliminated by
+  desugar")` arms in `ailang-codegen` remain correct: every
+  surviving LetRec is still gone before codegen runs (the
+  poly fast-path lifts here in desugar; the deferred path
+  is handled by `lift_letrecs`). The panic message in
+  codegen could be updated post-16b.3 to "by desugar OR
+  lift_letrecs"; left as-is for now (the invariant holds
+  either way).
+- Compiler bugs surfaced and fixed in dogfood since 14a:
+  5/5 (unchanged).
+
+**Queue update post-16b.6.** 16b.6 done. Open:
+**`closure-poly`** (informally 16b.5b — name-as-value of a
+LetRec inside a polymorphic enclosing fn; needs closure
+pair generic over the enclosing fn's type vars).
+**16b.5-body** (name-as-value INSIDE the LetRec's own body).
+**16b.7** (nested LetRec mutual capture). 16d
+(chain-machinery exhaustiveness or `__unreachable__`), 16e
+(`==` extension to Bool/Str/Unit), 17a (per-fn arena, gated)
+unchanged.

examples/poly_rec_capture.ail.json

@@ -0,0 +1 @@
+{"defs":[{"body":{"args":[{"name":"x","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"},"doc":"Helper: increment Int. Used as the Fn(Int) -> Int instance.","kind":"fn","name":"succ","params":["x"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"name":"b","t":"var"}],"fn":{"name":"not","t":"var"},"t":"app"},"doc":"Helper: boolean negation as a top-level fn (so it has an adapter for value-position).","kind":"fn","name":"flip","params":["b"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Bool"}],"ret":{"k":"con","name":"Bool"}}},{"body":{"body":{"cond":{"args":[{"name":"k","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"},"else":{"args":[{"args":[{"name":"k","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"args":[{"name":"acc","t":"var"}],"fn":{"name":"f","t":"var"},"t":"app"}],"fn":{"name":"loop","t":"var"},"t":"app"},"t":"if","then":{"name":"acc","t":"var"}},"in":{"args":[{"name":"n","t":"var"},{"name":"x","t":"var"}],"fn":{"name":"loop","t":"var"},"t":"app"},"name":"loop","params":["k","acc"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"k":"var","name":"a"}],"ret":{"k":"var","name":"a"}}},"doc":"Apply f to x exactly n times. Polymorphic in a.","kind":"fn","name":"apply_n_times","params":["n","x","f"],"type":{"body":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"k":"var","name":"a"},{"effects":[],"k":"fn","params":[{"k":"var","name":"a"}],"ret":{"k":"var","name":"a"}}],"ret":{"k":"var","name":"a"}},"k":"forall","vars":["a"]}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"},{"lit":{"kind":"int","value":0},"t":"lit"},{"name":"succ","t":"var"}],"fn":{"name":"apply_n_times","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"int","value":4},"t":"lit"},{"lit":{"kind":"bool","value":false},"t":"lit"},{"name":"flip","t":"var"}],"fn":{"name":"apply_n_times","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"t":"seq"},"doc":"Drive apply_n_times at Int (succ 5 times from 0) and Bool (not 4 times from false).","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"poly_rec_capture","schema":"ailang/v0"}

examples/poly_rec_capture.ailx

@@ -0,0 +1,57 @@
+; Iter 16b.6 — LetRec inside a polymorphic enclosing fn.
+; `apply_n_times : Forall(a). Fn(Int, a, Fn(a) -> a) -> a`
+; applies `f` to `x` exactly `n` times. The recursive helper `loop`
+; captures `f` from the enclosing fn's params — `f`'s declared type
+; is `Fn(a) -> a`, which mentions the outer fn's type var `a`. The
+; 16b.6 lift produces a synthetic top-level fn
+;   `loop$lr_0 : Forall(a). Fn(Int, a, Fn(a) -> a) -> a`
+; and rewrites `(app loop k acc)` → `(app loop$lr_0 k acc f)`.
+;
+; `main` drives `apply_n_times` at TWO distinct type instantiations
+; so codegen's monomorphisation queue picks up `loop$lr_0` twice
+; (once at `a = Int` to compute `succ` applied 5x to 0 → 5; once at
+; `a = Bool` to compute `not` applied 4x to false → false). This
+; exercises the substitution of the outer Forall.vars into both the
+; original LetRec params and the appended capture types.
+;
+; Expected stdout (one per line): 5, false.
+
+(module poly_rec_capture
+
+  (fn succ
+    (doc "Helper: increment Int. Used as the Fn(Int) -> Int instance.")
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params x)
+    (body (app + x 1)))
+
+  (fn flip
+    (doc "Helper: boolean negation as a top-level fn (so it has an adapter for value-position).")
+    (type (fn-type (params (con Bool)) (ret (con Bool))))
+    (params b)
+    (body (app not b)))
+
+  (fn apply_n_times
+    (doc "Apply f to x exactly n times. Polymorphic in a.")
+    (type
+      (forall (vars a)
+        (fn-type
+          (params (con Int) a (fn-type (params a) (ret a)))
+          (ret a))))
+    (params n x f)
+    (body
+      (let-rec loop
+        (params k acc)
+        (type (fn-type (params (con Int) a) (ret a)))
+        (body
+          (if (app == k 0)
+            acc
+            (app loop (app - k 1) (app f acc))))
+        (in (app loop n x)))))
+
+  (fn main
+    (doc "Drive apply_n_times at Int (succ 5 times from 0) and Bool (not 4 times from false).")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (seq (do io/print_int (app apply_n_times 5 0 succ))
+           (do io/print_bool (app apply_n_times 4 false flip))))))