[GHC] #8779: Exhaustiveness checks for pattern synonyms

[GHC]

#8779: Exhaustiveness checks for pattern synonyms
-------------------------------------------+-------------------------------
       Reporter:  nomeata                  |             Owner:
           Type:  feature request          |            Status:  new
       Priority:  normal                   |         Milestone:
      Component:  Compiler (Type checker)  |           Version:  7.6.3
       Keywords:                           |  Operating System:
   Architecture:  Unknown/Multiple         |  Unknown/Multiple
     Difficulty:  Unknown                  |   Type of failure:
     Blocked By:                           |  None/Unknown
Related Tickets:                           |         Test Case:
                                           |          Blocking:
-------------------------------------------+-------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8779>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler