Data.EqP

Heterogenous lifted equality.

This class is stronger version of Eq1 from base

class (forall a. Eq a => Eq (f a)) => Eq1 f where
    liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool

as we don't require a a -> b -> Bool function.

Morally Eq1 should be a superclass of EqP, but it cannot be, as GHC wouldn't allow EqP to be polykinded. https://gitlab.haskell.org/ghc/ghc/-/issues/22682

Laws

reflexivity

eqp x x ≡ True

symmetry

eqp x y ≡ eqp y x

transitivity

eqp x y ≡ eqp y z ≡ True ⇒ eqp x z ≡ True

compatibility

eqp x y ≡ x == y

extensionality

eqp x y ≡ True ⇒ f x == f y ≡ True

for polymorphic

f :: forall x. f x -> a

and

Eq a

.

Note: P stands for phantom.