EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is

GHC warns on this program:

{-# 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:

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

Or the case scrutinee:

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

Then the warning goes away.

Trac metadata

Trac field	Value
Version	8.2.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture