[GHC] #14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is

[GHC]

#14813: EmptyCase thinks pattern match involving type family is not exhaustive,
when it actually is
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
  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:
-------------------------------------+-------------------------------------
 GHC warns on this program:

 {{{#!hs
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# OPTIONS_GHC -Wall #-}
 module Bug where

 import Data.Kind
 import Data.Void

 data SBool (z :: Bool) where
   SFalse :: SBool 'False
   STrue  :: SBool 'True

 type family F (b :: Bool) (a :: Type) :: Type where
   F 'True  a = a
   F 'False _ = Void

 dispatch :: forall (b :: Bool) (a :: Type). SBool b -> F b a -> a
 dispatch STrue  x = x
 dispatch SFalse x = case x of {}
 }}}

 {{{
 $ /opt/ghc/8.2.2/bin/ghci Bug.hs
 GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:22:21: warning: [-Wincomplete-patterns]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: _ :: F b a
    |
 22 | dispatch SFalse x = case x of {}
    |                     ^^^^
 }}}

 This warning is incorrect, as `x` is of type `F 'False a`, or `Void`, in
 that case alternative.

 Curiously, if you ascribe either the pattern for `x`:

 {{{#!hs
 dispatch SFalse (x :: F 'False a) = case x of {}
 }}}

 Or the case scrutinee:

 {{{#!hs
 dispatch SFalse x = case x :: F 'False a of {}
 }}}

 Then the warning goes away.

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