> > -- 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
