Pattern match incompleteness / inaccessibility discrepancy

Consider this module:

{-# LANGUAGE PolyKinds, TypeOperators, DataKinds, TypeFamilies, GADTs #-}

module Bug where

data family Sing (a :: k)

data Schema = Sch [Bool]

data instance Sing (x :: Schema) where
  SSch :: Sing x -> Sing ('Sch x)

data instance Sing (x :: [k]) where
  SNil :: Sing '[]
  SCons :: Sing a -> Sing b -> Sing (a ': b)

data G a where
  GCons :: G ('Sch (a ': b))

eval :: G s -> Sing s -> ()
eval GCons s =
        case s of
          -- SSch SNil -> undefined
          SSch (SCons _ _) -> undefined

Upon seeing this, GHC says

Bug.hs:21:9: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (SSch SNil)

So I uncomment the second-to-last line, inducing GHC to say

Bug.hs:22:16: error:
    • Couldn't match type ‘a : b’ with ‘'[]’
      Inaccessible code in
        a pattern with constructor: SNil :: forall k. Sing '[],
        in a case alternative
    • In the pattern: SNil
      In the pattern: SSch SNil
      In a case alternative: SSch SNil -> undefined

Thankfully, this pattern is much rarer than it once was, but it's a bit sad that it's still possible.