Internal.hs

{-# 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 (Inf a b) = rnf a `seq` rnf b
  rnf Top = ()
  rnf (Inherit' w) = rnf 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 (AssocR w) = rnf w
  rnf (Inherit'' w) = rnf 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 Reflect = ()
  rnf InfL = ()
  rnf (InfIntroL w) = rnf 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 = Inf witness witness
  {-# NOINLINE witness #-}

instance α <= Static where
  witness = Top
  {-# NOINLINE witness #-}

instance {-# INCOHERENT #-} (α <=! β) => α <= β where
  witness = Inherit' witness'
  {-# NOINLINE witness #-}

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

instance (α /\ (β /\ γ) <=! δ) => (α /\ β) /\ γ <=! δ where
  witness' = AssocR witness'
  {-# NOINLINE witness' #-}

instance {-# INCOHERENT #-} (α <=!! β) => α <=! β where
  witness' = Inherit'' witness''
  {-# NOINLINE witness' #-}

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

instance α <=!! α where
  witness'' = Reflect
  {-# NOINLINE witness'' #-}

instance α /\ β <=!! α where
  witness'' = InfL
  {-# NOINLINE witness'' #-}

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

instance {-# INCOHERENT #-} (β <=! γ) => α /\ β <=!! γ where
  witness'' = InfIntroL witness'
  {-# NOINLINE witness'' #-}