fix: coercion of values into nested optional types #679
Conversation
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
Click to see raw report |
ilbertt
approved these changes
Sep 22, 2025
mraszyk
commented
Sep 22, 2025
| assert blob "DIDL\01\6e\7f\01\00\00" == "(null)" : (opt opt null) "opt: parsing (null : opt null) at opt opt null gives null, not opt null"; | ||
| assert blob "DIDL\00\01\7e\01" == "(null)" : (opt opt bool) "opt: parsing true : opt opt bool gives null"; | ||
| assert blob "DIDL\00\01\7e\01" == "(null)" : (Opt) "opt: parsing (true : bool) at \"fix opt\" gives null"; | ||
| assert blob "DIDL\00\01\7e\01" == "(opt opt true)" : (opt opt bool) "opt: parsing true : opt opt bool gives null"; |
Contributor
Author
There was a problem hiding this comment.
That's the change by this PR: true : bool coerces to opt opt true : opt opt bool.
mraszyk
commented
Sep 22, 2025
| assert blob "DIDL\00\01\7e\01" == "(null)" : (opt opt bool) "opt: parsing true : opt opt bool gives null"; | ||
| assert blob "DIDL\00\01\7e\01" == "(null)" : (Opt) "opt: parsing (true : bool) at \"fix opt\" gives null"; | ||
| assert blob "DIDL\00\01\7e\01" == "(opt opt true)" : (opt opt bool) "opt: parsing true : opt opt bool gives null"; | ||
| assert blob "DIDL\00\01\7e\01" !: (Opt) "opt: parsing (true : bool) at \"fix opt\" fails"; |
Contributor
Author
There was a problem hiding this comment.
true : bool cannot coerce into an infinitely nested optional type
This was referenced Sep 22, 2025
mraszyk
added a commit
that referenced
this pull request
Oct 7, 2025
This PR fixes the specification of subtyping and coercion rules for optional types. The changes to the specification are implemented in a separate [PR](#679). # Subtyping rules ## Subtyping fix 1 The specification claims that the rules allow "*any* type to be regarded as a subtype of an option". Hence, the pre-condition of the rule ``` not (<datatype> <: opt <datatype'>) --------------------------------- opt <datatype> <: opt <datatype'> ``` is always false and this rule can be dropped. ## Subtyping fix 2 The existing subtyping rule ``` not (null <: <datatype'>) <datatype> <: <datatype'> ----------------------------- <datatype> <: opt <datatype'> ``` should be fixed to ``` not (null <: <datatype>) <datatype> <: <datatype'> ----------------------------- <datatype> <: opt <datatype'> ``` according to the specification "It can also be specialised to its constituent type, unless that type is itself optional". Also the fact that `nat <: opt opt nat` cannot be derived otherwise. ## Subtyping fix 3 The pre-condition `not (null <: <datatype'>)` in the existing subtyping rule ``` not (null <: <datatype'>) not (<datatype> <: <datatype'>) --------------------------------- opt <datatype> <: opt <datatype'> ``` effectively only forbids `null` as `<datatype'>` because every other `<datatype'>` such that `null <: <datatype'>` would also satisfy `<datatype> <: <datatype'>` and thus violate the other pre-condition. Since the corresponding coercion rule coerces to `null` in this case anyway, we should enable `null` as `<datatype'>` in this rule (as otherwise a separate rule to cover this case is needed with the same coercion rule). Hence, the updated rule should read ``` not (<datatype> <: <datatype'>) --------------------------------- opt <datatype> <: opt <datatype'> ``` ## Subtyping fix 4 Analogously to the existing rule ``` ---------------------- null <: opt <datatype> ``` we need to add a new rule ``` -------------------------- reserved <: opt <datatype> ``` otherwise the type `reserved` is not a subtype of an option (contrary to the claim that every type is a subtype of an option). ## Subtyping fix 5 The specification claims that the rules allow "any type to be regarded as a subtype of an option". Hence, we need to add the rule ``` not (null <: <datatype>) not (<datatype> <: <datatype'>) ----------------------------- <datatype> <: opt <datatype'> ``` otherwise the type `nat` is not a subtype of `opt nat64`. ## Fixed subtyping rules The final set of subtyping rules for optional types is ``` ---------------------- null <: opt <datatype> ``` ``` -------------------------- reserved <: opt <datatype> ``` ``` <datatype> <: <datatype'> --------------------------------- opt <datatype> <: opt <datatype'> ``` ``` not (<datatype> <: <datatype'>) --------------------------------- opt <datatype> <: opt <datatype'> ``` ``` not (null <: <datatype>) <datatype> <: <datatype'> ----------------------------- <datatype> <: opt <datatype'> ``` ``` not (null <: <datatype>) not (<datatype> <: <datatype'>) ----------------------------- <datatype> <: opt <datatype'> ``` and it is easy to see that these rules are non-overlapping and correspond to coercion rules. # Coercion rules ## Coercion fix 1 The rule ``` --------------------------------- <v> : reserved ~> null : opt <t'> ``` is overlapping with ``` null <: <t> ----------------------------- null : <t> ~> null : opt <t'> ``` and thus the former should be fixed to ``` not (<v> = null) ----------------------------- <v> : reserved ~> null : opt <t'> ``` ## Coercion fix 2 The coercion rule ``` not (null <: <t>) not (null <: <t'>) <v> : <t> ~> <v'> : <t'> -------------------------------- <v> : <t> ~> opt <v'> : opt <t'> ``` has a pre-condition `not (null <: <t'>)` that does not correspond to any pre-condition in the corresponding subtyping rule (the fixed rule in the section "Subtyping fix 2") and prevents coercion of `nat` into `opt opt nat` (for instance). Hence, we drop the pre-condition and the updated rule is ``` not (null <: <t>) <v> : <t> ~> <v'> : <t'> -------------------------------- <v> : <t> ~> opt <v'> : opt <t'> ``` ## Coercion fix 3 The rule ``` not (null <: <t'>) not (exists <w>. <v> : <t> ~> <w> : <t'>) -------------------------------- <v> : <t> ~> null : opt <t'> ``` allows `opt 5 : opt nat` to coerce to `null : opt nat` which does not make sense as it loses data (`opt 5`) that could be preserved. This rule should be extended with an additional pre-condition `not (null <: <t>)` since there are separate coercion rules for such cases. ## Coercion fix 4 The rule ``` null <: <t'> not (null <: <t>) ---------------------------- <v> : <t> ~> null : opt <t'> ``` allows `5 : nat` to coerce to `null : opt opt nat` which does not make sense. This rule should be extended with an additional pre-condition ``` not (exists <w>. <v> : <t> ~> <w> : <t'>) ``` to only coerce to `null : opt <t'>` if coercion to `<t'>` failed. ## Coercion fix 5 But now we easily see that the two rules ``` not (null <: <t>) not (null <: <t'>) not (exists <w>. <v> : <t> ~> <w> : <t'>) -------------------------------- <v> : <t> ~> null : opt <t'> ``` and ``` not (null <: <t>) null <: <t'> not (exists <w>. <v> : <t> ~> <w> : <t'>) ---------------------------- <v> : <t> ~> null : opt <t'> ``` can be merged into a single rule ``` not (null <: <t>) not (exists <w>. <v> : <t> ~> <w> : <t'>) -------------------------------- <v> : <t> ~> null : opt <t'> ``` ## Fixed coercion rules The final set of coercion rules is ``` not (<v> = null) --------------------------------- <v> : reserved ~> null : opt <t'> ``` ``` null <: <t> ----------------------------- null : <t> ~> null : opt <t'> ``` ``` <v> : <t> ~> <v'> : <t'> ---------------------------------------- opt <v> : opt <t> ~> opt <v'> : opt <t'> ``` ``` not (exists <w>. <v> : <t> ~> <w> : <t'>) ---------------------------------------- opt <v> : opt <t> ~> null : opt <t'> ``` ``` not (null <: <t>) <v> : <t> ~> <v'> : <t'> -------------------------------- <v> : <t> ~> opt <v'> : opt <t'> ``` ``` not (null <: <t>) not (exists <w>. <v> : <t> ~> <w> : <t'>) -------------------------------- <v> : <t> ~> null : opt <t'> ``` and it is easy to see that these rules are non-overlapping and correspond to subtyping rules.
ggreif
added a commit
to dfinity/motoko
that referenced
this pull request
Nov 6, 2025
## Implement Martin's revised deserialization for Candid options > This PR fixes coercion of values into nested optional types. >Before the fix from this PR, `5 : nat64` would coerce to `opt 5 : opt na64` (as expected) and `null : opt opt nat64` (unexpected). >This PR fixes the unexpected result to be `opt opt 5 : opt opt nat64` (as expected). >Before the fix from this PR, `5 : int` would coerce to `null : opt opt nat`. This PR fixes the result to be `opt null : opt opt nat`. The >motivation for this change is to enable using optional types as follows: >- outer option characterizes if a value (of any type) is provided; >- inner option expresses to optimistically deserialize the actual value into the given type (without failing to deserialize and without losing the information if a value of any type is provided). >This PR also adds multiple test cases covering the change to coercion (including coercion to nested optional types over `null` and `reserved`). c.f. * Rust fix dfinity/candid#679 * Candid spec [PR](dfinity/candid#678), in particular this commit dfinity/candid@90af305 ## Furthermore (from #5619) fixes #5543. The spec says that every Candid value is a subtype of `opt T`, and gives `opt t` when `t <: T`. But the `null` type has no subtypes. I.e. we only get out a `null : Null` when the binary Candid has a `0x7F` there. In all other cases the coercion must fail, either trapping or indicating a coercion failure to the caller (when recoverable). However `null : ?T` can always be materialised when an argument is missing, similarly `null : Null`. So we have to treat missing arguments and coercion failures differently when the requested type is `Null` (or `null` respectively, in Candid). This PR corrects the reading of (e.g. `\x70`, `<reserved>`) in the non-recoverable case and makes it a coercion failure. Also adds improvements to the `candid-tests` runner to - not ignore the case when a field type can be inferred, but not in the record type (eliminating `M0164`, ignored test) - adds `null` values to top-level argument tuples where the type requests them - adds `null` fields to record values (in argument sequences) where the type requests them ------------------ TODO Tasks: - [x] bump candid dependency to pick up revised test suite - [x] It would be cool if the generated Motoko would be output on `stderr` when `--diag` is passed to `candid-tests` - [ ] potential simplifications suggested in #5619 --------- Co-authored-by: Gabor Greif <[email protected]> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: pr-automation-bot-public[bot] <189003650+pr-automation-bot-public[bot]@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
This PR fixes coercion of values into nested optional types.
Before the fix from this PR,
5 : nat64would coerce toopt 5 : opt na64(as expected) andnull : opt opt nat64(unexpected). This PR fixes the unexpected result to beopt opt 5 : opt opt nat64(as expected).Before the fix from this PR,
5 : intwould coerce tonull : opt opt nat. This PR fixes the result to beopt null : opt opt nat. The motivation for this change is to enable using optional types as follows:This PR also adds multiple test cases covering the change to coercion (including coercion to nested optional types over
nullandreserved).