Type equality in GADT/TypeFamily context

Nice.

The issue with Just Refl -> STrue is due to a weird definition of == in base (I guess it can’t decide it isn’t in the first case); it will go away if you define == the obvious way.

You can also replace eqSymbol with a smaller, more general apart primitive, allowing you to write the second pop case like so.

pop l@(ConsN x n) c = case decideSymbol x c of
  Left  (apart -> Refl) -> l
  Right           Refl  -> n