Repository navigation
fix: subtyping and coercion rules for optional types - #678
Merged
Merged
Conversation
Click to see raw report |
crusso
reviewed
Sep 19, 2025
crusso
reviewed
Sep 19, 2025
crusso
approved these changes
Sep 19, 2025
crusso
left a comment
crusso
left a comment
Contributor
There was a problem hiding this comment.
Looks good to me and I think the rules all match up with your final fixes in the doc.
To be honest, it might be good to include the doc in the PR description, in case anyone want to understand the PR later.
crusso
approved these changes
Sep 22, 2025
crusso
left a comment
crusso
left a comment
Contributor
There was a problem hiding this comment.
Still looks good to me.
(Motoko will need to change its implementation too is seems caffeinelabs/motoko#5504)
2 of 3 tasks
ggreif
added a commit
to caffeinelabs/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 <gabor@dfinity.org> 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>
lwshang
added a commit
that referenced
this pull request
Oct 21, 2026
## Summary `type Opt = opt Opt` is an *infinite option*: an option whose constituent is again an option, forever. The spec's coercion rules don't say what happens when a value whose type does not accept `null` (say `true : bool`) is coerced at one. The implementations and the test suite agree that decoding fails. This PR writes that into the spec. No implementation changes. ## Why the spec has a gap here Before #678, the rule via the constituent type had a premise `not (null <: <t'>)`, so it never unwrapped an option inside an option. Coercion was well founded, and `true : bool` at `Opt` gave `null` (test/construct.test.did asserted exactly that, from #126). #678 dropped the premise so that `5 : nat` coerces to `opt opt 5 : opt opt nat`. At an infinite option, that rule now asks for a coercion of the same value one level down, and the rule that goes to `null` applies only if that coercion doesn't exist. So the answer depends on its own negation, and the spec's own soundness property (`nat <: Opt`, so some coercion should exist) contradicts any reading of it. ## What the implementations do - **`candid` ≥ 0.10.20 (#679) rejects.** It keeps unwrapping the expected type until its recursion limit. That error is not a `Subtype` error, so the `opt` rule's recovery doesn't catch it, and the whole message fails, even under an enclosing `opt`, in a record field, or in a vector element. Probed directly; the new assertions cover those cases. - **test/construct.test.did** has asserted `!:` for `true : bool` at `Opt` since #679. The review comment there: `true : bool` "cannot coerce into an _infinitely_ nested optional type". - **Motoko** runs this repo's `test/` suite in CI with no expected-failure list, and #679's approver ported the change there (caffeinelabs/motoko#5505). The new assertions will check the enclosing-`opt`, record and vector cases on Motoko's side when it picks up this suite. ## The change - **`spec/Candid.md`, Coercion › Options:** - Defines an infinite option. - States that coercing a value whose type does not accept `null` at one is *undefined*. That is distinct from failing to coerce: a `not (exists <w>. ...)` premise only holds where coercion is defined. - So no enclosing option recovers, and deserialisation fails. - **`spec/Candid.md`, Properties:** soundness states this as its exception. - **`test/construct.test.did`:** new assertions: - the mutually recursive case (`type OptA = opt OptB; type OptB = opt OptA`) - an enclosing option (`opt true : opt bool` at `Opt`) - a record field and a vector element at `Opt` - an empty `vec bool` at `vec Opt`, which decodes, since there is nothing to coerce. Each rejected blob was checked to decode at a compatible type, so it fails because of the cycle and not because the bytes are malformed. - **`CHANGELOG.md`:** an `Unreleased` spec entry. The spec's `Version: 0.1.8` line is unchanged, as with #678 and #748. ## Follow-up The Lean model on `rewrite` (#777) currently answers `null` here. Once this lands it will follow the spec: `coerce` gets an "undefined" outcome that no `opt` absorbs, and the vector that is currently a known divergence becomes an agreement. ## Test ``` cargo test -p candid_parser --test test_suite ``` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 (1M context) <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.
This PR fixes the specification of subtyping and coercion rules for optional types.
The changes to the specification are implemented in a separate PR.
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
is always false and this rule can be dropped.
Subtyping fix 2
The existing subtyping rule
should be fixed to
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 natcannot be derived otherwise.Subtyping fix 3
The pre-condition
not (null <: <datatype'>)in the existingsubtyping rule
effectively only forbids
nullas<datatype'>because every other<datatype'>such thatnull <: <datatype'>would also satisfy<datatype> <: <datatype'>and thus violate the otherpre-condition. Since the corresponding coercion rule coerces to
nullinthis case anyway, we should enable
nullas<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
Subtyping fix 4
Analogously to the existing rule
we need to add a new rule
otherwise the type
reservedis not a subtype of an option (contrary tothe 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
otherwise the type
natis not a subtype ofopt nat64.Fixed subtyping rules
The final set of subtyping rules for optional types is
and it is easy to see that these rules are non-overlapping and
correspond to coercion rules.
Coercion rules
Coercion fix 1
The rule
is overlapping with
and thus the former should be fixed to
Coercion fix 2
The coercion rule
has a pre-condition
not (null <: <t'>)that does not correspond toany pre-condition in the corresponding subtyping rule (the fixed rule in
the section "Subtyping fix 2") and prevents coercion of
natintoopt opt nat(for instance). Hence, we drop the pre-condition and the updated
rule is
Coercion fix 3
The rule
allows
opt 5 : opt natto coerce tonull : opt natwhich does not makesense as it loses data (
opt 5) that could be preserved. This rule shouldbe extended with an additional pre-condition
not (null <: <t>)sincethere are separate coercion rules for such cases.
Coercion fix 4
The rule
allows
5 : natto coerce tonull : opt opt natwhich does not makesense. This rule should be extended with an additional pre-condition
to only coerce to
null : opt <t'>if coercion to<t'>failed.Coercion fix 5
But now we easily see that the two rules
and
can be merged into a single rule
Fixed coercion rules
The final set of coercion rules is
and it is easy to see that these rules are non-overlapping and
correspond to subtyping rules.