Exhaustiveness checks for pattern synonyms
Pattern synonyms are great, as they decouple interface from implementation. Especially if #8581 is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!
Another missing piece is exhaustiveness checks. Given this pattern
initLast [] = Nothing
initLast xs = Just (init xs, last xs)
pattern xs ::: x <- (initLast -> Just (xs,x))
we want the compiler to tell the programmer that
f [] = ...
f (xs ::: x) = ...
is complete, while
g (xs ::: x) = ...
is not.
With view pattern directly, this is impossible. But the programmer did not write view patterns!
So here is what I think might work well, inspired by the new MINIMAL
pragma:
We add a new pragma COMPLETE_PATTERNS
(any ideas for a shorter name). The syntax is essentially the same as for MINIMAL
, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case.
{-# COMPLETE_PATTERNS [] && (:::) #-}
Multiple pragmas are obviously combined with ||
, and there is an implicit {-# COMPLETE_PATTERNS [] && (:) #-}
listing all real data constructors.
When checking for exhaustiveness, this would be done before unfolding view patterns, and for g
above we get a warning that []
is not matched. Again, the implementation is very much analogous to MINIMAL
.
Clearly, a library author can mess up and give wrong COMPLETE_PATTERNS
pragmas. I think that is ok (like with MINIMAL
), and generally an improvement.