-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Leibnizian equality
--   
--   Leibnizian equality.
@package eq
@version 4.3


-- | Leibnizian equality. Injectivity in the presence of type families is
--   provided by a generalization of a trick by Oleg Kiselyov posted here:
--   
--   
--   <a>http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html</a>
module Data.Eq.Type

-- | Leibnizian equality states that two things are equal if you can
--   substitute one for the other in all contexts
newtype a := b
Refl :: (forall c. c a -> c b) -> (:=) a b
[subst] :: (:=) a b -> forall c. c a -> c b
infixl 4 :=

-- | Equality is reflexive
refl :: a := a

-- | Equality is transitive
trans :: (a := b) -> (b := c) -> a := c

-- | Equality is symmetric
symm :: (a := b) -> b := a

-- | If two things are equal you can convert one to the other
coerce :: (a := b) -> a -> b

-- | Apply one equality to another, respectively
apply :: (f := g) -> (a := b) -> f a := g b

-- | You can lift equality into any type constructor
lift :: (a := b) -> f a := f b

-- | ... in any position
lift2 :: (a := b) -> f a c := f b c
lift2' :: (a := b) -> (c := d) -> f a c := f b d
lift3 :: (a := b) -> f a c d := f b c d
lift3' :: (a := b) -> (c := d) -> (e := f) -> g a c e := g b d f

-- | Type constructors are generative and injective, so you can lower
--   equality through any type constructors ...
lower :: forall a b f g. (f a := g b) -> a := b

-- | ... in any position ...
lower2 :: forall a b f g c c'. (f a c := g b c') -> a := b

-- | ... these definitions are poly-kinded on GHC 7.6 and up.
lower3 :: forall a b f g c c' d d'. (f a c d := g b c' d') -> a := b
fromLeibniz :: (a := b) -> a :~: b
toLeibniz :: (a :~: b) -> a := b
reprLeibniz :: (a := b) -> Coercion a b
instance Control.Category.Category (Data.Eq.Type.:=)
instance Data.Semigroupoid.Semigroupoid (Data.Eq.Type.:=)
instance Data.Groupoid.Groupoid (Data.Eq.Type.:=)
instance forall k (a :: k). Data.Type.Equality.TestEquality ((Data.Eq.Type.:=) a)
instance forall k (a :: k). Data.Type.Coercion.TestCoercion ((Data.Eq.Type.:=) a)


-- | Leibnizian equality à la <a>Data.Eq.Type</a>, generalized to be
--   heterogeneous using higher-rank kinds.
--   
--   This module is only exposed on GHC 8.2 and later.
module Data.Eq.Type.Hetero

-- | Heterogeneous Leibnizian equality.
--   
--   Leibnizian equality states that two things are equal if you can
--   substitute one for the other in all contexts.
newtype (a :: j) :== (b :: k)
HRefl :: (forall (c :: forall i. i -> Type). c a -> c b) -> (:==) (a :: j) (b :: k)
[hsubst] :: (:==) (a :: j) (b :: k) -> forall (c :: forall i. i -> Type). c a -> c b
infixl 4 :==

-- | Equality is reflexive.
refl :: a :== a

-- | Equality is transitive.
trans :: (a :== b) -> (b :== c) -> a :== c

-- | Equality is symmetric.
symm :: (a :== b) -> b :== a

-- | If two things are equal, you can convert one to the other.
coerce :: (a :== b) -> a -> b

-- | Apply one equality to another, respectively
apply :: (f :== g) -> (a :== b) -> f a :== g b

-- | You can lift equality into any type constructor...
lift :: (a :== b) -> f a :== f b

-- | ... in any position.
lift2 :: (a :== b) -> f a c :== f b c
lift2' :: (a :== b) -> (c :== d) -> f a c :== f b d
lift3 :: (a :== b) -> f a c d :== f b c d
lift3' :: (a :== b) -> (c :== d) -> (e :== f) -> g a c e :== g b d f

-- | Type constructors are generative and injective, so you can lower
--   equality through any type constructors.
lower :: forall a b f g. (f a :== g b) -> a :== b
lower2 :: forall a b f g c c'. (f a c :== g b c') -> a :== b
lower3 :: forall a b f g c c' d d'. (f a c d :== g b c' d') -> a :== b

-- | Convert an appropriately kinded heterogeneous Leibnizian equality into
--   a homogeneous Leibnizian equality <a>(:=)</a>.
toHomogeneous :: (a :== b) -> a := b

-- | Convert a homogeneous Leibnizian equality <a>(:=)</a> to an
--   appropriately kinded heterogeneous Leibizian equality.
fromHomogeneous :: (a := b) -> a :== b
fromLeibniz :: forall a b. (a :== b) -> a :~: b
toLeibniz :: (a :~: b) -> a :== b
heteroFromLeibniz :: (a :== b) -> a :~~: b
heteroToLeibniz :: (a :~~: b) -> a :== b
reprLeibniz :: (a :== b) -> Coercion a b
instance Control.Category.Category (Data.Eq.Type.Hetero.:==)
instance Data.Semigroupoid.Semigroupoid (Data.Eq.Type.Hetero.:==)
instance Data.Groupoid.Groupoid (Data.Eq.Type.Hetero.:==)
instance forall j k (a :: j). Data.Type.Equality.TestEquality ((Data.Eq.Type.Hetero.:==) a)
instance forall j k (a :: j). Data.Type.Coercion.TestCoercion ((Data.Eq.Type.Hetero.:==) a)