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".
Use EmptyCase!
matchT :: T -> String
matchT = \case
Z (I n) -> show n
S (Z (I s)) -> s
S (S impossible) -> case impossible of {}