Reordering alternatives in case expression causes exhaustive function to become non-exhaustive

The following code emits no pattern-match coverage warnings on GHC HEAD, as I would expect:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

import Data.Kind
import Data.Void

type SFalse = SBool 'False
type STrue  = SBool 'True

data SBool :: Bool -> Type where
  SFalse :: SFalse
  STrue  :: STrue

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

data T (b :: Bool)
  = MkT1
  | MkT2 !(F b)

ex :: SBool b -> T b -> ()
ex sb t =
  case t of
    MkT1 -> ()
    MkT2 f ->
      case sb of
        STrue -> f

However, if you reorder the alternatives in the case expression in ex:

ex :: SBool b -> T b -> ()
ex sb t =
  case t of
    MkT2 f ->
      case sb of
        STrue -> f
    MkT1 -> ()

Then GHC HEAD will emit a spurious warning:

GHCi, version 8.11.0.20200526: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:30:7: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: SFalse
   |
30 |       case sb of
   |       ^^^^^^^^^^...

To the best of my knowledge, the order of alternatives should not affect exhaustivity in this example.

I originally discovered this in the wild while writing some TTG-heavy code in !3337 (closed). Thankfully, this bug has a workaround (just reorder the alternatives), so this isn't actively blocking !3337 (closed). But it would still be interesting to figure out why this is happening.

cc @sgraf812