rank 2-polymorphism and type checking

[Janis Voigtlaender]

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