Recursive exhaustivity checker for pattern
Motivation
GHC pattern exhaustivity checker is not able to compute exhaustivity when the cases are handled using a combination of multiples case
or pattern in function operations.
For example, the following:
foo :: Bool -> String
foo True = "True"
foo i = case i of
False -> "False"
bar :: Bool -> String
bar True = "True"
bar i = bir i
where
bir False = "False"
baz :: Bool -> String
baz i = case i of
True -> "True"
_ -> case i of
False -> "False"
-- Amazingly this does not trigger a warning
baz' :: Bool -> String
baz' i = case i of
True -> "True"
False -> case i of
False -> "False"
bur :: Bool -> String
bur True = "True"
bur i = case i of
True -> "True"
_ -> boz i
where
boz False = "False"
-- This should not fail
-- That's a proof that all function are total
test :: [String]
test = [foo, bar, baz, baz', bur] <*> [minBound..maxBound]
Implements five total functions (I tried multiples combination of case/equation pattern).
However warnings are generated for four of them:
BetterCase.hs:3:9: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: True
|
3 | foo i = case i of
| ^^^^^^^^^...
BetterCase.hs:10:5: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘bir’: Patterns not matched: True
|
10 | bir False = "False"
| ^^^^^^^^^^^^^^^^^^^
BetterCase.hs:15:8: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: True
|
15 | _ -> case i of
| ^^^^^^^^^...
BetterCase.hs:32:7: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘boz’: Patterns not matched: True
|
32 | boz False = "False"
| ^^^^^^^^^^^^^^^^^^^
Ok, one module loaded.
It is interesting to observe that baz'
, which seems highly similar to baz
does not trigger a warning.
Proposal
I'd like the exhaustivity checker to recognizes variations of theses cases and not generate a warning.