[Haskell-cafe] Rank-2 polymorphism and overloading

[Jochem Berndsen]

Thomas van Noort wrote:
> Hello all,
> 
> I'm having difficulties understanding rank-2 polymorphism in combination
> with overloading. Consider the following contrived definition:
> 
> 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