{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeData #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_HADDOCK hide #-}

module Control.Monad.Borrow.Pure.Lifetime.Internal (
  module Control.Monad.Borrow.Pure.Lifetime.Internal,
) where

import Control.DeepSeq (NFData (..))
import Data.Kind
import GHC.TypeLits hiding (type (<=))

infixr 3 /\, :/\

-- | The meet of the two lifetimes. It is the longest lifetime that is shorter than both of them.
type (/\) = (:/\)

-- NOTE:  We want to use @TypeData@ extension for Lifetime, but it makes Haddock panic!

-- Lifetime is a free bounded lower semilattice generated by atomic lifetimes.

-- | The kind (type) of lifetimes.
data Lifetime = Al Nat | Lifetime :/\ Lifetime | Static

type Al = 'Al

-- | 'Static' lifetime, which lives forever and 'Control.Monad.Borrow.Pure.Lifetime.Token.neverEnds'.
type Static = 'Static

infix 2 <=, <=!, <=!!

type Witness :: Lifetime -> Lifetime -> Type
data Witness a b where
  Inf :: Witness a b -> Witness a c -> Witness a (b /\ c)
  Top :: Witness a Static
  Inherit' :: Witness' a b -> Witness a b

instance NFData (Witness a b) where
  rnf :: Witness a b -> ()
rnf (Inf Witness a b
a Witness a c
b) = Witness a b -> ()
forall a. NFData a => a -> ()
rnf Witness a b
a () -> () -> ()
forall a b. a -> b -> b
`seq` Witness a c -> ()
forall a. NFData a => a -> ()
rnf Witness a c
b
  rnf Witness a b
Top = ()
  rnf (Inherit' Witness' a b
w) = Witness' a b -> ()
forall a. NFData a => a -> ()
rnf Witness' a b
w

deriving instance Show (Witness a b)

type Witness' :: Lifetime -> Lifetime -> Type
data Witness' a b where
  AssocR :: Witness' (a /\ (b /\ c)) d -> Witness' ((a /\ b) /\ c) d
  Inherit'' :: Witness'' a b -> Witness' a b

instance NFData (Witness' a b) where
  rnf :: Witness' a b -> ()
rnf (AssocR Witness' (a /\ (b /\ c)) b
w) = Witness' (a /\ (b /\ c)) b -> ()
forall a. NFData a => a -> ()
rnf Witness' (a /\ (b /\ c)) b
w
  rnf (Inherit'' Witness'' a b
w) = Witness'' a b -> ()
forall a. NFData a => a -> ()
rnf Witness'' a b
w

deriving instance Show (Witness' a b)

type Witness'' :: Lifetime -> Lifetime -> Type
data Witness'' a b where
  Reflect :: Witness'' a a
  InfL :: Witness'' (a /\ b) a
  InfIntroL :: Witness' b c -> Witness'' (a /\ b) c

instance NFData (Witness'' a b) where
  rnf :: Witness'' a b -> ()
rnf Witness'' a b
Reflect = ()
  rnf Witness'' a b
InfL = ()
  rnf (InfIntroL Witness' b b
w) = Witness' b b -> ()
forall a. NFData a => a -> ()
rnf Witness' b b
w

deriving instance Show (Witness'' a b)

type (<=) :: Lifetime -> Lifetime -> Constraint
class α <= β where
  -- | The witness of the relation.
  witness :: Witness α β

-- | Flipped version of '<='.
type (>=) :: Lifetime -> Lifetime -> Constraint
type α >= β = β <= α

instance (α <= β, α <= γ) => α <= β /\ γ where
  witness :: Witness α (β /\ γ)
witness = Witness α β -> Witness α γ -> Witness α (β /\ γ)
forall (a :: Lifetime) (b :: Lifetime) (a :: Lifetime).
Witness a b -> Witness a a -> Witness a (b /\ a)
Inf Witness α β
forall (α :: Lifetime) (β :: Lifetime). (α <= β) => Witness α β
witness Witness α γ
forall (α :: Lifetime) (β :: Lifetime). (α <= β) => Witness α β
witness
  {-# NOINLINE witness #-}

instance α <= Static where
  witness :: Witness α 'Static
witness = Witness α 'Static
forall (α :: Lifetime). Witness α 'Static
Top
  {-# NOINLINE witness #-}

instance {-# INCOHERENT #-} (α <=! β) => α <= β where
  witness :: Witness α β
witness = Witness' α β -> Witness α β
forall (a :: Lifetime) (b :: Lifetime). Witness' a b -> Witness a b
Inherit' Witness' α β
forall (α :: Lifetime) (β :: Lifetime). (α <=! β) => Witness' α β
witness'
  {-# NOINLINE witness #-}

type (<=!) :: Lifetime -> Lifetime -> Constraint
class α <=! β where
  -- | The witness of the relation.
  witness' :: Witness' α β

instance (α /\ (β /\ γ) <=! δ) => (α /\ β) /\ γ <=! δ where
  witness' :: Witness' ((α /\ β) /\ γ) δ
witness' = Witness' (α /\ (β /\ γ)) δ -> Witness' ((α /\ β) /\ γ) δ
forall (b :: Lifetime) (a :: Lifetime) (c :: Lifetime)
       (d :: Lifetime).
Witness' (b /\ (a /\ c)) d -> Witness' ((b /\ a) /\ c) d
AssocR Witness' (α /\ (β /\ γ)) δ
forall (α :: Lifetime) (β :: Lifetime). (α <=! β) => Witness' α β
witness'
  {-# NOINLINE witness' #-}

instance {-# INCOHERENT #-} (α <=!! β) => α <=! β where
  witness' :: Witness' α β
witness' = Witness'' α β -> Witness' α β
forall (a :: Lifetime) (b :: Lifetime).
Witness'' a b -> Witness' a b
Inherit'' Witness'' α β
forall (α :: Lifetime) (β :: Lifetime). (α <=!! β) => Witness'' α β
witness''
  {-# NOINLINE witness' #-}

type (<=!!) :: Lifetime -> Lifetime -> Constraint
class α <=!! β where
  -- | The witness of the relation.
  witness'' :: Witness'' α β

instance α <=!! α where
  witness'' :: Witness'' α α
witness'' = Witness'' α α
forall (α :: Lifetime). Witness'' α α
Reflect
  {-# NOINLINE witness'' #-}

instance α /\ β <=!! α where
  witness'' :: Witness'' (α /\ β) α
witness'' = Witness'' (α /\ β) α
forall (α :: Lifetime) (β :: Lifetime). Witness'' (α /\ β) α
InfL
  {-# NOINLINE witness'' #-}

{-
instance α /\ β <=!! β where
  witness'' = Witness -}

instance {-# INCOHERENT #-} (β <=! γ) => α /\ β <=!! γ where
  witness'' :: Witness'' (α /\ β) γ
witness'' = Witness' β γ -> Witness'' (α /\ β) γ
forall (b :: Lifetime) (c :: Lifetime) (a :: Lifetime).
Witness' b c -> Witness'' (a /\ b) c
InfIntroL Witness' β γ
forall (α :: Lifetime) (β :: Lifetime). (α <=! β) => Witness' α β
witness'
  {-# NOINLINE witness'' #-}