2

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".

Sridhar Ratnakumar
  • 81,433
  • 63
  • 146
  • 187

1 Answers1

3

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

Sridhar Ratnakumar
  • 81,433
  • 63
  • 146
  • 187
  • 1
    You might want to define `absurdNS :: NS f '[] -> a; absurdNS = \case`, it doesn't change anything but makes it a bit clearer and more uniform with `absurd :: Void -> a`. – Iceland_jack Jun 25 '22 at 01:36