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

{-#
LANGUAGE
  TypeData, DataKinds, TypeFamilies, QuantifiedConstraints, ImpredicativeTypes
#-}

{- |

Description : Singleton t'Data.Hetero.Role.Role's and corresponding constraints
Copyright   : (c) L. S. Leary, 2025

Singleton 'Role's and corresponding constraints.

-}

-- }}}

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

module Data.Hetero.Role (

  -- * Roles
  RoleKind(..), Role(..),
  KnownRole(..), expositRole,

  -- ** Constraints
  IsPhantom,
  IsRepresentational,
  IsNominal,
  SubNominal,
  SuperPhantom,

) where

-- }}}

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

-- GHC/base
import GHC.Exts (withDict)
-- base
import Data.Kind (Constraint)
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Type.Ord (Compare, OrderingI(..))
import Data.Coerce (Coercible)

-- ord-axiomata,
import Data.Type.Ord.Axiomata
  (Sing, Equivalence(..), TotalOrder(..), BoundedBelow(..), BoundedAbove(..))

-- }}}

-- --< Roles >-- {{{

-- | The kind of [/roles/](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/roles.html).
type data RoleKind = Phantom | Representational | Nominal

-- | Singleton roles.
data Role (r :: RoleKind) where
  Phantom          :: Role Phantom
  Representational :: Role Representational
  Nominal          :: Role Nominal

type instance Sing RoleKind = Role

type family CmpRole (a :: RoleKind) (b :: RoleKind) :: Ordering where
  CmpRole r       r       = EQ
  CmpRole Phantom _       = LT
  CmpRole Nominal _       = GT
  CmpRole _       Phantom = GT
  CmpRole _       Nominal = LT

type instance Compare @RoleKind a b = CmpRole a b

instance Equivalence RoleKind where
  Sing RoleKind a
Role a
Phantom          =? :: forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a
-> Sing RoleKind b -> Either ((a :~: b) -> Void) (a :~: b)
=? Sing RoleKind b
Role b
Phantom          = (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  Sing RoleKind a
Role a
Representational =? Sing RoleKind b
Role b
Representational = (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  Sing RoleKind a
Role a
Nominal          =? Sing RoleKind b
Role b
Nominal          = (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  Sing RoleKind a
_                =? Sing RoleKind b
_                = ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left \case{}

  refl :: forall (a :: RoleKind). Sing RoleKind a -> Proof (a == a)
refl Sing RoleKind a
_ = 'EQ :~: 'EQ
Proof (Compare a a ~ 'EQ)
forall {k} (a :: k). a :~: a
Refl

  sub :: forall (a :: RoleKind) (b :: RoleKind).
(a == b) =>
Sing RoleKind a -> Sing RoleKind b -> a :~: b
sub Sing RoleKind a
Role a
Phantom          Sing RoleKind b
Role b
Phantom          = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  sub Sing RoleKind a
Role a
Representational Sing RoleKind b
Role b
Representational = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  sub Sing RoleKind a
Role a
Nominal          Sing RoleKind b
Role b
Nominal          = a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance TotalOrder RoleKind where
  <|=|> :: forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a -> Sing RoleKind b -> OrderingI a b
(<|=|>) = \case
    Sing RoleKind a
Role a
Phantom          -> \case
      Sing RoleKind b
Role b
Phantom          -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
      Sing RoleKind b
Role b
Representational -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
      Sing RoleKind b
Role b
Nominal          -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
    Sing RoleKind a
Role a
Representational -> \case
      Sing RoleKind b
Role b
Phantom          -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
      Sing RoleKind b
Role b
Representational -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
      Sing RoleKind b
Role b
Nominal          -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
    Sing RoleKind a
Role a
Nominal          -> \case
      Sing RoleKind b
Role b
Phantom          -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
      Sing RoleKind b
Role b
Representational -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI
      Sing RoleKind b
Role b
Nominal          -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI

  transLeq :: forall (a :: RoleKind) (b :: RoleKind) (c :: RoleKind).
(a <= b, b <= c) =>
Sing RoleKind a
-> Sing RoleKind b -> Sing RoleKind c -> Proof (a <= c)
transLeq Sing RoleKind a
Role a
Phantom          Sing RoleKind b
_                Sing RoleKind c
t                = Sing RoleKind c -> Proof (LowerBound RoleKind <= c)
forall o (a :: o).
BoundedBelow o =>
Sing o a -> Proof (LowerBound o <= a)
forall (a :: RoleKind).
Sing RoleKind a -> Proof (LowerBound RoleKind <= a)
least Sing RoleKind c
t
  transLeq Sing RoleKind a
r                Sing RoleKind b
_                Sing RoleKind c
Role c
Nominal          = Sing RoleKind a -> Proof (a <= UpperBound RoleKind)
forall o (a :: o).
BoundedAbove o =>
Sing o a -> Proof (a <= UpperBound o)
forall (a :: RoleKind).
Sing RoleKind a -> Proof (a <= UpperBound RoleKind)
greatest Sing RoleKind a
r
  transLeq Sing RoleKind a
Role a
Representational Sing RoleKind b
Role b
Representational Sing RoleKind c
Role c
Representational = 'True :~: 'True
Proof (OrdCond (Compare a c) 'True 'True 'False ~ 'True)
forall {k} (a :: k). a :~: a
Refl
  transLeq Sing RoleKind a
r                Sing RoleKind b
s                Sing RoleKind c
t                = case Sing RoleKind a
r of
    Sing RoleKind a
Role a
Representational -> case Sing RoleKind b
s of -- b
      Sing RoleKind b
Role b
Nominal -> case Sing RoleKind c
t of        -- r
    Sing RoleKind a
Role a
Nominal          -> case Sing RoleKind b
s of -- u
      Sing RoleKind b
Role b
Nominal -> case Sing RoleKind c
t of        -- h

  antiSym :: forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a
-> Sing RoleKind b -> Compare a b :~: Reflect (Compare b a)
antiSym = \case
    Sing RoleKind a
Role a
Phantom          -> \case
      Sing RoleKind b
Role b
Phantom          -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
      Sing RoleKind b
Role b
Representational -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
      Sing RoleKind b
Role b
Nominal          -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
    Sing RoleKind a
Role a
Representational -> \case
      Sing RoleKind b
Role b
Phantom          -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
      Sing RoleKind b
Role b
Representational -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
      Sing RoleKind b
Role b
Nominal          -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
    Sing RoleKind a
Role a
Nominal          -> \case
      Sing RoleKind b
Role b
Phantom          -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
      Sing RoleKind b
Role b
Representational -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl
      Sing RoleKind b
Role b
Nominal          -> Compare a b :~: Compare a b
Compare a b :~: Reflect (Compare b a)
forall {k} (a :: k). a :~: a
Refl

instance BoundedBelow RoleKind where
  type LowerBound RoleKind = Phantom
  lowerBound :: Sing RoleKind (LowerBound RoleKind)
lowerBound = Sing RoleKind (LowerBound RoleKind)
Role Phantom
Phantom
  least :: forall (a :: RoleKind).
Sing RoleKind a -> Proof (LowerBound RoleKind <= a)
least = \case
    Sing RoleKind a
Role a
Phantom          -> 'True :~: 'True
Proof (LowerBound RoleKind <= a)
forall {k} (a :: k). a :~: a
Refl
    Sing RoleKind a
Role a
Representational -> 'True :~: 'True
Proof (LowerBound RoleKind <= a)
forall {k} (a :: k). a :~: a
Refl
    Sing RoleKind a
Role a
Nominal          -> 'True :~: 'True
Proof (LowerBound RoleKind <= a)
forall {k} (a :: k). a :~: a
Refl

instance BoundedAbove RoleKind where
  type UpperBound RoleKind = Nominal
  upperBound :: Sing RoleKind (UpperBound RoleKind)
upperBound = Sing RoleKind (UpperBound RoleKind)
Role Nominal
Nominal
  greatest :: forall (a :: RoleKind).
Sing RoleKind a -> Proof (a <= UpperBound RoleKind)
greatest = \case
    Sing RoleKind a
Role a
Phantom          -> 'True :~: 'True
Proof (a <= UpperBound RoleKind)
forall {k} (a :: k). a :~: a
Refl
    Sing RoleKind a
Role a
Representational -> 'True :~: 'True
Proof (a <= UpperBound RoleKind)
forall {k} (a :: k). a :~: a
Refl
    Sing RoleKind a
Role a
Nominal          -> 'True :~: 'True
Proof (a <= UpperBound RoleKind)
forall {k} (a :: k). a :~: a
Refl

instance TestEquality Role where
  testEquality :: forall (a :: RoleKind) (b :: RoleKind).
Role a -> Role b -> Maybe (a :~: b)
testEquality Role a
r Role b
s = (((a :~: b) -> Void) -> Maybe (a :~: b))
-> ((a :~: b) -> Maybe (a :~: b))
-> Either ((a :~: b) -> Void) (a :~: b)
-> Maybe (a :~: b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (a :~: b) -> ((a :~: b) -> Void) -> Maybe (a :~: b)
forall a b. a -> b -> a
const Maybe (a :~: b)
forall a. Maybe a
Nothing) (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just (Sing RoleKind a
Role a
r Sing RoleKind a
-> Sing RoleKind b -> Either ((a :~: b) -> Void) (a :~: b)
forall e (a :: e) (b :: e).
Equivalence e =>
Sing e a -> Sing e b -> Either ((a :~: b) -> Void) (a :~: b)
forall (a :: RoleKind) (b :: RoleKind).
Sing RoleKind a
-> Sing RoleKind b -> Either ((a :~: b) -> Void) (a :~: b)
=? Sing RoleKind b
Role b
s)

-- | Get the unique value corresponding to a 'RoleKind'.
class    KnownRole r                where knownRole :: Role r
instance KnownRole Phantom          where knownRole :: Role Phantom
knownRole = Role Phantom
Phantom
instance KnownRole Representational where knownRole :: Role Representational
knownRole = Role Representational
Representational
instance KnownRole Nominal          where knownRole :: Role Nominal
knownRole = Role Nominal
Nominal

-- | Make a 'Role' known.
expositRole :: Role r -> (KnownRole r => s) -> s
expositRole :: forall (r :: RoleKind) s. Role r -> (KnownRole r => s) -> s
expositRole = Role r -> (KnownRole r => s) -> s
forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
forall r. Role r -> (KnownRole r => r) -> r
withDict

-- }}}

-- --< Roles: Constraints >-- {{{

type IsPhantom :: (k -> l) -> Constraint
type IsPhantom f = forall x y. Coercible (f x) (f y)

type IsRepresentational :: (k -> l) -> Constraint
type IsRepresentational f = (SubNominal f, SuperPhantom f)

type IsNominal :: (k -> l) -> Constraint
type IsNominal f = forall x y. Coercible (f x) (f y) => x ~ y

type SuperPhantom :: (k -> l) -> Constraint
type SuperPhantom f = forall x y. Coercible (f x) (f y) => Coercible x y

type SubNominal :: (k -> l) -> Constraint
type SubNominal f = forall x y. Coercible x y => Coercible (f x) (f y)

-- }}}