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.