[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
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms,
                                     |  PatternMatchWarnings
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by dfeuer):

 Here's a full reproduction:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE Trustworthy #-}

 module Fin (Nat (..), Fin (FZ, FS), FinView (..), viewFin) where
 import Numeric.Natural
 import Unsafe.Coerce

 data Nat = Z | S Nat

 -- Fin *must* be exported abstractly (or placed in an Unsafe
 -- module) to maintain type safety.
 newtype Fin (n :: Nat) = Fin Natural
 deriving instance Show (Fin n)

 data FinView n where
   VZ :: FinView ('S n)
   VS :: !(Fin n) -> FinView ('S n)

 viewFin :: Fin n -> FinView n
 viewFin (Fin 0) = unsafeCoerce VZ
 viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1)))

 pattern FZ :: () => n ~ 'S m => Fin n
 pattern FZ <- (viewFin -> VZ) where
   FZ = Fin 0

 pattern FS :: () => n ~ 'S m => Fin m -> Fin n
 pattern FS m <- (viewFin -> VS m) where
   FS (Fin m) = Fin (1 + m)

 {-# COMPLETE FZ, FS #-}
 }}}

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