# rank 2-polymorphism and type checking

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

*Tue, 23 Oct 2001 15:46:12 +0200 (MET DST)*

Hello,
assume I want to have the following function:
>* test :: (forall t . (forall a . t a) -> t b) -> b -> b
*>* test g x = g (\f y -> y) id x
*
This should be well-typed if the type constructor t is instantiated as follows:
t c = forall d . (c->d) -> d -> d
Of course, I don't expect type inference to detect this, so I give explicit
annotations:
>* 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)
*
GHC 4.08 complains:
Couldn't match
`forall a d. (a -> d) -> d -> d' against `forall a. t a'
Expected type: (forall a d. (a -> d) -> d -> d)
-> (b -> e)
-> e
-> e
Inferred type: (forall a. t a) -> t b1
In an expression with a type signature:
g ::
forall b.
(forall a d. (a -> d) -> d -> d) -> forall e. (b -> e) -> e -> e
Clearly, giving the annotations was not enough to make the type checker accept
the program, since it still tries to perform a higher-order matching. But, how
can I make explicit for which type constructor t (namely the one given above) I
want to use g (which is polymorphic over t)? I guess, in polymorphic lambda
calculus (where types are explicitly abstracted) I should be able to apply a
polymorphic g to some concrete type to obtain an instance (does this also work
for type constructors?). But, how to do it in Haskell?
Note that it doesn't help me to choose another type for "test", because I'm
interested in the "free theorem" for exactly the given type of g.
Thanks for any hints!
Regards, Janis.
--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de