V5003 validate_target_not_refined
Untrusted.validate(u) takes its target V from the expected type Result<V, Violation>.
An error from the contract phase. sakura explain V5003 prints this explanation offline.
Untrusted.validate(u) takes its target V from the expected type Result<V, Violation>.
V must be a refined type whose base is the type inside the Untrusted (design §6.4, §17.71):
a plain type has no predicate, so nothing would be validated. Annotate the binding or the
function's return type with a refined type, or use Untrusted.check(u, clause, pred) for an
ad-hoc predicate.
Wrong:
import std/untrusted
import std/core.{Violation}
fn port(u: Untrusted<Int>) -> Result<Int, Violation> { Untrusted.validate(u) }Fixed:
type Port = Int where it >= 1 && it <= 65535
fn port(u: Untrusted<Int>) -> Result<Port, Violation> { Untrusted.validate(u) }Wrong program
compiler/tests/ui/V5003_validate_into_plain_type.sakura, which the compiler's ui suite runs through sakura check:
import std/core.{Violation}
import std/untrusted
fn plain() -> Result<Int, Violation> { Untrusted.validate(Untrusted.of(1)) }sakura check --json reports this record (pretty-printed; $DIR is the fixture's directory):
{
"schema_version": "1.0",
"kind": "diagnostic",
"id": "d:f2a22a0806b61270",
"code": "V5003",
"severity": "error",
"phase": "contract",
"message": "`Untrusted.validate` validates into a refined type, but `Int` is not one (design §6.4)",
"snapshot": "sha256:$SNAPSHOT",
"symbol_id": "main::V5003_validate_into_plain_type::plain",
"spans": [
{
"uri": "file://$DIR/V5003_validate_into_plain_type.sakura",
"content_hash": "sha256:688e845ee691da157ce4a7e6b697c4334c38635d9037f1c4cb6c0f52403ed14d",
"start_byte": 147,
"end_byte": 182,
"role": "primary"
}
],
"related_ids": [],
"expected": null,
"actual": null,
"obligation": null,
"counterexample": null,
"explanation_uri": "sakura://explain/V5003",
"fixes": [
{
"id": "f:f2a22a0806b61270.0",
"title": "Annotate the binding with a refined type, e.g. `let e: Email = Untrusted.validate(u)?`",
"applicability": "incomplete",
"impact": "local",
"edits": []
}
]
}Fixed program
compiler/tests/ui/V5003_validate_into_plain_type.fixed.sakura, which sakura check accepts with no diagnostics:
import std/core.{Violation}
import std/untrusted
type Small = Int where it >= 0 && it <= 10
fn small() -> Result<Small, Violation> { Untrusted.validate(Untrusted.of(1)) }V5002 refinement_checked_at_runtime (retired)
Retired (design §17.87, §12.3): never reported.
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).