{-# LANGUAGE TypeFamilies, GADTs, KindSignatures, TypeOperators, RankNTypes, FlexibleContexts #-}
module Foo where

data Equal a b = (b ~ a) => Refl

foo         :: forall a b. ((a ~ b) => a -> b -> Bool) -> Equal a b -> a -> b -> Bool
foo f Refl a b = f a b

x   :: Eq b => Equal a b -> a -> b -> Bool
x   = foo (==)

-- Doesn't typecheck
{-
y   :: Eq a => Equal a b -> a -> b -> Bool
y   = foo (==)
-}