Repository navigation
feat: recursive data types as iso-recursive mu, with fold and unfold (E9, D7) - #438
Merged
Merged
Conversation
…(E9, D7) v2 plan rung E9, the recursive type half. Decision D7 is ratified (owner, 2026-11-10): iso-recursive types, with fold and unfold from the desugarer. A `data` type that refers to itself was refused. It is now the core type `mu X. T`. The desugarer puts a `fold` at each constructor and an `unfold` at each `match`. A value of the type is a pointer to its unfolding (a sum cell, a pair), so fold and unfold do nothing at run time, in wasm and in the interpreter. The form is behind the flag `--unstable-core`, as the plan says for E9. - Core: `Ty::Mu`, `ExprKind::Fold`, `ExprKind::Unfold`. A recursive type is linear when its body is (the least fixed point of the plan). - Checker: the 2 rules, and equality of 2 recursive types up to the name of the bound variable. A recursive type is not equal to its unfolding. - A `data` type with type parameters works: `List(a)`. The annotation of a constructor binds the type parameters, and the checker finds them from the use of the value. - In the body of a `data` type, a type parameter now stands for its argument at each depth. Only a parameter that was a whole field got its argument before. - Refused by name: 2 `data` types that refer to each other, a type that refers to itself with other type arguments, and a `type` alias that refers to itself. A `type` alias in the cycle of a `data` type is permitted. The linear rules hold for a recursive type with a linear component: a value is used 1 time, each part is consumed, and it cannot leave its region. Tests: recursive_types.rs (6 tests, each program as wasm and in the interpreter), 1 IR round trip, 1 more test in linearity_holes.rs. The probe rec1 is now refused for the flag: its 2 rows in the probe battery have the new verdict UnstableCore. 636 tests pass; the all-target count is 633. Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
Contributor
|
Caution Review failedThe pull request is closed.
Warning Some tools did not complete. Review the errors below.
 |
|
hyperpolymath
marked this pull request as ready for review
November 10, 2026 19:56
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
hyperpolymath
added a commit
that referenced
this pull request
Nov 10, 2026
## Summary
A constructor of a `data` type with type parameters did not check when
the other side of its sum had a type parameter.
| Program | Before | Now |
|---|---|---|
| `fn none(): Option(I32) = None` | Type mismatch: expected `I32`, found
`Var("a")` | accepted |
| `or(None, 2)` with `or(o: Option(I32), d: I32)` | Type mismatch | 2 |
| `let o = None in match o of ...` | Type mismatch | runs |
| `pick(L(42))` with `pick(e: Either(I32, Bool))` | Type mismatch | runs
|
| `fn none<T>(): Option(T) = None` | Type mismatch (`Var("a")` against
`Var("T")`) | accepted |
`Some(n)` checked before, because the other side of its sum is `()`.
## Cause and change
The annotation of an injection had the type parameter itself
(`inl[a](())`), which is no type at the constructor. It checked only
when a generic function gave its own type parameter the same name as the
`data` type did.
The annotation now binds the type parameters of the `data` type
(`inl[forall a. a](())`), for each `data` type with type parameters.
#438 did this for a `data` type that refers to itself. The checker gives
each bound parameter a type from the use of the value.
Each annotation gets its own type: an injection has each type on its
other side. So a side that nothing uses stays free. A use at another
type is a type error, as before: `g(B(1))` with `g(t: T(Bool))` gives
"Type mismatch".
No flag: a `data` type with type parameters is not behind
`--unstable-core`.
## Verification
- `cargo test --workspace --no-fail-fast`: 637 passed, 0 failed. No
program of the corpus changed.
- `cargo fmt --all --check` and `cargo clippy --workspace
--all-targets`: clean.
- `scripts/status-gate.sh`: 634 all-target tests (1 more than before).
- `scripts/probe-battery.sh`: 51 SAME, 7 SKIP (the SKIP rows need the
wasmtime CLI).
- New test `a_constructor_gets_its_type_arguments_from_its_use` in
`run_wasm.rs`: 7 programs, as wasm and in the interpreter (a result, an
argument, no annotation, the 2 branches of an `if`, a generic function,
a constructor in a constructor, 2 type parameters at I64 and F64, 3
constructors), and 1 program that is refused.
---
_Generated by [Claude
Code](https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u)_
Co-authored-by: Claude <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a1f48c729f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+398
to
+400
| if let (false, Decl::Fn { params, ret_ty, .. }) = (unstable_core, decl) { | ||
| let tys = params.iter().map(|(_, ty)| ty).chain([ret_ty]); | ||
| if let Some(ty) = tys.filter_map(recursive_name).next() { |
There was a problem hiding this comment.
When a recursive type appears only in an extern function signature, both check and compile accept it without --unstable-core: the declaration loop skips every Decl::Extern, while this new signature check handles only local functions. For example, an unflagged program can declare extern source/sink functions over IntList and shuttle sink(source()) through an ordinary function whose own signature is non-recursive; no Fold or Unfold is present for the expression traversal to catch, bypassing the feature gate entirely.
Useful? React with 👍 / 👎.
Comment on lines
+1152
to
+1154
| (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) |
There was a problem hiding this comment.
Although this arm makes mu types equal modulo their bound variable, existing comparison sites still use derived Ty equality instead of unify, notably annotated let! bindings and list elements. Consequently, two recursive data declarations with identical structural bodies but different names are accepted in function arguments or ordinary let annotations yet rejected in let! x: A = EndB or [EndA, EndB], solely because their generated binders are #A and #B; those sites need to use the same alpha-equivalent comparison.
Useful? React with 👍 / 👎.
hyperpolymath
added a commit
that referenced
this pull request
Nov 10, 2026
…ve types (#440) ## Summary `data` types that refer to each other were refused by name (#438). They are now accepted, behind the flag `--unstable-core` as each recursive type is. ``` data Tree = Leaf | Node(I32, Forest) data Forest = FNil | FCons(Tree, Forest) ``` The core has no new former, and the checker and the 2 backends do not change. Only the type expansion of the desugarer changes. ## How The types of a cycle become nested `mu` 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`: ``` Forest = mu F. () + ((() + (I32 * F)) * F) Tree = () + (I32 * Forest) (not folded) ``` The reason for this order rule: with iso-recursive types, a type is not equal to its unfolding. So the unfolding of each type must have the other types in it as they are. With the rule it does, for a cycle of each form and each number of types. A field of a constructor then has the type that its declaration names, and no fold or unfold is missing or in excess. 2 more changes follow from the nesting: - A `data` type is folded when its own expansion refers to it. A type whose type is the recursive type of another `data` type (`data B = MkB(A)`) is not folded. - Equality of 2 recursive types gives the 2 bound variables a new name when their names differ: a body can have a recursive type in it that binds the name of the other variable. ## Limit, with a named error A dense cycle makes the nested types grow fast. | Cycle | Bodies in the largest type | |---|---| | 2 types, each refers to the 2 | 7 | | 3 types, each refers to the 3 | 64 | | 4 types, each refers to the 4 | 3613 | | 5 types, each refers to the 5 | 8 million | | a ring of 32 types | 127 | | 5 types as in a syntax tree (Expr, Stmt, Decl, Pat, Type) | fewer than 400 | A type of more than 10000 bodies, or of more than 256 nested named types, is refused: "the type `T4` is too large ...". Without the limit, the dense cycle of 5 does not end, and a ring of 700 types overflows the stack. The depth limit also applies to `data` types that do not refer to each other: 700 nested `data` types overflowed the stack before this change, and are now the named error. A recursive type of n variables (as the `rec` groups of WasmGC) removes the size limit. It is a change of the core language, so it is a decision for the owner and not part of this pull request. The plan document records this next to the D7 ratification. ## Verification - `cargo test --workspace --no-fail-fast`: 638 passed, 0 failed. - `cargo fmt --all --check` and `cargo clippy --workspace --all-targets`: clean. - `scripts/status-gate.sh`: 635 all-target tests (1 more than before). - `scripts/probe-battery.sh`: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI). - New test `data_types_that_refer_to_each_other_run`, each program as wasm and in the interpreter: - Tree and Forest, Even and Odd, a cycle where no type refers to itself, type parameters at I64, a linear component; - a cycle of 3 types where each one refers to the 2 others, in each of the 6 orders of its names (each order is another nesting); - refused: a value of a linear type of a cycle used 2 times (2 programs), a `Forest` as a `Tree`, a `Tree` as a `Forest`. - `a_recursive_form_with_no_lowering_is_refused_by_name`: the 2 limits (the dense cycle of 5, a ring of 300). - `a_recursive_data_type_crosses_a_module`: 2 types that refer to each other, used from another module. --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
v2 plan rung E9, the recursive type half. Decision D7 is ratified (owner, 2026-11-10): iso-recursive types, with fold and unfold from the desugarer. The closure half merged in #437.
A
datatype that refers to itself was refused. It is now the core typemu X. T, behind the flag--unstable-core.ephapax run --unstable-coreprints 6, as wasm and in the interpreter. This is the acceptance program of the rung.How
ephapax-syntax):Ty::Mu { var, body },ExprKind::Fold { ty, value },ExprKind::Unfold(e).datatype that is entered again during its own expansion becomesmu #Name. body. A constructor gets afold, and amatchgets anunfoldon its scrutinee. Adatatype that does not refer to itself has the same lowering as before.fold[mu X. T](e)needse : T[X := mu X. T], andunfoldgives that type. 2 recursive types are equal when their bodies are, up to the name of the bound variable. A recursive type is not equal to its unfolding.mu X. Tis linear whenTis linear withXnot linear. This is the least fixed point that the plan gives for the grade of a recursive type.Type parameters
data List(a) = Nil | Cons(a, List(a))works at each element type.datatype binds the type parameters (forall a. ...). The checker gives each one a type from the use of the value, and thefoldmakes the annotations of the injections agree.datatype, a type parameter now stands for its argument at each depth. Before, only a parameter that was a whole field got its argument:data Box(a) = MkBox((a, a))kepta.Refused by name
datatypes that refer to each otherdatatypes Tree -> Forest -> Tree refer to each otherGrowrefers to itself with other type argumentstypealias that refers to itselfdatatype can refer to itselfA
typealias in the cycle of adatatype is permitted: it is transparent.The flag
Without
--unstable-core,check,compileandrunrefuse a program that uses a recursive type: "behind the flag--unstable-core: the recursive typeIntList...". A declaration with no use is accepted. The proberec1now has this verdict, so its 2 rows intests/probes/expectations.tsvchange fromerror:DesugarErrortoerror:UnstableCore, andscripts/probe-battery.shknows that kind.Verification
cargo test --workspace --no-fail-fast: 636 passed, 0 failed.cargo fmt --all --checkandcargo clippy --workspace --all-targets: clean.scripts/status-gate.sh: 633 all-target tests (8 more than before).scripts/probe-battery.sh: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI).scripts/test-probe-battery.sh: 4 passed.recursive_types.rs, 6 tests, each program as wasm and in the interpreter:a_recursive_data_type_runs(10 programs: sum, range, append, map with a closure, guards and literals, values in pairs, lists and closures, 3 constructors, an alias in the cycle);a_recursive_data_type_with_type_parameters_runs(7 programs: Bool, I64, F64, a list of lists, a rose tree, a generic function, a type from its use);a_recursive_data_type_crosses_a_module(5 programs);a_recursive_type_keeps_the_linear_rules(a list of strings: used 2 times, a part not consumed, not used, and a region escape are each refused);a_recursive_form_with_no_lowering_is_refused_by_name;a_recursive_data_type_is_behind_the_flag.linearity_holes.rs: therec1test now checks the flag, and 1 new test checks the 3 named desugar errors.ephapax-ir: a round trip test forfold,unfold,muand a bound type parameter.Not in this pull request
datatypes that refer to each other (refused by name).data Self = MkSelf(Self -> I32)is accepted.--unstable-core(it waits for proof rung P17).Generated by Claude Code