Case-matching on `NS` type

Question

The NS type from sop-core creates an interesting conundrum. In S :: NS f xs -> NS f (x ': xs) where xs ~ '[] means that the argument to the S is inhabited. Yet Haskell's case matching forces me to match on it. Is there a resolution to this problem?

type T = NS I '[Int, String]

matchT :: T -> String
matchT = \case
  Z (I n) -> show n
  S (Z (I s)) -> s
  S (S _) -> error "FIXME" -- not reachable

If you remove that last case (which really shouldn't be necessary), Haskell complains "Pattern match(es) are non-exhaustive".

Answer 1

Use EmptyCase!

matchT :: T -> String
matchT = \case
  Z (I n) -> show n
  S (Z (I s)) -> s
  S (S impossible) -> case impossible of {}

Real-world example