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.