Home › Architecture Decisions › ADR 0106

ADR 0106: Opt-In Asserted match: Exhaustiveness (matchExhaustive:)

Status

Implemented (2026-07-07)

Context

Problem statement

ADR 0102 §4 (BT-2745) gave match: an advisory exhaustiveness check: when the type checker can prove a scrutinee is a closed union of #symbol singletons, it warns about any uncovered members. That ADR explicitly flagged a follow-up and left it out of scope:

Known discoverability cliff: the warning silently vanishes when inference widens the scrutinee (one Dynamic-returning arm, a reassignment) — the user cannot distinguish "exhaustive" from "checker gave up". An opt-in assertion (a marker on match: requesting exhaustiveness, analogous to TypeScript's satisfies never idiom, which would then diagnose "cannot verify: scrutinee is Dynamic") is the natural follow-up; deliberately out of scope here and left to a future issue so this ADR stays advisory-only.

This is that follow-up (BT-2763). The gap is real: a compass-direction match: that is exhaustive today can silently stop being checked the moment a helper function upstream starts returning Dynamic, or the variable is reassigned to a wider type — and nothing in the diagnostics output distinguishes "provably exhaustive" from "the checker gave up". Advisory warnings are the right default (ADR 0102 §4's reasoning — gradual typing, open-world FFI — still holds), but a developer who wants a hard guarantee at a specific match: site currently has no way to ask for one.

Current state

Constraints

Decision

Add matchExhaustive: as a second, parser-level keyword variant of match: that asserts — at Error severity — that the checker can prove the match is exhaustive.

direction :: #north | #south | #east | #west := readHeading

// Compile error: matchExhaustive: proves this is NOT exhaustive
direction matchExhaustive: [
  #north -> 0;
  #south -> 180;
  #east  -> 90
]
// ⛔ Error: non-exhaustive matchExhaustive: `#west` is not handled
//    (residual type: `#west`)

// Fine: all four members covered
direction matchExhaustive: [
  #north -> 0;
  #south -> 180;
  #east  -> 90;
  #west  -> 270
]

// Fine: an unguarded wildcard is still full coverage
direction matchExhaustive: [
  #north -> 0;
  _      -> -1
]

Surface syntax: a keyword variant of match:

matchExhaustive: parses exactly like match: — same arm syntax, same guards, same destructuring patterns — the parser's existing special case for match: followed by [ is extended to also recognise matchExhaustive:. The AST gains one field: Expression::Match now carries exhaustive: bool (true for matchExhaustive:, false for match:), threaded through unparse (round-trips the correct keyword) and through TypeChecker::infer_expr's Expression::Match arm, which now dispatches to one of two checks based on the flag. Every other AST consumer (codegen, lints, LSP queries, the BT-1299 pattern-based validator) pattern-matches Expression::Match { value, arms, .. } and is completely unaffected — the new field is inert everywhere except the one call site that reads it.

Behaviour when the scrutinee is not a closed singleton union

This is the case ADR 0102 §4 left undefined, and the reason this needs its own decision, not just a severity bump on the existing check. When matchExhaustive: is used and the scrutinee is not a known-closed #symbol-singleton union (Dynamic, a bare/open Symbol, a Negation co-finite set, a union with any non-singleton member, or an ordinary nominal type or union), the assertion fails loudly:

When the scrutinee is a closed singleton union, matchExhaustive: reuses BT-2745's residual computation (difference(scrutinee, covered)) verbatim, at Error severity instead of Warning, naming the uncovered members. A Never residual (fully covered, including via an unguarded wildcard or variable-binding arm — the same coverage rule as the advisory check) means the assertion holds, and — like a passing type check — is completely silent: no diagnostic at all.

Error examples

// Dynamic scrutinee — cannot verify, fails loudly
x matchExhaustive: [#ok -> 1; _ -> 0]
// ⛔ Error: cannot verify `matchExhaustive:` is exhaustive — scrutinee type
//    `Dynamic` is not a closed union of symbol singletons
//    hint: matchExhaustive: only proves exhaustiveness over a closed union
//    of `#symbol` singletons (e.g. `x :: #north | #south`). Annotate the
//    scrutinee with such a type, or use `match:` if exhaustiveness cannot
//    be guaranteed statically.

// Closed union, one member missing
status :: #ok | #error := checkStatus
status matchExhaustive: [#ok -> "done"]
// ⛔ Error: non-exhaustive matchExhaustive: `#error` is not handled
//    (residual type: `#error`)

Prior Art

LanguageApproachWhat we take / leave
TypeScriptconst _exhaustive: never = value; (the satisfies never idiom) — a value-level assertion computed from control-flow narrowing, reported as a type error at the assignment when the narrowed type isn't never.Adopt the spirit: opt-in, Error-severity, names what's left over. Diverge on mechanism: TS repurposes an assignment; Beamtalk has no structural narrowing-to-never to piggyback on, so a first-class keyword on match: itself is more legible and puts the assertion exactly where the claim is being made, not in a throwaway binding after the fact.
Rustmatch is exhaustive by default (compile error otherwise); #[non_exhaustive] opts a specific enum out.Inverted from Rust's default-strict model — Beamtalk stays default-advisory (ADR 0102 §4's reasoning: open-world, gradual typing, FFI can't be trusted) and offers strictness as an explicit per-site opt-in instead of a language-wide default.
Elixir/GleamNo opt-in assertion mechanism; Gleam's case is exhaustive by construction over closed nominal sum types (no gradual fallback needed).Confirms there's no direct prior art for a gradual language's opt-in exhaustiveness marker — this is genuinely new territory for the BEAM ecosystem, following ADR 0102's Elixir-inspired atom-set model rather than Gleam's nominal one.

User Impact

Steelman Analysis

Chosen: matchExhaustive: keyword variant

Rejected A: marker arm (e.g. a trailing exhaustive pseudo-pattern)

Rejected B: pragma/annotation prefix (@exhaustive x match: [...])

Rejected C: post-hoc assertion combinator ((x match: [...]) assertExhaustive)

Tension points

Purists (§Rejected B's newcomer voice) want annotation-style opt-in; Smalltalkers want a keyword message. The keyword-message answer wins because it needs no new grammar production — it is a second string compared in the same one if the parser already has for match:.

Alternatives Considered

See Steelman Analysis above — marker arm, pragma/annotation prefix, and a post-hoc combinator were all considered and rejected in favour of the keyword variant, for the reasons given there.

Consequences

Positive

Negative

Neutral

Implementation

References