rank 2-polymorphism and type checking

[Janis Voigtlaender]

Iavor S. Diatchki writes: 

> > > test :: (forall t . (forall a . t a) -> t b) -> b -> b
> i am not an expert on this, but isnt this rank 3?

Might be. Does this mean I cannot write it in Haskell? But, with 

 data T a = C

I can write:

 test' :: (forall t . (forall a . t a) -> t b) -> b -> b
 test' g x = case g C of C -> x

Here, the type checker finds out on its own that t is instantiated to T. Still, 
why are the annotations in the following code not enough to let it also accept 
the definition of "test" (see my earlier message), respectively how can I tell 
it that t should be instantiated to t c = forall d . (c->d) -> d -> d ?

 test :: (forall t . (forall a . t a) -> t b) -> b -> b
 test g x = (g           :: (forall a . (forall d . (a->d) -> d -> d)) -> 
(forall e . (b->e) -> e -> e))
            ((\f y -> y) :: (forall a . (forall d . (a->d) -> d -> d)))
            (id          :: (b -> b)) 
            (x           :: b)


--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de