badghcbad.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}

data X = C
data SX x where
  SC :: SX C

foo :: SX x -> IO ()
foo x = do
  case x of
    SC -> pure ()
  pure ()

{-
bug.hs:12:11: error:
    • Couldn't match type ‘a0’ with ‘()’
        ‘a0’ is untouchable
          inside the constraints: x ~ 'C
          bound by a pattern with constructor: SC :: SX 'C,
                   in a case alternative
          at newbug.hs:12:5-6
      Expected type: IO a0
        Actual type: IO ()
    • In the expression: pure ()
      In a case alternative: SC -> pure ()
      In a stmt of a 'do' block: case x of { SC -> pure () }
   |
13 |     SC -> pure ()
   |           ^^^^^^^
-}

-- Works
bar :: SX x -> IO ()
bar x = do
  id @(IO ()) $ case x of
    SC -> pure ()
  pure ()