V5004 literal_violates_refinement
A literal stands where a refined type is expected, and the compiler evaluated the type's where clause on it: the predicate is false, or evaluating it defects (an integer division by zero, a failed requires of a function it calls).
An error from the contract phase. sakura explain V5004 prints this explanation offline.
A literal stands where a refined type is expected, and the compiler evaluated the type's
where clause on it: the predicate is false, or evaluating it defects (an integer division
by zero, a failed requires of a function it calls). The literal can never be a value of the
type, so the program would stop with D010 before main (design §4.3, §17.87). Use a value
that satisfies the clause; there is no mechanical fix.
The compiler evaluates predicates over scalars (Bool, Int, Float, String), operators,
if, let, calls to pure functions and String.len/contains/starts_with/ends_with, for
at most 10,000 steps. A literal it cannot decide this way is checked at start-up instead,
with no diagnostic.
Wrong:
type Percent = Int where it >= 0 && it <= 100
let p: Percent = 150Fixed:
type Percent = Int where it >= 0 && it <= 100
let p: Percent = 50Wrong program
compiler/tests/ui/V5004_literal_violates_refinement.sakura, which the compiler's ui suite runs through sakura check:
type Percent = Int where it >= 0 && it <= 100
let p: Percent = 150sakura check --json reports this record (pretty-printed; $DIR is the fixture's directory):
{
"schema_version": "1.0",
"kind": "diagnostic",
"id": "d:f2031e38005324ab",
"code": "V5004",
"severity": "error",
"phase": "contract",
"message": "`150` does not satisfy the `where` clause of `Percent`",
"snapshot": "sha256:$SNAPSHOT",
"symbol_id": "main::V5004_literal_violates_refinement::p",
"spans": [
{
"uri": "file://$DIR/V5004_literal_violates_refinement.sakura",
"content_hash": "sha256:d2f1fca3817182d347c7d91f32404fd2a085f8b5002c18aacbcfed11d29340bd",
"start_byte": 149,
"end_byte": 152,
"role": "primary",
"label": "never a valid `Percent`"
},
{
"uri": "file://$DIR/V5004_literal_violates_refinement.sakura",
"content_hash": "sha256:d2f1fca3817182d347c7d91f32404fd2a085f8b5002c18aacbcfed11d29340bd",
"start_byte": 110,
"end_byte": 130,
"role": "definition",
"label": "the refinement of `Percent`"
}
],
"related_ids": [],
"expected": null,
"actual": null,
"obligation": null,
"counterexample": null,
"explanation_uri": "sakura://explain/V5004",
"fixes": []
}Fixed program
compiler/tests/ui/V5004_literal_violates_refinement.fixed.sakura, which sakura check accepts with no diagnostics:
type Percent = Int where it >= 0 && it <= 100
let p: Percent = 50