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