Pattern Matching and the Exhaustiveness Check

A match expression is the one place where a language can prove something about a program’s control flow without running it. The compiler knows the shape of every constructor a value can take, so it can determine whether the arms cover all of them, and it can determine whether some arm can never be reached. Both checks are useful, and both depend on the same underlying machinery: the patterns are compiled into a decision tree, and the checks are properties of that tree.

Patterns are a small language of their own

A pattern describes a set of values. A literal pattern 0 describes the singleton set containing zero. A constructor pattern Some x describes every value built with Some, with x bound to the payload. A wildcard _ describes everything. A tuple pattern describes a product, and an or-pattern describes a union. A guard, if the language has them, adds a boolean condition evaluated after the pattern matches.

The set semantics are what make exhaustiveness meaningful. Exhaustiveness asks whether the union of the sets described by the arms covers the set described by the scrutinee’s type. Usefulness, the dual question, asks whether a given arm’s set contains any value not already covered by the arms before it. An arm that is not useful is unreachable.

Both questions are answered by the same algorithm, and the algorithm does not enumerate values. Enumerating is impossible for types with infinitely many inhabitants, such as integers or lists, and impractical for types with many constructors. The algorithm works on the pattern matrix instead.

The pattern matrix

Maranget’s formulation, which is the basis of the check in OCaml, Haskell’s GHC, and Rust, arranges the patterns into a matrix whose columns correspond to the scrutinee’s components and whose rows correspond to the arms. A match on a pair of values has two columns; a match on a list has one column and patterns that decompose it.

The algorithm proceeds by case analysis on the first column. It partitions the rows into those whose first pattern is a constructor c, those whose first pattern is a wildcard, and it recurses on each constructor’s submatrix. For a constructor c with arity k, the submatrix takes the k sub-patterns from the c rows and prepends them to the remaining columns; wildcard rows contribute k wildcards. The recursion terminates because each step consumes a column or a constructor layer.

Exhaustiveness is then a question about whether the recursive call on a constructor’s submatrix reports a missing pattern. The algorithm returns either “the matrix is exhaustive” or a witness: a concrete pattern that no row covers. A witness is far more useful than a boolean, because it can be printed in the diagnostic, and it is why good compilers say non-exhaustive patterns: None not covered rather than “match may fail”.

Usefulness is the same recursion with one row marked. The algorithm asks whether the marked row’s pattern intersects the complement of the preceding rows; if it does not, the arm is unreachable. Running the check for each arm separately repeats the recursion once per arm, which is what makes the reachability pass more expensive than the exhaustiveness pass.

Why guards break the guarantee

A guard is a boolean expression evaluated after the pattern matches. The compiler cannot in general decide whether a guard is true, so a guarded arm cannot be assumed to cover anything. The consequence is that a match with a guard is never exhaustive on the strength of that arm:

fn classify(value: Option<i32>) -> &'static str {
    match value {
        Some(x) if x > 0 => "positive",
        Some(_) => "non-positive",
        None => "absent",
    }
}

The first arm does not make the Some case covered, because the compiler does not know that some Some value satisfies x > 0. It knows only that the arm might apply. A match that consisted solely of a guarded arm and no fallback would be rejected as non-exhaustive, and the diagnostic would point at the missing case rather than at the guard.

This is a deliberate limit rather than a defect. Deciding whether a guard is satisfiable is undecidable in general, since guards can call arbitrary functions. Restricting guards to decidable fragments, such as comparisons against literals, would let the checker do more, at the cost of a rule that programmers would have to learn. Most languages choose the conservative rule: guards contribute nothing to coverage.

The rule has a second consequence for reachability. A guarded arm can never make a later arm unreachable, because the guard might fail. A later arm with the same pattern is therefore considered reachable, even though it is only reachable when the guard fails. That is correct and occasionally surprising.

Nested patterns and the cost of the tree

The decision tree that the compiler builds is also the implementation. Rather than testing each arm in source order, the compiler groups tests by constructor and shares the tests that several arms have in common. A match on a deeply nested structure is compiled into a tree whose depth is bounded by the nesting depth, and whose width is bounded by the number of distinct constructors at each level.

Sharing matters for performance. Two arms that both match Some(Some(x)) and Some(None) can share the outer Some test, so the outer tag is read once. A naive compilation that tests each arm in sequence would read the same tag repeatedly. The tree form is what makes matching cost proportional to the number of distinct paths rather than to the number of arms.

The tree is also why a match on a large enum can be compiled to a jump table. When every arm tests a tag against a distinct constant, the compiler can emit an indexed branch, which costs one indirect jump regardless of the number of arms. Languages with dense tag numbering make this easy; languages that allow arbitrary discriminants make it harder.

What exhaustiveness buys

The check converts a runtime failure into a compile-time one. A match on an enum with no wildcard is checked, and adding a constructor to the enum causes every non-exhaustive match to fail to compile. That is the property that makes enums useful for modelling states: the compiler enumerates the places that must be updated when a state is added.

The property depends on the enum being closed. A type that can be extended by another module, such as an open class hierarchy or an interface with unknown implementors, cannot be checked exhaustively, and a match on it needs a fallback. Languages that support both closed and open sums therefore have two kinds of match, and the distinction is visible in the type declaration rather than at the match site. That visibility is the design decision: a reader can tell from the type whether a wildcard arm is a completeness fallback or a silent default.

The second benefit is refactoring safety. Renaming a constructor or reordering the payload is caught by the same check, and a wildcard arm defeats it, because the wildcard accepts the new shape without complaint. This is the argument against wildcards in matches on closed types: the wildcard makes the match compile after a change that the programmer should have reviewed.

Where the check is weaker than it looks

Three gaps are worth knowing. The first is guards, described above. The second is integer ranges: a match on an int cannot be exhaustive without a wildcard, because the type has too many inhabitants, and a match on a u8 with 256 literal arms would be exhaustive in principle, though no compiler is required to accept it. The third is nested patterns whose type is not fully known at the match site, as with generic parameters or trait objects, where the set of possible constructors is not visible.

The fourth gap is more subtle: a match can be exhaustive and still fail at runtime if the pattern involves a dereference that the type system does not track. A pattern that matches a reference and then binds through it can panic if the reference is invalid, and the exhaustiveness check says nothing about that. The check is about the shape of the value, not about the validity of the memory it points to.

The check also interacts with the evaluation order of the arms. Because the first matching arm wins, an exhaustive match with overlapping patterns is still deterministic, and the usefulness check reports the overlap. A language that evaluated arms in an unspecified order would make the check meaningless, which is one reason match arms are always ordered.

The syntax that makes the check usable

The check is only useful if the source makes the covered cases visible. Languages differ in how much they require the programmer to spell out. A match that binds every field of a constructor can use a shorthand, and a match that ignores fields can use ... Both reduce the amount of syntax per arm, which matters when the point of the construct is to enumerate many cases.

The deeper interaction is with the type system’s notion of a closed set. In Short-Circuit Evaluation as a Language Guarantee, a test guards an expression and the guarantee is a runtime one. Here the same idea is static: the pattern is the test, and the exhaustiveness check is the proof that the test always succeeds. The two mechanisms are complementary, and a language that has both can choose which one to use at each site.

The compilation of the matrix into a tree is also where Expression-Oriented Syntax and the Value of a Block becomes relevant, because a match used as an expression must produce a value on every path, which is exactly the exhaustiveness condition restated as a typing rule. The two checks are the same check viewed from different sides.