Type Designspec

Exhaustiveness Checking

The compiler proves that every variant is handled, and reports a concrete value if one is not. This is the payoff that makes sum types worth having — and the reason adding a variant is a breaking change.

The question

How do I make the compiler tell me every place I need to update when I add a variant?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute

What the program is here

The set of values of the scrutinee type minus the set covered by the arms written so far, computed as a *usefulness* judgement over pattern matrices. If the remainder is non-empty the checker constructs a witness — a concrete value that no arm accepts — and that witness, not a yes/no answer, is what makes the diagnostic actionable.

What this phase may assume or do

The check is sound only where the variant set is closed at the point of the match. Across a module or crate boundary that closedness is a promise the type's author makes and can withdraw: #[non_exhaustive] in Rust, an unsealed hierarchy in Java or Scala, a wire format that may carry unknown tags. Where the promise is withdrawn, the compiler must require a wildcard arm — so the strength of the check is exactly the strength of the module system's guarantee, never more.

Key points

Exhaustiveness checking turns "find everywhere affected by this change" from a search into a compiler-produced list.
It is computed as a usefulness query over a pattern matrix, and the useful output is the witness value, not the yes/no answer.
The same analysis produces unreachable-arm warnings, which is why the two diagnostics always ship together.
The check is sound only while the variant set is closed; a non-exhaustive marker, an unsealed hierarchy or a wire format withdraws that.
TypeScript gets the check through the empty type plus flow narrowing — opt-in per site, and defeated by any any upstream.
The cost is that adding a variant breaks every exhaustive consumer, which makes it a major version change across a published boundary.
The common silent failure is a team fixing fifty exhaustiveness errors with fifty wildcards, permanently disabling the check at every one of them.

The payoff that justifies sum types

A sum type on its own is a tagged record. What makes it worth the ceremony is that the compiler knows the variant set is closed, and can therefore answer a question no other construct allows: have you handled all of them? Add a variant, rebuild, and every incomplete match in the program becomes an error with a file and a line. That is the mechanism, and it is the only widely available mechanism that turns "find every place affected by this change" from a grep into a proof.

The value is not in the first write. Writing three arms for three variants is easy either way. The value arrives eighteen months later, when a fourth variant is added by someone who has never seen most of the code that consumes it, and the compiler produces the list. Nothing else in mainstream tooling does this: tests only find the paths they exercise, and a search for the type name finds the sites that mention it, not the sites that switch on it.

The check is also what makes the closed-set design defensible. Closing the variant set costs you extensibility — third parties cannot add cases. You accept that cost specifically to buy this proof, and if the language does not perform the check you have paid the cost and received nothing, which is the situation Python's match is in.

Adding a variant produces the work list

1enum Event { Click(Point), Key(char) }
2 
3fn handle(e: Event) -> Action {
4    match e {
5        Event::Click(p) => Action::Focus(p),
6        Event::Key(c)   => Action::Insert(c),
7    }
8}
9 
10// Someone adds a variant:
11enum Event { Click(Point), Key(char), Scroll(f64) }
12 
13// error[E0004]: non-exhaustive patterns: `Event::Scroll(_)` not covered
14//   --> src/input.rs:14:11
15//    = note: the matched value is of type `Event`
16//    help: ensure the match is exhaustive by adding an arm

The error names the *witness* — Event::Scroll(_) — not just "some case is missing". A checker that reports only a boolean is far less useful, because the engineer then has to work out which case, and for a nested pattern that is genuinely hard.

How it is computed: usefulness, and witnesses

implementationMaranget's usefulness algorithm is what rustc, OCaml and GHC's newer checker are built on, with different extensions: rustc handles integer and slice ranges by splitting into constructor sets, GHC's lower-bound checker handles guards and strictness via a separate constraint solver, and OCaml handles or-patterns by expansion. The witnesses each prints therefore differ in form, and none of the three is required by a specification to print anything in particular.

The algorithm most implementations use is Maranget's: arrange the arms as a matrix of patterns and ask, for a candidate pattern vector, whether it is *useful* with respect to the matrix — whether there is a value it matches that no row matches. Exhaustiveness is then a single query: is the wildcard vector useful against the whole matrix? If yes, the value witnessing that usefulness is a value nothing covers, and the checker prints it.

The same query answers reachability. An arm is unreachable exactly when its pattern is not useful with respect to the arms above it, which is why the two diagnostics come from one implementation and why languages tend to ship them together.

The algorithm is worst-case exponential in the depth and width of the patterns, which is why implementations bound it: rustc has a recursion limit and OCaml gives up on very large matrices with a note rather than an answer. In practice human-written matches are far below any of those bounds, and the cost is not visible in build times.

The interesting part is the witness construction, because it is what makes the feature usable rather than merely correct. Constructing "some uncovered value exists" is easy; constructing a readable representative of it — Some(Ok(Point { x: 0, .. })) rather than a set description — takes real work in the compiler, and is the difference between a diagnostic that fixes itself and one that starts an investigation.

The `never` trick, and getting the check in a language that lacks it

implementationThe never idiom depends on TypeScript's discriminant narrowing reaching never in the default branch, which requires strictNullChecks and a discriminant of literal-union type. It reports nothing under any, nothing when the union is widened by a library boundary, and nothing at all in a switch where somebody forgot to add the default. Java's sealed-type switch and Rust's match check every site by construction and need no idiom — which is the substantive difference, not the syntax.

TypeScript has no exhaustive match, but it has an empty type and a flow-sensitive checker, and those two together are enough. Inside a switch on a discriminant, after every declared case has been handled, the narrowed type of the scrutinee in the default branch is never — because no member remains. Assigning that value to a variable declared never therefore succeeds. Add a variant, and the default branch now narrows to the new member, which is not assignable to never, and the assignment fails with an error that names the member.

This is a genuinely good use of an uninhabited type and it is worth understanding rather than copying, because the same idea works anywhere the checker has an empty type and flow narrowing. It also has real limitations. It is opt-in per site: a switch without the assertion is not checked, so the guarantee is only as good as the team's discipline plus a lint rule. It runs in the default branch, so the code has to have one. And it is defeated entirely by an any upstream, since narrowing an any produces any — which is the hole [[gradual-typing]] is about.

Java and Scala reach the check the other way, through sealing. A sealed interface names its permitted implementations, which closes the set, and a switch over a sealed type is then checked by the compiler with no idiom required. C# checks where it can prove a hierarchy is closed and warns rather than errors. The trade in every case is the same: closedness in exchange for the proof.

The `never` idiom, and where it stops working

1type Shape =
2  | { kind: "circle"; r: number }
3  | { kind: "rect"; w: number; h: number }
4 
5function assertNever(x: never): never {
6  throw new Error("unhandled variant: " + JSON.stringify(x))
7}
8 
9function area(s: Shape): number {
10  switch (s.kind) {
11    case "circle": return Math.PI * s.r ** 2
12    case "rect":   return s.w * s.h
13    default:       return assertNever(s)
14    // add a third member and this line errors:
15    //   Argument of type "{ kind: "tri"; ... }" is not assignable to parameter of type "never"
16  }
17}
18 
19// Defeated by any upstream:
20function areaUnsafe(s: any) {
21  switch (s.kind) { /* ... */ default: return assertNever(s) }  // `any` narrows to `any`; no error, ever
22}

The runtime throw is deliberate and is the second half of the idiom: the compile-time check covers the code you compiled, and the throw covers the value that arrived from JSON, from a wire format, or from a differently versioned module.

The cost: adding a variant is a breaking change

The check has a price and it is not small. If every consumer of your type has an exhaustive match, then adding a variant breaks every consumer. Inside one codebase that is the feature: the build turns red and you fix the sites. Across a published API boundary it is a semver-major change, which means a library cannot add a variant to a public enum without a major release, and a protocol cannot add a message kind without breaking every strict client.

Rust's answer is #[non_exhaustive]: an attribute on a public enum that tells downstream crates the variant set may grow, forcing every external match to carry a wildcard arm. It converts the guarantee into a boundary-crossing decision — inside the defining crate the check still applies in full, outside it does not. Java's sealed interface with a permits clause makes the same decision in the other direction, by opting *in* to closedness. Protocol buffers take the third route: unknown enum values are preserved as an opaque number rather than rejected, so a new variant is forward-compatible by design and no client can ever be exhaustive.

The failure mode this creates is worth naming, because it is common and it is silent. A team adds a variant, gets fifty compile errors, and fixes all fifty by adding _ => {} or default: break. The build is green, the check has been permanently disabled at fifty sites, and the new variant is unhandled everywhere. The wildcard was the right answer at some of those sites and the wrong answer at most of them, and nothing distinguishes them afterwards.

The defensible discipline is to treat a wildcard arm as a decision that needs a reason, not as a way to satisfy the compiler. Where the reason is "this code genuinely does not care about the variant", say so — many codebases lint for a bare _ => and require either an explicit list or a comment.

What each language does about the breaking-change problemimplementation

Mechanism	Default for a public type	What a consumer must write	What it costs
Rust `enum`spec	Closed. Exhaustive matching enforced everywhere.	Every variant, or a wildcard.	Adding a variant is semver-major.
Rust `#[non_exhaustive]`implementation	Open to other crates, closed within the defining crate.	A wildcard arm, always.	External consumers lose the check entirely.
Java `sealed` + `permits`spec	Open unless sealed; sealing is opt-in.	Every permitted type, in a switch.	The permitted list is part of the public API.
Scala 3 `enum` / `sealed`implementation	Closed within the file.	Every case, or accept a warning.	Warning rather than error, so it is easy to ignore.
TypeScript union + `never`implementation	Closed by declaration; unchecked unless the idiom is used.	Nothing, unless the site opted in.	Per-site opt-in; an `any` upstream disables it silently.
Protobuf enumspec	Open by design; unknown values are preserved.	A default case.	No exhaustiveness is ever possible, by construction.

How it works

The steps, in the order the compiler takes them.

The arms are collected into a matrix, one row per pattern, one column per position in the scrutinee.
The usefulness query asks whether a candidate vector matches some value that no row matches; it recurses by specialising the matrix on each constructor of the type at the first column.
Exhaustiveness is the usefulness of the all-wildcard vector against the whole matrix; reachability of arm *i* is the usefulness of row *i* against rows 1..i-1.
Where the query succeeds, the recursion is unwound to build a concrete witness value, filling wildcards with a representative constructor at each position.
Integer, character and slice patterns are handled by splitting the value space into ranges rather than enumerating it, so the algorithm stays finite over large primitive types.
Guards are excluded from the matrix entirely: a guarded arm contributes nothing to coverage, because the checker cannot decide its condition.
A type marked non-exhaustive at a module boundary is treated as having an additional unnameable constructor from outside, which is exactly what forces the wildcard.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

A variant is added, fifty matches fail, the team adds a wildcard to each, and the new variant silently does nothing in every one of them — the feature ships half-implemented with a green build.
A switch in TypeScript has no assertNever call, so adding a union member produces no error anywhere; the new case falls through to a default that returns a plausible wrong value.
The scrutinee is any because it came from JSON.parse, narrowing produces any, the never assertion accepts it, and a completely unknown variant reaches the default branch at runtime with the check reporting success at compile time.
A library adds a variant to a public enum in a minor release; downstream builds break, and the maintainer is told the change was additive.
A protocol adds a message kind, a strict client rejects the unknown tag, and a partial rollout produces errors only on the mixed-version path — visible as a small percentage of failures that disappears when the rollout completes.
An exhaustiveness warning is a warning rather than an error, accumulates to four hundred instances, and stops being read.

When it helps

Refactoring a data model in a large codebase: adding, splitting or renaming a variant produces the exact list of sites needing attention.
Reviewing a change that adds a case, where the reviewer can ask the compiler rather than the author whether everything was handled.
State machines and protocol handlers, where the cost of an unhandled transition is a stuck or corrupted session rather than a visible crash.
Long-lived code with high staff turnover, where nobody has the whole consumer set in their head and the compiler is the only thing that does.

When it hurts

Across a published API boundary, where it converts an additive change into a major version bump for every consumer.
At a deserialization boundary, where the closed-set assumption is simply false — a wire value can be anything, and a match that assumes otherwise is a crash rather than a check.
When the diagnostic arrives in overwhelming volume. Fifty simultaneous errors reliably produce fifty wildcards, which is worse than no check at all because it looks like one.
In a language where it is a warning: warnings that number in the hundreds are indistinguishable from no warnings.

What it costs

Every one of these is paid by something.

The proof costs extensibility. Closing the variant set is what makes the check possible, and it is also what stops a third party adding a case — you cannot have both, and languages that try end up with a check that holds only inside one compilation boundary.
The check buys a complete work list and pays in change amplification: a one-line addition to a type produces edits in every consumer, which is exactly the intended behaviour and is genuinely expensive on a large codebase.
Escape hatches (#[non_exhaustive], an unsealed hierarchy, a wildcard) buy evolution and pay by silently converting a compile-time guarantee into a runtime assumption at every site that uses them.
A high-quality witness diagnostic buys a self-fixing error and pays in compiler implementation: constructing a readable representative value for a deeply nested uncovered case is substantially harder than deciding that one exists.

What else you could do

What a different compiler or language does instead, and when that is better.

A runtime assertion in the default branch — the assertNever throw — catches what the compiler cannot see, including values from JSON and from differently versioned modules. Weaker (it fires in production) and strictly complementary rather than an alternative.
Virtual dispatch removes the need for the check entirely: with a method per variant, adding a variant means implementing the method and the compiler enforces that instead. Correct when operations are stable and variants grow, which is the opposite of when matching is correct.
Open enums with a preserved unknown value (protobuf, most wire formats) give forward compatibility and give up exhaustiveness by design — the right trade at a protocol boundary where old clients must survive new messages.
A lint rule that forbids bare wildcard arms recovers much of the check in a language whose compiler will not do it, at the cost of being advisory and of needing a suppression mechanism that people will use.

See it for yourself

The flag, dump or tool that shows you this directly.

rustc emits E0004 with a witness; add #![deny(unreachable_patterns)] to make the sibling reachability warning an error too.
ghc -Wincomplete-patterns -Wincomplete-uni-patterns -Werror=incomplete-patterns — GHC does not enable these by default, so a Haskell codebase without them in its cabal file is not being checked.
ocamlc -w +8 -warn-error +8 turns the partial-match warning into an error and prints an uncovered value.
javac with a sealed interface and a switch expression reports a missing case as an error with no flag required; the same switch over an unsealed type reports nothing.
For TypeScript, the check exists only where you wrote it. grep for switch (.*\.kind) and compare against grep for assertNever — the difference is the set of unchecked sites, and that comparison is worth running once on any codebase that believes it has exhaustiveness.

Plausible wrong readings

Stated the way a confident engineer states them.

"The compiler checks my switches are complete." It checks the ones it can, over closed sets, in languages that do it. In TypeScript it checks the ones where you asked; in Python it checks none.
"Adding an enum variant is a backwards-compatible change." It breaks every exhaustive consumer, which is the check working. Treating it as additive is how libraries break downstream builds in minor releases.
"A wildcard arm is a reasonable default." It is the off switch for this feature at that site. Sometimes correct, never automatic, and a bare _ => {} added to silence an error is almost always the wrong one.
"Exhaustiveness means the code handles every case correctly." It means every case is mentioned. An arm that returns a wrong value passes the check exactly as well as one that returns the right one.

Misconceptions

The claim, and what is actually true.

Exhaustiveness checking is a linter feature.

Where it exists as a type-system rule (Rust, sealed Java, sealed Scala) it is part of what makes the sum type sound to compile as a closed set. A linter cannot see across the module boundary the same way, and cannot be relied on by the code generator.

If I add a default branch, nothing changes.

You have removed the check at that site permanently and silently. The next variant added will be handled by your default, which is almost never what the default was written to do.

The check protects against bad data at runtime.

It reasons about the types the compiler saw. A value from JSON, a wire format or a differently versioned module can carry a tag the compiler never heard of, which is why the runtime assertion in the default branch is part of the idiom rather than belt-and-braces.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

If a type has a fixed set of variants, the compiler can check that a match handles all of them and refuse to compile if it does not — naming the one you missed. That is what makes sum types pay for themselves: when someone adds a variant a year later, the build produces the exact list of places that need updating.

practical

In Rust, Java (sealed) and Scala you get it for free; in TypeScript you have to ask, with a default branch that passes the scrutinee to a function taking never. Wherever you have it, the discipline that matters is what you do when it fires en masse: adding a wildcard to every failing site turns the check off at every one of them. Fix the ones that need fixing, and where a wildcard is genuinely right, write down why. And keep a runtime throw in the default branch regardless — the compile-time check does not extend to values that arrived as JSON.

advanced

The design question underneath this is where a language draws its closed-world boundary, and every answer is a different product. Rust draws it at the crate, with an explicit opt-out for public types. Java draws it at the permits clause, opt-in, which makes sealing an API design decision rather than a default. Protobuf refuses to draw one at all, because a wire protocol whose old clients reject new messages is unusable in a partial rollout — and that refusal is why no protobuf consumer can ever be exhaustive, no matter what the generated code looks like. The pattern generalises: exhaustiveness is available exactly where you control every consumer at build time, which means it is a language feature inside a binary and an architectural decision across a network.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

specThat Rust rejects a non-exhaustive match is a language rule, not a lint: it is E0004, an error, and cannot be downgraded. That GHC and OCaml report incomplete matches as *warnings* which are off or non-fatal by default is equally specified, and is why a Haskell codebase can contain hundreds of partial matches and still build cleanly. Check the flags before assuming a language "has" the check.

implementationThe never-assignment idiom relies on TypeScript narrowing the discriminated union to never in the default branch under strictNullChecks. It is disabled by an any anywhere upstream, by a union widened at a library boundary, and by the absence of the default clause. Java and Rust check every site with no idiom and no opt-in, which is a different guarantee with the same name.

implementationWitness quality varies enormously and is worth evaluating when choosing tooling: rustc prints a constructor-shaped value with .. elisions, GHC prints a value plus the constraints under which it is uncovered, and some checkers report only that the match is inexhaustive. The last is technically the same check and practically a different feature.

If you were asked this in an interview

What does exhaustiveness checking actually buy you, and at what point in a codebase's life does the benefit arrive?
Explain the never trick in TypeScript, and name two situations in which it silently fails to check anything.
Your library needs to add a variant to a public enum. What are your options and what does each cost a consumer?

Connections

Securityfail-open-vs-fail-closed input-validation

API Designenum-evolution versioning backward-compatibility removing-fields

Backenderror-taxonomy parse-dont-validate

Runtime gain1

Compile cost2

Debuggability3

Implementation4

Context dependence4

Nothing is emitted, so runtime gain is nil; the modest debuggability score reflects that an exhaustive match plus a witness-bearing error moves a class of defect from runtime to build time, which is a debugging benefit even though it is not a runtime one. Compile cost is low in practice despite a worst-case exponential algorithm, because real patterns are shallow. Implementation complexity is high: the usefulness algorithm must understand every pattern form the language has, and witness construction is harder than the decision itself. Context dependence is high because the guarantee is entirely a property of the module system — the same written match is checked, warned about, or ignored depending on the language.