[Haskell-cafe] Existential problem

[Niklas Broberg]

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