I just can't see why the following code will not type check. I have scaled it down as much as possible: ------------------------------------- -- IO with an extra level annotation newtype IO' t a = MkIO' (IO a) -- levels data H data L -- Explicitly recursive continuation type data C t a = forall t2 . C (C t2 a -> IO t a) transition :: Bool -> IO tx () -> IO t () -> IO t () transition b c d = undefined s1 :: C t () -> IO H () s1 (C k) = trans (True) (k (C s1)) -- :: IO t () (s1 (C k)) -- :: IO H () -------------------------------------- The error message is: Inferred type is less polymorphic than expected Quantified type variable `t2' is unified with `H' When checking an existential match that binds k :: C t2 a -> IO t a The pattern(s) have type(s): C t1 () The body has type: IO H () In the definition of `s1': s1 (C k) = trans (True) (k (C s1)) (s1 (C k)) The thing is, I'm perfectly happy with t2 being unified with H for this particular definition of s1, but I want to use it in other cases as well. The code that follows the one above is s2 :: C t () -> IO L () s2 (C k) = trans (True) (k (C s2)) -- :: IO t () (s2 (C k)) -- :: IO L () main = s1 (C s2) where t2 instead gets unified with L for the definition of s2. Could someone tell me why this does not work? I'm using GHC 6.2.2. Thanks, /Niklas