Some type-family rules are ignored when deducing equality constraints under GADT match

With GHC 8.8.3:

Test.hs

{-# LANGUAGE GADTs, TypeFamilies, PolyKinds, DataKinds, ConstraintKinds, TypeOperators, PolyKinds,
  RankNTypes, ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
  UndecidableInstances, LambdaCase, EmptyCase, TypeFamilyDependencies #-}

import Data.Kind
import GHC.TypeLits
import Data.Singletons
import Data.Singletons.TypeLits
import Data.Singletons.Decide

data TMaybe (t :: Maybe k) where
  TNothing :: TMaybe 'Nothing
  TJust :: !t -> TMaybe ('Just t)

data KVList (kk :: [Symbol]) (vv :: [Type]) :: Type where
  KVNil :: KVList '[] '[]
  KVCons :: !(Sing k) -> !v -> !(KVList kk vv) -> KVList (k : kk) (v : vv)

type family LookupKV (k :: Symbol) (tab :: Type) = v where
  LookupKV k (KVList '[] '[]) = TMaybe 'Nothing
  LookupKV k (KVList (k  ': kk1) (v ': vv1)) = TMaybe ('Just v)
  LookupKV k (KVList (k1 ': kk1) (v ': vv1)) = LookupKV k (KVList kk1 vv1)

lookupKV
  :: Sing k -> KVList kk vv -> LookupKV k (KVList kk vv)
lookupKV k = \case
  KVNil -> TNothing
  KVCons k' v r -> case k %~ k' of
    Proved Refl -> TJust v
    Disproved d -> lookupKV k r

The last line gives:

    • Could not deduce: LookupKV k (KVList kk1 vv1)
                        ~ LookupKV k (KVList (k1 : kk1) (v : vv1))
      from the context: (kk ~ (k1 : kk1), vv ~ (v : vv1))
        bound by a pattern with constructor:
                   KVCons :: forall (k :: Symbol) v (kk :: [Symbol]) (vv :: [*]).
                             Sing k -> v -> KVList kk vv -> KVList (k : kk) (v : vv),
                 in a case alternative
        at Test.hs:28:3-15
      Expected type: Decision (LookupKV k (KVList kk vv))
        Actual type: Decision (LookupKV k (KVList kk1 vv1))

With -fprint-explicit-kinds:

    • Could not deduce: (LookupKV k (KVList kk1 vv1) :: *)
                        ~ (LookupKV k (KVList ((':) @Symbol k1 kk1) ((':) @* v vv1)) :: *)
      from the context: ((kk :: [Symbol])
                         ~ ((':) @Symbol k1 kk1 :: [Symbol]),
                         (vv :: [*]) ~ ((':) @* v vv1 :: [*]))
        bound by a pattern with constructor:
                   KVCons :: forall (k :: Symbol) v (kk :: [Symbol]) (vv :: [*]).
                             Sing @Symbol k
                             -> v -> KVList kk vv -> KVList ((':) @Symbol k kk) ((':) @* v vv),
                 in a case alternative
        at Test.hs:28:3-15

which doesn't seem to raise anything suspicious, all the kinds are fully-resolved and contain no variables that could be ambiguous.

But in the definition for type family LookupKV it specifically says

      LookupKV k (KVList (_ ': kk) (v ': vv)) = LookupKV k (KVList kk vv)

Considering the fact the Proved (TJust v) branch type-checks, GHC must have deduced LookupKV k (KVList (k ': kk1) (v ': vv1)) ~ TMaybe ('Just v) via the corresponding type-family rule. So it's strange it doesn't use another type-family rule for this unsatisfied deduction. I'm pretty sure this is unrelated to injectivity since k, kk, and vv all appear as themselves in the actual type signature, unapplied to a type family.