# V5004 literal_violates_refinement

URL: /docs/errors/V5004
Markdown: /docs/errors/V5004.md

> 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:

```sakura
type Percent = Int where it >= 0 && it <= 100
let p: Percent = 150
```

Fixed:

```sakura
type Percent = Int where it >= 0 && it <= 100
let p: Percent = 50
```

## Wrong program [#wrong-program]

[`compiler/tests/ui/V5004_literal_violates_refinement.sakura`](https://github.com/icantcodefyi/sakuralang/blob/master/compiler/tests/ui/V5004_literal_violates_refinement.sakura), which the compiler's ui suite runs through `sakura check`:

```sakura
type Percent = Int where it >= 0 && it <= 100

let p: Percent = 150
```

`sakura check --json` reports this record (pretty-printed; `$DIR` is the fixture's directory):

```json
{
  "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 [#fixed-program]

[`compiler/tests/ui/V5004_literal_violates_refinement.fixed.sakura`](https://github.com/icantcodefyi/sakuralang/blob/master/compiler/tests/ui/V5004_literal_violates_refinement.fixed.sakura), which `sakura check` accepts with no diagnostics:

```sakura
type Percent = Int where it >= 0 && it <= 100

let p: Percent = 50
```