Response to Oleg Grenrus

Twitter_Oleg.md

https://twitter.com/phadej/status/958227051374350336

{-# Language QuantifiedConstraints #-}

class    (forall xx. Eq xx => Eq (f xx)) => Eq1 f
instance (forall xx. Eq xx => Eq (f xx)) => Eq1 f

newtype New s a = New a

instance Reifies s (a -> a -> Bool) => Eq (New s a) where
  New a == New a' = reflect @s Proxy a a'

newtype WithEq s f a = WithEq (f (New s a))

instance (Eq1 f, Reifies s (a -> a -> Bool)) => Eq (WithEq s f a) where
  WithEq fa == WithEq fa' = fa == fa'

liftEq :: forall f a. Eq1 f => (a -> a -> Bool) -> (f a -> f a -> Bool)
liftEq eq fa fb = reify eq reifying where

  reifying :: forall ss. Reifies ss (a -> a -> Bool) => Proxy ss -> Bool
  reifying Proxy = fa2 == fb2 where

    fa2 :: f (New ss a)
    fa2 = unsafeCoerce fa

    fb2 :: f (New ss a)
    fb2 = unsafeCoerce fa

unsafeCoerce can be replaced by coerce if we know that f is rep

type RepArg1 m = (forall a b. Coercible a b => Coercible (m a) (m b))

liftEq :: forall f a. (RepArg1 f, Eq1 f) => (a -> a -> Bool) -> (f a -> f a -> Bool)

I'm interested in a better way!