Type equality in GADT/TypeFamily context

Hi,

How to make GHC to type-check the last branch of pop ? GHC understands that x == c in Just Refl case, but it cannon unify default branch with last type family case.

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

import Prelude
import GHC.TypeLits
import Data.Proxy
import Data.Type.Equality

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 (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 ->   l




Could not deduce ‘Pop (x : l) c ~ (x : l)’
   from the context: (n ~ (x : l), KnownSymbol x)
     bound by a pattern with constructor:
                ConsN :: forall (x :: Symbol) (l :: [Symbol]).
                         KnownSymbol x =>
                         Proxy x -> N l -> N (x : l),
              in an equation for ‘pop’

(GHC 9.12.2)