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

{-#
LANGUAGE
  GADTs, DataKinds, PatternSynonyms, ViewPatterns,
  ExplicitNamespaces, UnboxedTuples
#-}

-- }}}

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

module Data.Hetero.Evidence.AtLeast.Internal (
  AtLeast(AtLeast),
  reflAL,
  transAL,
  hetTransAL,
) where

-- }}}

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

-- GHC/base
import GHC.Exts (Any)

-- base
import Prelude hiding (id, (.))
import Data.Type.Equality ((:~:)(..))
import Data.Type.Ord (Min)
import Control.Category (Category(..))
import Unsafe.Coerce (unsafeCoerce)

-- ord-axiomata
import Data.Type.Ord.Axiomata (type (<=), BoundedAbove(..), Proof)
import Data.Type.Ord.Lemmata (minMono)

-- heterogeneous-comparison
import Data.Hetero.Role (RoleKind, KnownRole(..))
import Data.Hetero.Evidence.Exactly (Exactly(..), hetTransEx, roleEx)

-- }}}

-- --< AtLeast >-- {{{

-- NOTE: This module provides what is morally
--
-- > data AtLeast r a b where
-- >   AtLeast :: r <= s => !(Exactly s a b) -> AtLeast r a b
--
-- but encoded as a newtype with a pattern synonym.
--
-- For an explanation of the techniques used, see:
--   https://gist.github.com/LSLeary/dd52b3086eb153e3c99e578f19eec1ee
--
-- In particular, the 'Existentials' and 'Equality Constaints' sections.

-- | Evidence @AtLeast@ as strong as that 'Exactly' corresponding to a given 'Data.Hetero.Role.Role'.
newtype AtLeast (r :: RoleKind) a b
  = UnsafeAtLeast{ forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> Exactly Any a b
extract :: Exactly Any a b }
type role AtLeast nominal nominal nominal
               -- ^^^^^^^ Necessary for soundness!

{-# INLINE view #-}
view :: AtLeast r a b -> (# Proof (r <= Any), Exactly Any a b #)
view :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> (# Proof (r <= Any), Exactly Any a b #)
view !AtLeast r a b
al = (# ('True :~: 'True)
-> OrdCond (CmpRole r Any) 'True 'True 'False :~: 'True
forall a b. a -> b
unsafeCoerce (forall (a :: Bool). a :~: a
forall {k} (a :: k). a :~: a
Refl @True), AtLeast r a b -> Exactly Any a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> Exactly Any a b
extract AtLeast r a b
al #)
  -- ^ Necessary for soundness!

{-# COMPLETE AtLeast #-}
{-# INLINE   AtLeast #-}
pattern AtLeast :: () => r <= s => Exactly s a b -> AtLeast r a b
pattern $mAtLeast :: forall {r} {k} {r :: RoleKind} {a :: k} {b :: k}.
AtLeast r a b
-> (forall {s :: RoleKind}. (r <= s) => Exactly s a b -> r)
-> ((# #) -> r)
-> r
$bAtLeast :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast x <- (view -> (# Refl, x #))
  where AtLeast Exactly s a b
x = Exactly Any a b -> AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly Any a b -> AtLeast r a b
UnsafeAtLeast (Exactly s a b -> Exactly Any a b
forall a b. a -> b
unsafeCoerce Exactly s a b
x)

-- }}}

-- --< AtLeast: Instances & Deps >-- {{{

instance KnownRole r => Category (AtLeast r) where
  id :: forall (a :: k). AtLeast r a a
id  = AtLeast r a a
forall {k} (r :: RoleKind) (a :: k). KnownRole r => AtLeast r a a
reflAL
  . :: forall (b :: k) (c :: k) (a :: k).
AtLeast r b c -> AtLeast r a b -> AtLeast r a c
(.) = (AtLeast r a b -> AtLeast r b c -> AtLeast r a c)
-> AtLeast r b c -> AtLeast r a b -> AtLeast r a c
forall a b c. (a -> b -> c) -> b -> a -> c
flip AtLeast r a b -> AtLeast r b c -> AtLeast r a c
forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
KnownRole r =>
AtLeast r a b -> AtLeast r b c -> AtLeast r a c
transAL

-- | Reflexivity.
reflAL :: forall r a. KnownRole r => AtLeast r a a
reflAL :: forall {k} (r :: RoleKind) (a :: k). KnownRole r => AtLeast r a a
reflAL = case Sing RoleKind r -> Proof (r <= 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 (forall (r :: RoleKind). KnownRole r => Role r
knownRole @r) of
  OrdCond (CmpRole r Nominal) 'True 'True 'False :~: 'True
Proof (r <= UpperBound RoleKind)
Refl -> Exactly Nominal a a -> AtLeast r a a
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast Exactly Nominal a a
forall {k} (a :: k). Exactly Nominal a a
NomEx

-- | 'Data.Hetero.Role.Role'-homogeneous transitivity.
transAL :: KnownRole r => AtLeast r a b -> AtLeast r b c -> AtLeast r a c
transAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k) (c :: k).
KnownRole r =>
AtLeast r a b -> AtLeast r b c -> AtLeast r a c
transAL = AtLeast r a b -> AtLeast r b c -> AtLeast r a c
AtLeast r a b -> AtLeast r b c -> AtLeast (Min r r) a c
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k)
       (c :: k).
(KnownRole r, KnownRole s) =>
AtLeast r a b -> AtLeast s b c -> AtLeast (Min r s) a c
hetTransAL

{- |

t'AtLeast' is a category graded by the 'Min' monoid on 'RoleKind' with identity:

@
'Data.Hetero.Evidence.AtLeast.NomAL' :: t'AtLeast' t'Data.Hetero.Role.Nominal' a a
@

-}
hetTransAL
  :: forall r s a b c
  .  (KnownRole r, KnownRole s)
  => AtLeast r a b -> AtLeast s b c {- ^ -}
  -> AtLeast (Min r s) a c
hetTransAL :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k)
       (c :: k).
(KnownRole r, KnownRole s) =>
AtLeast r a b -> AtLeast s b c -> AtLeast (Min r s) a c
hetTransAL (AtLeast Exactly s a b
e1) (AtLeast Exactly s b c
e2) = case Sing RoleKind r
-> Sing RoleKind s
-> Sing RoleKind s
-> Sing RoleKind s
-> Proof (Min r s <= Min s s)
forall o (a :: o) (c :: o) (b :: o) (d :: o).
(TotalOrder o, a <= c, b <= d) =>
Sing o a
-> Sing o b -> Sing o c -> Sing o d -> Proof (Min a b <= Min c d)
minMono Sing RoleKind r
Role r
r Sing RoleKind s
Role s
s Sing RoleKind s
Role s
t Sing RoleKind s
Role s
u of
  OrdCond
  (CmpRole
     (OrdCond (CmpRole r s) r r s) (OrdCond (CmpRole s s) s s s))
  'True
  'True
  'False
:~: 'True
Proof (Min r s <= Min s s)
Refl -> Exactly (OrdCond (CmpRole s s) s s s) a c
-> AtLeast (OrdCond (CmpRole r s) r r s) a c
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast (Exactly s a b -> Exactly s b c -> Exactly (Min s s) a c
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k)
       (c :: k).
Exactly r a b -> Exactly s b c -> Exactly (Min r s) a c
hetTransEx Exactly s a b
e1 Exactly s b c
e2)
 where
  r :: Role r
r = forall (r :: RoleKind). KnownRole r => Role r
knownRole @r
  s :: Role s
s = forall (r :: RoleKind). KnownRole r => Role r
knownRole @s
  t :: Role s
t = Exactly s a b -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s a b
e1
  u :: Role s
u = Exactly s b c -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s b c
e2

-- }}}