[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    |              Version:  7.8.1
  checker)                           |             Keywords:
      Resolution:                    |  PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 The ticket mentions

 > Multiple pragmas are obviously combined with `||`, and there is an
 implicit `{-# COMPLETE_PATTERNS [] && (:) #-}` listing all real data
 constructors.

 which sounds like

 {{{#!hs
 {-# COMPLETE_PATTERNS Empty, (:<|) #-}
 {-# COMPLETE_PATTERNS Empty, (:|>) #-}
 }}}

 would equal what I proposed (if I got the precedence right)

 {{{#!hs
 {-# COMPLETE_PATTERNS Empty, (:<|) | Empty, (:|>) #-}
 }}}

 ----

 Tangent: The second part (“there is an implicit `{-# COMPLETE_PATTERNS []
 && (:) #-}` listing all real data constructors.”) sounds awful similar to
 this part of the
 [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/pragmas.html
 users guide]:

 > If no MINIMAL pragma is given in the class declaration, it is just as if
 a pragma
 > {{{#!hs
 > {-# MINIMAL op1, op2, ..., opn #-}
 > }}}
 > was given, where the `opi` are the methods
 > a. that lack a default method in the class declaration, and
 > b. whose name that does not start with an underscore (c.f. -fwarn-
 missing-methods, Section 4.8, “Warnings and sanity-checking”).

 As I understand it means that when the user defines

 {{{#!hs
 data ABC = A | B | C
 }}}

 it is as if the she had also written `{-# COMPLETE_PATTERNS A, B, C #-}`.
 Would this work with GADTs?

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