-- Explicitly recursive continuation type data C t a = forall t2 . C (C t2 a -> IO t a)
If you write
data C t a = C (forall t2 . C t2 a -> IO' t a),
it will compile (versions 6.2.2, 6.4). Whether that'll do exactly what you want, I don't know :-(
Actually, I think it does. Originally I thought this would be too restrictive, since all possible continuations must then be polymorphic in their argument, but in practise that's actually the case anyway. :-)
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 ()
trans = transition, I suppose?
Indeed... the dangers of trimming code for the sake of presentation... :-)
-------------------------------------- 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)) [...]
Now I'm not an expert, but I think it's roughly thus: by the original definition, from the pattern 'C k', it follows that there is some type, call it t1, such that k has type C t1 () -> IO' t (). Now applying k to C s1 requires t1 to be H, which may or may not be the case, that can't be decided by pattern matching.
You are right of course. k is not polymorphic in its argument, since t1 is not a type variable but an actual type. we just don't know which type that is, and we certainly can't guarantee that it's H. Moving the forall to make k polymorphic solves the problem, just like you said above. Thanks a lot, /Niklas