Type equality in GADT/TypeFamily context

In Agda you would write it like this (I’ve used Char instead of String because that felt simpler while still presenting the same problems):

open import Data.Char
open import Data.List
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality

data N : List Char → Set where
  [] : N []
  _∷_ : ∀{xs} → (x : Char) → N xs → N (x ∷ xs)

popHelper : {x c : Char} → Dec (x ≡ c) → List Char → List Char → List Char
popHelper (yes refl) _ n = n
popHelper (no _) l _ = l

pop : (n : List Char) (c : Char) → List Char
pop [] _ = []
pop l@(x ∷ n) c = popHelper (x ≟ c) l n

popNHelper : ∀ {xs} {x} {c} (w : Dec (x ≡ c)) → N (x ∷ xs) → N xs → N (popHelper w (x ∷ xs) xs)
popNHelper (yes refl) l n = n
popNHelper (no _) l n = l

popN : ∀{n} → N n → (c : Char) → N (pop n c)
popN [] _ = []
popN l@(x ∷ n) c = popNHelper (x ≟ c) l n

They also use this Dec type instead of Maybe which includes an explicit proof of refutation:

data Dec (a : Set) : Set where
  yes : a → Dec a
  no : (a → ⊥) → Dec a

But I don’t think that’s very relevant here. I think a more important problem is the nonlinear matching that type families allow you to do. This is not allowed in Agda and in my opinion questionable in general.