question about GADT's and error messages

[S. Doaitse Swierstra]

Given the following code:

{-# LANGUAGE GADTs #-}
data Any a where
AInt :: Int -> Any Int

-- demo 1 does not compile
{-
demo1 a = do case a of
            (AInt i) -> print i

 Couldn't match expected type ‘t’ with actual type ‘IO ()’
   ‘t’ is untouchable
     inside the constraints (t1 ~ Int)
     bound by a pattern with constructor
                AInt :: Int -> Any Int,
              in a case alternative
     at /Users/doaitse/TryHaskell/TestGADT.hs:6:17-22
   ‘t’ is a rigid type variable bound by
       the inferred type of demo1 :: Any t1 -> t
       at /Users/doaitse/TryHaskell/TestGADT.hs:5:1
 Relevant bindings include
   demo1 :: Any t1 -> t
     (bound at /Users/doaitse/TryHaskell/TestGADT.hs:5:1)
 In the expression: print i
 In a case alternative: (AInt i) -> print i
Failed, modules loaded: none.
-}


-- all the following go through without complaints:

a = AInt 3
demo2 = do case a of
            (AInt i) -> print i

demo3 :: IO ()
demo3 = do case a of
            (AInt i) -> print i


demo4 = do case AInt 3 of
            (AInt i) -> print i

demo5 :: Any Int -> IO ()
demo5 a = do case a of
            (AInt i) -> print i

I do not see why the error message in demo1 arises. It claims it can't match some t with the type IO (), but when I tell that the result is IO () it can?
I think at least the error message is confusing, and not very helpful. I would have in no way been able to get the clue that add a type signature as in the case of demo5 would solve the problem.

What am I overlooking?

Doaitse