Jochem Berndsen jochem at functor.nl
Mon Apr 26 14:13:39 EDT 2010

```Thomas van Noort wrote:
> Hello all,
>
> I'm having difficulties understanding rank-2 polymorphism in combination
>
> f :: (forall a . Eq a => a -> a -> Bool) -> Bool
> f eq = eq True True
>
> Then, we pass f both an overloaded function and a regular polymorphic
> function:
>
> x :: forall a . Eq => a -> a -> Bool
> x = \x y -> x == y
>
> y :: forall a . a -> a -> Bool
> y = \x y -> True
>
> g :: (Bool, Bool)
> g = (f x, f y)
>
> Could someone explain to me, or point me to some reading material, why g
> is correctly typed?
>
> I understand that x's type is what f expects, but why does y's
> polymorphic type fulfill the overloaded type of f's argument? I can
> imagine that it is justified since f's argument type is more restrictive
> than y's type. However, it requires y to throw away the provided
> dictionary under the hood, which seems counter intuitive to me.

f requires a function that is able to compute, for two values of type a
(which instantiates Eq), a Boolean.

y certainly fulfills that requirement: it does not even require that the
values are of a type instantiating Eq.

This is also well-typed and might or might not be enlightening:

> z :: forall a. Eq a => a -> a -> Bool
> z = y
>
> g :: (Bool, Bool)
> g = (f x, f z) -- note the use of z here instead of y

Jochem
--
Jochem Berndsen | jochem at functor.nl

```