What must be true of the ticket-state type before a compiler can prove a match over it is exhaustive?

## Exhaustiveness is a subtraction The check a compiler performs is arithmetic on sets: take the variants the matched type can hold, remove every variant some listed pattern covers, and demand that the remainder be empty. Everything a type must provide follows from that one sentence. There has to be a **set**, it has to be **finite**, and it has to be **known to the compiler at the match site**. A type that supplies all three is called **closed**. ## What "closed" means in practice - The **complete list of variants is declared in one place**, alongside the type itself, rather than accumulated from wherever someone happened to add one. - **Nothing outside that declaration may add a variant.** If another module — or another team's library, compiled separately — could introduce a fifth ticket state, no match anywhere could ever be proved complete, because the compiler would be reasoning about a set it cannot see all of. - The set is fixed **when the program is compiled**, not when it runs. Loading something later that claims to be a new state does not extend it; a value must be one of the declared variants to be a value of that type at all. - Being closed says nothing about how *many* variants there are. Four is closed, forty is closed. Finiteness, not smallness, is the requirement. The pay-off is that the compiler can answer a question about the *whole program* from one declaration: "which shapes can this value have?" No analysis of who constructs the value, and no scan of call sites, is involved. ## Domains with nothing enumerable in them Not every value has a variant set. A ticket's priority as a number, its title as text, or its identifier as an opaque key all live in domains far too large to list. A match on three specific numbers leaves an enormous uncovered remainder, and no amount of typing shrinks it to nothing, so such a match needs a case that matches whatever is left. That case is not a lapse of discipline — it is the only way to be total over a domain the compiler cannot enumerate, and it is a good reason to model a lifecycle as a closed set of variants rather than as a number or a string in the first place. | What is being matched | Can it be proved exhaustive without an all-matching case? | |---|---| | A closed set of four ticket states | Yes — the remainder is computable and can be driven to empty | | A type that any module may extend with new variants | No — there is no complete set to enumerate | | A numeric priority over an unbounded range | No — a finite list of literals always leaves a remainder | | A pair of two values from closed sets | Yes — completeness is judged over the combinations | | Text read from storage, before it is decoded | No — it is not yet a variant of anything | ## The static type at the match site A subtle failure: the analysis uses the type the value is **declared** to have where the match appears, not the type it was originally constructed as. If a ticket state is widened to some broader type before being matched — passed through a parameter or a field declared more generally — the compiler enumerates the variants of *that* type. The set may be larger, or may not be closed at all, and a match that felt complete stops being provable. The habit worth forming is to keep the closed type all the way to the match rather than losing it somewhere in the middle of the call chain. ## Nested values and conditioned cases Two refinements come up as soon as the patterns get more interesting than one variant name: 1. **Nested patterns need nested closure.** Matching a pair of ticket states means the compiler is enumerating combinations — with four variants on each side, sixteen of them. A pattern that fixes one side and leaves the other unconstrained covers the four combinations underneath it. If either side is drawn from an open or unbounded domain, the pair cannot be proved complete however the outer patterns are written. 2. **A case conditioned on a run-time test does not count as coverage.** If a case matches a variant only when some extra condition holds, the compiler has no way to prove the condition holds, so the variant is still treated as potentially uncovered. That is not a defect in the check — it is the check declining to assert something it cannot prove. ## Why the precondition is the interview question Candidates who have only used the feature describe the error message. Candidates who understand it describe the property that makes the error message possible, and can therefore predict when it will not appear: an extensible type, a widened value, an unbounded domain, a guarded case. That prediction is the difference between relying on the compiler and hoping for it.