[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:                    |
-------------------------------------+-------------------------------------
Changes (by dfeuer):

 * cc: dfeuer (added)


Comment:

 I suspect making this really work right may require some modifications to
 the pattern synonym concept. For example,

 {{{#!hs
 pattern Empty = Seq EmptyT
 pattern x :<| xs <- (viewl -> x :< xs)
 pattern xs :|> x <- (viewr -> xs :> x)
 }}}

 To see that either `x :<| xs` or `xs :|> x` is complete when combined with
 `Empty`, the exhaustiveness checker would have to recognize that `viewl`
 and `viewr` will give non-empty results under the same circumstances. This
 may be feasible in this case (I'm not sure), but in principle it seems
 rather hard. I think a good target would be to ensure that multiple
 pattern synonyms using the ''same'' view are handled properly. An
 alternative blunt instrument: let the user promise that a certain
 combination of pattern synonyms will always be exhaustive when applied to
 a particular type.

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