[Haskell-cafe] Existential problem

[Niklas Broberg]

> > -- 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