{-# LANGUAGE TypeInType, GADTs, ScopedTypeVariables, FlexibleInstances,
             TypeOperators, ConstraintKinds, TypeFamilies, PartialTypeSignatures,
             UndecidableInstances, ViewPatterns, RankNTypes, TypeApplications,
             MultiParamTypeClasses, UndecidableSuperClasses, TemplateHaskell,
             StandaloneDeriving, DerivingStrategies, GeneralizedNewtypeDeriving #-}

{-|

Monadic capabilities are additional methods for a base monad. For instance, when
our base monad is 'IO', our capabilities might include logging, networking,
database access, and so on.

This framework allows mutually recursive late-bound capabilities with runtime
dispatch and a type-safe interface.

A capability is defined as a record type with methods parametrized over a base
monad:

@
data Logging m =
  Logging
    { _logError :: String -> m (),
      _logDebug :: String -> m ()
    }
@

We can define implementations as values of this record type:

@
loggingDummy :: Monad m => CapImpl Logging '[] m
loggingDummy = CapImpl $ Logging (\\_ -> return ()) (\\_ -> return ())

loggingIO :: MonadIO m => CapImpl Logging '[] m
loggingIO = CapImpl $
  Logging
    { _logError = \\msg -> liftIO . putStrLn $ "[Error] " ++ msg
      _logDebug = \\msg -> liftIO . putStrLn $ "[Debug] " ++ msg
    }
@

The dictionary is wrapped in 'CapImpl' to guarantee that it is sufficiently
polymorphic (this is required to support simultaneous use of monadic actions in
negative position and capability extension).

Then we want to use this capability in the 'CapsT' monad (which is nothing more
but a synonym for 'ReaderT' of 'Capabilities'), and for this we define a helper
per method:

@
logError :: HasCap Logging caps => String -> CapsT caps m ()
logError message = withCap $ \\cap -> _logError cap message

logDebug :: HasCap Logging caps => String -> CapsT caps m ()
logDebug message = withCap $ \\cap -> _logDebug cap message
@

We can define other capabilities in a similar manner:

@
data Networking m =
  Networking
    { _sendRequest :: ByteString -> m ByteString }

data FileStorage m =
  FileStorage
    { _readFile :: FilePath -> m ByteString,
      _writeFile :: FilePath -> ByteString -> m ()
    }
@

Implementations of capabilities may depend on other capabilities, which are
listed in their signature. For instance, this is how we can define the
'FileStorage' capability using the 'Logging' capability:

@
fileStorageIO :: MonadIO m => CapImpl FileStorage '[Logging] m
fileStorageIO = CapImpl $
  FileStorage
    { _readFile = \\path -> do
        logDebug $ "readFile " ++ path
        lift $ ByteString.readFile path
      _writeFile = \\path content -> do
        logDebug $
          "writeFile " ++ path ++
          " (" ++ show (ByteString.length content) ++
          " bytes)"
        lift $ ByteString.writeFile path content
    }
@

Here the @fileStorageIO@ implementation requires a logging capability,
but it's not specified which one.

When we decided what set of capabilities our application needs, we can put them
together in a 'Capabilities' map and run the application with this map in a
'ReaderT' context:

@
caps = buildCaps $
  AddCap loggingIO $
  AddCap fileStorageIO $
  BaseCaps emptyCaps

flip runReaderT caps $ do
  config <- readFile "config.yaml"
  ...
@

Capabilities passed to 'buildCaps' can depend on each other. The order does not
matter (although it is reflected in the types), and duplicate capabilities are
disallowed.

We can override a capability locally:

@
do
  config <- readFile "config.yaml"
  withReaderT (overrideCap loggingDummy) $ do
    -- logging is disabled here
    writeFile "config-backup.yaml" config
    ...
@

or we can add more capabilities:

@
do
  config <- readFile "config.yaml"
  networkingImpl <- parseNetworkingConfig config
  withReaderT (addCap networkingImpl) $ do
    -- networking capability added
    resp <- sendRequest req
    ...
@

-}

module Monad.Capabilities
  (
    -- * Capabilities
    Capabilities(),
    CapsT,
    emptyCaps,
    buildCaps,
    CapabilitiesBuilder(..),
    CapImpl(..),
    getCap,
    overrideCap,
    addCap,
    insertCap,
    withCap,
    checkCap,
    adjustCap,

    -- * Default capabilities
    Context(..),
    HasContext,
    newContext,
    askContext,
    localContext,

    -- * Type-level checks
    type HasCap,
    type HasCaps,
    type HasNoCap,
    HasCapDecision(..),

    -- * Utils
    makeCap

  ) where

import Control.Monad.Trans.Reader
import Data.Kind (Type, Constraint)
import Data.Traversable
import Data.Proxy
import Data.Type.Equality
import Data.List (foldl1')
import GHC.TypeLits (TypeError, ErrorMessage(..))
import Type.Reflection (Typeable)
import Data.Coerce (coerce)
import Unsafe.Coerce (unsafeCoerce)

import qualified Data.TypeRepMap as TypeRepMap
import Data.TypeRepMap (TypeRepMap)

import qualified Language.Haskell.TH as TH

type MonadK = Type -> Type

type CapK = MonadK -> Type

-- | @'Capabilities' caps m@ is a map of capabilities @caps@ over a base monad
-- @m@. Consider the following capabilities:
--
-- @
-- data X m = X (String -> m String)
-- data Y m = Y (Int -> m Bool)
-- @
--
-- We can construct a map of capabilities with the following type:
--
-- @
-- capsXY :: Capabilities '[X, Y] IO
-- @
--
-- In this case, @capsXY@ would be a map with two elements, one at key @X@ and
-- one at key @Y@. The types of capabilities themselves serve as keys.
--
-- 'Capabilities' is a heterogeneous collection, meaning that its values have
-- different types. The type of a value is determined by the key:
--
-- @
--
--  X:   X (\\_ -> return "hi") :: X (CapsT '[X, Y] IO)
--  Y:   Y (\\_ -> return True) :: Y (CapsT '[X, Y] IO)
-- ----  ---------------------    --------------------
-- keys         values              types of values
-- @
--
-- Notice that stored dictionaries are parametrized not just by the base monad
-- @IO@, but with the 'CapsT' transformer on top. This means that each
-- capability has access to all other capabilities and itself.
--
newtype Capabilities (caps :: [CapK]) (m :: MonadK) =
  Capabilities (TypeRepMap (CapElem m))

emptyCaps :: Capabilities '[] m
emptyCaps :: Capabilities '[] m
emptyCaps = TypeRepMap (CapElem m) -> Capabilities '[] m
forall (caps :: [CapK]) (m :: MonadK).
TypeRepMap (CapElem m) -> Capabilities caps m
Capabilities TypeRepMap (CapElem m)
forall k (f :: k -> *). TypeRepMap f
TypeRepMap.empty

deriving newtype instance Show (Capabilities caps m)

-- | The 'CapsT' transformer adds access to capabilities. This is a convenience
-- synonym for 'ReaderT' of 'Capabilities', and all 'ReaderT' functions
-- ('runReaderT', 'withReaderT') can be used with it.
type CapsT caps m = ReaderT (Capabilities caps m) m

-- | The 'CapImpl' newtype guarantees that the wrapped capability implementation
-- is sufficiently polymorphic so that required subtyping properties hold in
-- methods that take monadic actions as input (negative position).
--
-- This rules out using 'addCap', 'insertCap', and 'buildCaps' inside capability
-- implementations in an unsafe manner.
data CapImpl cap icaps m where
  CapImpl ::
    WithSpine icaps =>
    { CapImpl cap icaps m
-> forall (caps :: [CapK]).
   HasCaps icaps caps =>
   cap (CapsT caps m)
getCapImpl :: forall caps. HasCaps icaps caps => cap (CapsT caps m)
    } ->
    CapImpl cap icaps m

newtype CapElem m cap =
  CapElem { CapElem m cap -> forall (caps :: [CapK]). cap (CapsT caps m)
getCapElem :: forall caps. cap (CapsT caps m) }

overCapElem ::
  (forall caps. cap (CapsT caps m) -> cap' (CapsT caps m')) ->
  CapElem m cap ->
  CapElem m' cap'
overCapElem :: (forall (caps :: [CapK]).
 cap (CapsT caps m) -> cap' (CapsT caps m'))
-> CapElem m cap -> CapElem m' cap'
overCapElem forall (caps :: [CapK]). cap (CapsT caps m) -> cap' (CapsT caps m')
f (CapElem forall (caps :: [CapK]). cap (CapsT caps m)
cap) = (forall (caps :: [CapK]). cap' (CapsT caps m')) -> CapElem m' cap'
forall (m :: MonadK) (cap :: CapK).
(forall (caps :: [CapK]). cap (CapsT caps m)) -> CapElem m cap
CapElem (cap (CapsT caps m) -> cap' (CapsT caps m')
forall (caps :: [CapK]). cap (CapsT caps m) -> cap' (CapsT caps m')
f cap (CapsT caps m)
forall (caps :: [CapK]). cap (CapsT caps m)
cap)

-- Continuation-passing encoding of a list spine:
--
-- data Spine xs where
--   Cons :: Spine xs -> Spine (x : xs)
--   Nil :: Spine '[]
--
class WithSpine xs where
  onSpine ::
    forall r.
    Proxy xs ->
    ((xs ~ '[]) => r) ->
    (forall y ys.
      (xs ~ (y : ys)) =>
      WithSpine ys =>
      Proxy y ->
      Proxy ys ->
      r) ->
    r

instance WithSpine '[] where
  onSpine :: Proxy '[]
-> (('[] ~ '[]) => r)
-> (forall (y :: k) (ys :: [k]).
    ('[] ~ (y : ys), WithSpine ys) =>
    Proxy y -> Proxy ys -> r)
-> r
onSpine Proxy '[]
_ ('[] ~ '[]) => r
onNil forall (y :: k) (ys :: [k]).
('[] ~ (y : ys), WithSpine ys) =>
Proxy y -> Proxy ys -> r
_ = r
('[] ~ '[]) => r
onNil

instance WithSpine xs => WithSpine (x : xs) where
  onSpine :: Proxy (x : xs)
-> (((x : xs) ~ '[]) => r)
-> (forall (y :: k) (ys :: [k]).
    ((x : xs) ~ (y : ys), WithSpine ys) =>
    Proxy y -> Proxy ys -> r)
-> r
onSpine Proxy (x : xs)
_ ((x : xs) ~ '[]) => r
_ forall (y :: k) (ys :: [k]).
((x : xs) ~ (y : ys), WithSpine ys) =>
Proxy y -> Proxy ys -> r
onCons = Proxy x -> Proxy xs -> r
forall (y :: k) (ys :: [k]).
((x : xs) ~ (y : ys), WithSpine ys) =>
Proxy y -> Proxy ys -> r
onCons Proxy x
forall k (t :: k). Proxy t
Proxy Proxy xs
forall k (t :: k). Proxy t
Proxy

toCapElem ::
  forall cap icaps m.
  CapImpl cap icaps m ->
  CapElem m cap
toCapElem :: CapImpl cap icaps m -> CapElem m cap
toCapElem (CapImpl forall (caps :: [CapK]). HasCaps icaps caps => cap (CapsT caps m)
cap) = (forall (caps :: [CapK]). cap (CapsT caps m)) -> CapElem m cap
forall (m :: MonadK) (cap :: CapK).
(forall (caps :: [CapK]). cap (CapsT caps m)) -> CapElem m cap
CapElem
  (Proxy icaps
-> Proxy caps
-> (HasCaps icaps caps => cap (CapsT caps m))
-> cap (CapsT caps m)
forall k (icaps :: [k]) (caps :: [k]).
WithSpine icaps =>
Proxy icaps
-> Proxy caps -> forall r. (HasCaps icaps caps => r) -> r
fiatHasElems (Proxy icaps
forall k (t :: k). Proxy t
Proxy @icaps) (Proxy caps
forall k (t :: k). Proxy t
Proxy @caps) HasCaps icaps caps => cap (CapsT caps m)
forall (caps :: [CapK]). HasCaps icaps caps => cap (CapsT caps m)
cap :: forall caps. cap (CapsT caps m))

fiatHasElems ::
  forall icaps caps.
  WithSpine icaps =>
  Proxy icaps ->
  Proxy caps ->
  forall r. (HasCaps icaps caps => r) -> r
fiatHasElems :: Proxy icaps
-> Proxy caps -> forall r. (HasCaps icaps caps => r) -> r
fiatHasElems Proxy icaps
Proxy Proxy caps
Proxy HasCaps icaps caps => r
r =
  Proxy icaps
-> ((icaps ~ '[]) => r)
-> (forall (y :: k) (ys :: [k]).
    (icaps ~ (y : ys), WithSpine ys) =>
    Proxy y -> Proxy ys -> r)
-> r
forall k (xs :: [k]) r.
WithSpine xs =>
Proxy xs
-> ((xs ~ '[]) => r)
-> (forall (y :: k) (ys :: [k]).
    (xs ~ (y : ys), WithSpine ys) =>
    Proxy y -> Proxy ys -> r)
-> r
onSpine (Proxy icaps
forall k (t :: k). Proxy t
Proxy @icaps)
    -- nil
    (icaps ~ '[]) => r
HasCaps icaps caps => r
r
    -- cons
    (\(Proxy y
Proxy :: Proxy cap) (Proxy ys
Proxy :: Proxy icaps') ->
       case HasCap y caps :~: (() :: Constraint)
forall (c :: Constraint). c :~: (() :: Constraint)
unsafeUnitConstr @(HasCap cap caps) of
         HasCap y caps :~: (() :: Constraint)
Refl -> Proxy ys -> Proxy caps -> (HasCaps ys caps => r) -> r
forall k (icaps :: [k]) (caps :: [k]).
WithSpine icaps =>
Proxy icaps
-> Proxy caps -> forall r. (HasCaps icaps caps => r) -> r
fiatHasElems (Proxy ys
forall k (t :: k). Proxy t
Proxy @icaps') (Proxy caps
forall k (t :: k). Proxy t
Proxy @caps) HasCaps icaps caps => r
HasCaps ys caps => r
r)

{-

Since 'caps' is phantom, we can reorder capabilities, remove non-unique
capabilities, or extend them.

The tricky case is extension. Assume @caps'@ subsumes @caps@, and consider each
@cap n@ where @n ~ CapsT caps m@ individually. When we cast this to use @caps'@,
we must know that @cap@ will continue to work correctly.

1. Assume @cap@ uses @n@ in positive position exclusively. This means that the
   capability defines methods that take @Capabilities caps m@ as input, and
   it's okay if we pass @Capabilities caps' m@ instead, as we will simply have
   some unnecessary input.

2. Assume @cap@ uses @n@ in a negative poistion as well. This means that the
   capability defines method that will be passing @Capabilities caps m@ to
   other monadic actions. But when we cast to @caps'@, these monadic actions
   require @Capabilities caps' m@, where @caps'@ subsumes @caps@, so at runtime
   it's possible that we don't pass all needed capabilities for them.

In order for (2) to be safe, we need to place an additional requirement on
capabilities which use the provided @Capabilities caps m@ in a negative position:

  The positive occurence of @Capabilities caps m@ must come from a value
  provided by an occurence of @Capabilities caps m@ in a negative position,
  unmodified, rather than be constructed.

Essentially, we want capabilities to do only two things with @Capabilities@:

* extract parts of it with 'getCap'
* pass it along

In this case, even when on types we put @Capabilities caps m@ in a positive
position (where @caps@ might be insufficient), at runtime we know that these
capabilities actually contain @caps'@.

We guarantee this property by the 'CapImpl' newtype.

-}

-- | 'CapabilitiesBuilder' is a type to extend capabilities.
--
-- The @allCaps@ parameter is a list of capabilities that will be provided to
-- 'buildCaps' eventually, when the building process is done. The @caps@
-- parameter is the part of capabilities that was constructed so far. The
-- builder is considered complete when @allCaps ~ caps@, only then it can be
-- passed to 'buildCaps'.
data CapabilitiesBuilder (allCaps :: [CapK]) (caps :: [CapK]) (m :: MonadK) where
  AddCap ::
    (Typeable cap, HasCaps icaps allCaps, HasNoCap cap caps) =>
    CapImpl cap icaps m ->
    CapabilitiesBuilder allCaps caps m ->
    CapabilitiesBuilder allCaps (cap : caps) m
  BaseCaps ::
    Capabilities caps m ->
    CapabilitiesBuilder allCaps caps m

-- | Build a map of capabilities from individual implementations:
--
-- @
-- capsXY :: Capabilities '[X, Y] IO
-- capsXY = buildCaps $
--     AddCap xImpl $
--     AddCap yImpl $
--     BaseCaps emptyCaps
-- @
buildCaps :: forall caps m. CapabilitiesBuilder caps caps m -> Capabilities caps m
buildCaps :: CapabilitiesBuilder caps caps m -> Capabilities caps m
buildCaps = TypeRepMap (CapElem m) -> Capabilities caps m
forall (caps :: [CapK]) (m :: MonadK).
TypeRepMap (CapElem m) -> Capabilities caps m
Capabilities (TypeRepMap (CapElem m) -> Capabilities caps m)
-> (CapabilitiesBuilder caps caps m -> TypeRepMap (CapElem m))
-> CapabilitiesBuilder caps caps m
-> Capabilities caps m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CapabilitiesBuilder caps caps m -> TypeRepMap (CapElem m)
forall (caps' :: [CapK]).
CapabilitiesBuilder caps caps' m -> TypeRepMap (CapElem m)
go
  where
    go ::
      CapabilitiesBuilder caps caps' m ->
      TypeRepMap (CapElem m)
    go :: CapabilitiesBuilder caps caps' m -> TypeRepMap (CapElem m)
go (BaseCaps (Capabilities TypeRepMap (CapElem m)
caps)) = TypeRepMap (CapElem m)
caps
    go (AddCap CapImpl cap icaps m
capImpl CapabilitiesBuilder caps caps m
otherCaps) =
      CapElem m cap -> TypeRepMap (CapElem m) -> TypeRepMap (CapElem m)
forall k (a :: k) (f :: k -> *).
Typeable a =>
f a -> TypeRepMap f -> TypeRepMap f
TypeRepMap.insert (CapImpl cap icaps m -> CapElem m cap
forall (cap :: CapK) (icaps :: [CapK]) (m :: MonadK).
CapImpl cap icaps m -> CapElem m cap
toCapElem CapImpl cap icaps m
capImpl) (CapabilitiesBuilder caps caps m -> TypeRepMap (CapElem m)
forall (caps' :: [CapK]).
CapabilitiesBuilder caps caps' m -> TypeRepMap (CapElem m)
go CapabilitiesBuilder caps caps m
otherCaps)

-- | Ensure that the @caps@ list has an element @cap@.
type family HasCap cap caps :: Constraint where
  HasCap cap (cap  : _) = ()
  HasCap cap (cap' : caps) = HasCap cap caps
  HasCap cap '[] =
    TypeError
      (Text "Capability " :<>:
       ShowType cap :<>:
       Text " must be available")

-- | Ensure that the @caps@ list subsumes @icaps@. It is equivalent
-- to a @HasCap icap caps@ constraint for each @icap@ in @icaps@.
type family HasCaps icaps caps :: Constraint where
  HasCaps '[] _ = ()
  HasCaps (icap : icaps) caps = (HasCap icap caps, HasCaps icaps caps)

-- | Ensure that the @caps@ list does not have an element @cap@.
type family HasNoCap cap caps :: Constraint where
  HasNoCap cap (cap : _) =
    TypeError
      (Text "Capability " :<>:
       ShowType cap :<>:
       Text " is already present")
  HasNoCap cap (cap' : caps) = HasNoCap cap caps
  HasNoCap cap '[] = ()

-- | Lookup a capability in a 'Capabilities' map. The 'HasCap' constraint
-- guarantees that the lookup does not fail.
getCap :: forall cap m caps. (Typeable cap, HasCap cap caps) => Capabilities caps m -> cap (CapsT caps m)
getCap :: Capabilities caps m -> cap (CapsT caps m)
getCap (Capabilities TypeRepMap (CapElem m)
m) =
  case TypeRepMap (CapElem m) -> Maybe (CapElem m cap)
forall k (a :: k) (f :: k -> *).
Typeable a =>
TypeRepMap f -> Maybe (f a)
TypeRepMap.lookup TypeRepMap (CapElem m)
m of
    Maybe (CapElem m cap)
Nothing -> String -> cap (CapsT caps m)
forall a. HasCallStack => String -> a
error String
"getCap: impossible"
    Just CapElem m cap
e -> CapElem m cap -> forall (caps :: [CapK]). cap (CapsT caps m)
forall (m :: MonadK) (cap :: CapK).
CapElem m cap -> forall (caps :: [CapK]). cap (CapsT caps m)
getCapElem CapElem m cap
e

-- An internal function that adds capabilities.
unsafeInsertCap ::
  (Typeable cap, HasCaps icaps caps') =>
  CapImpl cap icaps m ->
  Capabilities caps m ->
  Capabilities caps' m
unsafeInsertCap :: CapImpl cap icaps m -> Capabilities caps m -> Capabilities caps' m
unsafeInsertCap CapImpl cap icaps m
capImpl (Capabilities TypeRepMap (CapElem m)
caps) =
  TypeRepMap (CapElem m) -> Capabilities caps' m
forall (caps :: [CapK]) (m :: MonadK).
TypeRepMap (CapElem m) -> Capabilities caps m
Capabilities (CapElem m cap -> TypeRepMap (CapElem m) -> TypeRepMap (CapElem m)
forall k (a :: k) (f :: k -> *).
Typeable a =>
f a -> TypeRepMap f -> TypeRepMap f
TypeRepMap.insert (CapImpl cap icaps m -> CapElem m cap
forall (cap :: CapK) (icaps :: [CapK]) (m :: MonadK).
CapImpl cap icaps m -> CapElem m cap
toCapElem CapImpl cap icaps m
capImpl) TypeRepMap (CapElem m)
caps)

-- | Extend the set of capabilities. In case the capability is already present,
-- it will be overriden (as with 'overrideCap'), but occur twice in the type.
insertCap ::
  (Typeable cap, HasCaps icaps (cap : caps)) =>
  CapImpl cap icaps m ->
  Capabilities caps m ->
  Capabilities (cap : caps) m
insertCap :: CapImpl cap icaps m
-> Capabilities caps m -> Capabilities (cap : caps) m
insertCap = CapImpl cap icaps m
-> Capabilities caps m -> Capabilities (cap : caps) m
forall (cap :: CapK) (icaps :: [CapK]) (caps' :: [CapK])
       (m :: MonadK) (caps :: [CapK]).
(Typeable cap, HasCaps icaps caps') =>
CapImpl cap icaps m -> Capabilities caps m -> Capabilities caps' m
unsafeInsertCap

-- | Extend the set of capabilities. In case the capability is already present,
-- a type error occurs.
addCap ::
  (Typeable cap, HasNoCap cap caps, HasCaps icaps (cap : caps)) =>
  CapImpl cap icaps m ->
  Capabilities caps m ->
  Capabilities (cap : caps) m
addCap :: CapImpl cap icaps m
-> Capabilities caps m -> Capabilities (cap : caps) m
addCap CapImpl cap icaps m
capImpl Capabilities caps m
caps = CapabilitiesBuilder (cap : caps) (cap : caps) m
-> Capabilities (cap : caps) m
forall (caps :: [CapK]) (m :: MonadK).
CapabilitiesBuilder caps caps m -> Capabilities caps m
buildCaps (CapImpl cap icaps m
-> CapabilitiesBuilder (cap : caps) caps m
-> CapabilitiesBuilder (cap : caps) (cap : caps) m
forall (cap :: CapK) (icaps :: [CapK]) (allCaps :: [CapK])
       (caps :: [CapK]) (m :: MonadK).
(Typeable cap, HasCaps icaps allCaps, HasNoCap cap caps) =>
CapImpl cap icaps m
-> CapabilitiesBuilder allCaps caps m
-> CapabilitiesBuilder allCaps (cap : caps) m
AddCap CapImpl cap icaps m
capImpl (CapabilitiesBuilder (cap : caps) caps m
 -> CapabilitiesBuilder (cap : caps) (cap : caps) m)
-> CapabilitiesBuilder (cap : caps) caps m
-> CapabilitiesBuilder (cap : caps) (cap : caps) m
forall a b. (a -> b) -> a -> b
$ Capabilities caps m -> CapabilitiesBuilder (cap : caps) caps m
forall (caps :: [CapK]) (m :: MonadK) (allCaps :: [CapK]).
Capabilities caps m -> CapabilitiesBuilder allCaps caps m
BaseCaps Capabilities caps m
caps)

-- | Override the implementation of an existing capability.
overrideCap ::
  (Typeable cap, HasCap cap caps, HasCaps icaps caps) =>
  CapImpl cap icaps m ->
  Capabilities caps m ->
  Capabilities caps m
overrideCap :: CapImpl cap icaps m -> Capabilities caps m -> Capabilities caps m
overrideCap = CapImpl cap icaps m -> Capabilities caps m -> Capabilities caps m
forall (cap :: CapK) (icaps :: [CapK]) (caps' :: [CapK])
       (m :: MonadK) (caps :: [CapK]).
(Typeable cap, HasCaps icaps caps') =>
CapImpl cap icaps m -> Capabilities caps m -> Capabilities caps' m
unsafeInsertCap

-- | Override the implementation of an existing capability using the previous
-- implementation. This is a more efficient equivalent to extracting a
-- capability with 'getCap', adjusting it with a function, and putting it back
-- with 'overrideCap'.
adjustCap ::
  forall cap caps m.
  (Typeable cap, HasCap cap caps) =>
  (forall caps'. cap (CapsT caps' m) -> cap (CapsT caps' m)) ->
  Capabilities caps m ->
  Capabilities caps m
adjustCap :: (forall (caps' :: [CapK]).
 cap (CapsT caps' m) -> cap (CapsT caps' m))
-> Capabilities caps m -> Capabilities caps m
adjustCap forall (caps' :: [CapK]).
cap (CapsT caps' m) -> cap (CapsT caps' m)
f (Capabilities TypeRepMap (CapElem m)
caps) =
  TypeRepMap (CapElem m) -> Capabilities caps m
forall (caps :: [CapK]) (m :: MonadK).
TypeRepMap (CapElem m) -> Capabilities caps m
Capabilities ((CapElem m cap -> CapElem m cap)
-> TypeRepMap (CapElem m) -> TypeRepMap (CapElem m)
forall k (a :: k) (f :: k -> *).
Typeable a =>
(f a -> f a) -> TypeRepMap f -> TypeRepMap f
TypeRepMap.adjust ((forall (caps' :: [CapK]).
 cap (CapsT caps' m) -> cap (CapsT caps' m))
-> CapElem m cap -> CapElem m cap
forall (cap :: CapK) (m :: MonadK) (cap' :: CapK) (m' :: MonadK).
(forall (caps :: [CapK]).
 cap (CapsT caps m) -> cap' (CapsT caps m'))
-> CapElem m cap -> CapElem m' cap'
overCapElem forall (caps' :: [CapK]).
cap (CapsT caps' m) -> cap (CapsT caps' m)
f) TypeRepMap (CapElem m)
caps)

-- | Extract a capability from 'CapsT' and provide it to a continuation.
withCap :: (Typeable cap, HasCap cap caps) => (cap (CapsT caps m) -> CapsT caps m a) -> CapsT caps m a
withCap :: (cap (CapsT caps m) -> CapsT caps m a) -> CapsT caps m a
withCap cap (CapsT caps m) -> CapsT caps m a
cont = (Capabilities caps m -> m a) -> CapsT caps m a
forall r (m :: MonadK) a. (r -> m a) -> ReaderT r m a
ReaderT ((Capabilities caps m -> m a) -> CapsT caps m a)
-> (Capabilities caps m -> m a) -> CapsT caps m a
forall a b. (a -> b) -> a -> b
$ \Capabilities caps m
caps -> CapsT caps m a -> Capabilities caps m -> m a
forall r (m :: MonadK) a. ReaderT r m a -> r -> m a
runReaderT (cap (CapsT caps m) -> CapsT caps m a
cont (Capabilities caps m -> cap (CapsT caps m)
forall (cap :: CapK) (m :: MonadK) (caps :: [CapK]).
(Typeable cap, HasCap cap caps) =>
Capabilities caps m -> cap (CapsT caps m)
getCap Capabilities caps m
caps)) Capabilities caps m
caps

-- | Evidence that @cap@ is present or absent in @caps@.
data HasCapDecision cap caps where
  HasNoCap :: HasNoCap cap caps => HasCapDecision cap caps
  HasCap :: HasCap cap caps => HasCapDecision cap caps

instance Show (HasCapDecision cap caps) where
  show :: HasCapDecision cap caps -> String
show HasCapDecision cap caps
HasNoCap = String
"HasNoCap"
  show HasCapDecision cap caps
HasCap = String
"HasCap"

-- | Determine at runtime whether 'HasCap cap caps' or 'HasNoCap cap caps' holds.
checkCap :: forall cap caps m. Typeable cap => Capabilities caps m -> HasCapDecision cap caps
checkCap :: Capabilities caps m -> HasCapDecision cap caps
checkCap (Capabilities TypeRepMap (CapElem m)
m) =
  if TypeRepMap (CapElem m) -> Bool
forall k (a :: k) (f :: k -> *). Typeable a => TypeRepMap f -> Bool
TypeRepMap.member @cap TypeRepMap (CapElem m)
m
  then case HasCap cap caps :~: (() :: Constraint)
forall (c :: Constraint). c :~: (() :: Constraint)
unsafeUnitConstr @(HasCap cap caps) of HasCap cap caps :~: (() :: Constraint)
Refl -> HasCapDecision cap caps
forall k (cap :: k) (caps :: [k]).
HasCap cap caps =>
HasCapDecision cap caps
HasCap
  else case HasNoCap cap caps :~: (() :: Constraint)
forall (c :: Constraint). c :~: (() :: Constraint)
unsafeUnitConstr @(HasNoCap cap caps) of HasNoCap cap caps :~: (() :: Constraint)
Refl -> HasCapDecision cap caps
forall k (cap :: k) (caps :: [k]).
HasNoCap cap caps =>
HasCapDecision cap caps
HasNoCap

-- Use to construct 'HasCap' or 'HasNoCap'.
unsafeUnitConstr :: c :~: (() :: Constraint)
unsafeUnitConstr :: c :~: (() :: Constraint)
unsafeUnitConstr = (Any :~: Any) -> c :~: (() :: Constraint)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl

-- | The 'Context' capability is used to model the @Reader@ effect within the
-- capabilities framework.
newtype Context x (m :: MonadK) = Context x

-- | The 'HasContext' constraint is a shorthand for 'HasCap' of 'Context'.
class (Typeable x, HasCap (Context x) caps) => HasContext x caps
instance (Typeable x, HasCap (Context x) caps) => HasContext x caps

-- | Initialize a 'Context' capability.
newContext :: forall x m. x -> CapImpl (Context x) '[] m
newContext :: x -> CapImpl (Context x) '[] m
newContext x
x = (forall (caps :: [CapK]).
 HasCaps '[] caps =>
 Context x (CapsT caps m))
-> CapImpl (Context x) '[] m
forall (icaps :: [CapK]) (cap :: CapK) (m :: MonadK).
WithSpine icaps =>
(forall (caps :: [CapK]). HasCaps icaps caps => cap (CapsT caps m))
-> CapImpl cap icaps m
CapImpl (x -> Context x (CapsT caps m)
forall x (m :: MonadK). x -> Context x m
Context x
x)

-- | Retrieve the context value. Moral equivalent of 'ask'.
askContext :: (HasContext x caps, Applicative m) => CapsT caps m x
askContext :: CapsT caps m x
askContext = (Context x (CapsT caps m) -> CapsT caps m x) -> CapsT caps m x
forall (cap :: CapK) (caps :: [CapK]) (m :: MonadK) a.
(Typeable cap, HasCap cap caps) =>
(cap (CapsT caps m) -> CapsT caps m a) -> CapsT caps m a
withCap (\(Context x
x) -> x -> CapsT caps m x
forall (f :: MonadK) a. Applicative f => a -> f a
pure x
x)

-- | Execute a computation with a modified context value. Moral equivalent of 'local'.
localContext :: forall x caps m a. (HasContext x caps) => (x -> x) -> CapsT caps m a -> CapsT caps m a
localContext :: (x -> x) -> CapsT caps m a -> CapsT caps m a
localContext x -> x
f = (Capabilities caps m -> Capabilities caps m)
-> CapsT caps m a -> CapsT caps m a
forall r (m :: MonadK) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local ((forall (caps' :: [CapK]).
 Context x (CapsT caps' m) -> Context x (CapsT caps' m))
-> Capabilities caps m -> Capabilities caps m
forall (cap :: CapK) (caps :: [CapK]) (m :: MonadK).
(Typeable cap, HasCap cap caps) =>
(forall (caps' :: [CapK]).
 cap (CapsT caps' m) -> cap (CapsT caps' m))
-> Capabilities caps m -> Capabilities caps m
adjustCap @(Context x) ((x -> x) -> Context x (CapsT caps' m) -> Context x (CapsT caps' m)
coerce x -> x
f))

makeCap :: TH.Name -> TH.DecsQ
makeCap :: Name -> DecsQ
makeCap Name
capName = do
  let className :: Name
className = String -> Name
TH.mkName (String
"Monad" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
capName)
  Info
info <- Name -> Q Info
TH.reify Name
capName
  ([VarBangType]
vbts, [TyVarBndr]
tyVars) <-
    case Info
info of
      TH.TyConI (TH.DataD    Cxt
_ Name
_ [TyVarBndr]
tyVars Maybe Kind
_ [TH.RecC Name
_ [VarBangType]
vbts] [DerivClause]
_) -> ([VarBangType], [TyVarBndr]) -> Q ([VarBangType], [TyVarBndr])
forall (m :: MonadK) a. Monad m => a -> m a
return ([VarBangType]
vbts, [TyVarBndr]
tyVars)
      TH.TyConI (TH.NewtypeD Cxt
_ Name
_ [TyVarBndr]
tyVars Maybe Kind
_ (TH.RecC Name
_ [VarBangType]
vbts) [DerivClause]
_) -> ([VarBangType], [TyVarBndr]) -> Q ([VarBangType], [TyVarBndr])
forall (m :: MonadK) a. Monad m => a -> m a
return ([VarBangType]
vbts, [TyVarBndr]
tyVars)
      Info
_ -> String -> Q ([VarBangType], [TyVarBndr])
forall (m :: MonadK) a. MonadFail m => String -> m a
fail String
"Capabilities must be single-constructor record types"
  (TyVarBndr
mVar, [TyVarBndr]
extraTyVars) <-
    case [TyVarBndr] -> [TyVarBndr]
forall a. [a] -> [a]
reverse [TyVarBndr]
tyVars of
      (TyVarBndr
tv:[TyVarBndr]
tvs) -> (TyVarBndr, [TyVarBndr]) -> Q (TyVarBndr, [TyVarBndr])
forall (m :: MonadK) a. Monad m => a -> m a
return (TyVarBndr
tv, [TyVarBndr] -> [TyVarBndr]
forall a. [a] -> [a]
reverse [TyVarBndr]
tvs)
      [TyVarBndr]
_ -> String -> Q (TyVarBndr, [TyVarBndr])
forall (m :: MonadK) a. MonadFail m => String -> m a
fail String
"Capability must have a monadic parameter"
  let
    parametrize :: Name -> TypeQ
parametrize Name
name = (TypeQ -> TypeQ -> TypeQ) -> [TypeQ] -> TypeQ
forall a. (a -> a -> a) -> [a] -> a
foldl1' TypeQ -> TypeQ -> TypeQ
TH.appT (Name -> TypeQ
TH.conT Name
name TypeQ -> [TypeQ] -> [TypeQ]
forall a. a -> [a] -> [a]
: (TyVarBndr -> TypeQ) -> [TyVarBndr] -> [TypeQ]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr -> TypeQ
tyVarBndrT [TyVarBndr]
extraTyVars)
    capType :: TypeQ
capType = Name -> TypeQ
parametrize Name
capName
    classType :: TypeQ
classType = Name -> TypeQ
parametrize Name
className
  [(Name, Name, Kind, Cxt)]
methodSpecs <- [VarBangType]
-> (VarBangType -> Q (Name, Name, Kind, Cxt))
-> Q [(Name, Name, Kind, Cxt)]
forall (t :: MonadK) (f :: MonadK) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarBangType]
vbts ((VarBangType -> Q (Name, Name, Kind, Cxt))
 -> Q [(Name, Name, Kind, Cxt)])
-> (VarBangType -> Q (Name, Name, Kind, Cxt))
-> Q [(Name, Name, Kind, Cxt)]
forall a b. (a -> b) -> a -> b
$ \(Name
fieldName, Bang
_, Kind
ty) -> do
    Name
methodName <-
      case Name -> String
TH.nameBase Name
fieldName of
        (Char
'_':String
methodName) -> Name -> Q Name
forall (m :: MonadK) a. Monad m => a -> m a
return (Name -> Q Name) -> Name -> Q Name
forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
methodName
        String
_ -> String -> Q Name
forall (m :: MonadK) a. MonadFail m => String -> m a
fail String
"Capability method names must start with underscores"
    Cxt
tyArgList <-
      let
        toArgList :: Kind -> Cxt
toArgList (Kind
TH.ArrowT `TH.AppT` Kind
a `TH.AppT` Kind
b) = Kind
aKind -> Cxt -> Cxt
forall a. a -> [a] -> [a]
:Kind -> Cxt
toArgList Kind
b
        toArgList (TH.ForallT [TyVarBndr]
_ Cxt
_ Kind
a) = Kind -> Cxt
toArgList Kind
a
        toArgList Kind
_ = []
      in
        Cxt -> Q Cxt
forall (m :: MonadK) a. Monad m => a -> m a
return (Cxt -> Q Cxt) -> Cxt -> Q Cxt
forall a b. (a -> b) -> a -> b
$ Kind -> Cxt
toArgList Kind
ty
    (Name, Name, Kind, Cxt) -> Q (Name, Name, Kind, Cxt)
forall (m :: MonadK) a. Monad m => a -> m a
return (Name
methodName, Name
fieldName, Kind
ty, Cxt
tyArgList)
  [Dec]
class_decs <- (Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
:[]) (Dec -> [Dec]) -> Q Dec -> DecsQ
forall (f :: MonadK) a b. Functor f => (a -> b) -> f a -> f b
<$>
    Q Cxt -> Name -> [TyVarBndr] -> [FunDep] -> [Q Dec] -> Q Dec
TH.classD
      ([TypeQ] -> Q Cxt
TH.cxt [])
      Name
className
      [TyVarBndr]
tyVars
      []
      [ Name -> TypeQ -> Q Dec
TH.sigD Name
methodName (Kind -> TypeQ
forall (m :: MonadK) a. Monad m => a -> m a
return Kind
ty)
      | (Name
methodName, Name
_, Kind
ty, Cxt
_) <- [(Name, Name, Kind, Cxt)]
methodSpecs
      ]
  let
    methodDec :: Name -> Name -> Cxt -> Q Dec
methodDec Name
methodName Name
fieldName Cxt
tyArgList = do
      Name -> [ClauseQ] -> Q Dec
TH.funD Name
methodName
        [do
          [Name]
argNames <- do
            [(Int, Kind)] -> ((Int, Kind) -> Q Name) -> Q [Name]
forall (t :: MonadK) (f :: MonadK) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([Int] -> Cxt -> [(Int, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] Cxt
tyArgList) (((Int, Kind) -> Q Name) -> Q [Name])
-> ((Int, Kind) -> Q Name) -> Q [Name]
forall a b. (a -> b) -> a -> b
$ \(Int
i, Kind
_tyArg) ->
              String -> Q Name
TH.newName (String
"arg" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
i::Int))
          let
            pats :: [PatQ]
pats = (Name -> PatQ) -> [Name] -> [PatQ]
forall a b. (a -> b) -> [a] -> [b]
map Name -> PatQ
TH.varP [Name]
argNames
            args :: [ExpQ]
args = (Name -> ExpQ) -> [Name] -> [ExpQ]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ExpQ
TH.varE [Name]
argNames
            body :: BodyQ
body = ExpQ -> BodyQ
TH.normalB (ExpQ -> BodyQ) -> ExpQ -> BodyQ
forall a b. (a -> b) -> a -> b
$ do
              Name
lamName <- String -> Q Name
TH.newName String
"cap"
              ExpQ -> ExpQ -> ExpQ
TH.appE (ExpQ -> TypeQ -> ExpQ
TH.appTypeE [e|withCap|] TypeQ
capType) (ExpQ -> ExpQ) -> ExpQ -> ExpQ
forall a b. (a -> b) -> a -> b
$
                PatQ -> ExpQ -> ExpQ
TH.lam1E (Name -> PatQ
TH.varP Name
lamName) (ExpQ -> ExpQ) -> ExpQ -> ExpQ
forall a b. (a -> b) -> a -> b
$
                  (ExpQ -> ExpQ -> ExpQ) -> [ExpQ] -> ExpQ
forall a. (a -> a -> a) -> [a] -> a
foldl1' ExpQ -> ExpQ -> ExpQ
TH.appE (Name -> ExpQ
TH.varE Name
fieldName ExpQ -> [ExpQ] -> [ExpQ]
forall a. a -> [a] -> [a]
: Name -> ExpQ
TH.varE Name
lamName ExpQ -> [ExpQ] -> [ExpQ]
forall a. a -> [a] -> [a]
: [ExpQ]
args)
          [PatQ] -> BodyQ -> [Q Dec] -> ClauseQ
TH.clause [PatQ]
pats BodyQ
body []
        ]
  [Dec]
instance_decs <- (Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
:[]) (Dec -> [Dec]) -> Q Dec -> DecsQ
forall (f :: MonadK) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    Name
rVar <- String -> Q Name
TH.newName String
"r"
    Name
capsVar <- String -> Q Name
TH.newName String
"caps"
    let typeableConstraints :: [TypeQ]
typeableConstraints = [ [t|Typeable $(tyVarBndrT v)|] | TyVarBndr
v <- [TyVarBndr]
extraTyVars ]
    Q Cxt -> TypeQ -> [Q Dec] -> Q Dec
TH.instanceD
      ([TypeQ] -> Q Cxt
TH.cxt ([TypeQ] -> Q Cxt) -> [TypeQ] -> Q Cxt
forall a b. (a -> b) -> a -> b
$
        [ [t|HasCap $capType $(TH.varT capsVar)|],
          [t| $(TH.varT rVar) ~ Capabilities $(TH.varT capsVar) $(tyVarBndrT' mVar) |]
        ] [TypeQ] -> [TypeQ] -> [TypeQ]
forall a. [a] -> [a] -> [a]
++ [TypeQ]
typeableConstraints)
      [t| $classType (ReaderT $(TH.varT rVar) $(tyVarBndrT' mVar)) |]
      [ Name -> Name -> Cxt -> Q Dec
methodDec Name
methodName Name
fieldName Cxt
tyArgList
      | (Name
methodName, Name
fieldName, Kind
_, Cxt
tyArgList) <- [(Name, Name, Kind, Cxt)]
methodSpecs
      ]
  [Dec] -> DecsQ
forall (m :: MonadK) a. Monad m => a -> m a
return ([Dec]
class_decs [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
instance_decs)
  where
    tyVarBndrT :: TyVarBndr -> TypeQ
tyVarBndrT (TH.PlainTV Name
name) = Name -> TypeQ
TH.varT Name
name
    tyVarBndrT (TH.KindedTV Name
name Kind
k) = TypeQ -> Kind -> TypeQ
TH.sigT (Name -> TypeQ
TH.varT Name
name) Kind
k

    tyVarBndrT' :: TyVarBndr -> TypeQ
tyVarBndrT' (TH.PlainTV Name
name) = Name -> TypeQ
TH.varT Name
name
    tyVarBndrT' (TH.KindedTV Name
name Kind
_) = Name -> TypeQ
TH.varT Name
name