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