[GHC] #13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase

[GHC]

#13717: Pattern synonym exhaustiveness checks don't play well with EmptyCase
-------------------------------------+-------------------------------------
           Reporter:  dfeuer         |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.2.1-rc1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternSynonyms,                   |
  PatternMatchWarnings               |
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In #8779, mpickering added a `COMPLETE` pragma to allow exhaustiveness
 checking for matches involving pattern synonyms. Unfortunately, there is
 still one piece missing: the interaction with `EmptyCase`. Suppose I write

 {{{#!hs
 newtype Fin (n :: Nat) = Fin Natural  -- constructor not exported

 pattern FZ :: () => forall m. n ~ 'S m => Fin n
 pattern FS :: () => n ~ 'S m => Fin m -> Fin n
 {-# COMPLETE FZ, FS #-}
 }}}

 I would very much like to be able to write

 {{{#!hs
 finZAbsurd :: Fin 'Z -> Void
 finZAbsurd x = case x of
 }}}

 but this gives me a pattern coverage warning! That's certainly not what we
 want. I believe what we actually want is this:

   When checking empty case, check that ''at least one'' complete pattern
 set is impossible.

 In this case, it would see two complete pattern sets: the built-in `{Fin}`
 and the user-decreed `{FZ, FS}`. Since neither `FZ` nor `FS` have matching
 types, we should conclude that the empty case is fine.

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