Patterns

Patterns appear in match arms, let bindings, function parameters, if let, while let, and for.

Simple patterns

Pattern	Matches
`42`, `"str"`, `true`, `'c'`	exact literal
`x`, `name`	binds the value
`_`	anything, no binding
`..`	rest (in tuples / arrays / records)
`mut x`	binds and marks as mutable
`ref x`	binds a reference instead of moving — but see the note below for record variants

danger

ref mut into a RECORD variant loses the write, silently

Checked on the interpreter. Three forms in one program, one run:

type Tup is One(Int) | Two;
type Sum is Pair { x: Int, y: Int } | Nil;
type Rec is { a: Int };

let mut t = Tup.One(1);
match t { Tup.One(ref mut v) => { *v = *v + 2; }, _ => {} }   // tuple=3   works

let mut r = Rec { a: 1 };
r.a = r.a + 2;                                                // struct=3  works

let mut s = Sum.Pair { x: 1, y: 0 };
match s { Sum.Pair { x: ref mut xv, .. } => { *xv = *xv + 2; }, _ => {} }
                                                              // sum=1     LOST

A ref mut binding into a TUPLE variant writes through. The same binding into a RECORD variant does not, and nothing says so: the programme exits 0 and the field keeps its old value. The near-identical form standing next to it is what makes this dangerous — the difference between the two is not visible from the call site, the type, or the diagnostic.

The other spellings do not rescue it, and which way each one fails depends on how the value was matched. The cases below use Int fields; the expected answer for each is 3:

What you write	Matched as	Result
`x = x + n`	`match s` (by value)	refused — `cannot assign to immutable variable: x`
`x = x + n`	`match &mut s` (local)	refused — same message
`x = x + n`	`match &mut self.field`	compiles, prints `1` — the write is lost
`x = x + n`	`match s` (by value)	compiles, prints `1` — the write is lost
`{ x: ref mut xv }`, `xv = xv + n`	`match s` (by value)	compiles, prints `1` — the write is lost

So a reader gets a refusal or a silent loss depending on a detail of the match header, and the two forms that lose are the two that look most like the ones that work. The refusal is not a type error either — it arrives from code generation (VBC codegen error (user bodies)), which is why it has no error code to look up.

Only the record-variant case behaves this way: the same ref mut write into a TUPLE variant (Tup.One(ref mut v)) writes through correctly.

What works today is rebuilding the variant — and the borrow matters, so both spellings below are the ones that were actually run:

// Match BY VALUE. `match &s { … s = … }` does NOT compile:
// error<E310>: cannot borrow `s` as mutable because it is already
// borrowed as immutable.
match s {
    Sum.Pair { x, y } => { s = Sum.Pair { x: x + 2, y: y }; },
    _ => {},
}

// Or compute first and assign after, which keeps the `&`:
let next = match &s {
    Sum.Pair { x, y } => Sum.Pair { x: x + 2, y: y },
    _ => Sum.Nil,
};
s = next;

Inside a method the &-form DOES work on self, and that asymmetry is worth knowing before you copy code between the two places:

implement Holder {
    public fn bump(&mut self, n: Int) {
        match &self.s {                                   // works: C sum=3
            Sum.Pair { x, y } => { self.s = Sum.Pair { x: x + n, y: y }; },
            _ => {},
        }
    }
}

The same shape on a LOCAL holder is refused:

let mut h = Holder { s: Sum.Pair { x: 1, y: 0 } };
match &h.s {                                              // error<E310>
    Sum.Pair { x, y } => { h.s = Sum.Pair { x: x + 2, y: y }; },
    _ => {},
}

Both were run. So a snippet lifted out of a method into a fn main stops compiling, and one lifted the other way starts — with no change to the pattern itself.

Until this is fixed, treat a record variant as immutable-through-patterns and rebuild it.

Tuples and arrays

match point {
    (0, 0)       => "origin",
    (0, _)       => "on y-axis",
    (_, 0)       => "on x-axis",
    (x, y) if x == y => "diagonal",
    _            => "elsewhere",
}

match items {
    []             => "empty",
    [only]         => f"one: {only}",
    [first, ..]    => f"first is {first}",
    [first, .., last] => f"{first}..{last}",
}

Records

match user {
    User { age: 0..18, .. }           => "minor",
    User { email, age: 18..=120, .. } => f"adult: {email}",
    User { .. }                       => "other",
}

// Also available: field shorthand
let User { id, email, .. } = user;

Variants

match shape {
    Shape.Circle   { radius }       => 3.14 * radius * radius,
    Shape.Square   { side }         => side * side,
    Shape.Triangle (a, b, c)        => heron(a, b, c),
}

Ranges

match code {
    0..100     => "low",
    100..=999  => "mid",
    _          => "high",
}

.. is exclusive; ..= is inclusive.

Or-patterns

match event {
    Key.Up | Key.W     => move_up(),
    Key.Down | Key.S   => move_down(),
    Key.Q | Key.Escape => quit(),
    _ => (),
}

And-patterns

match value {
    (x & 1..100) => ...,   // x bound, constrained to [1, 100)
}

Guards

Arbitrary boolean expressions extending a pattern:

match n {
    x if x < 0        => "negative",
    0                  => "zero",
    x if x.is_prime() => "prime",
    _                 => "composite",
}

// `where` is a synonym for guard:
match xs {
    [x, ..] where x > 0 => ...,
}

Type tests

match value {
    x is Int   => process_int(x),
    x is Text  => process_text(x),
    _          => reject(),
}

x is T is a pattern that matches values of the compile-time type T and narrows the binding. It also exists as an expression for boolean predicates:

if value is Maybe.Some(x) && x > 0 { ... }

Reference patterns

match &pair {
    &(a, b)      => ...,     // dereference then destructure
    &(ref a, _)  => ...,     // keep `a` as a reference
}

Active patterns

Active patterns are named, user-defined matchers. They come in two flavours:

Total (boolean return)

fn is_even(n: Int) -> Bool { n % 2 == 0 }
pattern Even(n: Int) -> Bool = is_even(n);

match n {
    Even()  => "even",
    _       => "odd",
}

Partial (`Maybe` return — extracts a value)

fn parse_int(s: Text) -> Maybe<Int> { ... }
pattern ParseInt(n: Int)(s: Text) = parse_int(s);

match input {
    ParseInt(n) => f"got {n}",
    _           => "not a number",
}

Rest

.. skips fields or elements:

let Point { x, .. } = p;              // ignore other fields
let [first, .., last] = xs;           // first and last, ignore middle
match tuple { (a, _, _, d) => ..., }  // position-based (for tuples)

Exhaustiveness

match is exhaustive by default — that's the design intent. This section's transcript has been removed, not corrected, because the underlying claim is currently an open question, confirmed two independent ways today: a match on a 5-variant sum type with one variant's arm omitted and no wildcard, checked with both verum check and verum verify, compiled/verified clean with no diagnostic at all — no missing-arm error, on either entry point. Until that's resolved, don't rely on this page's specific claim that omitting an arm is caught.

How exhaustiveness is decided

Each arm becomes a row in a coverage matrix; each column corresponds to one component of the scrutinee. The algorithm asks two questions:

Is every value reachable? — for each constructor of the scrutinee type, check that some row covers it. Missing constructors produce E0601.
Is every arm useful? — a later row is useful only if it matches something none of the earlier rows do. Redundant rows produce W0602 unreachable pattern.

Coverage for each pattern kind:

Pattern kind	Treatment
Wildcard / identifier	Covers everything (terminates analysis)
Literal	Covers exactly one value
Variant / record / tuple	Recursive: product or sum decomposition
Range	Interval arithmetic — gaps and overlaps detected
Or	Union of alternatives
And	Conservative intersection (more restrictive than either)
Guard	Conservative — treated as may fail
Active (`Bool`)	Conservative, like a guard
Active (`Maybe<T>`)	Constructor match, like `Some/None`
Active (variant-returning)	Full exhaustiveness on return variants
TypeTest (`x is T`)	Coverage over the tested type's variants
Stream	Nil / single / two-or-more cases

Guards never prove exhaustiveness (by default)

Because a guard can evaluate to false, a match whose arms are all guarded is not exhaustive:

match n {
    x if x > 0 => positive(),
    x if x < 0 => negative(),
    // E0601: `0` not covered — both guards are false for x == 0
}

Add an unguarded arm (0 => zero() or _ => other()) to close the match.

Guard verification with SMT

Opt in to SMT verification of boolean/arithmetic guards with @verify(exhaustiveness):

@verify(exhaustiveness)
fn classify(n: Int) -> Text {
    match n {
        x if x > 0   => "pos",
        x if x < 0   => "neg",
        x if x == 0  => "zero",   // SMT proves the three guards partition Int
    }
}

The solver proves (or refutes) that the guard disjunction covers the scrutinee type. Unprovable cases degrade to W0603 match with all guarded patterns (may fail) rather than silently passing.

Variant-returning active patterns

A custom active pattern that returns a sum type lets the compiler prove exhaustiveness even though the match looks user-defined:

type Parity is Even | Odd;
pattern Parity(n: Int) -> Parity =
    if n % 2 == 0 { Parity.Even } else { Parity.Odd };

match Parity(x) {
    Parity.Even => "even",
    Parity.Odd  => "odd",   // proven exhaustive — no wildcard needed
}

Range overlap detection

Overlapping ranges trigger W0606, and the compiler suggests a partition:

warning[W0606]: range patterns `1..=10` and `5..=15` overlap in `5..=10`
  --> src/main.vr:12:9
   |
11 |         1..=10  => "low",
12 |         5..=15  => "medium",
   |         ^^^^^^^
   |
   = help: consider non-overlapping ranges: 1..=4, 5..=10, 11..=15

Error and warning codes

Code	Severity	Meaning
E0601	error	non-exhaustive pattern match
W0602	warning	unreachable pattern
W0603	warning	all arms guarded — match may fail
E0604	error	invalid pattern for the scrutinee's type
W0605	warning	`is T` on a concrete type (redundant)
W0606	warning	overlapping range patterns
W0607	warning	range fully covered by earlier arms

Configuration knobs

The exhaustiveness checker exposes four config surfaces; every documented field on each is honoured by the consumer (no inert defenses). The user-facing contract is "set the field, observe the difference". The main ExhaustivenessConfig and the dependent-pattern variant share the same emission semantics — toggling warn_all_guarded or max_witnesses produces identical observable effects regardless of which checker the orchestrator routes through.

`ExhaustivenessConfig` (main path)

Field	Default	What it gates
`max_witnesses`	`3`	Truncates the uncovered-cases enumeration after the standard / refinement-aware check fills the list. `0` means "unlimited"; any positive value caps the enumeration to bound the diagnostic size on cardinality-exploding scrutinees.
`check_redundancy`	`true`	Toggles the redundancy pass over the matrix.
`warn_all_guarded`	`true`	When every pattern in a non-empty match carries a guard, emits the W0603 `AllGuarded` warning into the result's `warnings` list.
`use_refinement`	`true`	Routes refined types (`Int{x: x > 0}` etc.) through the refinement-aware analysis that eliminates impossible cases.
`use_smt_guards`	`false`	Master switch over the SMT-backed guard verification path. The path also requires `guard_verifier` to be `Some` (callers inject from `verum_smt::exhaustiveness_backend::SmtGuardVerifier`).
`smt_timeout_ms`	`100`	Forwarded into `SmtGuardConfig.timeout_ms` when the SMT path runs.
`guard_verifier`	`None`	Optional injected `&dyn GuardVerifier`. The trait lives in `verum_types`; concrete adapter implementations live in `verum_smt`.

`CacheConfig`

Field	Default	What it gates
`max_entries`	`10_000`	LRU-style eviction trigger.
`max_age`	`5 min`	Per-entry expiration before re-computation.
`enable_structural_cache`	`true`	Master switch. When `false`, `get` is miss-only and `put` is a no-op — useful for correctness pinning or debugging cache invariants.
`track_type_definitions`	`true`	Hash type definitions into the cache key so re-defining a type invalidates dependent entries.

`DependentExhaustivenessConfig`

Field	Default	What it gates
`max_witnesses`	`3`	Caps the number of uncovered cases enumerated.
`check_redundancy`	`true`	Toggles the redundancy pass over the matrix.
`warn_all_guarded`	`true`	Emits the W0603 `AllGuarded` diagnostic when every pattern carries a guard. Surfaced via `warn_all_guarded_enabled()`.
`use_smt_for_guards`	`false`	Surfaced via `use_smt_for_guards_enabled()`. Downstream orchestrators that wrap the checker with an `SmtGuardVerifier` (from `verum_smt`) consult this to decide whether to feed guarded patterns through SMT before declaring the match exhaustive.
`track_index_refinements`	`true`	Phase 4 (compute per-pattern index refinements).

`SmtGuardConfig` (verum_types interface, verum_smt implementation)

Field	Default	What it gates
`timeout_ms`	`100`	Per-query timeout forwarded to the active solver adapter.
`max_guards`	`10`	Skips SMT analysis when guard count exceeds this — falls back to the syntactic-only verdict with `skipped: true`.
`extract_witnesses`	`true`	Whether SAT counterexamples are surfaced as `SmtWitness` entries.
`detect_redundancy`	`true`	Whether the redundancy pass runs alongside coverage.

Witness generation

For every non-exhaustive match, the compiler is designed to produce a concrete example of an uncovered value — not just "incomplete." As noted above, exhaustiveness checking itself did not fire in direct testing today, so this section's witness-format example has been removed along with the other one rather than left showing output from a check that currently doesn't run.

The IDE surfaces the witness in real time through the LSP.

Performance

The usefulness algorithm is O(n²) typical and memoised across match expressions via an LRU cache. Target budgets: under 10 ms for typical matches, under 100 ms for deeply-nested ones with dozens of or-patterns.

Irrefutable patterns

In let and function parameters, the pattern must match every value of the type (irrefutable). Point { x, y } is irrefutable (records have only one shape); Shape.Circle { .. } is not (it is one variant of several).

Simple patterns​

Tuples and arrays​

Records​

Variants​

Ranges​

Or-patterns​

And-patterns​

Guards​

Type tests​

Reference patterns​

Active patterns​

Total (boolean return)​

Partial (Maybe return — extracts a value)​

Rest​

Exhaustiveness​

How exhaustiveness is decided​

Guards never prove exhaustiveness (by default)​

Guard verification with SMT​

Variant-returning active patterns​

Range overlap detection​

Error and warning codes​

Configuration knobs​

ExhaustivenessConfig (main path)​

CacheConfig​

DependentExhaustivenessConfig​

SmtGuardConfig (verum_types interface, verum_smt implementation)​

Witness generation​

Performance​

Irrefutable patterns​

See also​