diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index c126f77..daa8db7 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *634 tests* (`+cargo test --workspace --all-targets+`); +* Total: *635 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 634 +* Documented all-target tests: 635 === CRG Testing Taxonomy — Status @@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) ==== Build & Execution * [x] cargo build — compiles -* [x] cargo test –workspace –all-targets — 634 pass, 0 fail +* [x] cargo test –workspace –all-targets — 635 pass, 0 fail * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays diff --git a/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc index 85abe4d..fb4f994 100644 --- a/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc +++ b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc @@ -1395,7 +1395,7 @@ Ephapax's soundness statements are *theory* under PROOF-POLICY §1: the typing j === D7 — Recursive types -*Ratified 2026-11-10 (owner):* the recommended option, iso-recursive `TMu` with fold/unfold inserted by desugar. Its first use is rung E9 in the Rust implementation (gate `src/ephapax-cli/tests/recursive_types.rs`), behind `--unstable-core`. In that step a `data` type can refer only to itself: a cycle through another `data` type, and a reference with other type arguments, are named errors. +*Ratified 2026-11-10 (owner):* the recommended option, iso-recursive `TMu` with fold/unfold inserted by desugar. Its first use is rung E9 in the Rust implementation (gate `src/ephapax-cli/tests/recursive_types.rs`), behind `--unstable-core`. `data` types that refer to each other become nested `TMu` types (Bekic's construction, in the order of their names), so the core has no new former. A dense cycle makes these types grow fast (4 types that each refer to each of the 4 need 3613 bodies, 5 need 8 million), so a type of more than 10000 bodies, or of more than 256 nested named types, is a named error. A recursive type of n variables (as the `rec` groups of WasmGC) removes that limit and is a change of the core. A reference with other type arguments is a named error. [cols="3,1,1,4",options="header"] |=== diff --git a/src/ephapax-cli/tests/linearity_holes.rs b/src/ephapax-cli/tests/linearity_holes.rs index 59ecda6..27edaca 100644 --- a/src/ephapax-cli/tests/linearity_holes.rs +++ b/src/ephapax-cli/tests/linearity_holes.rs @@ -453,13 +453,16 @@ fn a_recursive_form_with_no_lowering_is_a_named_desugar_error() { Err(PipelineError::Desugar(error)) => error, other => panic!("expected a desugar error, got {other:?}"), }; - // 2 `data` types that refer to each other. + // 5 `data` types that each refer to each of the 5: the nested + // recursive type of the last one by name needs 8 million bodies. + let dense: String = (0..5) + .map(|i| format!("data T{i} = L{i} | N{i}(T0, T1, T2, T3, T4)\n")) + .collect(); assert!(matches!( - refused( - "data Tree = Leaf | Node(Forest)\ndata Forest = FNil | FCons(Tree, Forest)\n\ - fn f(t: Tree): I32 = 0\nfn main(): I32 = 0\n" - ), - DesugarError::MutualRecursion { cycle } if cycle == "Tree -> Forest -> Tree" + refused(&format!( + "{dense}fn f(t: T4): I32 = 0\nfn main(): I32 = 0\n" + )), + DesugarError::TypeTooLarge { .. } )); // A `data` type that refers to itself with other type arguments. assert!(matches!( diff --git a/src/ephapax-cli/tests/recursive_types.rs b/src/ephapax-cli/tests/recursive_types.rs index 4e1f531..3fa34bc 100644 --- a/src/ephapax-cli/tests/recursive_types.rs +++ b/src/ephapax-cli/tests/recursive_types.rs @@ -272,7 +272,13 @@ fn a_recursive_data_type_crosses_a_module() { "module lib\n\npub data IntList = Nil | Cons(I32, IntList)\n\n\ pub data List(a) = LNil | LCons(a, List(a))\n\n\ pub fn sum(l: IntList): I32 = match l of | Nil => 0 | Cons(h, t) => h + sum(t) end\n\n\ - pub fn one(n: I32): IntList = Cons(n, Nil)\n", + pub fn one(n: I32): IntList = Cons(n, Nil)\n\n\ + pub data Tree = Leaf | Node(I32, Forest)\n\n\ + pub data Forest = FNil | FCons(Tree, Forest)\n\n\ + pub fn size(t: Tree): I32 =\n \ + match t of | Leaf => 0 | Node(v, kids) => v + sizes(kids) end\n\n\ + pub fn sizes(f: Forest): I32 =\n \ + match f of | FNil => 0 | FCons(t, rest) => size(t) + sizes(rest) end\n", ) .expect("write module"); let app = |name: &str, head: &str, main: &str| { @@ -315,6 +321,18 @@ fn a_recursive_data_type_crosses_a_module() { ), "2", ), + // 2 types that refer to each other, in a type of this module. + ( + "each_other", + app( + "each_other", + "import lib\n\ndata Wrap = W(Tree, Forest) | Stop\n\n\ + fn total(w: Wrap): I32 =\n \ + match w of | Stop => 0 | W(t, f) => size(t) + sizes(f) end\n", + "total(W(Node(40, FNil), FCons(Node(2, FNil), FNil)))", + ), + "42", + ), // A declaration of the module hides the imported type. ( "hidden", @@ -390,15 +408,166 @@ fn a_recursive_type_keeps_the_linear_rules() { ); } +/// `data` types that refer to each other. They become nested recursive +/// types, in the order of their names, and the unfolding of each one has +/// the types of the others in it as they are. So a field of a +/// constructor has the type that its declaration names: each program +/// here passes the type checker, and then runs. +#[test] +fn data_types_that_refer_to_each_other_run() { + let tmp = tempfile::tempdir().expect("tempdir"); + let forest = "fn size(t: Tree): I32 =\n \ + match t of | Leaf => 0 | Node(v, kids) => v + sizes(kids) end\n\n\ + fn sizes(f: Forest): I32 =\n \ + match f of | FNil => 0 | FCons(t, rest) => size(t) + sizes(rest) end\n\n"; + let mut programs = vec![ + // The first type by name (`Forest`) is the one that is folded. + ( + "forest".to_string(), + format!( + "data Tree = Leaf | Node(I32, Forest)\n\n\ + data Forest = FNil | FCons(Tree, Forest)\n\n{forest}\ + fn grow(n: I32): Tree =\n if n == 0 then Leaf\n \ + else Node(n, FCons(grow(n - 1), FCons(grow(n - 1), FNil)))\n\n\ + fn main(): I32 = size(grow(4))\n" + ), + "26", + ), + // A type with 1 constructor in the cycle. + ( + "even_odd".to_string(), + "data Even = Zero | SuccE(Odd)\n\ndata Odd = SuccO(Even)\n\n\ + fn even(e: Even): I32 = match e of | Zero => 0 | SuccE(o) => 1 + odd(o) end\n\n\ + fn odd(o: Odd): I32 = match o of | SuccO(e) => 1 + even(e) end\n\n\ + fn main(): I32 = even(SuccE(SuccO(SuccE(SuccO(Zero)))))\n" + .to_string(), + "4", + ), + // No type of the cycle refers to itself. + ( + "no_self".to_string(), + "data A = MkA(B) | EndA\n\ndata B = MkB(I32, A)\n\n\ + fn sa(a: A): I32 = match a of | EndA => 0 | MkA(b) => sb(b) end\n\n\ + fn sb(b: B): I32 = match b of | MkB(n, a) => n + sa(a) end\n\n\ + fn main(): I32 = sa(MkA(MkB(40, MkA(MkB(2, EndA)))))\n" + .to_string(), + "42", + ), + // Type parameters, and an element that is not 32 bits wide. + ( + "parameters".to_string(), + "data Tree(a) = Leaf | Node(a, Forest(a))\n\n\ + data Forest(a) = FNil | FCons(Tree(a), Forest(a))\n\n\ + fn size(t: Tree(I64)): I64 =\n match t of\n \ + | Leaf => 5000000000 - 5000000000\n | Node(v, kids) => v + sizes(kids)\n end\n\n\ + fn sizes(f: Forest(I64)): I64 =\n match f of\n \ + | FNil => 5000000000 - 5000000000\n | FCons(t, rest) => size(t) + sizes(rest)\n \ + end\n\n\ + fn main(): I64 = size(Node(5000000000, FCons(Node(5000000000, FNil), FNil)))\n" + .to_string(), + "10000000000i64", + ), + // A linear component: each string is consumed 1 time. + ( + "linear".to_string(), + "data STree = SLeaf | SNode(String@r, SForest)\n\n\ + data SForest = SNil | SCons(STree, SForest)\n\n\ + fn len(t: STree): I32 =\n match t of\n | SLeaf => 0\n \ + | SNode(s, kids) => String.len(&s) + (let _ = drop(s) in lens(kids))\n end\n\n\ + fn lens(f: SForest): I32 =\n \ + match f of | SNil => 0 | SCons(t, rest) => len(t) + lens(rest) end\n\n\ + fn main(): I32 =\n region r {\n \ + len(SNode(String.new@r(\"ab\"), SCons(SNode(String.new@r(\"abc\"), SNil), SNil)))\n \ + }\n" + .to_string(), + "5", + ), + ]; + // 3 types, where each one refers to the 2 others. Each order of the 3 + // names is another nesting of the 3 recursive types. + for [a, b, c] in [ + ["X", "Y", "Z"], + ["X", "Z", "Y"], + ["Y", "X", "Z"], + ["Y", "Z", "X"], + ["Z", "X", "Y"], + ["Z", "Y", "X"], + ] { + programs.push(( + format!("cycle_{a}{b}{c}"), + format!( + "data {a} = L{a} | N{a}(I32, {b}, {c})\n\n\ + data {b} = L{b} | N{b}({c}, {a}, I32)\n\n\ + data {c} = L{c} | N{c}({a}, {b}, {c})\n\n\ + fn s{a}(x: {a}): I32 =\n \ + match x of | L{a} => 1 | N{a}(n, p, q) => n + s{b}(p) + s{c}(q) end\n\n\ + fn s{b}(x: {b}): I32 =\n \ + match x of | L{b} => 2 | N{b}(p, q, n) => n + s{c}(p) + s{a}(q) end\n\n\ + fn s{c}(x: {c}): I32 =\n \ + match x of | L{c} => 3 | N{c}(p, q, r) => s{a}(p) + s{b}(q) + s{c}(r) end\n\n\ + fn main(): I32 =\n \ + s{a}(N{a}(10, N{b}(L{c}, N{a}(5, L{b}, L{c}), 20),\n \ + N{c}(L{a}, L{b}, N{c}(L{a}, N{b}(L{c}, L{a}, 1), L{c}))))\n" + ), + "55", + )); + } + let programs: Vec<(&str, String, &str)> = programs + .iter() + .map(|(name, text, want)| (name.as_str(), text.clone(), *want)) + .collect(); + each_runs(tmp.path(), &programs); + + // The linear rules hold for each type of a cycle. + let strings = "data STree = SLeaf | SNode(String@r, SForest)\n\n\ + data SForest = SNil | SCons(STree, SForest)\n\n"; + for (name, ty) in [("forest_2_times", "SForest"), ("tree_2_times", "STree")] { + check_refuses( + name, + &format!("{strings}fn two(x: {ty}): ({ty}, {ty}) = (x, x)\n\nfn main(): I32 = 0\n"), + "Linear variable `x` used more than once", + ); + } + // A `Tree` is not a `Forest`, and a `Forest` is not a `Tree`: in a + // constructor of the folded type, and as an argument of a function. + let forest = "data Tree = Leaf | Node(I32, Forest)\n\n\ + data Forest = FNil | FCons(Tree, Forest)\n\n\ + fn size(t: Tree): I32 = match t of | Leaf => 0 | Node(v, kids) => v end\n\n"; + for (name, main) in [ + ( + "forest_as_tree", + "match FCons(FNil, FNil) of | FNil => 0 | FCons(t, rest) => 1 end", + ), + ("tree_as_forest", "size(Node(1, Leaf))"), + ] { + check_refuses( + name, + &format!("{forest}fn main(): I32 = {main}\n"), + "Type mismatch", + ); + } +} + /// The recursive forms that have no lowering yet are refused by name. #[test] fn a_recursive_form_with_no_lowering_is_refused_by_name() { - check_refuses( - "each_other", - "data Tree = Leaf | Node(Forest)\n\ndata Forest = FNil | FCons(Tree, Forest)\n\n\ - fn f(t: Tree): I32 = 0\n\nfn main(): I32 = 0\n", - "the `data` types Tree -> Forest -> Tree refer to each other", - ); + // 5 `data` types that each refer to each of the 5: the nested + // recursive type of the last one by name needs 8 million bodies. And + // 300 `data` types in a ring: the types nest too deep. Without the + // limit, the first does not end and the second overflows the stack. + let dense: String = (0..5) + .map(|i| format!("data T{i} = L{i} | N{i}(T0, T1, T2, T3, T4)\n\n")) + .collect(); + let ring: String = (0..300) + .map(|i| format!("data T{i} = L{i} | N{i}(T{})\n\n", (i + 1) % 300)) + .collect(); + for (name, types, ty) in [("dense_cycle", dense, "T4"), ("deep_ring", ring, "T0")] { + check_refuses( + name, + &format!("{types}fn f(t: {ty}): I32 = 0\n\nfn main(): I32 = 0\n"), + &format!("the type `{ty}` is too large"), + ); + } check_refuses( "other_arguments", "data Grow(a) = Stop | More(Grow((a, a)))\n\n\ diff --git a/src/ephapax-desugar/src/lib.rs b/src/ephapax-desugar/src/lib.rs index b3cb112..6eeb7bc 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -141,11 +141,12 @@ pub enum DesugarError { #[error("recursive type alias `{name}` is not supported: only a `data` type can refer to itself (expansion cycle: {cycle})")] RecursiveAlias { name: String, cycle: String }, - /// 2 or more `data` types refer to each other. A `data` type can - /// refer to itself (v2 plan rung E9); a cycle through another `data` - /// type has no lowering yet. - #[error("the `data` types {cycle} refer to each other, which is not supported yet: a recursive `data` type can refer only to itself (a `type` alias in the cycle is permitted)")] - MutualRecursion { cycle: String }, + /// The expansion of a named type is too large or too deep. `data` + /// types that refer to each other become nested recursive types, and + /// a dense cycle makes them grow fast: 4 types that each refer to + /// each of the 4 need 3613 bodies, and 5 such types need 8 million. + #[error("the type `{name}` is too large: its expansion needs more than {MAX_EXPANSIONS} bodies of named types, or nests them more than {MAX_EXPANSION_DEPTH} deep. `data` types that refer to each other in a dense cycle have this effect: use fewer references between them, or 1 `data` type for the cycle")] + TypeTooLarge { name: String }, /// A `data` type refers to itself with other type arguments /// (`data Grow(a) = More(Grow([a]))`): its expansion does not end. @@ -335,6 +336,16 @@ impl DataRegistry { // Desugarer // ========================================================================= +/// The most bodies of named types that the expansion of 1 type can have +/// ([`DesugarError::TypeTooLarge`]). A cycle of 5 `data` types as in a +/// syntax tree needs fewer than 400. +const MAX_EXPANSIONS: usize = 10_000; + +/// The most named types that an expansion can nest. Each one is a level +/// of recursion in this pass and in each later pass over the type: a +/// chain of 700 nested `data` types overflowed the stack. +const MAX_EXPANSION_DEPTH: usize = 256; + /// A named type whose body is being expanded by `desugar_named_type`. #[derive(Debug, Clone)] struct Expansion { @@ -349,6 +360,10 @@ struct Expansion { params: HashMap, /// The body referred to the type itself: the type is recursive. recursive: bool, + /// The type is not a variable for the expansion in progress: a `data` + /// type that comes before it was entered after it + /// ([`Desugarer::expand_data`]). + hidden: bool, } /// The variable of the recursive type of the `data` type `name`. A @@ -384,6 +399,9 @@ pub struct Desugarer { /// innermost last. A `data` type that is entered again is a recursive /// type (v2 plan rung E9). expanding: RefCell>, + /// The number of bodies of named types in the expansion in progress, + /// for [`MAX_EXPANSIONS`]. + expansions: std::cell::Cell, /// Key of the module whose scope gives a name its meaning: the module /// being desugared, or, while the body of a named type expands, the /// module that declares that type. @@ -401,6 +419,7 @@ impl Desugarer { registry: DataRegistry::new(), module_qualifiers: HashSet::new(), expanding: RefCell::new(Vec::new()), + expansions: std::cell::Cell::new(0), scope: RefCell::default(), fn_type_params: Vec::new(), } @@ -412,6 +431,7 @@ impl Desugarer { registry, module_qualifiers: HashSet::new(), expanding: RefCell::new(Vec::new()), + expansions: std::cell::Cell::new(0), scope: RefCell::default(), fn_type_params: Vec::new(), } @@ -1050,9 +1070,10 @@ impl Desugarer { .collect::, _>>()?; // Build right-nested sum from constructor field types - self.expand_data(name, home, params, core_args, |this| { + let expanded = self.expand_data(name, home, params, core_args, |this| { this.build_sum_type(ctors) - }) + }); + expanded.map(|(ty, _)| ty) } /// The names of the expansions from `start`, then `name`: the cycle @@ -1063,6 +1084,23 @@ impl Desugarer { names.join(" -> ") } + /// Count one more body of a named type in the expansion in progress, + /// which starts when `stack` is empty. An expansion that is too large + /// or too deep is an error by name, not a compiler that does not end + /// or that overflows its stack. + fn count_expansion(&self, stack: &[Expansion], name: &SmolStr) -> Result<(), DesugarError> { + let count = match stack { + [] => 1, + _ => self.expansions.get() + 1, + }; + self.expansions.set(count); + if count > MAX_EXPANSIONS || stack.len() >= MAX_EXPANSION_DEPTH { + let name = stack.first().map_or(name, |e| &e.name).to_string(); + return Err(DesugarError::TypeTooLarge { name }); + } + Ok(()) + } + /// Run `f`, which expands the body of the alias `name` of the module /// `home`, with the names of `home` in scope. An alias that refers to /// itself with no `data` type between is an error: only a `data` type @@ -1085,6 +1123,7 @@ impl Desugarer { cycle: Self::cycle(&stack, seen, name), }); } + self.count_expansion(&stack, name)?; } self.expanding.borrow_mut().push(Expansion { home: home.clone(), @@ -1092,6 +1131,7 @@ impl Desugarer { args: None, params: HashMap::new(), recursive: false, + hidden: false, }); let result = self.in_scope(home, f); self.expanding.borrow_mut().pop(); @@ -1101,13 +1141,34 @@ impl Desugarer { /// The type of the `data` type `name` of the module `home`, with the /// type parameters `params`, at the type arguments `args`. `f` builds /// the sum of its constructors, with the names of `home` in scope and - /// each type parameter as its argument. + /// each type parameter as its argument. The result also says if the + /// type is folded: a value of it is made by `fold` and read by `unfold`. /// /// A reference to the type inside its own body, with the same - /// arguments, is the variable of a recursive type, and the result is - /// then `mu var. body` (v2 plan decision D7: iso-recursive). Not - /// supported, each with its own error: a cycle through another `data` - /// type, and a reference with other arguments. + /// arguments, is the variable of a recursive type. The result is then + /// `mu var. body`, and the type is folded (v2 plan decision D7: + /// iso-recursive). + /// + /// `data` types that refer to each other become nested recursive + /// types (Bekic's construction), in the order of their names. A + /// `data` type that is entered hides, for its body, each `data` type + /// in progress that comes after it: in that body, such a type is not + /// a variable, and it is expanded again. For `Forest` before `Tree`: + /// + /// ```text + /// Forest = mu F. () + ((() + F) * F) -- Tree is expanded in it + /// Tree = () + Forest -- not folded + /// ``` + /// + /// So the unfolding of `Forest` has `Tree` and `Forest` themselves in + /// it, and not types that are only equal to them after more unfolds: + /// a field of a constructor has the type that its declaration names. + /// + /// Not supported, with its own error: a reference with other + /// arguments. + // snip: nested recursive types; a cycle of n `data` types can make + // types of a size up to 2^n bodies. Upgrade to a recursive type of n + // variables (as the `rec` groups of WasmGC) if a large cycle is slow. fn expand_data( &self, name: &SmolStr, @@ -1115,24 +1176,34 @@ impl Desugarer { params: &[SmolStr], args: Vec, f: impl FnOnce(&Self) -> Result, - ) -> Result { - let is_data = |e: &Expansion| e.args.is_some(); + ) -> Result<(Ty, bool), DesugarError> { + let hidden: Vec; { let mut stack = self.expanding.borrow_mut(); - let entered = stack + let same = |e: &Expansion| e.args.is_some() && e.home == *home && e.name == *name; + // In progress with other arguments, as a variable or not. + if let Some(entered) = stack .iter() - .rposition(|e| is_data(e) && e.home == *home && e.name == *name); - if let Some(entered) = entered { - let cycle = Self::cycle(&stack, entered, name); - let name = name.to_string(); - if stack[entered + 1..].iter().any(is_data) { - return Err(DesugarError::MutualRecursion { cycle }); - } - if stack[entered].args.as_ref() != Some(&args) { - return Err(DesugarError::NonRegularRecursion { name, cycle }); - } - stack[entered].recursive = true; - return Ok(Ty::Var(mu_var(&name))); + .position(|e| same(e) && e.args.as_ref() != Some(&args)) + { + return Err(DesugarError::NonRegularRecursion { + name: name.to_string(), + cycle: Self::cycle(&stack, entered, name), + }); + } + if let Some(entered) = stack.iter_mut().find(|e| same(e) && !e.hidden) { + entered.recursive = true; + return Ok((Ty::Var(mu_var(name)), false)); + } + self.count_expansion(&stack, name)?; + hidden = stack + .iter() + .enumerate() + .filter(|(_, e)| e.args.is_some() && !e.hidden && (&e.home, &e.name) > (home, name)) + .map(|(i, _)| i) + .collect(); + for &i in &hidden { + stack[i].hidden = true; } stack.push(Expansion { home: home.clone(), @@ -1140,46 +1211,46 @@ impl Desugarer { params: params.iter().cloned().zip(args.iter().cloned()).collect(), args: Some(args), recursive: false, + hidden: false, }); } let body = self.in_scope(home, f); - let recursive = self - .expanding - .borrow_mut() - .pop() - .is_some_and(|e| e.recursive); + let recursive = { + let mut stack = self.expanding.borrow_mut(); + let recursive = stack.pop().is_some_and(|e| e.recursive); + for &i in &hidden { + stack[i].hidden = false; + } + recursive + }; let body = body?; Ok(if recursive { - Ty::Mu { - var: mu_var(name), - body: Box::new(body), - } + let var = mu_var(name); + let body = Box::new(body); + (Ty::Mu { var, body }, true) } else { - body + (body, false) }) } - /// The type parameters of the `data` type of the constructor `info`, - /// and the type of that `data` type with them as type variables. The - /// type is a recursive type (`Ty::Mu`) if the `data` type refers to - /// itself. - fn data_ty(&self, info: &ConstructorInfo) -> Result<(Vec, Ty), DesugarError> { - let params = match self.registry.get_type(&info.home, &info.data_name) { - Some(TypeInfo { - def: TypeDef::Data { params, .. }, - .. - }) => params.clone(), - _ => { - return Err(DesugarError::UnknownType { - name: info.data_name.to_string(), - }) - } + /// For the `data` type of the constructor `info`: its type parameters, + /// its type with them as type variables, and if the type is folded + /// ([`Self::expand_data`]). + fn data_ty(&self, info: &ConstructorInfo) -> Result<(Vec, Ty, bool), DesugarError> { + let Some(TypeInfo { + def: TypeDef::Data { params, ctors }, + .. + }) = self.registry.get_type(&info.home, &info.data_name) + else { + return Err(DesugarError::UnknownType { + name: info.data_name.to_string(), + }); }; - let args: Vec = params.iter().cloned().map(SurfaceTy::Var).collect(); - let ty = self.in_scope(&info.home, |this| { - this.desugar_named_type(&info.data_name, &args) + let args = params.iter().cloned().map(Ty::Var).collect(); + let (ty, folded) = self.expand_data(&info.data_name, &info.home, params, args, |this| { + this.build_sum_type(ctors) })?; - Ok((params, ty)) + Ok((params.clone(), ty, folded)) } /// Build the right-nested binary sum type for a list of constructors. @@ -1260,7 +1331,7 @@ impl Desugarer { // annotation: the type checker finds a type for each one from the // use of the value. (An annotation had the parameter itself, which // is no type at the constructor: `None` was not an `Option(I32)`.) - let (params, ty) = self.data_ty(&info)?; + let (params, ty, folded) = self.data_ty(&info)?; // Wrap in inl/inr chain based on index. The types of the other // constructors are names of the module that declares the type. @@ -1269,15 +1340,16 @@ impl Desugarer { })?; // A value of a recursive type is folded (v2 plan rung E9). The // fold makes the annotations of the injections agree. - Ok(match ty { - Ty::Mu { .. } => Expr::new( + Ok(if folded { + Expr::new( ExprKind::Fold { ty: quantify(ty, ¶ms), value: Box::new(value), }, span, - ), - _ => value, + ) + } else { + value }) } @@ -1461,9 +1533,10 @@ impl Desugarer { let ctors = self.ctors_of(info)?; // A value of a recursive type is unfolded before its sum is read // (v2 plan rung E9). - let core_scrutinee = match self.data_ty(info)?.1 { - Ty::Mu { .. } => Expr::new(ExprKind::Unfold(Box::new(core_scrutinee)), span), - _ => core_scrutinee, + let core_scrutinee = if self.data_ty(info)?.2 { + Expr::new(ExprKind::Unfold(Box::new(core_scrutinee)), span) + } else { + core_scrutinee }; // The constructor index of each arm; `None` for an arm that takes diff --git a/src/ephapax-typing/src/lib.rs b/src/ephapax-typing/src/lib.rs index 35891c1..7228b9f 100644 --- a/src/ephapax-typing/src/lib.rs +++ b/src/ephapax-typing/src/lib.rs @@ -1149,9 +1149,15 @@ impl TypeChecker { // 2 recursive types are equal when their bodies are, with one // name for the 2 bound variables. A recursive type is not // equal to its unfolding (iso-recursive, decision D7). + (Ty::Mu { var: v1, body: b1 }, Ty::Mu { var: v2, body: b2 }) if v1 == v2 => { + self.unify(s, b1, b2) + } + // The one name is a new one: a body can have a recursive type + // in it that binds the name of the other variable. (Ty::Mu { var: v1, body: b1 }, Ty::Mu { var: v2, body: b2 }) => { - let b2 = b2.subst_var(v2, &Ty::Var(v1.clone())); - self.unify(s, b1, &b2) + let fresh = Ty::Var(format!("#{}", self.next_unif).into()); + self.next_unif += 1; + self.unify(s, &b1.subst_var(v1, &fresh), &b2.subst_var(v2, &fresh)) } (Ty::Tuple(e1), Ty::Tuple(e2)) if e1.len() == e2.len() => { for (t1, t2) in e1.iter().zip(e2.iter()) {