{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Eq.Type.Hetero
-- Copyright   :  (C) 2011-2014 Edward Kmett, 2018 Ryan Scott
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
-- Stability   :  provisional
-- Portability :  GHC
--
-- Leibnizian equality à la "Data.Eq.Type", 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
    (:==)(..)
  -- * Equality as an equivalence relation
  , refl
  , trans
  , symm
  , coerce
  , apply
  -- * Lifting equality
  , lift
  , lift2, lift2'
  , lift3, lift3'
  -- * Lowering equality
  , lower
  , lower2
  , lower3
  -- * 'ET.:=' equivalence
  -- | 'ET.:=' is equivalent in power
  , toHomogeneous
  , fromHomogeneous
  -- * 'Eq.:~:' equivalence
  -- | 'Eq.:~:' is equivalent in power
  , fromLeibniz
  , toLeibniz
  -- * 'Eq.:~~:' equivalence
  -- | 'Eq.:~~:' is equivalent in power
  , heteroFromLeibniz
  , heteroToLeibniz
  -- * 'Co.Coercion' conversion
  -- | Leibnizian equality can be converted to representational equality
  , reprLeibniz
  ) where

import           Control.Category
import           Data.Groupoid
import           Data.Semigroupoid
import qualified Data.Type.Coercion as Co
import qualified Data.Type.Equality as Eq
import           Data.Kind
import qualified Data.Eq.Type as ET
import           Prelude hiding (id, (.))

infixl 4 :==

-- | 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 { (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst :: forall (c :: forall i. i -> Type). c a -> c b }
type role (:==) nominal nominal

-- | Equality is reflexive.
refl :: a :== a
refl :: a :== a
refl = (forall (c :: forall i. i -> *). c a -> c a) -> a :== a
forall j k (a :: j) (b :: k).
(forall (c :: forall i. i -> *). c a -> c b) -> a :== b
HRefl forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
forall (c :: forall i. i -> *). c a -> c a
id

data family Coerce :: forall k. k -> Type
newtype instance Coerce (a :: Type) = Coerce { Coerce a -> a
uncoerce :: a }

-- | If two things are equal, you can convert one to the other.
coerce :: a :== b -> a -> b
coerce :: (a :== b) -> a -> b
coerce a :== b
f = Coerce b -> b
forall a. Coerce a -> a
uncoerce (Coerce b -> b) -> (a -> Coerce b) -> a -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Coerce a -> Coerce b) -> (a -> Coerce a) -> a -> Coerce b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Coerce a
forall a. a -> Coerce a
Coerce

newtype Pair1 :: forall j1 k1 j2.
                 j1 -> k1 -> j2
              -> forall k2. k2 -> Type where
  Pair1 :: { Pair1 a1 b1 a2 b2 -> '(a1, a2) :== '(b1, b2)
unpair1 :: '(a1, a2) :== '(b1, b2) } -> Pair1 a1 b1 a2 b2

newtype Pair2 :: forall j2 k2 j1.
                 j2 -> k2 -> j1
              -> forall k1. k1 -> Type where
  Pair2 :: { Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
unpair2 :: '(a1, a2) :== '(b1, b2) } -> Pair2 a2 b2 a1 b1

-- | Lift two equalities pairwise.
pair :: a1 :== b1 -> a2 :== b2 -> '(a1, a2) :== '(b1, b2)
pair :: (a1 :== b1) -> (a2 :== b2) -> '(a1, a2) :== '(b1, b2)
pair a1 :== b1
ab1 a2 :== b2
ab2 = Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
forall j2 (a2 :: j2) k2 (b2 :: k2) j1 (a1 :: j1) k1 (b1 :: k1).
Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
unpair2 (Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2))
-> Pair2 a2 b2 a1 b1 -> '(a1, a2) :== '(b1, b2)
forall a b. (a -> b) -> a -> b
$ (a1 :== b1) -> forall (c :: forall i. i -> *). c a1 -> c b1
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a1 :== b1
ab1 (Pair2 a2 b2 a1 a1 -> Pair2 a2 b2 a1 b1)
-> Pair2 a2 b2 a1 a1 -> Pair2 a2 b2 a1 b1
forall a b. (a -> b) -> a -> b
$ ('(a1, a2) :== '(a1, b2)) -> Pair2 a2 b2 a1 a1
forall j1 j2 k1 k2 (a1 :: j1) (a2 :: j2) (b1 :: k1) (b2 :: k2).
('(a1, a2) :== '(b1, b2)) -> Pair2 a2 b2 a1 b1
Pair2 (('(a1, a2) :== '(a1, b2)) -> Pair2 a2 b2 a1 a1)
-> ('(a1, a2) :== '(a1, b2)) -> Pair2 a2 b2 a1 a1
forall a b. (a -> b) -> a -> b
$ Pair1 a1 a1 a2 b2 -> '(a1, a2) :== '(a1, b2)
forall j1 (a1 :: j1) k1 (b1 :: k1) j2 (a2 :: j2) k2 (b2 :: k2).
Pair1 a1 b1 a2 b2 -> '(a1, a2) :== '(b1, b2)
unpair1 (Pair1 a1 a1 a2 b2 -> '(a1, a2) :== '(a1, b2))
-> Pair1 a1 a1 a2 b2 -> '(a1, a2) :== '(a1, b2)
forall a b. (a -> b) -> a -> b
$ (a2 :== b2) -> forall (c :: forall i. i -> *). c a2 -> c b2
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a2 :== b2
ab2 (Pair1 a1 a1 a2 a2 -> Pair1 a1 a1 a2 b2)
-> Pair1 a1 a1 a2 a2 -> Pair1 a1 a1 a2 b2
forall a b. (a -> b) -> a -> b
$ ('(a1, a2) :== '(a1, a2)) -> Pair1 a1 a1 a2 a2
forall j1 j2 k1 k2 (a1 :: j1) (a2 :: j2) (b1 :: k1) (b2 :: k2).
('(a1, a2) :== '(b1, b2)) -> Pair1 a1 b1 a2 b2
Pair1 '(a1, a2) :== '(a1, a2)
forall k (a :: k). a :== a
refl

data family Apply :: forall j1 j2.
                     (j1 -> j2) -> j1
                  -> forall k. k -> Type
newtype instance Apply (f :: j1 -> j2) (a :: j1) '((g :: k1 -> k2), (b :: k1))
  = Apply { Apply f a '(g, b) -> f a :== g b
unapply :: f a :== g b }

-- | Apply one equality to another, respectively
apply :: f :== g -> a :== b -> f a :== g b
apply :: (f :== g) -> (a :== b) -> f a :== g b
apply f :== g
fg a :== b
ab = Apply f a '(g, b) -> f a :== g b
forall j2 j1 (f :: j1 -> j2) (a :: j1) k2 k1 (g :: k1 -> k2)
       (b :: k1).
Apply f a '(g, b) -> f a :== g b
unapply (Apply f a '(g, b) -> f a :== g b)
-> Apply f a '(g, b) -> f a :== g b
forall a b. (a -> b) -> a -> b
$ ('(f, a) :== '(g, b))
-> forall (c :: forall i. i -> *). c '(f, a) -> c '(g, b)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst ((f :== g) -> (a :== b) -> '(f, a) :== '(g, b)
forall k k k k (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k).
(a1 :== b1) -> (a2 :== b2) -> '(a1, a2) :== '(b1, b2)
pair f :== g
fg a :== b
ab) (Apply f a '(f, a) -> Apply f a '(g, b))
-> Apply f a '(f, a) -> Apply f a '(g, b)
forall a b. (a -> b) -> a -> b
$ (f a :== f a) -> Apply f a '(f, a)
forall j1 j2 k1 k2 (f :: j1 -> j2) (a :: j1) (g :: k1 -> k2)
       (b :: k1).
(f a :== g b) -> Apply f a '(g, b)
Apply f a :== f a
forall k (a :: k). a :== a
refl

newtype Push :: (forall j k. j -> k -> Type)
             -> forall j. j -> forall k. k -> Type where
  Push :: forall (p :: forall j k. j -> k -> Type)
                 j k (a :: j) (b :: k).
          { Push p a b -> p a b
unpush :: p a b } -> Push p a b

-- | Equality is compositional.
comp :: b :== c -> a :== b -> a :== c
comp :: (b :== c) -> (a :== b) -> a :== c
comp b :== c
f = Push (:==) a c -> a :== c
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) a c -> a :== c)
-> ((a :== b) -> Push (:==) a c) -> (a :== b) -> a :== c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (b :== c) -> forall (c :: forall i. i -> *). c b -> c c
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst b :== c
f (Push (:==) a b -> Push (:==) a c)
-> ((a :== b) -> Push (:==) a b) -> (a :== b) -> Push (:==) a c
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a :== b) -> Push (:==) a b
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push

-- | Equality forms a category.
instance Category (:==) where
  id :: a :== a
id  = a :== a
forall k (a :: k). a :== a
refl
  . :: (b :== c) -> (a :== b) -> a :== c
(.) = (b :== c) -> (a :== b) -> a :== c
forall k k j (b :: k) (c :: k) (a :: j).
(b :== c) -> (a :== b) -> a :== c
comp

instance Semigroupoid (:==) where
  o :: (j :== k1) -> (i :== j) -> i :== k1
o = (j :== k1) -> (i :== j) -> i :== k1
forall k k j (b :: k) (c :: k) (a :: j).
(b :== c) -> (a :== b) -> a :== c
comp

instance Groupoid (:==) where
  inv :: (a :== b) -> b :== a
inv = (a :== b) -> b :== a
forall k j (a :: k) (b :: j). (a :== b) -> b :== a
symm

-- | Equality is transitive.
trans :: a :== b -> b :== c -> a :== c
trans :: (a :== b) -> (b :== c) -> a :== c
trans = ((b :== c) -> (a :== b) -> a :== c)
-> (a :== b) -> (b :== c) -> a :== c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (b :== c) -> (a :== b) -> a :== c
forall k k j (b :: k) (c :: k) (a :: j).
(b :== c) -> (a :== b) -> a :== c
comp

newtype Symm :: (forall j. j -> forall k. k -> Type)
             ->  forall j. j -> forall k. k -> Type where
  Symm :: forall (p :: forall j. j -> forall k. k -> Type)
                 j k (a :: j) (b :: k).
          { Symm p a b -> p b a
unsymm :: p b a } -> Symm p a b

-- | Equality is symmetric.
symm :: a :== b -> b :== a
symm :: (a :== b) -> b :== a
symm a :== b
ab = Push (:==) b a -> b :== a
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) b a -> b :== a) -> Push (:==) b a -> b :== a
forall a b. (a -> b) -> a -> b
$ Symm (Push (:==)) a b -> Push (:==) b a
forall (p :: forall j. j -> forall i. i -> *) j (a :: j) k
       (b :: k).
Symm p a b -> p b a
unsymm (Symm (Push (:==)) a b -> Push (:==) b a)
-> Symm (Push (:==)) a b -> Push (:==) b a
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
ab (Symm (Push (:==)) a a -> Symm (Push (:==)) a b)
-> Symm (Push (:==)) a a -> Symm (Push (:==)) a b
forall a b. (a -> b) -> a -> b
$ Push (:==) a a -> Symm (Push (:==)) a a
forall (p :: forall j. j -> forall i. i -> *) j k (a :: j)
       (b :: k).
p b a -> Symm p a b
Symm (Push (:==) a a -> Symm (Push (:==)) a a)
-> Push (:==) a a -> Symm (Push (:==)) a a
forall a b. (a -> b) -> a -> b
$ (a :== a) -> Push (:==) a a
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push a :== a
forall k (a :: k). a :== a
refl

data family Lift :: forall j r. (j -> r) -> j
                 -> forall k. k
                 -> Type
newtype instance Lift f (a :: j) (b :: j) =
  Lift { Lift f a b -> f a :== f b
unlift :: f a :== f b }

-- | You can lift equality into any type constructor...
lift :: a :== b -> f a :== f b
lift :: (a :== b) -> f a :== f b
lift a :== b
f = Lift f a b -> f a :== f b
forall k j (f :: j -> k) (a :: j) (b :: j).
Lift f a b -> f a :== f b
unlift (Lift f a b -> f a :== f b) -> Lift f a b -> f a :== f b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Lift f a a -> Lift f a b) -> Lift f a a -> Lift f a b
forall a b. (a -> b) -> a -> b
$ (f a :== f a) -> Lift f a a
forall j k (f :: j -> k) (a :: j) (b :: j).
(f a :== f b) -> Lift f a b
Lift f a :== f a
forall k (a :: k). a :== a
refl

data family Lift2 :: forall j1 j2 r.
                     (j1 -> j2 -> r) -> j1 -> j2
                  -> forall k. k
                  -> Type
newtype instance Lift2 f (a :: j1) (c :: j2) (b :: j1) =
  Lift2 { Lift2 f a c b -> f a c :== f b c
unlift2 :: f a c :== f b c }

-- | ... in any position.
lift2 :: a :== b -> f a c :== f b c
lift2 :: (a :== b) -> f a c :== f b c
lift2 a :== b
f = Lift2 f a c b -> f a c :== f b c
forall k j2 j1 (f :: j1 -> j2 -> k) (a :: j1) (c :: j2) (b :: j1).
Lift2 f a c b -> f a c :== f b c
unlift2 (Lift2 f a c b -> f a c :== f b c)
-> Lift2 f a c b -> f a c :== f b c
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Lift2 f a c a -> Lift2 f a c b) -> Lift2 f a c a -> Lift2 f a c b
forall a b. (a -> b) -> a -> b
$ (f a c :== f a c) -> Lift2 f a c a
forall j1 j2 k (f :: j1 -> j2 -> k) (a :: j1) (c :: j2) (b :: j1).
(f a c :== f b c) -> Lift2 f a c b
Lift2 f a c :== f a c
forall k (a :: k). a :== a
refl

lift2' :: a :== b -> c :== d -> f a c :== f b d
lift2' :: (a :== b) -> (c :== d) -> f a c :== f b d
lift2' a :== b
ab c :== d
cd = Push (:==) (f a c) (f b d) -> f a c :== f b d
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) (f a c) (f b d) -> f a c :== f b d)
-> Push (:==) (f a c) (f b d) -> f a c :== f b d
forall a b. (a -> b) -> a -> b
$ (a :== b) -> f a d :== f b d
forall k k k (a :: k) (b :: k) (f :: k -> k -> k) (c :: k).
(a :== b) -> f a c :== f b c
lift2 a :== b
ab (f a d :== f b d)
-> Push (:==) (f a c) (f a d) -> Push (:==) (f a c) (f b d)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
`hsubst` (f a c :== f a d) -> Push (:==) (f a c) (f a d)
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push ((c :== d) -> f a c :== f a d
forall k k (a :: k) (b :: k) (f :: k -> k).
(a :== b) -> f a :== f b
lift c :== d
cd)

data family Lift3 :: forall j1 j2 j3 r.
                     (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3
                  -> forall k. k
                  -> Type
newtype instance Lift3 f (a :: j1) (c :: j2) (d :: j3) (b :: j1) =
  Lift3 { Lift3 f a c d b -> f a c d :== f b c d
unlift3 :: f a c d :== f b c d }

lift3 :: a :== b -> f a c d :== f b c d
lift3 :: (a :== b) -> f a c d :== f b c d
lift3 a :== b
f = Lift3 f a c d b -> f a c d :== f b c d
forall k j2 j3 j1 (f :: j1 -> j2 -> j3 -> k) (a :: j1) (c :: j2)
       (d :: j3) (b :: j1).
Lift3 f a c d b -> f a c d :== f b c d
unlift3 (Lift3 f a c d b -> f a c d :== f b c d)
-> Lift3 f a c d b -> f a c d :== f b c d
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Lift3 f a c d a -> Lift3 f a c d b)
-> Lift3 f a c d a -> Lift3 f a c d b
forall a b. (a -> b) -> a -> b
$ (f a c d :== f a c d) -> Lift3 f a c d a
forall j1 j2 j3 k (f :: j1 -> j2 -> j3 -> k) (a :: j1) (c :: j2)
       (d :: j3) (b :: j1).
(f a c d :== f b c d) -> Lift3 f a c d b
Lift3 f a c d :== f a c d
forall k (a :: k). a :== a
refl

lift3' :: a :== b -> c :== d -> e :== f -> g a c e :== g b d f
lift3' :: (a :== b) -> (c :== d) -> (e :== f) -> g a c e :== g b d f
lift3' a :== b
ab c :== d
cd e :== f
ef = Push (:==) (g a c e) (g b d f) -> g a c e :== g b d f
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:==) (g a c e) (g b d f) -> g a c e :== g b d f)
-> Push (:==) (g a c e) (g b d f) -> g a c e :== g b d f
forall a b. (a -> b) -> a -> b
$ Push (:==) (g a c f) (g b d f) -> g a c f :== g b d f
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush ((a :== b) -> g a d f :== g b d f
forall k k k k (a :: k) (b :: k) (f :: k -> k -> k -> k) (c :: k)
       (d :: k).
(a :== b) -> f a c d :== f b c d
lift3 a :== b
ab (g a d f :== g b d f)
-> Push (:==) (g a c f) (g a d f) -> Push (:==) (g a c f) (g b d f)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
`hsubst` (g a c f :== g a d f) -> Push (:==) (g a c f) (g a d f)
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push ((c :== d) -> g a c f :== g a d f
forall k k k (a :: k) (b :: k) (f :: k -> k -> k) (c :: k).
(a :== b) -> f a c :== f b c
lift2 c :== d
cd)) (g a c f :== g b d f)
-> Push (:==) (g a c e) (g a c f) -> Push (:==) (g a c e) (g b d f)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
`hsubst` (g a c e :== g a c f) -> Push (:==) (g a c e) (g a c f)
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push ((e :== f) -> g a c e :== g a c f
forall k k (a :: k) (b :: k) (f :: k -> k).
(a :== b) -> f a :== f b
lift e :== f
ef)

data family Lower :: forall j. j
                  -> forall k. k
                  -> Type
newtype instance Lower a (f x) = Lower { Lower a (f x) -> a :== x
unlower :: a :== x }

-- | 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
lower :: (f a :== g b) -> a :== b
lower f a :== g b
f = Lower a (g b) -> a :== b
forall j (a :: j) k k (f :: k -> k) (x :: k).
Lower a (f x) -> a :== x
unlower (Lower a (g b) -> a :== b) -> Lower a (g b) -> a :== b
forall a b. (a -> b) -> a -> b
$ (f a :== g b) -> Lower a (f a) -> Lower a (g b)
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst f a :== g b
f ((a :== a) -> Lower a (f a)
forall j k k (a :: j) (f :: k -> k) (x :: k).
(a :== x) -> Lower a (f x)
Lower a :== a
forall k (a :: k). a :== a
refl :: Lower a (f a))

data family Lower2 :: forall j. j
                   -> forall k. k
                   -> Type
newtype instance Lower2 a (f x c) = Lower2 { Lower2 a (f x c) -> a :== x
unlower2 :: a :== x }

lower2 :: forall a b f g c c'. f a c :== g b c' -> a :== b
lower2 :: (f a c :== g b c') -> a :== b
lower2 f a c :== g b c'
f = Lower2 a (g b c') -> a :== b
forall j (a :: j) k k k (f :: k -> k -> k) (x :: k) (c :: k).
Lower2 a (f x c) -> a :== x
unlower2 (Lower2 a (g b c') -> a :== b) -> Lower2 a (g b c') -> a :== b
forall a b. (a -> b) -> a -> b
$ (f a c :== g b c') -> Lower2 a (f a c) -> Lower2 a (g b c')
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst f a c :== g b c'
f ((a :== a) -> Lower2 a (f a c)
forall j k k k (a :: j) (f :: k -> k -> k) (x :: k) (c :: k).
(a :== x) -> Lower2 a (f x c)
Lower2 a :== a
forall k (a :: k). a :== a
refl :: Lower2 a (f a c))

data family Lower3 :: forall j. j
                   -> forall k. k
                   -> Type
newtype instance Lower3 a (f x c d) = Lower3 { Lower3 a (f x c d) -> a :== x
unlower3 :: a :== x }

lower3 :: forall a b f g c c' d d'. f a c d :== g b c' d' -> a :== b
lower3 :: (f a c d :== g b c' d') -> a :== b
lower3 f a c d :== g b c' d'
f = Lower3 a (g b c' d') -> a :== b
forall j (a :: j) k k k k (f :: k -> k -> k -> k) (x :: k) (c :: k)
       (d :: k).
Lower3 a (f x c d) -> a :== x
unlower3 (Lower3 a (g b c' d') -> a :== b)
-> Lower3 a (g b c' d') -> a :== b
forall a b. (a -> b) -> a -> b
$ (f a c d :== g b c' d')
-> Lower3 a (f a c d) -> Lower3 a (g b c' d')
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst f a c d :== g b c' d'
f ((a :== a) -> Lower3 a (f a c d)
forall j k k k k (a :: j) (f :: k -> k -> k -> k) (x :: k) (c :: k)
       (d :: k).
(a :== x) -> Lower3 a (f x c d)
Lower3 a :== a
forall k (a :: k). a :== a
refl :: Lower3 a (f a c d))

data family Flay :: forall j.
                    (j -> j -> Type) -> j
                 -> forall k. k
                 -> Type
newtype instance Flay p (a :: j) (b :: j) = Flay { Flay p a b -> p a b
unflay :: p a b }

-- | Convert an appropriately kinded heterogeneous Leibnizian equality into
-- a homogeneous Leibnizian equality '(ET.:=)'.
toHomogeneous :: a :== b -> a ET.:= b
toHomogeneous :: (a :== b) -> a := b
toHomogeneous a :== b
f = Flay (:=) a b -> a := b
forall j (p :: j -> j -> *) (a :: j) (b :: j). Flay p a b -> p a b
unflay (Flay (:=) a b -> a := b) -> Flay (:=) a b -> a := b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Flay (:=) a a -> Flay (:=) a b) -> Flay (:=) a a -> Flay (:=) a b
forall a b. (a -> b) -> a -> b
$ (a := a) -> Flay (:=) a a
forall j (p :: j -> j -> *) (a :: j) (b :: j). p a b -> Flay p a b
Flay a := a
forall k (a :: k). a := a
ET.refl

-- | Convert a homogeneous Leibnizian equality '(ET.:=)' to an appropriately kinded
-- heterogeneous Leibizian equality.
fromHomogeneous :: a ET.:= b -> a :== b
fromHomogeneous :: (a := b) -> a :== b
fromHomogeneous a := b
f = (a := b) -> (a :== a) -> a :== b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
ET.subst a := b
f a :== a
forall k (a :: k). a :== a
refl

fromLeibniz :: forall a b. a :== b -> a Eq.:~: b
fromLeibniz :: (a :== b) -> a :~: b
fromLeibniz a :== b
f = Flay (:~:) a b -> a :~: b
forall j (p :: j -> j -> *) (a :: j) (b :: j). Flay p a b -> p a b
unflay (Flay (:~:) a b -> a :~: b) -> Flay (:~:) a b -> a :~: b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Flay (:~:) a a -> Flay (:~:) a b)
-> Flay (:~:) a a -> Flay (:~:) a b
forall a b. (a -> b) -> a -> b
$ (a :~: a) -> Flay (:~:) a a
forall j (p :: j -> j -> *) (a :: j) (b :: j). p a b -> Flay p a b
Flay a :~: a
forall k (a :: k). a :~: a
Eq.Refl

toLeibniz :: a Eq.:~: b -> a :== b
toLeibniz :: (a :~: b) -> a :== b
toLeibniz a :~: b
Eq.Refl = a :== b
forall k (a :: k). a :== a
refl

heteroFromLeibniz :: a :== b -> a Eq.:~~: b
heteroFromLeibniz :: (a :== b) -> a :~~: b
heteroFromLeibniz a :== b
f = Push (:~~:) a b -> a :~~: b
forall (p :: forall j k. j -> k -> *) j (a :: j) k (b :: k).
Push p a b -> p a b
unpush (Push (:~~:) a b -> a :~~: b) -> Push (:~~:) a b -> a :~~: b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Push (:~~:) a a -> Push (:~~:) a b)
-> Push (:~~:) a a -> Push (:~~:) a b
forall a b. (a -> b) -> a -> b
$ (a :~~: a) -> Push (:~~:) a a
forall (p :: forall j k. j -> k -> *) j k (a :: j) (b :: k).
p a b -> Push p a b
Push a :~~: a
forall k1 (a :: k1). a :~~: a
Eq.HRefl

heteroToLeibniz :: a Eq.:~~: b -> a :== b
heteroToLeibniz :: (a :~~: b) -> a :== b
heteroToLeibniz a :~~: b
Eq.HRefl = a :== b
forall k (a :: k). a :== a
refl

instance Eq.TestEquality ((:==) a) where
  testEquality :: (a :== a) -> (a :== b) -> Maybe (a :~: b)
testEquality a :== a
fa a :== b
fb = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((a :== b) -> a :~: b
forall k (a :: k) (b :: k). (a :== b) -> a :~: b
fromLeibniz ((a :== a) -> (a :== b) -> a :== b
forall j j k (a :: j) (b :: j) (c :: k).
(a :== b) -> (b :== c) -> a :== c
trans ((a :== a) -> a :== a
forall k j (a :: k) (b :: j). (a :== b) -> b :== a
symm a :== a
fa) a :== b
fb))

reprLeibniz :: a :== b -> Co.Coercion a b
reprLeibniz :: (a :== b) -> Coercion a b
reprLeibniz a :== b
f = Flay Coercion a b -> Coercion a b
forall j (p :: j -> j -> *) (a :: j) (b :: j). Flay p a b -> p a b
unflay (Flay Coercion a b -> Coercion a b)
-> Flay Coercion a b -> Coercion a b
forall a b. (a -> b) -> a -> b
$ (a :== b) -> forall (c :: forall i. i -> *). c a -> c b
forall j (a :: j) k (b :: k).
(a :== b) -> forall (c :: forall i. i -> *). c a -> c b
hsubst a :== b
f (Flay Coercion a a -> Flay Coercion a b)
-> Flay Coercion a a -> Flay Coercion a b
forall a b. (a -> b) -> a -> b
$ Coercion a a -> Flay Coercion a a
forall j (p :: j -> j -> *) (a :: j) (b :: j). p a b -> Flay p a b
Flay Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Co.Coercion

instance Co.TestCoercion ((:==) a) where
  testCoercion :: (a :== a) -> (a :== b) -> Maybe (Coercion a b)
testCoercion a :== a
fa a :== b
fb = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just ((a :== b) -> Coercion a b
forall k (a :: k) (b :: k). (a :== b) -> Coercion a b
reprLeibniz ((a :== a) -> (a :== b) -> a :== b
forall j j k (a :: j) (b :: j) (c :: k).
(a :== b) -> (b :== c) -> a :== c
trans ((a :== a) -> a :== a
forall k j (a :: k) (b :: j). (a :== b) -> b :== a
symm a :== a
fa) a :== b
fb))