Type inference with GADTs - a0 is untouchable

Question

Lets say I have this program

{-# LANGUAGE GADTs #-}

data My a where
  A :: Int  -> My Int
  B :: Char -> My Char


main :: IO ()
main = do
  let x = undefined :: My a

  case x of
    A v -> print v

  -- print x

compiles fine.

But when I comment in the print x, I get:

gadt.hs: line 13, column 12:
  Couldn't match type ‘a0’ with ‘()’
    ‘a0’ is untouchable
      inside the constraints (a1 ~ GHC.Types.Int)
      bound by a pattern with constructor
                 Main.A :: GHC.Types.Int -> Main.My GHC.Types.Int,
               in a case alternative
      at /home/niklas/src/hs/gadt-binary.hs:13:5-7
  Expected type: GHC.Types.IO a0
    Actual type: GHC.Types.IO ()
  In the expression: System.IO.print v
  In a case alternative: Main.A v -> System.IO.print v

Why do I get this error in line 13 (A v -> print v) instead of only in the print x line?

I thought the first occurrence should determine the type.

Please enlighten me :)

Answer 1

Well, first note that this has nothing to do with the particular print x: you get the same error when ending main with e.g. putStrLn "done".

So the problem is indeed in the case block, namely in that only the last statement of a do is required to have the type of the do block's signature. The other statements merely have to be in the same monad, i.e. IO a0 rather than IO ().

Now, usually this a0 is inferred from the statement itself, so for instance you can write

do getLine
   putStrLn "discarded input"

though getLine :: IO String rather than IO (). However, in your example the information print :: ... -> IO () comes from inside the case block, from a GADT match. And such GADT matches behave differently from other Haskell statements: basically, they don't let any type information escape its scope, because if the information came from the GADT constructor then it's not correct outside of the case.

In that particular example, it seems obvious enough that a0 ~ () has nothing at all to do with the a1 ~ Int from the GADT match, but in general, such a fact could only be proven if GHC traced for all type information where it came from. I don't know if that's even possible, it would certainly be more complicated than Haskell's Hindley-Milner system, which heavily relies on unifying type information, which essentially assumes that it doesn't matter where the information came from.

Therefore, GADT matches simply act as a rigid “type information diode”: the stuff inside can never be used to determine types on the outside, like that the case block as a whole should be IO ().

However, you can manually assert that, with the rather ugly

  (case x of
     A v -> print v
    ) :: IO ()

or by writing

  () <- case x of
          A v -> print v