PmCheck: Mutually incompatible residual COMPLETE matches
Consider the following program:
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE PatternSynonyms #-}
module Lib where
pattern P :: Bool
pattern P = True
{-# COMPLETE P, True #-}
{-# COMPLETE P, False #-}
f :: Bool -> ()
f P = ()
One could argue that the definition of f
is exhaustive: The first COMPLETE pragma basically says "after matching on P, there can only be values matching True", similarly for the second pragma and False. We can infer from this that "after matching on P, there can only be values matching True and False", e.g. their intersection. But since we consider data constructors non-overlapping, that intersection is empty and a match on P
is a complete match by those two pragmas.
In practice, this argument is supported by trying to instantiate one ConLike
of each COMPLETE pragma. All solutions (True
from the first pragma and False
from the second) must be compatible with each other at the same time! Which is impossible for the above case.
Currently, we aren't so rigorous and the program above warns that True
is uncovered, but that's not technically correct by the above reasoning. But at the same time, I'm not sure if I like the outlined semantics, hence the ticket.
We could go for the semantics as currently implemented, e.g., that each COMPLETE pragma must have at least one inhabitant, independently of the chosen inhabitants of other COMPLETE pragmas. In the program above, we'd choose True
as the inhabitant for the first set and False
for the second one and completely ignore the fact that they are mutually incompatible. But I'm not sure if there are any weird edge cases.