From 76d61aecedf8cd5e8655158e685194752077486b Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 7 May 2026 22:39:28 +0200 Subject: [PATCH] Iter 16b.6: LetRec inside polymorphic enclosing fn MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- crates/ail/tests/e2e.rs | 28 +++ crates/ailang-check/src/lib.rs | 162 +++++++++++++++ crates/ailang-check/src/lift.rs | 64 +++++- crates/ailang-core/src/desugar.rs | 309 ++++++++++++++++++++++++++--- docs/JOURNAL.md | 179 +++++++++++++++++ examples/poly_rec_capture.ail.json | 1 + examples/poly_rec_capture.ailx | 57 ++++++ 7 files changed, 772 insertions(+), 28 deletions(-) create mode 100644 examples/poly_rec_capture.ail.json create mode 100644 examples/poly_rec_capture.ailx diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index 1273a21..57f52c8 100644 --- a/crates/ail/tests/e2e.rs +++ b/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. diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index f805399..84c925d 100644 --- a/crates/ailang-check/src/lib.rs +++ b/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::>() + ); + 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!(¶ms[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!(¶ms[1], Type::Var { name } if name == "a"), + "second param: x: a; got {:?}", + params[1] + ); + assert!( + matches!(¶ms[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()] + ); + } } diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index a9d821a..f961df1 100644 --- a/crates/ailang-check/src/lift.rs +++ b/crates/ailang-check/src/lift.rs @@ -130,6 +130,7 @@ pub fn lift_letrecs(m: &Module) -> Result { 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 { } } } + // 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 { /// 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, lifted: Vec, + /// Iter 16b.6: enclosing fn's Forall.vars (or empty if mono). + /// Reset on entry to each `Def::Fn`. + current_def_forall_vars: Vec, } 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 = 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()); diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index b91fa53..8991269 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/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 = 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 = BTreeMap::new(); @@ -329,11 +349,23 @@ fn collect_used_in_pattern(p: &Pattern, used: &mut BTreeSet) { /// 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, lifted: Vec, module_top_names: BTreeSet, + /// 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, } 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 = 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::>() + ); + 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!(¶ms[0], Type::Con { name, .. } if name == "Int"), + "first param must be Int (loop's own k); got {:?}", + params[0] + ); + assert!( + matches!(¶ms[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` diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 9932ba1..47f7156 100644 --- a/docs/JOURNAL.md +++ b/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` 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. diff --git a/examples/poly_rec_capture.ail.json b/examples/poly_rec_capture.ail.json new file mode 100644 index 0000000..1ba493c --- /dev/null +++ b/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"} \ No newline at end of file diff --git a/examples/poly_rec_capture.ailx b/examples/poly_rec_capture.ailx new file mode 100644 index 0000000..10b44c7 --- /dev/null +++ b/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))))))