Type equality in GADT/TypeFamily context

I tried solutions from @Lysxia and @Leary. Thanks a lot, I totally missed the coerce hammer option! The original attempt checks if I just put unsafeCoerce in the last branch. Without If typefamily UndecidableInstances can be turned off.

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

pop :: forall c n. KnownSymbol c => N n -> Proxy c -> N (Pop n c)
pop (NilN ()) _  = NilN ()
pop l@(ConsN x n) c =
 case sameSymbol x c of
   Just Refl -> n
   Nothing   -> unsafeCoerce l