some-1.0.5: Existential type: Some
Safe HaskellSafe
LanguageHaskell2010

Data.EqP

Synopsis
  • class (forall a. Eq (f a)) => EqP (f :: k -> Type) where

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
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.

Since: 1.0.5

Methods

eqp :: f a -> f b -> Bool Source #

Instances

Instances details
EqP StableName Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a :: k) (b :: k). StableName a -> StableName b -> Bool Source #

EqP (Proxy :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a :: k0) (b :: k0). Proxy a -> Proxy b -> Bool Source #

EqP (TypeRep :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Bool Source #

Eq a => EqP (Const a :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a0 :: k0) (b :: k0). Const a a0 -> Const a b -> Bool Source #

EqP ((:~:) a :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Bool Source #

EqP ((:~~:) a :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Bool Source #

(EqP a, EqP b) => EqP (a :*: b :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a0 :: k0) (b0 :: k0). (a :*: b) a0 -> (a :*: b) b0 -> Bool Source #

(EqP f, EqP g) => EqP (f :+: g :: k -> Type) Source # 
Instance details

Defined in Data.EqP

Methods

eqp :: forall (a :: k0) (b :: k0). (f :+: g) a -> (f :+: g) b -> Bool Source #