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

{-# LANGUAGE GADTs, QuantifiedConstraints, UndecidableInstances #-}

{- |

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

Heterogeneous comparison with evidence capture.

-}

-- }}}

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

module Data.Hetero.Ord (

  -- * HetOrdering
  HetOrdering(..),
  mapHO, bindHO,

  -- * HetOrd
  HetOrd(..), HetOrd',
  defaultHEq, hcompareVia,

) where

-- }}}

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

-- GHC/base
import GHC.TypeLits (SNat, fromSNat, SSymbol, fromSSymbol, SChar, fromSChar)

-- base
import Type.Reflection (TypeRep, SomeTypeRep(..))
import Data.Kind (Type, Constraint)
import Data.Type.Equality ((:~:)(..), (:~~:)(..))
import Data.Type.Ord (OrderingI(..))
import Data.Type.Coercion (Coercion(..))
import Data.Proxy (Proxy(..))
import Data.Functor.Const (Const(..))
import Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))
import Data.Functor.Compose (Compose(..))

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

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

-- }}}

-- --< HetOrdering >-- {{{

-- | 'Ordering' with captured evidence.
data HetOrdering r a b = HLT | HEQ (AtLeast r a b) | HGT

-- | Map over the contained @t'AtLeast' r a b@.
mapHO
  :: (AtLeast r a b -> AtLeast s c d) {- ^ -}
  -> HetOrdering r a b -> HetOrdering s c d
mapHO :: forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
(AtLeast r a b -> AtLeast s c d)
-> HetOrdering r a b -> HetOrdering s c d
mapHO AtLeast r a b -> AtLeast s c d
f HetOrdering r a b
ro = HetOrdering r a b
-> (AtLeast r a b -> HetOrdering s c d) -> HetOrdering s c d
forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
HetOrdering r a b
-> (AtLeast r a b -> HetOrdering s c d) -> HetOrdering s c d
bindHO HetOrdering r a b
ro (AtLeast s c d -> HetOrdering s c d
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ (AtLeast s c d -> HetOrdering s c d)
-> (AtLeast r a b -> AtLeast s c d)
-> AtLeast r a b
-> HetOrdering s c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtLeast r a b -> AtLeast s c d
f)

-- | Bind the contained @t'AtLeast' r a b@.
bindHO
  :: HetOrdering r a b {- ^ -}
  -> (AtLeast r a b -> HetOrdering s c d)
  -> HetOrdering s c d
bindHO :: forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
HetOrdering r a b
-> (AtLeast r a b -> HetOrdering s c d) -> HetOrdering s c d
bindHO  HetOrdering r a b
HLT     AtLeast r a b -> HetOrdering s c d
_ = HetOrdering s c d
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
bindHO (HEQ AtLeast r a b
eq) AtLeast r a b -> HetOrdering s c d
f = AtLeast r a b -> HetOrdering s c d
f AtLeast r a b
eq
bindHO  HetOrdering r a b
HGT     AtLeast r a b -> HetOrdering s c d
_ = HetOrdering s c d
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT

-- }}}

-- --< HetOrd >-- {{{

-- | Heterogeneous comparison with evidence capture of type equivalence.
class HetEq f => HetOrd f where
  -- | Compare an @f a@ and an @f b@, opportunistically capturing the strongest
  --   type-equivalence evidence we can given the arguments.
  hcompare :: f a -> f b -> HetOrdering (Strength f) a b

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

instance HetOrd Proxy where
  hcompare :: forall (a :: k) (b :: k).
Proxy a -> Proxy b -> HetOrdering (Strength Proxy) a b
hcompare Proxy a
Proxy Proxy b
Proxy = AtLeast Phantom a b -> HetOrdering Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL

instance Ord a => HetOrd (Const a) where
  hcompare :: forall (a :: k) (b :: k).
Const a a -> Const a b -> HetOrdering (Strength (Const a)) a b
hcompare (Const a
x) (Const a
y) = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
    Ordering
LT -> HetOrdering Phantom a b
HetOrdering (Strength (Const a)) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
    Ordering
EQ -> AtLeast Phantom a b -> HetOrdering Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL
    Ordering
GT -> HetOrdering Phantom a b
HetOrdering (Strength (Const a)) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT

instance HetOrd (Coercion a) where hcompare :: forall (a :: k) (b :: k).
Coercion a a
-> Coercion a b -> HetOrdering (Strength (Coercion a)) a b
hcompare Coercion a a
Coercion Coercion a b
Coercion = AtLeast Representational a b -> HetOrdering Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL
instance HetOrd ((:~:)    a) where hcompare :: forall (a :: k) (b :: k).
(a :~: a) -> (a :~: b) -> HetOrdering (Strength ((:~:) a)) a b
hcompare a :~: a
Refl     a :~: b
Refl     = AtLeast Nominal a b -> HetOrdering Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL
instance HetOrd ((:~~:)   a) where hcompare :: forall (a :: k) (b :: k).
(a :~~: a) -> (a :~~: b) -> HetOrdering (Strength ((:~~:) a)) a b
hcompare a :~~: a
HRefl    a :~~: b
HRefl    = AtLeast Nominal a b -> HetOrdering Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL

instance HetOrd TypeRep where hcompare :: forall (a :: k) (b :: k).
TypeRep a -> TypeRep b -> HetOrdering (Strength TypeRep) a b
hcompare = (forall (x :: k). TypeRep x -> SomeTypeRep)
-> TypeRep a -> TypeRep b -> HetOrdering (Strength TypeRep) a b
forall {k} (f :: k -> *) y (a :: k) (b :: k).
(HetEq f, Ord y) =>
(forall (x :: k). f x -> y)
-> f a -> f b -> HetOrdering (Strength f) a b
hcompareVia TypeRep x -> SomeTypeRep
forall (x :: k). TypeRep x -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
SomeTypeRep
instance HetOrd SNat    where hcompare :: forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> HetOrdering (Strength SNat) a b
hcompare = (forall (x :: Nat). SNat x -> Integer)
-> SNat a -> SNat b -> HetOrdering (Strength SNat) a b
forall {k} (f :: k -> *) y (a :: k) (b :: k).
(HetEq f, Ord y) =>
(forall (x :: k). f x -> y)
-> f a -> f b -> HetOrdering (Strength f) a b
hcompareVia SNat x -> Integer
forall (x :: Nat). SNat x -> Integer
fromSNat
instance HetOrd SSymbol where hcompare :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> HetOrdering (Strength SSymbol) a b
hcompare = (forall (x :: Symbol). SSymbol x -> String)
-> SSymbol a -> SSymbol b -> HetOrdering (Strength SSymbol) a b
forall {k} (f :: k -> *) y (a :: k) (b :: k).
(HetEq f, Ord y) =>
(forall (x :: k). f x -> y)
-> f a -> f b -> HetOrdering (Strength f) a b
hcompareVia SSymbol x -> String
forall (x :: Symbol). SSymbol x -> String
fromSSymbol
instance HetOrd SChar   where hcompare :: forall (a :: Char) (b :: Char).
SChar a -> SChar b -> HetOrdering (Strength SChar) a b
hcompare = (forall (x :: Char). SChar x -> Char)
-> SChar a -> SChar b -> HetOrdering (Strength SChar) a b
forall {k} (f :: k -> *) y (a :: k) (b :: k).
(HetEq f, Ord y) =>
(forall (x :: k). f x -> y)
-> f a -> f b -> HetOrdering (Strength f) a b
hcompareVia SChar x -> Char
forall (x :: Char). SChar x -> Char
fromSChar

instance HetOrd Role where
  hcompare :: forall (a :: RoleKind) (b :: RoleKind).
Role a -> Role b -> HetOrdering (Strength Role) a b
hcompare Role a
r Role b
s = case Sing RoleKind a
Role a
r Sing RoleKind a -> Sing RoleKind b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a -> Sing RoleKind b -> OrderingI a b
<|=|> Sing RoleKind b
Role b
s of
    OrderingI a b
LTI -> HetOrdering Nominal a b
HetOrdering (Strength Role) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
    OrderingI a b
EQI -> AtLeast Nominal a b -> HetOrdering Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL
    OrderingI a b
GTI -> HetOrdering Nominal a b
HetOrdering (Strength Role) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT

instance HetOrd (Exactly r a) where
  hcompare :: forall (a :: k) (b :: k).
Exactly r a a
-> Exactly r a b -> HetOrdering (Strength (Exactly r a)) a b
hcompare Exactly r a a
PhantEx Exactly r a b
PhantEx = AtLeast Phantom a b -> HetOrdering Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Phantom a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL
  hcompare Exactly r a a
ReprEx  Exactly r a b
ReprEx  = AtLeast Representational a b -> HetOrdering Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Representational a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL
  hcompare Exactly r a a
NomEx   Exactly r a b
NomEx   = AtLeast Nominal a b -> HetOrdering Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast Nominal a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL

instance HetOrd (AtLeast r a) where
  hcompare :: forall (a :: k) (b :: k).
AtLeast r a a
-> AtLeast r a b -> HetOrdering (Strength (AtLeast r a)) a b
hcompare AtLeast r a a
PhantAL AtLeast r a b
PhantAL = AtLeast r a b -> HetOrdering r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL
  hcompare AtLeast r a a
PhantAL AtLeast r a b
_       = HetOrdering r a b
HetOrdering (Strength (AtLeast r a)) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
  hcompare AtLeast r a a
ReprAL  AtLeast r a b
PhantAL = HetOrdering r a b
HetOrdering (Strength (AtLeast r a)) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT
  hcompare AtLeast r a a
ReprAL  AtLeast r a b
ReprAL  = AtLeast r a b -> HetOrdering r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL
  hcompare AtLeast r a a
ReprAL  AtLeast r a b
NomAL   = HetOrdering r a b
HetOrdering (Strength (AtLeast r a)) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
  hcompare AtLeast r a a
NomAL   AtLeast r a b
NomAL   = AtLeast r a b -> HetOrdering r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL
  hcompare AtLeast r a a
NomAL   AtLeast r a b
_       = HetOrdering r a b
HetOrdering (Strength (AtLeast r a)) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT

instance (HetOrd' f, HetOrd' g) => HetOrd (Product f g) where
  Pair f a
fx g a
gx hcompare :: forall (a :: k) (b :: k).
Product f g a
-> Product f g b -> HetOrdering (Strength (Product f g)) a b
`hcompare` Pair f b
fy g b
gy = HetOrdering (Strength f) a b
-> (AtLeast (Strength f) a b
    -> HetOrdering
         (OrdCond
            (CmpRole (Strength f) (Strength g))
            (Strength g)
            (Strength g)
            (Strength f))
         a
         b)
-> HetOrdering
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength g)
        (Strength g)
        (Strength f))
     a
     b
forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
HetOrdering r a b
-> (AtLeast r a b -> HetOrdering s c d) -> HetOrdering s c d
bindHO (f a
fx f a -> f b -> HetOrdering (Strength f) a b
forall (a :: k) (b :: k).
f a -> f b -> HetOrdering (Strength f) a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> HetOrdering (Strength f) a b
`hcompare` f b
fy) \AtLeast (Strength f) a b
eqf ->
    (AtLeast (Strength g) a b
 -> AtLeast
      (OrdCond
         (CmpRole (Strength f) (Strength g))
         (Strength g)
         (Strength g)
         (Strength f))
      a
      b)
-> HetOrdering (Strength g) a b
-> HetOrdering
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength g)
        (Strength g)
        (Strength f))
     a
     b
forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
(AtLeast r a b -> AtLeast s c d)
-> HetOrdering r a b -> HetOrdering s c d
mapHO (AtLeast (Strength f) a b
-> AtLeast (Strength g) a b
-> AtLeast (Max (Strength f) (Strength g)) 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 AtLeast (Strength f) a b
eqf) (g a
gx g a -> g b -> HetOrdering (Strength g) a b
forall (a :: k) (b :: k).
g a -> g b -> HetOrdering (Strength g) a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> HetOrdering (Strength f) a b
`hcompare` g b
gy)

instance (HetOrd' f, HetOrd' g) => HetOrd (Sum f g) where
  hcompare :: forall (a :: k) (b :: k).
Sum f g a -> Sum f g b -> HetOrdering (Strength (Sum f g)) a b
hcompare = 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)) =>
    Sum f g a
    -> Sum f g b
    -> HetOrdering
         (OrdCond
            (CmpRole (Strength f) (Strength g))
            (Strength f)
            (Strength f)
            (Strength g))
         a
         b)
-> Sum f g a
-> Sum f g b
-> HetOrdering
     (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
    InL f a
fx -> \case
      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)
-> HetOrdering (Strength f) a b
-> HetOrdering
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     a
     b
forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
(AtLeast r a b -> AtLeast s c d)
-> HetOrdering r a b -> HetOrdering s c d
mapHO 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 (f a
fx f a -> f b -> HetOrdering (Strength f) a b
forall (a :: k) (b :: k).
f a -> f b -> HetOrdering (Strength f) a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> HetOrdering (Strength f) a b
`hcompare` f b
fy)
      InR g b
_  -> HetOrdering
  (OrdCond
     (CmpRole (Strength f) (Strength g))
     (Strength f)
     (Strength f)
     (Strength g))
  a
  b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
    InR g a
gx -> \case
      InL f b
_  -> HetOrdering
  (OrdCond
     (CmpRole (Strength f) (Strength g))
     (Strength f)
     (Strength f)
     (Strength g))
  a
  b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT
      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)
-> HetOrdering (Strength g) a b
-> HetOrdering
     (OrdCond
        (CmpRole (Strength f) (Strength g))
        (Strength f)
        (Strength f)
        (Strength g))
     a
     b
forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
(AtLeast r a b -> AtLeast s c d)
-> HetOrdering r a b -> HetOrdering s c d
mapHO 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 (g a
gx g a -> g b -> HetOrdering (Strength g) a b
forall (a :: k) (b :: k).
g a -> g b -> HetOrdering (Strength g) a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> HetOrdering (Strength f) a b
`hcompare` g b
gy)
   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 (HetOrd f, SuperPhantom g) => HetOrd (Compose f g) where
  Compose f (g a)
fgx hcompare :: forall (a :: k) (b :: k).
Compose f g a
-> Compose f g b -> HetOrdering (Strength (Compose f g)) a b
`hcompare` Compose f (g b)
fgy
    = (AtLeast (Strength f) (g a) (g b) -> AtLeast (Strength f) a b)
-> HetOrdering (Strength f) (g a) (g b)
-> HetOrdering (Strength f) a b
forall {k} {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind)
       (c :: k) (d :: k).
(AtLeast r a b -> AtLeast s c d)
-> HetOrdering r a b -> HetOrdering s c d
mapHO 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 (f (g a)
fgx f (g a) -> f (g b) -> HetOrdering (Strength f) (g a) (g b)
forall (a :: k) (b :: k).
f a -> f b -> HetOrdering (Strength f) a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> HetOrdering (Strength f) a b
`hcompare` f (g b)
fgy)

-- | A default implementation of 'heq' in terms of 'hcompare'.
defaultHEq :: HetOrd f => f a -> f b -> Maybe (AtLeast (Strength f) a b)
defaultHEq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> Maybe (AtLeast (Strength f) a b)
defaultHEq f a
fx f b
fy = case f a
fx f a -> f b -> HetOrdering (Strength f) a b
forall (a :: k) (b :: k).
f a -> f b -> HetOrdering (Strength f) a b
forall {k} (f :: k -> *) (a :: k) (b :: k).
HetOrd f =>
f a -> f b -> HetOrdering (Strength f) a b
`hcompare` f b
fy of
  HEQ AtLeast (Strength f) a b
eq -> AtLeast (Strength f) a b -> Maybe (AtLeast (Strength f) a b)
forall a. a -> Maybe a
Just AtLeast (Strength f) a b
eq
  HetOrdering (Strength f) a b
_      -> Maybe (AtLeast (Strength f) a b)
forall a. Maybe a
Nothing

-- | An implementation of 'hcompare' in terms of 'heq' and a strictly increasing /unifier/.
hcompareVia
  :: (HetEq f, Ord y)
  => (forall x. f x -> y) -> f a -> f b {- ^ -}
  -> HetOrdering (Strength f) a b
hcompareVia :: forall {k} (f :: k -> *) y (a :: k) (b :: k).
(HetEq f, Ord y) =>
(forall (x :: k). f x -> y)
-> f a -> f b -> HetOrdering (Strength f) a b
hcompareVia forall (x :: k). f x -> y
unify f a
fx f b
fy = case y -> y -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (f a -> y
forall (x :: k). f x -> y
unify f a
fx) (f b -> y
forall (x :: k). f x -> y
unify f b
fy) of
  Ordering
LT -> HetOrdering (Strength f) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HLT
  Ordering
EQ -> AtLeast (Strength f) a b -> HetOrdering (Strength f) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> HetOrdering r a b
HEQ case 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 of
    Just AtLeast (Strength f) a b
eq -> AtLeast (Strength f) a b
eq
    Maybe (AtLeast (Strength f) a b)
Nothing -> String -> AtLeast (Strength f) a b
forall a. HasCallStack => String -> a
error String
"hcompareVia: bad unifier."
  Ordering
GT -> HetOrdering (Strength f) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k). HetOrdering r a b
HGT

-- }}}