Repository navigation
fix(desugar): a constructor gets its type arguments from its use - #439
Conversation
A constructor of a `data` type with type parameters did not check when the other side of its sum had a type parameter: `None` was not an `Option(I32)`, and `L(1)` was not an `Either(I32, Bool)`. The annotation of the injection had the type parameter itself, which is no type at the constructor. It checked only when a generic function gave its own type parameter the same name. The annotation now binds the type parameters of the `data` type, 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. A use at another type is a type error, as before. No program of the corpus changed. New test: a_constructor_gets_its_type_arguments_from_its_use (7 programs, as wasm and in the interpreter). 637 tests pass; the all-target count is 634. Co-Authored-By: Claude Fable 5.2 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u
|
Caution Review failedThe pull request is closed.
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
|
|
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. |
Codex Review Summary: ✅ CompletedThis 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. |
![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: 352456f5e3
ℹ️ 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".
| // constructors are names of the module that declares the type. | ||
| let value = self.in_scope(&info.home, |this| { | ||
| this.wrap_injection(payload, info.index, &ctors, params, span) | ||
| this.wrap_injection(payload, info.index, &ctors, ¶ms, span) |
There was a problem hiding this comment.
For a nonrecursive data T(a) = A | B(a) | C(a), this passes params into every nested injection, but each annotation is quantified separately and check_inl/check_inr therefore instantiates it with a different unification variable. Consequently, if true then B(1) else C(true) now type-checks as Unit + (I32 + Bool), and a subsequent match can use the B payload numerically and the C payload as a boolean even though both occurrences are declared to have the same a. The constructor needs one shared instantiation for all occurrences of each data parameter rather than an independent one per injection annotation.
Useful? React with 👍 / 👎.
| // 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)?; |
There was a problem hiding this comment.
Giving a nonrecursive constructor a fresh inferred parameter also lets an affine binding be classified before that parameter is solved. For example, with data Option(a) = None | Some(a), let x = None in eat(x) + eat(x) is accepted when eat takes and consumes an Option(String@r): x is stored as Unit + ?a, so its context entry is considered non-linear; the first call solves ?a to the linear String@r, but mark_used still checks the unresolved entry and permits the second use. This bypasses the checker's documented rule that a sum is linear whenever any component is linear, so inferred constructor parameters must be resolved when enforcing reuse (or the binding must be updated when unification solves them).
Useful? React with 👍 / 👎.
…#441) ## Summary 1. A top-level constant works: `let K = 40` and `let K: I32 = 40`. 2. A fix for a defect that #439 exposed: a type that a function body fixes late gave a wasm module that was not valid. ## 1. Top-level constants The grammar had the declaration (`const_decl`), and only the core parser read it. | Step | Before | Now | |---|---|---| | Surface parser | "Unexpected declaration: const_decl" | `SurfaceDecl::Const` | | Type checker | the value was not checked, and no function body had the constant in scope | the value is checked, and each function body sees the constant | | wasm | no code; a use of the name was a trap | a function with no parameter; a use is a call | | Interpreter | no code | the value, from an empty environment | The rules: - **Scope.** The value of a constant sees the functions of the module and the constants before it. Each function sees each constant. A `let` or a parameter of the same name hides the constant. - **Type.** The type in the declaration, or else the type of the value. A linear type is an error (a constant is used many times). A value that does not fix the type (`let K = None`) is an error that asks for a type in the declaration. - **Modules.** A constant is private to its module (the grammar has no `pub` for it). 2 modules can have a constant of one name: in the merge, a constant gets a module name as a function does. - **Evaluation.** The value is computed at each use. A value that is costly, or that has an effect that must happen 1 time, needs a wasm global that a start function sets. The code names that step. - **Upper-case names.** The parser reads a name with an upper-case first letter as a constructor. Such a name that is no constructor in scope, and that is a constant of the module, is the constant. A constructor of the same name comes first. - **One declaration for a name.** A module declares a name 1 time, as a function or as a constant. This also refuses 2 functions of one name, which passed the checker and then gave a wasm module that was not valid ("duplicate export name"). The forms behind `--unstable-core` are behind it in the value of a constant too. ## 2. Fix: a type that a function body fixes late ``` data Option(a) = None | Some(a) fn main(): I64 = let o = None in match o of | None => 5000000000 | Some(n) => n end ``` `check` accepted this program, and `run` then stopped: "emitted wasm failed structural validation: type mismatch: expected i64, found i32". The validator stopped the module, so no wrong program ran. Cause: the arms of the `match` fix the type of `o` after the checker recorded the type of the scrutinee. The solutions of a function body were dropped at the end of its check, before the type table was resolved, so the table kept the type as not known and the wasm backend read the payload as an i32. Before #439 this program did not pass the checker, so the gap was not reachable. The types of a body are now resolved when its check ends. ## Verification - `cargo test --workspace --no-fail-fast`: 642 passed, 0 failed. No program of the corpus changed. - `cargo fmt --all --check` and `cargo clippy --workspace --all-targets`: clean. - `scripts/status-gate.sh`: 639 all-target tests (4 more than before). - `scripts/probe-battery.sh`: 51 SAME, 7 SKIP (the SKIP rows need the wasmtime CLI). - New file `constants.rs`, each program as wasm and in the interpreter: - `a_top_level_constant_runs` (10 programs: plain, lower-case with a type, order, in a lambda, hidden by a local, I64 and F64 and Bool, a closure and a pair and a list and a `data` value, a generic function, a constructor of the same name, a function value); - `a_constant_is_private_to_its_module`; - `a_constant_follows_the_flag`; - `a_constant_that_is_not_valid_is_refused_by_name` (8 programs). - `a_constructor_gets_its_type_arguments_from_its_use`: 2 more programs for the fix (I64 and F64). --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
Summary
A constructor of a
datatype with type parameters did not check when the other side of its sum had a type parameter.fn none(): Option(I32) = NoneI32, foundVar("a")or(None, 2)withor(o: Option(I32), d: I32)let o = None in match o of ...pick(L(42))withpick(e: Either(I32, Bool))fn none<T>(): Option(T) = NoneVar("a")againstVar("T"))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 thedatatype did.The annotation now binds the type parameters of the
datatype (inl[forall a. a](())), for eachdatatype with type parameters. #438 did this for adatatype 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))withg(t: T(Bool))gives "Type mismatch".No flag: a
datatype 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 --checkandcargo 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).a_constructor_gets_its_type_arguments_from_its_useinrun_wasm.rs: 7 programs, as wasm and in the interpreter (a result, an argument, no annotation, the 2 branches of anif, 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