# rank 2-polymorphism and type checking

**Janis Voigtlaender
**
Janis Voigtlaender <voigt@orchid.inf.tu-dresden.de>

*Wed, 24 Oct 2001 08:59:39 +0200 (MET DST)*

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