Type equality in GADT/TypeFamily context

Here is a trick: instead of defining Pop with non-linear patterns in the equality case, you branch on a boolean equality test:

type family Pop n c where
  Pop '[] _ = '[]
  Pop (d ': n) c = If (d == c) n (d ': n)

Then in the pop function you need to match on this boolean. From a KnownSymbol constraint, there is no way to do this safely AFAIK, so here is a way that defines the missing primitive eqSymbol using unsafeCoerce:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Prelude
import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Unsafe.Coerce (unsafeCoerce)

data N (l :: [Symbol]) where
  NilN :: () -> N '[]
  ConsN :: KnownSymbol x => Proxy x -> N l -> N (x : l)

type family Pop n c where
  Pop '[]       _  = '[]
  Pop (d ': n)  c  = If (d == c) n (d ': n)

pop :: forall c n. KnownSymbol c => N n -> Proxy c -> N (Pop n c)
pop (NilN ()) _  = NilN ()
pop l@(ConsN x n) c =
 case eqSymbol x c of
   STrue -> n
   SFalse -> l

data SBool (b :: Bool) where
  STrue :: SBool True
  SFalse :: SBool False

eqSymbol :: (KnownSymbol c, KnownSymbol d) => Proxy c -> Proxy d -> SBool (c == d)
eqSymbol c d = case sameSymbol c d of
  Just Refl -> unsafeCoerce STrue  -- can't solve (c == c) ~ True ???
  Nothing -> unsafeCoerce SFalse

main :: IO ()
main = pure ()