-- --< Header >-- {{{

{-#
LANGUAGE
  DataKinds, TypeFamilies, UndecidableInstances, MagicHash,
  QuantifiedConstraints
#-}

{- |

Description : Heterogeneous equality with evidence capture
Copyright   : (c) L. S. Leary, 2025

Heterogeneous equality with evidence capture.

-}

-- }}}

-- --< Exports >-- {{{

module Data.Hetero.Eq (

  -- * HetEq
  HetEq(..),
  HetEq',

  -- * Newtypes for @DerivingVia@
  TestCo(..),
  TestEq(..),

) where

-- }}}

-- --< Imports >-- {{{

-- GHC/base
import GHC.TypeLits (SNat, SSymbol, SChar)
import GHC.STRef (STRef(..))
import GHC.IORef (IORef(..))
import GHC.MVar (MVar(..))
import GHC.Conc (TVar(..))

-- base
import Type.Reflection (TypeRep)
import Data.Kind (Type, Constraint)
import Data.Type.Equality (TestEquality(..), (:~:)(..), (:~~:)(..))
import Data.Type.Ord (Min, Max)
import Data.Type.Coercion (TestCoercion(..), Coercion(..))
import Data.Proxy (Proxy(..))
import Data.Functor ((<&>), ($>))
import Data.Functor.Const (Const(..))
import Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))
import Data.Functor.Compose (Compose(..))
import Control.Monad (guard)

-- primitive
import Data.Primitive
  ( Array(..), MutableArray(..), SmallArray(..), SmallMutableArray(..)
  , MutVar(..)
  )
import Data.Primitive.MVar qualified as Prim

-- ord-axiomata
import Data.Type.Ord.Axiomata (minTO)
import Data.Type.Ord.Lemmata (minDefl1, minDefl2)

-- heterogeneous-comparison
import Data.Hetero.PtrEq
import Data.Hetero.Role
  (RoleKind(..), Role(..), KnownRole(..), expositRole, SuperPhantom)
import Data.Hetero.Evidence.Exactly (Exactly(..))
import Data.Hetero.Evidence.AtLeast (AtLeast(..), maxAL, weakenAL, innerAL)

-- }}}

-- --< HetEq >-- {{{

-- | Heterogeneous equality with evidence capture of type equivalence.
class HetEq f where

  -- | Does not correspond precisely to the role signature of @f@ according to GHC, but rather a lower bound on the @Strength@ of the evidence gleaned from a positive equality test.
  type Strength f :: RoleKind

  -- | Compare an @f a@ and an @f b@ for equality, opportunistically capturing the strongest type-equivalence evidence we can given the arguments.
  heq :: f a -> f b -> Maybe (AtLeast (Strength f) a b)

type HetEq' :: (k -> Type) -> Constraint
type HetEq' f = (KnownRole (Strength f), HetEq f)

-- }}}

-- --< HetEq: Phantom >-- {{{

instance HetEq Proxy where
  type Strength Proxy = Phantom
  heq :: forall (a :: k) (b :: k).
Proxy a -> Proxy b -> Maybe (AtLeast (Strength Proxy) a b)
heq Proxy a
Proxy Proxy b
Proxy = AtLeast Phantom a b -> Maybe (AtLeast Phantom a b)
forall a. a -> Maybe a
Just AtLeast Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL

instance Eq a => HetEq (Const a) where
  type Strength (Const a) = Phantom
  heq :: forall (a :: k) (b :: k).
Const a a -> Const a b -> Maybe (AtLeast (Strength (Const a)) a b)
heq (Const a
x) (Const a
y) = Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y) Maybe () -> AtLeast Phantom a b -> Maybe (AtLeast Phantom a b)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> AtLeast Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL

-- }}}

-- --< HetEq: Representational >-- {{{

-- | Derives a 'HetEq' instance from 'TestCoercion'.
newtype TestCo f a = TestCo (f a)

instance TestCoercion f => HetEq (TestCo f) where
  type Strength (TestCo f) = Representational
  heq :: forall (a :: k) (b :: k).
TestCo f a
-> TestCo f b -> Maybe (AtLeast (Strength (TestCo f)) a b)
heq (TestCo f a
fx) (TestCo f b
fy) = f a -> f b -> Maybe (Coercion a b)
forall (a :: k) (b :: k). f a -> f b -> Maybe (Coercion a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestCoercion f =>
f a -> f b -> Maybe (Coercion a b)
testCoercion f a
fx f b
fy Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

deriving via TestCo (Coercion a) instance HetEq (Coercion a)

instance HetEq (STRef s) where
  type Strength (STRef s) = Representational
  STRef MutVar# s a
mv1 heq :: forall a b.
STRef s a -> STRef s b -> Maybe (AtLeast (Strength (STRef s)) a b)
`heq` STRef MutVar# s b
mv2 = MutVar# s a -> MutVar# s b -> Maybe (Coercion a b)
forall s a b. MutVar# s a -> MutVar# s b -> Maybe (Coercion a b)
sameMutVar# MutVar# s a
mv1 MutVar# s b
mv2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq IORef where
  type Strength IORef = Representational
  IORef STRef RealWorld a
r1 heq :: forall a b.
IORef a -> IORef b -> Maybe (AtLeast (Strength IORef) a b)
`heq` IORef STRef RealWorld b
r2 = STRef RealWorld a
r1 STRef RealWorld a
-> STRef RealWorld b
-> Maybe (AtLeast (Strength (STRef RealWorld)) a b)
forall a b.
STRef RealWorld a
-> STRef RealWorld b
-> Maybe (AtLeast (Strength (STRef RealWorld)) a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetEq f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
`heq` STRef RealWorld b
r2

instance HetEq MVar where
  type Strength MVar = Representational
  MVar MVar# RealWorld a
mv1 heq :: forall a b. MVar a -> MVar b -> Maybe (AtLeast (Strength MVar) a b)
`heq` MVar MVar# RealWorld b
mv2 = MVar# RealWorld a -> MVar# RealWorld b -> Maybe (Coercion a b)
forall s a b. MVar# s a -> MVar# s b -> Maybe (Coercion a b)
sameMVar# MVar# RealWorld a
mv1 MVar# RealWorld b
mv2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq TVar where
  type Strength TVar = Representational
  TVar TVar# RealWorld a
mv1 heq :: forall a b. TVar a -> TVar b -> Maybe (AtLeast (Strength TVar) a b)
`heq` TVar TVar# RealWorld b
mv2 = TVar# RealWorld a -> TVar# RealWorld b -> Maybe (Coercion a b)
forall s a b. TVar# s a -> TVar# s b -> Maybe (Coercion a b)
sameTVar# TVar# RealWorld a
mv1 TVar# RealWorld b
mv2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq Chan where
  type Strength Chan = Representational
  Chan a
c1 heq :: forall a b. Chan a -> Chan b -> Maybe (AtLeast (Strength Chan) a b)
`heq` Chan b
c2 = Chan a -> Chan b -> Maybe (Coercion a b)
forall a b. Chan a -> Chan b -> Maybe (Coercion a b)
sameChan Chan a
c1 Chan b
c2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq TBQueue where
  type Strength TBQueue = Representational
  TBQueue a
c1 heq :: forall a b.
TBQueue a -> TBQueue b -> Maybe (AtLeast (Strength TBQueue) a b)
`heq` TBQueue b
c2 = TBQueue a -> TBQueue b -> Maybe (Coercion a b)
forall a b. TBQueue a -> TBQueue b -> Maybe (Coercion a b)
sameTBQueue TBQueue a
c1 TBQueue b
c2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq TChan where
  type Strength TChan = Representational
  TChan a
c1 heq :: forall a b.
TChan a -> TChan b -> Maybe (AtLeast (Strength TChan) a b)
`heq` TChan b
c2 = TChan a -> TChan b -> Maybe (Coercion a b)
forall a b. TChan a -> TChan b -> Maybe (Coercion a b)
sameTChan TChan a
c1 TChan b
c2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq TMVar where
  type Strength TMVar = Representational
  TMVar a
c1 heq :: forall a b.
TMVar a -> TMVar b -> Maybe (AtLeast (Strength TMVar) a b)
`heq` TMVar b
c2 = TMVar a -> TMVar b -> Maybe (Coercion a b)
forall a b. TMVar a -> TMVar b -> Maybe (Coercion a b)
sameTMVar TMVar a
c1 TMVar b
c2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq TQueue where
  type Strength TQueue = Representational
  TQueue a
c1 heq :: forall a b.
TQueue a -> TQueue b -> Maybe (AtLeast (Strength TQueue) a b)
`heq` TQueue b
c2 = TQueue a -> TQueue b -> Maybe (Coercion a b)
forall a b. TQueue a -> TQueue b -> Maybe (Coercion a b)
sameTQueue TQueue a
c1 TQueue b
c2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq Array where
  type Strength Array = Representational
  Array Array# a
xs heq :: forall a b.
Array a -> Array b -> Maybe (AtLeast (Strength Array) a b)
`heq` Array Array# b
ys = Array# a -> Array# b -> Maybe (Coercion a b)
forall a b. Array# a -> Array# b -> Maybe (Coercion a b)
sameArray# Array# a
xs Array# b
ys Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq (MutableArray s) where
  type Strength (MutableArray s) = Representational
  MutableArray MutableArray# s a
xs heq :: forall a b.
MutableArray s a
-> MutableArray s b
-> Maybe (AtLeast (Strength (MutableArray s)) a b)
`heq` MutableArray MutableArray# s b
ys
    = MutableArray# s a -> MutableArray# s b -> Maybe (Coercion a b)
forall s a b.
MutableArray# s a -> MutableArray# s b -> Maybe (Coercion a b)
sameMutableArray# MutableArray# s a
xs MutableArray# s b
ys Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq SmallArray where
  type Strength SmallArray = Representational
  SmallArray SmallArray# a
xs heq :: forall a b.
SmallArray a
-> SmallArray b -> Maybe (AtLeast (Strength SmallArray) a b)
`heq` SmallArray SmallArray# b
ys
    = SmallArray# a -> SmallArray# b -> Maybe (Coercion a b)
forall a b. SmallArray# a -> SmallArray# b -> Maybe (Coercion a b)
sameSmallArray# SmallArray# a
xs SmallArray# b
ys Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq (SmallMutableArray s) where
  type Strength (SmallMutableArray s) = Representational
  SmallMutableArray SmallMutableArray# s a
xs heq :: forall a b.
SmallMutableArray s a
-> SmallMutableArray s b
-> Maybe (AtLeast (Strength (SmallMutableArray s)) a b)
`heq` SmallMutableArray SmallMutableArray# s b
ys
    = SmallMutableArray# s a
-> SmallMutableArray# s b -> Maybe (Coercion a b)
forall s a b.
SmallMutableArray# s a
-> SmallMutableArray# s b -> Maybe (Coercion a b)
sameSmallMutableArray# SmallMutableArray# s a
xs SmallMutableArray# s b
ys Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq (MutVar s) where
  type Strength (MutVar s) = Representational
  MutVar MutVar# s a
mv1 heq :: forall a b.
MutVar s a
-> MutVar s b -> Maybe (AtLeast (Strength (MutVar s)) a b)
`heq` MutVar MutVar# s b
mv2 = MutVar# s a -> MutVar# s b -> Maybe (Coercion a b)
forall s a b. MutVar# s a -> MutVar# s b -> Maybe (Coercion a b)
sameMutVar# MutVar# s a
mv1 MutVar# s b
mv2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

instance HetEq (Prim.MVar s) where
  type Strength (Prim.MVar s) = Representational
  Prim.MVar MVar# s a
mv1 heq :: forall a b.
MVar s a -> MVar s b -> Maybe (AtLeast (Strength (MVar s)) a b)
`heq` Prim.MVar MVar# s b
mv2
    = MVar# s a -> MVar# s b -> Maybe (Coercion a b)
forall s a b. MVar# s a -> MVar# s b -> Maybe (Coercion a b)
sameMVar# MVar# s a
mv1 MVar# s b
mv2 Maybe (Coercion a b)
-> (Coercion a b -> AtLeast Representational a b)
-> Maybe (AtLeast Representational a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Coercion a b
Coercion -> AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL

-- primitive instances elided due to lack of opacity:
--
-- instance HetEq PrimArray
-- instance HetEq (MutablePrimArray s)
-- instance HetEq (PrimVar s)

-- }}}

-- --< HetEq: Nominal >-- {{{

-- | Derives a 'HetEq' instance from 'TestEquality'.
newtype TestEq f a = TestEq (f a)

instance TestEquality f => HetEq (TestEq f) where
  type Strength (TestEq f) = Nominal
  heq :: forall (a :: k) (b :: k).
TestEq f a
-> TestEq f b -> Maybe (AtLeast (Strength (TestEq f)) a b)
heq (TestEq f a
fx) (TestEq f b
fy) = f a -> f b -> Maybe (a :~: b)
forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f a
fx f b
fy Maybe (a :~: b)
-> ((a :~: b) -> AtLeast Nominal a b)
-> Maybe (AtLeast Nominal a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \a :~: b
Refl -> AtLeast Nominal a a
AtLeast Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL

deriving via TestEq ((:~:)  a) instance HetEq ((:~:)  a)
deriving via TestEq ((:~~:) a) instance HetEq ((:~~:) a)
deriving via TestEq  TypeRep   instance HetEq  TypeRep
deriving via TestEq  SNat      instance HetEq  SNat
deriving via TestEq  SSymbol   instance HetEq  SSymbol
deriving via TestEq  SChar     instance HetEq  SChar
deriving via TestEq  Role      instance HetEq  Role

-- }}}

-- --< HetEq: Dependent >-- {{{

instance HetEq (Exactly r a) where
  type Strength (Exactly r a) = r
  heq :: forall (a :: k) (b :: k).
Exactly r a a
-> Exactly r a b -> Maybe (AtLeast (Strength (Exactly r a)) a b)
heq Exactly r a a
PhantEx Exactly r a b
PhantEx = AtLeast Phantom a b -> Maybe (AtLeast Phantom a b)
forall a. a -> Maybe a
Just AtLeast Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL
  heq Exactly r a a
ReprEx  Exactly r a b
ReprEx  = AtLeast Representational a b
-> Maybe (AtLeast Representational a b)
forall a. a -> Maybe a
Just AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL
  heq Exactly r a a
NomEx   Exactly r a b
NomEx   = AtLeast Nominal a b -> Maybe (AtLeast Nominal a b)
forall a. a -> Maybe a
Just AtLeast Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL

instance HetEq (AtLeast r a) where
  type Strength (AtLeast r a) = r
  heq :: forall (a :: k) (b :: k).
AtLeast r a a
-> AtLeast r a b -> Maybe (AtLeast (Strength (AtLeast r a)) a b)
heq AtLeast r a a
PhantAL AtLeast r a b
PhantAL = AtLeast r a b -> Maybe (AtLeast r a b)
forall a. a -> Maybe a
Just AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL
  heq AtLeast r a a
ReprAL  AtLeast r a b
ReprAL  = AtLeast r a b -> Maybe (AtLeast r a b)
forall a. a -> Maybe a
Just AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL
  heq AtLeast r a a
NomAL   AtLeast r a b
NomAL   = AtLeast r a b -> Maybe (AtLeast r a b)
forall a. a -> Maybe a
Just AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL
  heq AtLeast r a a
_       AtLeast r a b
_       = Maybe (AtLeast r a b)
Maybe (AtLeast (Strength (AtLeast r a)) a b)
forall a. Maybe a
Nothing

instance (HetEq' f, HetEq' g) => HetEq (Product f g) where
  type Strength (Product f g) = Max (Strength f) (Strength g)
  Pair f a
fx g a
gx heq :: forall (a :: k) (b :: k).
Product f g a
-> Product f g b -> Maybe (AtLeast (Strength (Product f g)) a b)
`heq` Pair f b
fy g b
gy = (AtLeast (Strength f) a b
 -> AtLeast (Strength g) a b
 -> AtLeast
      (OrdCond
         (CmpRole (Strength f) (Strength g))
         (Strength g)
         (Strength g)
         (Strength f))
      a
      b)
-> Maybe (AtLeast (Strength f) a b)
-> Maybe (AtLeast (Strength g) a b)
-> Maybe
     (AtLeast
        (OrdCond
           (CmpRole (Strength f) (Strength g))
           (Strength g)
           (Strength g)
           (Strength f))
        a
        b)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 AtLeast (Strength f) a b
-> AtLeast (Strength g) a b
-> AtLeast (Max (Strength f) (Strength g)) a b
AtLeast (Strength f) a b
-> AtLeast (Strength g) a b
-> AtLeast
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength g)
        (Strength g)
        (Strength f))
     a
     b
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, KnownRole s) =>
AtLeast r a b -> AtLeast s a b -> AtLeast (Max r s) a b
maxAL (f a
fx f a -> f b -> Maybe (AtLeast (Strength f) a b)
forall (a :: k) (b :: k).
f a -> f b -> Maybe (AtLeast (Strength f) a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetEq f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
`heq` f b
fy) (g a
gx g a -> g b -> Maybe (AtLeast (Strength g) a b)
forall (a :: k) (b :: k).
g a -> g b -> Maybe (AtLeast (Strength g) a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetEq f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
`heq` g b
gy)

instance (HetEq' f, HetEq' g) => HetEq (Sum f g) where
  type Strength (Sum f g) = Min (Strength f) (Strength g)
  Sum f g a
sfg1 heq :: forall (a :: k) (b :: k).
Sum f g a -> Sum f g b -> Maybe (AtLeast (Strength (Sum f g)) a b)
`heq` Sum f g b
sfg2 = Role
  (OrdCond
     (CmpRole (Strength f) (Strength g))
     (Strength f)
     (Strength f)
     (Strength g))
-> (KnownRole
      (OrdCond
         (CmpRole (Strength f) (Strength g))
         (Strength f)
         (Strength f)
         (Strength g)) =>
    Maybe
      (AtLeast
         (OrdCond
            (CmpRole (Strength f) (Strength g))
            (Strength f)
            (Strength f)
            (Strength g))
         a
         b))
-> Maybe
     (AtLeast
        (OrdCond
           (CmpRole (Strength f) (Strength g))
           (Strength f)
           (Strength f)
           (Strength g))
        a
        b)
forall (r :: RoleKind) s. Role r -> (KnownRole r => s) -> s
expositRole Sing RoleKind (Min (Strength f) (Strength g))
Role
  (OrdCond
     (CmpRole (Strength f) (Strength g))
     (Strength f)
     (Strength f)
     (Strength g))
mfg case (Sum f g a
sfg1, Sum f g b
sfg2) of
    (InL f a
fx, InL f b
fy) -> case Sing RoleKind (Strength f)
-> Sing RoleKind (Strength g)
-> Proof (Min (Strength f) (Strength g) <= Strength f)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (Min a b <= a)
minDefl1 Sing RoleKind (Strength f)
Role (Strength f)
rf Sing RoleKind (Strength g)
Role (Strength g)
rg of
      OrdCond
  (CmpRole
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     (Strength f))
  'True
  'True
  'False
:~: 'True
Proof (Min (Strength f) (Strength g) <= Strength f)
Refl -> AtLeast (Strength f) a b
-> AtLeast
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     a
     b
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, KnownRole s, r <= s) =>
AtLeast s a b -> AtLeast r a b
weakenAL (AtLeast (Strength f) a b
 -> AtLeast
      (OrdCond
         (CmpRole (Strength f) (Strength g))
         (Strength f)
         (Strength f)
         (Strength g))
      a
      b)
-> Maybe (AtLeast (Strength f) a b)
-> Maybe
     (AtLeast
        (OrdCond
           (CmpRole (Strength f) (Strength g))
           (Strength f)
           (Strength f)
           (Strength g))
        a
        b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
fx f a -> f b -> Maybe (AtLeast (Strength f) a b)
forall (a :: k) (b :: k).
f a -> f b -> Maybe (AtLeast (Strength f) a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetEq f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
`heq` f b
fy
    (InR g a
gx, InR g b
gy) -> case Sing RoleKind (Strength f)
-> Sing RoleKind (Strength g)
-> Proof (Min (Strength f) (Strength g) <= Strength g)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Proof (Min a b <= b)
minDefl2 Sing RoleKind (Strength f)
Role (Strength f)
rf Sing RoleKind (Strength g)
Role (Strength g)
rg of
      OrdCond
  (CmpRole
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     (Strength g))
  'True
  'True
  'False
:~: 'True
Proof (Min (Strength f) (Strength g) <= Strength g)
Refl -> AtLeast (Strength g) a b
-> AtLeast
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     a
     b
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, KnownRole s, r <= s) =>
AtLeast s a b -> AtLeast r a b
weakenAL (AtLeast (Strength g) a b
 -> AtLeast
      (OrdCond
         (CmpRole (Strength f) (Strength g))
         (Strength f)
         (Strength f)
         (Strength g))
      a
      b)
-> Maybe (AtLeast (Strength g) a b)
-> Maybe
     (AtLeast
        (OrdCond
           (CmpRole (Strength f) (Strength g))
           (Strength f)
           (Strength f)
           (Strength g))
        a
        b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g a
gx g a -> g b -> Maybe (AtLeast (Strength g) a b)
forall (a :: k) (b :: k).
g a -> g b -> Maybe (AtLeast (Strength g) a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetEq f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
`heq` g b
gy
    (Sum f g a, Sum f g b)
_                -> Maybe
  (AtLeast
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     a
     b)
forall a. Maybe a
Nothing
   where
    rf :: Role (Strength f)
rf = forall (r :: RoleKind). KnownRole r => Role r
knownRole @(Strength f)
    rg :: Role (Strength g)
rg = forall (r :: RoleKind). KnownRole r => Role r
knownRole @(Strength g)
    mfg :: Sing RoleKind (Min (Strength f) (Strength g))
mfg = Sing RoleKind (Strength f)
-> Sing RoleKind (Strength g)
-> Sing RoleKind (Min (Strength f) (Strength g))
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Min a b)
minTO Sing RoleKind (Strength f)
Role (Strength f)
rf Sing RoleKind (Strength g)
Role (Strength g)
rg

instance (HetEq f, SuperPhantom g) => HetEq (Compose f g) where
  type Strength (Compose f g) = Strength f
  Compose f (g a)
fgx heq :: forall (a :: k) (b :: k).
Compose f g a
-> Compose f g b -> Maybe (AtLeast (Strength (Compose f g)) a b)
`heq` Compose f (g b)
fgy = f (g a)
fgx f (g a) -> f (g b) -> Maybe (AtLeast (Strength f) (g a) (g b))
forall (a :: k) (b :: k).
f a -> f b -> Maybe (AtLeast (Strength f) a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetEq f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
`heq` f (g b)
fgy Maybe (AtLeast (Strength f) (g a) (g b))
-> (AtLeast (Strength f) (g a) (g b) -> AtLeast (Strength f) a b)
-> Maybe (AtLeast (Strength f) a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> AtLeast (Strength f) (g a) (g b) -> AtLeast (Strength f) a b
forall {k1} {k2} (f :: k1 -> k2) (r :: RoleKind) (a :: k1)
       (b :: k1).
SuperPhantom f =>
AtLeast r (f a) (f b) -> AtLeast r a b
innerAL

-- }}}