Type family fails to reduce when unmatchable application is involved

The title of this issue is rather vague, but I'm not quite sure how to describe this phenomenon. I originally noticed this when attempting to port over the singletons test suite, as there was a specific piece of code that worked with a defunctionalized unmatchable arrow, but not with (->) @U. Here is a minimized version of that code:

{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

#if __GLASGOW_HASKELL__ >= 811
{-# LANGUAGE UnsaturatedTypeFamilies #-}
#endif
module Bug where

import Data.Kind
#if __GLASGOW_HASKELL__ >= 811
import GHC.Exts
#endif

type Hm :: (a ~> Bool) -> a -> Bool
type family Hm f x where
  Hm f x = HmCase (f @@ x)

type HmCase :: Bool -> Bool
type family HmCase b where
  HmCase True  = False
  HmCase False = True

sHm :: forall a (f :: a ~> Bool) (x :: a).
       Sing f -> Sing x -> Sing (Hm f x)
sHm sF sX = case sF @@ sX of
  STrue  -> SFalse
  SFalse -> STrue

-----

type Sing :: k -> Type
type family Sing :: k -> Type

type SBool :: Bool -> Type
data SBool z where
  SFalse :: SBool False
  STrue  :: SBool True
type instance Sing = SBool

type SLambda :: forall k1 k2. (k1 ~> k2) -> Type
newtype SLambda (f :: k1 ~> k2) =
  SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }
type instance Sing = SLambda

#if __GLASGOW_HASKELL__ >= 811
type (~>) :: Type -> Type -> Type
type a ~> b = a -> @U b

type (@@) :: (k1 ~> k2) -> k1 -> k2
type family f @@ x where
  f @@ x = f x
#else
type TyFun :: Type -> Type -> Type
data TyFun x y

type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type

type (@@) :: (k1 ~> k2) -> k1 -> k2
type family f @@ x
#endif

The CPP in this program is only included to allow this file to be compile with both GHC 8.10 (which uses defunctionalization) and your fork (which uses (->) @U). This compiles with GHC 8.10, but not with your fork:

[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:34:13: error:
    • Could not deduce: HmCase (f x) ~ 'False
      from the context: f x ~ 'True
        bound by a pattern with constructor: STrue :: SBool 'True,
                 in a case alternative
        at Bug.hs:34:3-7
      Expected: Sing (Hm f x)
        Actual: SBool 'False
    • In the expression: SFalse
      In a case alternative: STrue -> SFalse
      In the expression:
        case sF @@ sX of
          STrue -> SFalse
          SFalse -> STrue
    • Relevant bindings include
        sX :: Sing x (bound at Bug.hs:33:8)
        sF :: Sing f (bound at Bug.hs:33:5)
        sHm :: Sing f -> Sing x -> Sing (Hm f x) (bound at Bug.hs:33:1)
   |
34 |   STrue  -> SFalse
   |             ^^^^^^

Bug.hs:35:13: error:
    • Could not deduce: HmCase (f x) ~ 'True
      from the context: f x ~ 'False
        bound by a pattern with constructor: SFalse :: SBool 'False,
                 in a case alternative
        at Bug.hs:35:3-8
      Expected: Sing (Hm f x)
        Actual: SBool 'True
    • In the expression: STrue
      In a case alternative: SFalse -> STrue
      In the expression:
        case sF @@ sX of
          STrue -> SFalse
          SFalse -> STrue
    • Relevant bindings include
        sX :: Sing x (bound at Bug.hs:33:8)
        sF :: Sing f (bound at Bug.hs:33:5)
        sHm :: Sing f -> Sing x -> Sing (Hm f x) (bound at Bug.hs:33:1)
   |
35 |   SFalse -> STrue
   |             ^^^^^

This seems like it ought to typecheck. Since HmCase True = False, shouldn't GHC be able to deduce HmCase (f x) ~ 'False from f x ~ 'True?