[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 rwbarton):

 I have to say I don't care for this `COMPLETE_PATTERNS` pragma at all, for
 several reasons:

 * In general there may be many sets of complete patterns for a data type,
 and ensuring that the `COMPLETE_PATTERNS` are correct and complete may be
 difficult.

 * The `COMPLETE_PATTERNS` pragmas are hand-written and unchecked, and
 therefore likely to go out of date as the data type changes, making
 pattern exhaustiveness checking unreliable.

 * Unlike the situation of type class methods with their `MINIMAL` pragmas,
 any module can define new view patterns for a given data type. How can two
 different modules cooperate to produce new sets of complete patterns
 containing pattern synonyms from both modules?

 * Also unlike type classes, it's not obvious (to me anyways) that there is
 a unique best way to use the information of the `COMPLETE_PATTERNS`
 pragmas, as pattern matches can be nested.

 Overall this proposed new feature doesn't seem to offer a very compelling
 solution (for full disclosure, I don't consider the problem of pattern
 synonym exhaustiveness checks particularly compelling in the first place;
 seems like scope creep).

 I would prefer something simple like

 * Pattern synonyms are checked for exhaustiveness as though they were
 expanded to their definitions. No hand-written pragmas needed.

 * GHC understands that if `p1`, ..., `pn` are exhaustive patterns for the
 result type of `f`, then `f -> p1`, ..., `f -> pn` are exhaustive patterns
 for the input type of `f`. This to some extent solves the problem of
 mixing patterns defined in different modules, as long as those patterns
 are defined in terms of the same "view functions".

 In some cases this may require defining several equivalent patterns with
 different definitions, such as `EmptyL` and `EmptyR`. This seems quite
 acceptable to me and probably clarifies the intent at the use site of the
 pattern anyways.

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