[Haskell-cafe] Rank-2 polymorphism and overloading

[Thomas van Noort]

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.

Regards,
Thomas