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
