| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.EqP
Documentation
class (forall a. Eq (f a)) => EqP (f :: k -> Type) where Source #
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
eqpx x ≡ True- symmetry
eqpx y ≡eqpy x- transitivity
eqpx y ≡eqpy z ≡ True ⇒eqpx z ≡ True- compatibility
eqpx y ≡ x==y- extensionality
for polymorphiceqpx y ≡ True ⇒ f x == f y ≡ Truef :: forall x. f x -> aand.Eqa
Note: P stands for phantom.
Since: 1.0.5
Instances
| EqP StableName Source # | |
Defined in Data.EqP Methods eqp :: forall (a :: k) (b :: k). StableName a -> StableName b -> Bool Source # | |
| EqP (Proxy :: k -> Type) Source # | |
| EqP (TypeRep :: k -> Type) Source # | |
| Eq a => EqP (Const a :: k -> Type) Source # | |
| EqP ((:~:) a :: k -> Type) Source # | |
| EqP ((:~~:) a :: k -> Type) Source # | |
| (EqP a, EqP b) => EqP (a :*: b :: k -> Type) Source # | |
| (EqP f, EqP g) => EqP (f :+: g :: k -> Type) Source # | |