V4003 or_pattern_bindings
All alternatives of an or-pattern must bind the same names with the same types (design §3.2).
An error from the pattern phase. sakura explain V4003 prints this explanation offline.
All alternatives of an or-pattern must bind the same names with the same types (design §3.2).
Bind the name in every alternative, replace it with _, or split the alternatives into arms.
Wrong:
(x, 0) | (0, _) => 1Fixed:
(_, 0) | (0, _) => 1Wrong program
compiler/tests/ui/V4003_or_pattern_bindings.sakura, which the compiler's ui suite runs through sakura check:
fn pick(p: (Int, Int)) -> Int {
match p {
(x, 0) | (0, _) => 1,
_ => 0,
}
}sakura check --json reports this record (pretty-printed; $DIR is the fixture's directory):
{
"schema_version": "1.0",
"kind": "diagnostic",
"id": "d:a98f0035700d955c",
"code": "V4003",
"severity": "error",
"phase": "pattern",
"message": "alternatives of an or-pattern must bind the same names: the first binds {x}, this one binds {}",
"snapshot": "sha256:$SNAPSHOT",
"symbol_id": "main::V4003_or_pattern_bindings::pick",
"spans": [
{
"uri": "file://$DIR/V4003_or_pattern_bindings.sakura",
"content_hash": "sha256:5a1c45ebaa3fce59725ab156882795b3723d76bb541d0b4ad9bf11715c24b8b4",
"start_byte": 91,
"end_byte": 97,
"role": "primary"
}
],
"related_ids": [],
"expected": null,
"actual": null,
"obligation": null,
"counterexample": null,
"explanation_uri": "sakura://explain/V4003",
"fixes": []
}Fixed program
compiler/tests/ui/V4003_or_pattern_bindings.fixed.sakura, which sakura check accepts with no diagnostics:
fn pick(p: (Int, Int)) -> Int {
match p {
(_, 0) | (0, _) => 1,
_ => 0,
}
}V4002 unreachable_arm
A match arm can never be reached because earlier arms already cover every value it matches.
V5001 impure_contract
Predicates in where, requires, ensures and property bodies must be pure, terminating and deterministic: no loops, no recursion, and calls only to @total functions in the contract subset (design §7.1).