Repository navigation
fix: a constructor checks its arguments against the declaration - #442
Conversation
A constructor of a `data` type that is not recursive left no core node that carries the declared type. `MkBox(true)` passed for `data Box = MkBox(I32)` until a use of the value as a `Box`. The desugarer now emits `let #<Ctor>: T = <value> in #<Ctor>`. `T` is the declared type and binds the type parameters of the `data` type. The type checker instantiates the annotation, and a mismatch is the new error `ConstructorMismatch`, which names the constructor. The check is on the full value, so the arguments of 1 constructor fix the type parameters for the other constructors also. Wasm codegen reads the type of such a `let` from the type table, because the annotation binds type parameters. Owner decisions 2026-11-10: the annotated `let` is the interim form; decision D14 in the plan document records the type ascription for the P4 core, to be decided with `TMu`, `fold` and `unfold`. A constructor of a recursive type has the check from its `fold`, as before. 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. |
|
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. |
![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: b6bad20a78
ℹ️ 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".
| ExprKind::Let { | ||
| name: name.clone(), | ||
| ty: Some(quantify(ty, ¶ms)), | ||
| value: Box::new(value), | ||
| body: Box::new(Expr::new(ExprKind::Var(name), span)), |
There was a problem hiding this comment.
The new safety check exists only in this annotated let, but ephapax_ir::expr_to_sexpr serializes Let without its ty and decode_expr restores it as None. Consequently, serializing a desugared module and compiling it through the public compile_sexpr_module/CLI S-expression path silently removes the check, so invalid terms such as data Box = MkBox(I32) with MkBox(true) are accepted again. Either the IR codec must preserve this annotation or the constructor invariant must be represented by a core form that survives the round trip.
Useful? React with 👍 / 👎.
| if let Some(declared) = ty_ann { | ||
| // The desugarer gives a constructor the binder `#<name>` and | ||
| // the declared type of its `data` type, which binds the type | ||
| // parameters. A written annotation binds none. | ||
| let declared = &self.instantiate(declared.clone()).0; |
There was a problem hiding this comment.
This now instantiates every annotated let, not just the synthetic #Ctor bindings. For callers constructing the public core AST, a declaration such as let id: forall a. a -> a = (fn (x: I32) -> x) in ... was previously rejected because the value is monomorphic, but is now accepted by choosing a = I32, even though Ty::ForAll is documented as universal polymorphism. Gate this instantiation on the synthetic constructor binding (or use a separate constructor-ascription mechanism) so ordinary core annotations continue to check the declared universal type rather than an arbitrary instance.
Useful? React with 👍 / 👎.
Summary
A constructor of a
datatype that is not recursive left no core node that carries the declared type.MkBox(true)passed fordata Box = MkBox(I32)until a use of the value as aBox. This pull request adds the check.Before:
checkaccepts the program. After:Changes
datatype that is not recursive becomeslet #<Ctor>: T = <value> in #<Ctor>.Tis the declared type and binds the type parameters of thedatatype.check_letinstantiates the annotation. A mismatch on a#<Ctor>binder is the new errorConstructorMismatch, which names the constructor. The check is on the full value, so the arguments of 1 constructor fix the type parameters for the other constructors also (P2(1, 2)fordata P(a) = P2(a, a) | Q(a)makesQhold anI32).compile_letreads the type of such aletfrom the type table, because the annotation binds type parameters. (With the annotation, a value of 64 bits got a local of 32 bits.)TMu,foldandunfold.Owner decisions of 2026-11-10: the annotated
letis the interim form, and the error names the constructor.No file in
formal/changes. The calculus has the term already (ELet v (EVar 0)).Not in this pull request
fold, as before. Its error text stays the general "Type mismatch".datatypes stay structural: a value that no constructor made passes as thedatatype (f(5)forfn f(b: Box)). D14 lists the nominal form that closes this.Test plan
a_constructor_checks_its_arguments_against_the_declaration(src/ephapax-cli/tests/run_wasm.rs): 4 programs thatcheckrefuses, and 2 programs that run in wasm and in the interpreter (a generic function whose type parameter has the name of the parameter of thedatatype, with a value of 64 bits; a linear argument).data_types_that_refer_to_each_other_run: aTreeas aForestis now refused at the constructorNode.cargo test --workspace: 643 pass, 0 fail.cargo fmt --checkandcargo clippy --workspace --all-targets -- -D warningsare clean.checkon each of the 149.ephfiles of the repository gives the same result before and after.Generated by Claude Code