Exhaustiveness/Redundancy Check
As stated in #595, GHC's overlapping/nonexhaustive pattern checking is old and crufty and misbehaves with several GHC's extensions, notably GADTs. In this page we describe the problem and the algorithm. It forms part of GHC 8.0.
Status
The ticket #11528 tracks our aspiration to return to a more elegant (but currently less performant) implementation.
Tickets should include PatternMatchWarnings
in their Keywords to appear in these summary lists.
Open Tickets:
#10116  Closed type families: Warn if it doesn't handle all cases 

#11195  New patternmatch check can be nonperformant 
#11253  Duplicate warnings for pattern guards and relevant features (e.g. View Patterns) 
#11503  TypeError woes (incl. pattern match checker) 
#11528  Representation of value set abstractions as trees causes performance issues 
#11822  Pattern match checker exceeded (2000000) iterations 
#12694  GHC HEAD no longer reports inaccessible code 
#12949  Pattern coverage checker ignores dictionary arguments 
#13021  Inaccessible RHS warning is confusing for users 
#13363  Wildcard patterns and COMPLETE sets can lead to misleading redundant patternmatch warnings 
#13717  Pattern synonym exhaustiveness checks don't play well with EmptyCase 
#13766  Confusing "redundant pattern match" in 8.0, no warning at all in 8.2 
#13964  Patternmatch warnings for datatypes with COMPLETE sets break abstraction 
#13965  COMPLETE sets nerf redundant patternmatch warnings 
#14059  COMPLETE sets don't work at all with data family instances 
#14133  COMPLETE pragmas seem to be ignored when using view patterns 
#14253  Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable 
#14838  missing "incompletepatterns" warning for THgenerated functions 
#14851  "Pattern match has inaccessible right hand side" with TypeRep 
#14899  Significant compilation time regression between 8.4 and HEAD due to coverage checking 
#14987  Memory usage exploding for complex pattern matching 
#15014  Exhaustivity check should suggest when COMPLETE could be helpful 
#15554  COMPLETE pragmas make overlappingpatterns warnings behave oddly 
#15681  Take exhaustiveness checking into consideration when using MonadFailDesugaring 
#15713  Bogus Woverlappingpatterns warning with OverloadedStrings 
#15744  Existence of complete pattern synonym hides unrelated incomplete pattern warning 
#15753  Inconsistent patternmatch warnings when using guards versus case expressions 
#15885  Enhancing COMPLETE pragma to support pattern synonyms with polymorphic (output) types 
#16128  Pattern match checker should shortcut on simple cases 
#16278  Exhaustivity checking GADT with free variables 
#16289  GHC thinks pattern match is exhaustive 
Closed Tickets:
#322  fromIntegerrelated pattern match overlap warnings 

#595  Overhaul GHC's overlapping/nonexhaustive pattern checking 
#2204  Improve 'patterns not matched' warnings 
#3927  Incomplete/overlapped pattern warnings + GADTs = inadequate 
#4139  Spurious nonexhaustive pattern match warnings are given using GADTs 
#5724  Confusing warning message for incomplete patterns 
#5728  Warnings from fwarnincompleterecordupdates even with all constructors matched 
#5762  GHC gives incorrect warnings with simple applications of the view patterns extension 
#6124  Spurious nonexhaustive warning with GADT and newtypes 
#7669  Empty case causes warning 
#8016  case expression with mixed use of Num instances cause spurious overlap warning 
#8494  Warn if a pattern guard obviates all others 
#8710  Overlapping patterns warning misplaced 
#8853  Surprising mention of unboxed integers in pattern exhaustiveness warning 
#8970  Nonexhaustive pattern match warning with DataKinds and TypeFamilies 
#9113  Template Haskell should warn about nonexhaustive pattern matches 
#9951  OverloadedLists breaks exhaustiveness check 
#10393  Bogus warning with OverloadedLists 
#10746  No nonexhaustive pattern match warning given for empty case analysis 
#11160  New exhaustiveness checker breaks ghcirun004 
#11161  New exhaustiveness checker breaks concurrent/prog001 
#11162  T783 regresses severely in allocations with new pattern match checker 
#11163  New exhaustiveness checker breaks T5642 
#11276  GHC hangs/takes an exponential amount of time with simple program 
#11302  GHC HEAD uses up all memory while compiling \`genprimcode\` 
#11303  Pattern matching against sets of strings sharing a prefix blows up pattern checker 
#11316  Too many guards warning causes issues 
#11374  \`Woverlappingpatterns\` induced memoryblowup 
#11390  GHC does not warn about redundant patterns 
#11806  GHC does not warn for mistakenly empty case 
#11984  Pattern match incompleteness / inaccessibility discrepancy 
#12158  ghc: panic! (the 'impossible' happened) translateConPatVec: lookup 
#13517  No warnings produced, yet the pattern matching fails at runtime. 
#14098  Incorrect pattern match warning on nested GADTs 
#14546  Woverlappingpatterns warns on wrong patterns for Int 
#14547  Wrong warning by Wincompletepatterns 
#14773  MultiWayIf makes it easy to write partial programs that are not catched by Wall 
#14813  EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is 
#15305  Erroneous "nonexhaustive pattern match" using nested GADT with strictness annotation 
#15385  Wincompletepatterns gets confused when combining GADTs and pattern guards 
#15398  GADT deriving Ord generates inaccessible code in a pattern with constructor. 
#15450  Inconsistency w.r.t. coverage checking warnings for EmptyCase under unsatisfiable constraints 
#15584  nonVoid is too conservative w.r.t. strict argument types 
#15884  Completeness of View Patterns With a Complete Set of Output Patterns 
#15886  Spurious warning about incomplete pattern with PatternSynonyms 
#16129  Incorrect nonexhaustive pattern warning with PatternSynonyms 
#16377  \`TypeError\` in a pattern should flag inaccessible code 
Background:
 The paper on which the previous approach was based Two techniques for compiling lazy pattern matching
 Peter Sestoft's paper for negative patterns ML's pattern matching compilation and partial evaluation
Our solution
 Our paper, describing the algorithm we implemented GADTs meet their match.
 PatternMatchCheckImplementation talks about the implementation in GHC.
Related tickets (ones that are closed are still useful examples in the wild; they were only closed as duplicates):
 #29
 #322
 #366
 #595
 #851
 #1307
 #2006
 #2204
 #3078
 #3927
 #4139
 #5724
 #5728
 #5762
 #6124
 #8016
 #8494
 #8779
 #8853
 #8970
 #9113
 #9951
 #10116
 #10600
The main problem we wish to solve
Since GHC's exhaustiveness/redundancy checker was outdated, it did not take into account constraints introduced by GADT matches when reporting warnings. This is illustrated in the following example (#3927):
dataT a whereT1::TIntT2::TBoolf::T a >T a >BoolfT1T1=TruefT2T2=False
Even though the above definition for f
is exhaustive, we get a warning of the form:
Pattern match(es) are nonexhaustive
In an equation for `f':
Patterns not matched:
T1 T2
T2 T1
Obviously, both pattern vectors issued as not matched, are illtyped, because they both generate the inconsistent
constraint Int ~ Bool
. This becomes more clear if we rewrite the definition of T
in the equivalent form:
dataT a whereT1:: forall a.(a ~Int)=>T a
T2:: forall a.(a ~Bool)=>T a
Additionally, if we add one more branch to f
:
f::T a >T a >BoolfT1T1=TruefT2T2=Falsef__= undefined  inaccessible
we get no warning about the redundancy of the last clause.
Two more problems
It has not been only GADTs that have not been handled by the coverage/exhaustiveness checker. More exotic pattern matching features like pattern guards, view patterns, overloaded literals etc. usually made the pattern match checker give imprecise warnings because there was no systematic way to treat them. Additionally, laziness has been fully taken into account by the previous checker. The new pattern match checker addresses these problems too.
General approach
Note that improving the redundancy check is quite more challenging than the exhaustiveness check. For
exhaustiveness it is sufficient to collect all potentially missing vectors using the previous syntaxbased approach
and then filter out the illtyped. Nevertheless, for redundancy we need to compute the cases that are covered by
every clause and then filter out the illtyped. The difficulty lies in the fact that what the last branch of f
covers depends on what remains uncovered by the above two clauses. This indicates that for the redundancy check we
need an incremental way of computing uncovered vectors.
The solution
Until now, the algorithm used by GHC was based on a technique originally introduced for compilation of pattern
matching in decision trees (see paper above). Hence, it used a columnbased approach to traverse the pattern
matrix, which cannot be used incrementally as we described above. (By pattern matrix we mean a list of matches.
Since every clause has the same length, let's call say m
 a match of n
clauses, each of length m
defines
a pattern matrix of dimensions n x m
. For more details see the paper Two techniques for compiling lazy pattern matching).
Additionally, this pattern matrix approach assumes that each clause has the same length, which is rather restrictive since we may have arbitrary guards accompanying a pattern vector (clauses may have different lengths).
Instead, we traverse the clauses linebyline (onebyone, from left to right, topdown), following the semantics of the source language. The general approach is the following: We assume that initially nothing is covered (everything is uncovered) and the, for every clause we compute:
 Which cases it covers
 If it forces the evaluation of arguments (see Laziness below)
 Which cases are left unhandled
There are two major differences with previous approaches:
 We use a core pattern syntax that allows guards to appear anywhere in a clause. As we have shown in the paper, in this expressive pattern language we can encode all source features (and even more).
 The sets of covered/uncovered and divergent cases we mention above do not contain pattern vectors. Instead, they contain vectors accompanied by a set of type and term constraints. We illustrate:
For example, for function f
above we have:

initial_missing =
[(x y)]
wherex :: T a
andy :: T a
fT1T1=True first clause

Covers
[(T1 T1 > {a ~ Int, a ~ Int})]

Forces the evaluation of the 1st argument

If 1st argument is
T1
forces the evaluation of the 2nd argument 
Remain uncovered:
[(T2 y > {a ~ Bool}) , (T1 T2 > {a ~ Int, a ~ Bool) ]
The main idea is that every vector we generate comes with a set of constraints that have to be satisfied. This set
of constraints is the > {...}
part of every vector. Now it becomes apparent that case
(T1 T2 > {a ~ Int, a ~ Bool)
can be removed. The type constraints it contains
(a ~ Int, a ~ Bool
) is not satisfiable (which in turn means that it represents an inaccessible case).
Removing the second vector gives us:
uncovered = [(T2 y > {a ~ Bool})]
With this, we now process the second clause:
fT2T2=False second clause
 Covers
[(T2 T2 > {a ~ Bool, a ~ Bool})]
 If 1st argument is
T2
forces the evaluation of the 2nd argument  Remain uncovered
[(T2 T1 > {a ~ Bool, a ~ Int})]
Same as before, the uncovered set contains non satisfiable constraints, so we end up with
uncovered = []
Finally, checking the last clause given that nothing is uncovered we get:
f__= undefined  third clause (inaccessible)
 Covers:
[]
 Doesn't force anything
 Remain uncovered:
[]
Which means that we rightly now detect the last clause as redundant. Also note that the uncovered set was empty
after the first clauses, which means that the first two clauses make f
exhaustive and the bogus warnings go
away.
Although not illustrated here, we check for satisfiability both the covered and the uncovered sets of clauses. Finally, note that in this example we showed only the type constraints, for simplicity. We also store and check term constraints so that we can handle guards (see section below).
Pattern Guards
A pattern guard (p < e
) behaves exactly like if we had one more argument to pattern match against. For example:
f x ::[a]>Boolf x (z:zs)< x =...
is equivalent to:
g x ::[a]>[a]>Boolg x (z:zs)=...f::[a]>Boolf x = g x x
Using this trick, we can reason about pattern guards in the same way we reason about normal pattern matching. Consider the following example:
 the above example, written using guardsf::T a >T a >Boolf c d T1< c,T1< d =TrueT2< c,T2< d =False otherwise = undefined  inaccessible
Again, we have:

initial_missing =
[(x y)]
wherex :: T a
andy :: T a

1st Clause: Covered (zvariables represent the fake arguments we match against):
[(x y > { x ~ c, z1 ~ c, c ~ T1, a ~ Int , y ~ d, z2 ~ d, d ~ T1, a ~ Int })]
Solving the constraints gives us a solution: { x = c = z1 = T1, y = d = z2 = T2 } which we can use to simplify the clause
(x y)
to(T1 T1)
(exactly like we had in the nonguard example). 
1st Clause: Uncovered:
[(x y > { x ~ c, z1 ~ c, c ~ T2, a ~ Bool , x ~ c, z1 ~ c, c ~ T1, a ~ Int, y ~ d, z2 ~ d, d ~ T2, a ~ Bool })]
Again, the second uncovered vector has nonsatisfiable constraints and can be removed. Solving the constraints for the first uncovered vector gives us a solution: { x = c = z1 = T2 }. Using this, we can again simplify the clause
(x y)
to(T2 y)
, and we end up with exactly the same state we had in the nonguard example. 
etc.
Obviously, pattern guards generate more constraints while the actual patterns of the clause are unaffected (until we solve and substitute back our findings like we did in the above example). Hence, the expressivity of the checker concerning guards heavily relies on the expressive power of the term oracle. Similarly, the expressivity concerning guards totally relies on OutsideIn(X), GHC's inference engine, which we use to check for satisfiability of type constraints.
Laziness
The previous algorithm was not exactly lazinessaware. The two examples below illustrate some (rather pathological) cases:
Example 1
Consider the following function:
g::Bool>Bool>Boolg_True=TruegTrueTrue=Trueg__=False
The old checker emits the following warning:
Pattern match(es) are overlapped
In an equation for `g': g True True = ...
Even though this is correct (indeed the second clause is totally overlapped by the first clause), the above warning
until now was used to mean that the respective clause is redundant, which is not true in this case.
If we call g
we get:
ghci> g undefined False
*** Exception: Prelude.undefined
because the second clause forces the evaluation of the first argument. Yet, if we remove it we get instead:
ghci> g undefined False
False
That is, we changed the semantics of g
. What happens is that all cases that match the second clause match the
first too, which in turn means that the second clause has an inaccessible righthandside. Yet, pattern matching in
a lazy language like Haskell is not only used for matching but also for evaluating. The second clause is useful,
not for matching, but for evaluating the first argument of g
. With our new checker these cases can be easily
detected: The covered set for the second clause is empty (it is overlapped from the above equations) but we detect
that it evaluates something. In principle, we follow the following reasoning:
 Covers = Yes, Forces = Yes ==> Useful clause
 Covers = Yes, Forces = No ==> Useful clause
 Covers = No, Forces = Yes ==> Clause with inaccessible RHS
 Covers = No, Forces = No ==> Redundant clause
By "useful" we mean that the RHS will be returned if matched.
Example 2
Interestingly, one can trigger this behaviour indirectly, using GADTs. Consider the function h
:
dataF a whereF1::FIntF2::FBooldataG a whereG1::GIntG2::GCharh::F a >G a >InthF1G1=1h_G1=2 what about this clause?
Running the check on the first clause leaves us with an uncovered set:
uncovered = [(F2 y > {a ~ Bool})
, (F1 G2 > {a ~ Int, a ~ Char}) ]
and by dropping the second (has nonsatisfiable type constraints) we end up with:
uncovered = [(F2 y > {a ~ Bool}) ]
About the second clause:

Both the uncovered vector
(F2 y)
and the constraints make clear that the second argument is not evaluated yet. By matching with the second clause(_ G1)
we certainly force the evaluation of the second argument. 
The covered set is:
covered = [(F2 G1 > {a ~ Bool, a ~Int}) ]
and because {a ~ Bool, a ~Int}
is nonsatisfiable, the covered set is empty. Hence, even though h
can never
return a 2
, the second clause is not actually redundant.
Note that this case is a bit different from the one above: If we consider the type ofemits warning that the RHS is
inaccessible h
, indeed the only welltyped values that can match are F1
and G1
. But since Haskell is not
callbyvalue, F2 undefined
is a perfectly welltyped combination of arguments! Hence, this example illustrates
the following interesting behaviour:
h1::F a >G a >Inth1F1G1=1h1_G1=2 emits warning that the RHS is inaccessible but h1 is considered exhaustiveh2::F a >G a >Inth2F1G1=1 emits a warning that h2 is nonexhaustive with (F2 _) being the missing caseh3::F a >G a >Inth3F1G1=1h3F2_=2 no warning for this one