{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- |

--    This package provices the 'Advice' datatype, along for functions for creating,

--    manipulating, composing and applying values of that type.

--

--    'Advice's represent generic transformations on 'DepT'-effectful functions of

--    any number of arguments.

--

-- >>> :{

--    foo0 :: DepT NilEnv IO (Sum Int)

--    foo0 = pure (Sum 5)

--    foo1 :: Bool -> DepT NilEnv IO (Sum Int)

--    foo1 _ = foo0

--    foo2 :: Char -> Bool -> DepT NilEnv IO (Sum Int)

--    foo2 _ = foo1

-- :}

--

-- They work for @DepT@-actions of zero arguments:

--

-- >>> advise (printArgs @Top stdout "foo0") foo0 `runDepT` NilEnv

-- foo0:

-- <BLANKLINE>

-- Sum {getSum = 5}

--

-- And for functions of one or more arguments, provided they end on a @DepT@-action:

--

-- >>> advise (printArgs @Top stdout "foo1") foo1 False `runDepT` NilEnv

-- foo1: False

-- <BLANKLINE>

-- Sum {getSum = 5}

--

-- >>> advise (printArgs @Top stdout "foo2") foo2 'd' False `runDepT` NilEnv

-- foo2: 'd' False

-- <BLANKLINE>

-- Sum {getSum = 5}

--

-- 'Advice's can also tweak the result value of functions:

--

-- >>> advise (returnMempty @Top @Top2) foo2 'd' False `runDepT` NilEnv

-- Sum {getSum = 0}

--

-- And they can be combined using @Advice@'s 'Monoid' instance before being applied

-- (although that might require harmonizing their constraint parameters):

--

-- >>> advise (printArgs stdout "foo2" <> returnMempty) foo2 'd' False `runDepT` NilEnv

-- foo2: 'd' False

-- <BLANKLINE>

-- Sum {getSum = 0}

module Control.Monad.Dep.Advice
  ( -- * The Advice type

    Advice,

    -- * Creating Advice values

    makeAdvice,
    makeArgsAdvice,
    makeExecutionAdvice,

    -- * Applying Advices

    advise,

    -- * Constraint helpers

    -- $constrainthelpers

    Ensure,
    Top2,
    And2,
    MonadConstraint,
    EnvConstraint,
    MustBe,
    MustBe2,

    -- * Combining Advices by harmonizing their constraints

    -- $restrict

    restrictArgs,
    restrictEnv,
    restrictResult,

    -- * Invocation helpers

    -- $invocation

    runFinalDepT,
    runFromEnv,

    -- * "sop-core" re-exports

    -- $sop

    Top,
    And,
    All,
    NP (..),
    I (..),
    cfoldMap_NP,

    -- * "constraints" re-exports

    -- $constraints

    type (:-) (..),
    Dict (..),
  )
where

import Control.Monad.Dep
import Data.Constraint
import Data.Kind
import Data.SOP
import Data.SOP.Dict qualified as SOP
import Data.SOP.NP

-- $setup

--

-- >>> :set -XTypeApplications

-- >>> :set -XStandaloneKindSignatures

-- >>> :set -XMultiParamTypeClasses

-- >>> :set -XFunctionalDependencies

-- >>> :set -XRankNTypes

-- >>> :set -XTypeOperators

-- >>> :set -XConstraintKinds

-- >>> :set -XNamedFieldPuns

-- >>> import Control.Monad

-- >>> import Control.Monad.Dep

-- >>> import Control.Monad.Dep.Advice

-- >>> import Control.Monad.Dep.Advice.Basic (printArgs,returnMempty)

-- >>> import Data.Constraint

-- >>> import Data.Kind

-- >>> import Data.SOP

-- >>> import Data.SOP.NP

-- >>> import Data.Monoid

-- >>> import System.IO

-- >>> import Data.IORef


-- | A generic transformation of a 'DepT'-effectful function of any number of

-- arguments, provided the function satisfies certain constraints on the

-- arguments, the environment type constructor and base monad, and the return type.

--

-- It is parameterized by three constraints:

--

-- * @ca@ of kind @Type -> Constraint@, the constraint required of each argument (usually something like @Show@).

-- * @cem@ of kind @((Type -> Type) -> Type) -> (Type -> Type) -> Constraint@,

-- a two-place constraint required of the environment type constructor / base

-- monad combination. Note that the environment type constructor remains

-- unapplied. That is, for a given @cem@, @cem NilEnv IO@ kind-checks but @cem

-- (NilEnv IO) IO@ doesn't. See also 'Ensure'.

-- * @cr@ of kind @Type -> Constraint@, the constraint required of the return type.

--

-- We can define 'Advice's that work with concrete types by using 'MustBe' in

-- the case of @ca@ and @cr@, and 'MustBe2' in the case of @cem@.

--

-- 'Advice's that don't care about a particular constraint can leave it

-- polymorphic, and this facilitates composition, but the constraint must be

-- given some concrete value ('Top' in the case of @ca@ and @cr@, 'Top2' in

-- the case of @cem@) through type application at the moment of calling

-- 'advise'.

--

-- See "Control.Monad.Dep.Advice.Basic" for examples.

type Advice ::
  (Type -> Constraint) ->
  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
  (Type -> Constraint) ->
  Type
data Advice ca cem cr where
  Advice ::
    forall u ca cem cr.
    Proxy u ->
    ( forall as e m.
      (All ca as, cem e m, Monad m) =>
      NP I as ->
      DepT e m (u, NP I as)
    ) ->
    ( forall e m r.
      (cem e m, Monad m, cr r) =>
      u ->
      DepT e m r ->
      DepT e m r
    ) ->
    Advice ca cem cr

-- |

--    Aspects compose \"sequentially\" when tweaking the arguments, and

--    \"concentrically\" when tweaking the final 'DepT' action.

--

--    The first 'Advice' is the \"outer\" one. It tweaks the function arguments

--    first, and wraps around the execution of the second, \"inner\" 'Advice'.

instance Semigroup (Advice ca cem cr) where
  Advice Proxy u
outer forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsOuter forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionOuter <> :: Advice ca cem cr -> Advice ca cem cr -> Advice ca cem cr
<> Advice Proxy u
inner forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsInner forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionInner =
    let captureExistentials ::
          forall ca cem cr outer inner.
          Proxy outer ->
          ( forall as e m.
            (All ca as, cem e m, Monad m) =>
            NP I as ->
            DepT e m (outer, NP I as)
          ) ->
          ( forall e m r.
            (cem e m, Monad m, cr r) =>
            outer ->
            DepT e m r ->
            DepT e m r
          ) ->
          Proxy inner ->
          ( forall as e m.
            (All ca as, cem e m, Monad m) =>
            NP I as ->
            DepT e m (inner, NP I as)
          ) ->
          ( forall e m r.
            (cem e m, Monad m, cr r) =>
            inner ->
            DepT e m r ->
            DepT e m r
          ) ->
          Advice ca cem cr
        captureExistentials :: Proxy outer
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (outer, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    outer -> DepT e m r -> DepT e m r)
-> Proxy inner
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (inner, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    inner -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
captureExistentials Proxy outer
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (outer, NP I as)
tweakArgsOuter' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
outer -> DepT e m r -> DepT e m r
tweakExecutionOuter' Proxy inner
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (inner, NP I as)
tweakArgsInner' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
inner -> DepT e m r -> DepT e m r
tweakExecutionInner' =
          Proxy (Pair outer inner)
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (Pair outer inner, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    Pair outer inner -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
            (Proxy (Pair outer inner)
forall k (t :: k). Proxy t
Proxy @(Pair outer inner))
            ( let tweakArgs ::
                    forall as e m.
                    (All ca as, cem e m, Monad m) =>
                    NP I as ->
                    DepT e m (Pair outer inner, NP I as)
                  tweakArgs :: NP I as -> DepT e m (Pair outer inner, NP I as)
tweakArgs NP I as
args =
                    do
                      (outer
uOuter, NP I as
argsOuter) <- NP I as -> DepT e m (outer, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (outer, NP I as)
tweakArgsOuter' @as @e @m NP I as
args
                      (inner
uInner, NP I as
argsInner) <- NP I as -> DepT e m (inner, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (inner, NP I as)
tweakArgsInner' @as @e @m NP I as
argsOuter
                      (Pair outer inner, NP I as) -> DepT e m (Pair outer inner, NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (outer -> inner -> Pair outer inner
forall a b. a -> b -> Pair a b
Pair outer
uOuter inner
uInner, NP I as
argsInner)
               in NP I as -> DepT e m (Pair outer inner, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (Pair outer inner, NP I as)
tweakArgs
            )
            ( let tweakExecution ::
                    forall e m r.
                    (cem e m, Monad m, cr r) =>
                    Pair outer inner ->
                    DepT e m r ->
                    DepT e m r
                  tweakExecution :: Pair outer inner -> DepT e m r -> DepT e m r
tweakExecution =
                    ( \(Pair outer
uOuter inner
uInner) DepT e m r
action ->
                        outer -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
outer -> DepT e m r -> DepT e m r
tweakExecutionOuter' @e @m @r outer
uOuter (inner -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
inner -> DepT e m r -> DepT e m r
tweakExecutionInner' @e @m @r inner
uInner DepT e m r
action)
                    )
               in Pair outer inner -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
Pair outer inner -> DepT e m r -> DepT e m r
tweakExecution
            )
     in Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint) outer inner.
Proxy outer
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (outer, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    outer -> DepT e m r -> DepT e m r)
-> Proxy inner
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (inner, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    inner -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
captureExistentials @ca @cem @cr Proxy u
outer forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsOuter forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionOuter Proxy u
inner forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgsInner forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecutionInner

instance Monoid (Advice ca cem cr) where
  mappend :: Advice ca cem cr -> Advice ca cem cr -> Advice ca cem cr
mappend = Advice ca cem cr -> Advice ca cem cr -> Advice ca cem cr
forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: Advice ca cem cr
mempty = Proxy ()
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m ((), NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    () -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice (Proxy ()
forall k (t :: k). Proxy t
Proxy @()) (\NP I as
args -> ((), NP I as) -> DepT e m ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NP I as -> ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP I as
args)) ((DepT e m r -> DepT e m r) -> () -> DepT e m r -> DepT e m r
forall a b. a -> b -> a
const DepT e m r -> DepT e m r
forall a. a -> a
id)

-- |

--    The most general (and complex) way of constructing 'Advice's.

--

--    'Advice's work in two phases. First, the arguments of the transformed

--    function are collected into an n-ary product 'NP', and passed to the

--    first argument of 'makeAdvice', which produces a (possibly transformed)

--    product of arguments, along with some summary value of type @u@. Use @()@

--    as the summary value if you don't care about it.

--

--    In the second phase, the monadic action produced by the function once all

--    arguments have been given is transformed using the second argument of

--    'makeAdvice'. This second argument also receives the summary value of

--    type @u@ calculated earlier.

--

-- >>> :{

--  doesNothing :: forall ca cem cr. Advice ca cem cr

--  doesNothing = makeAdvice @() (\args -> pure (pure args)) (\() action -> action)

-- :}

--

--    __/IMPORTANT!/__ When invoking 'makeAdvice', you must always give the

--    type of the existential @u@ through a type application. Otherwise you'll

--    get weird \"u is untouchable\" errors.

makeAdvice ::
  forall u ca cem cr.
  -- | The function that tweaks the arguments.

  ( forall as e m.
    (All ca as, cem e m, Monad m) =>
    NP I as ->
    DepT e m (u, NP I as)
  ) ->
  -- | The function that tweaks the execution.

  ( forall e m r.
    (cem e m, Monad m, cr r) =>
    u ->
    DepT e m r ->
    DepT e m r
  ) ->
  Advice ca cem cr
makeAdvice :: (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
 (All ca as, cem e m, Monad m) =>
 NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeAdvice = Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice (Proxy u
forall k (t :: k). Proxy t
Proxy @u)

-- |

--    Create an advice which only tweaks and/or analyzes the function arguments.

--

--    Notice that there's no @u@ parameter, unlike with 'makeAdvice'.

--

-- >>> :{

--  doesNothing :: forall ca cem cr. Advice ca cem cr

--  doesNothing = makeArgsAdvice pure

-- :}

makeArgsAdvice ::
  forall ca cem cr.
  -- | The function that tweaks the arguments.

  ( forall as e m.
    (All ca as, cem e m, Monad m) =>
    NP I as ->
    DepT e m (NP I as)
  ) ->
  Advice ca cem cr
makeArgsAdvice :: (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
 (All ca as, cem e m, Monad m) =>
 NP I as -> DepT e m (NP I as))
-> Advice ca cem cr
makeArgsAdvice forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (NP I as)
tweakArgs =
  (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
 (All ca as, cem e m, Monad m) =>
 NP I as -> DepT e m ((), NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    () -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
(forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
 (All ca as, cem e m, Monad m) =>
 NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeAdvice @()
    ( \NP I as
args -> do
        NP I as
args <- NP I as -> DepT e m (NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (NP I as)
tweakArgs NP I as
args
        ((), NP I as) -> DepT e m ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((), NP I as
args)
    )
    ((DepT e m r -> DepT e m r) -> () -> DepT e m r -> DepT e m r
forall a b. a -> b -> a
const DepT e m r -> DepT e m r
forall a. a -> a
id)

-- |

--    Create an advice which only tweaks the execution of the final monadic action.

--

--    Notice that there's no @u@ parameter, unlike with 'makeAdvice'.

--

-- >>> :{

--  doesNothing :: forall ca cem cr. Advice ca cem cr

--  doesNothing = makeExecutionAdvice id

-- :}

makeExecutionAdvice ::
  forall ca cem cr.
  -- | The function that tweaks the execution.

  ( forall e m r.
    (cem e m, Monad m, cr r) =>
    DepT e m r ->
    DepT e m r
  ) ->
  Advice ca cem cr
makeExecutionAdvice :: (forall (e :: (* -> *) -> *) (m :: * -> *) r.
 (cem e m, Monad m, cr r) =>
 DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeExecutionAdvice forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
DepT e m r -> DepT e m r
tweakExecution = (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
 (All ca as, cem e m, Monad m) =>
 NP I as -> DepT e m ((), NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    () -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
(forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
 (All ca as, cem e m, Monad m) =>
 NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
makeAdvice @() (\NP I as
args -> ((), NP I as) -> DepT e m ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NP I as -> ((), NP I as)
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP I as
args)) (\() DepT e m r
action -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
DepT e m r -> DepT e m r
tweakExecution DepT e m r
action)

data Pair a b = Pair !a !b

-- |

-- 'Ensure' is a helper for lifting typeclass definitions of the form:

--

-- >>> :{

--  type HasLogger :: Type -> (Type -> Type) -> Constraint

--  class HasLogger em m | em -> m where

--    logger :: em -> String -> m ()

-- :}

--

-- To work as the @cem@ constraint, like this:

--

-- >>> type FooAdvice = Advice Top (Ensure HasLogger) Top

--

-- Why is it necessary? Two-place @HasX@-style constraints receive the \"fully

-- applied\" type of the record-of-functions. That is: @NilEnv IO@ instead of

-- simply @NilEnv@. This allows them to also work with monomorphic

-- environments (like those in <http://hackage.haskell.org/package/rio RIO>) whose type isn't parameterized by any monad.

--

-- But the @cem@ constraint works with the type constructor of the environment

-- record, of kind @(Type -> Type) -> Type@, and not with the fully applied

-- type of kind @Type@.

type Ensure :: (Type -> (Type -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class c (e (DepT e m)) (DepT e m) => Ensure c e m

instance c (e (DepT e m)) (DepT e m) => Ensure c e m

-- | Apply an 'Advice' to some compatible function. The function must have its

-- effects in 'DepT', and satisfy the constraints required by the 'Advice'.

--

-- __/IMPORTANT!/__ If the @ca@, @cem@ or @cr@ constraints of the supplied

-- 'Advice' remain polymorphic, they must be given types by means of type

-- applications:

--

-- >>> :{

--  foo :: Int -> DepT NilEnv IO String

--  foo _ = pure "foo"

--  advisedFoo1 = advise (returnMempty @Top @Top2) foo

--  advisedFoo2 = advise @Top @Top2 returnMempty foo

--  advisedFoo3 = advise (printArgs @Top stdout "args: ") foo

--  advisedFoo4 = advise @_ @_ @Top (printArgs stdout "args: ") foo

-- :}

advise ::
  forall ca cem cr as e m r advisee.
  (Multicurryable as e m r advisee, All ca as, cem e m, Monad m, cr r) =>
  -- | The advice to apply.

  Advice ca cem cr ->
  -- | A function to be adviced.

  advisee ->
  advisee
advise :: Advice ca cem cr -> advisee -> advisee
advise (Advice Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) advisee
advisee = do
  let uncurried :: NP I as -> DepT e m r
uncurried = advisee -> NP I as -> DepT e m r
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
curried -> NP I as -> DepT e m r
multiuncurry @as @e @m @r advisee
advisee
      uncurried' :: NP I as -> DepT e m r
uncurried' NP I as
args = do
        (u
u, NP I as
args') <- NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs NP I as
args
        u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution u
u (NP I as -> DepT e m r
uncurried NP I as
args')
   in (NP I as -> DepT e m r) -> advisee
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
(NP I as -> DepT e m r) -> curried
multicurry @as @e @m @r NP I as -> DepT e m r
uncurried'

type Multicurryable ::
  [Type] ->
  ((Type -> Type) -> Type) ->
  (Type -> Type) ->
  Type ->
  Type ->
  Constraint
class Multicurryable as e m r curried | curried -> as e m r where
  type BaseMonadAtTheTip as e m r curried :: Type
  multiuncurry :: curried -> NP I as -> DepT e m r
  multicurry :: (NP I as -> DepT e m r) -> curried
  _runFromEnv :: m (e (DepT e m)) -> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried

instance Monad m => Multicurryable '[] e m r (DepT e m r) where
  type BaseMonadAtTheTip '[] e m r (DepT e m r) = m r
  multiuncurry :: DepT e m r -> NP I '[] -> DepT e m r
multiuncurry DepT e m r
action NP I '[]
Nil = DepT e m r
action
  multicurry :: (NP I '[] -> DepT e m r) -> DepT e m r
multicurry NP I '[] -> DepT e m r
f = NP I '[] -> DepT e m r
f NP I '[]
forall k (a :: k -> *). NP a '[]
Nil
  _runFromEnv :: m (e (DepT e m))
-> (e (DepT e m) -> DepT e m r)
-> BaseMonadAtTheTip '[] e m r (DepT e m r)
_runFromEnv m (e (DepT e m))
producer e (DepT e m) -> DepT e m r
extractor = do
    e (DepT e m)
e <- m (e (DepT e m))
producer
    DepT e m r -> e (DepT e m) -> m r
forall (env :: (* -> *) -> *) (m :: * -> *) r.
DepT env m r -> env (DepT env m) -> m r
runDepT (e (DepT e m) -> DepT e m r
extractor e (DepT e m)
e) e (DepT e m)
e

instance Multicurryable as e m r curried => Multicurryable (a ': as) e m r (a -> curried) where
  type BaseMonadAtTheTip (a ': as) e m r (a -> curried) = a -> BaseMonadAtTheTip as e m r curried
  multiuncurry :: (a -> curried) -> NP I (a : as) -> DepT e m r
multiuncurry a -> curried
f (I x
a :* NP I xs
as) = curried -> NP I as -> DepT e m r
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
curried -> NP I as -> DepT e m r
multiuncurry @as @e @m @r @curried (a -> curried
f a
x
a) NP I as
NP I xs
as
  multicurry :: (NP I (a : as) -> DepT e m r) -> a -> curried
multicurry NP I (a : as) -> DepT e m r
f a
a = (NP I as -> DepT e m r) -> curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
(NP I as -> DepT e m r) -> curried
multicurry @as @e @m @r @curried (NP I (a : as) -> DepT e m r
f (NP I (a : as) -> DepT e m r)
-> (NP I as -> NP I (a : as)) -> NP I as -> DepT e m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I a -> NP I as -> NP I (a : as)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
(:*) (a -> I a
forall a. a -> I a
I a
a))
  _runFromEnv :: m (e (DepT e m))
-> (e (DepT e m) -> a -> curried)
-> BaseMonadAtTheTip (a : as) e m r (a -> curried)
_runFromEnv m (e (DepT e m))
producer e (DepT e m) -> a -> curried
extractor a
a = m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
_runFromEnv @as @e @m @r @curried m (e (DepT e m))
producer (\e (DepT e m)
f -> e (DepT e m) -> a -> curried
extractor e (DepT e m)
f a
a)

-- | Given a base monad @m@ action that gets hold of the 'DepT' environment, run

-- the 'DepT' transformer at the tip of a curried function.

--

-- >>> :{

--  foo :: Int -> Int -> Int -> DepT NilEnv IO ()

--  foo _ _ _ = pure ()

-- :}

--

--  >>> runFinalDepT (pure NilEnv) foo 1 2 3 :: IO ()

runFinalDepT ::
  forall as e m r curried.
  Multicurryable as e m r curried =>
  -- | action that gets hold of the environment

  m (e (DepT e m)) ->
  -- | function to invoke with effects in 'DepT'

  curried ->
  -- | a new function with effects in the base monad

  BaseMonadAtTheTip as e m r curried
runFinalDepT :: m (e (DepT e m)) -> curried -> BaseMonadAtTheTip as e m r curried
runFinalDepT m (e (DepT e m))
producer curried
extractor = m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
_runFromEnv m (e (DepT e m))
producer (curried -> e (DepT e m) -> curried
forall a b. a -> b -> a
const curried
extractor)

-- | Given a base monad @m@ action that gets hold of the 'DepT' environment,

-- and a function capable of extracting a curried function from the

-- environment, run the 'DepT' transformer at the tip of the resulting curried

-- function.

--

-- Why put the environment behind the @m@ action? Well, since getting to the

-- end of the curried function takes some work, it's a good idea to have some

-- flexibility once we arrive there. For example, the environment could be

-- stored in a "Data.IORef" and change in response to events, perhaps with

-- advices being added or removed.

--

-- >>> :{

--   type MutableEnv :: (Type -> Type) -> Type

--   data MutableEnv m = MutableEnv { _foo :: Int -> m (Sum Int) }

--   :}

--

-- >>> :{

--   do envRef <- newIORef (MutableEnv (pure . Sum))

--      let foo' = runFromEnv (readIORef envRef) _foo

--      do r <- foo' 7

--         print r

--      modifyIORef envRef (\e -> e { _foo = advise @Top @Top2 returnMempty (_foo e) })

--      do r <- foo' 7

--         print r

-- :}

-- Sum {getSum = 7}

-- Sum {getSum = 0}

runFromEnv ::
  forall as e m r curried.
  (Multicurryable as e m r curried, Monad m) =>
  -- | action that gets hold of the environment

  m (e (DepT e m)) ->
  -- | gets a function from the environment with effects in 'DepT'

  (e (DepT e m) -> curried) ->
  -- | a new function with effects in the base monad

  BaseMonadAtTheTip as e m r curried
runFromEnv :: m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
runFromEnv = m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *) r curried.
Multicurryable as e m r curried =>
m (e (DepT e m))
-> (e (DepT e m) -> curried) -> BaseMonadAtTheTip as e m r curried
_runFromEnv

-- |

--    A two-place constraint which requires nothing of the environment and the

--    base monad.

--

--    Useful as the @cem@ type application argument of 'advise' and 'restrictEnv'.

--

--    For similar behavior with the @ar@ and @cr@ type arguments of 'advise' and

--    'restrictEnv', use 'Top' from \"sop-core\".

--

-- >>> type UselessAdvice = Advice Top Top2 Top

type Top2 :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class Top2 e m

instance Top2 e m

-- |

--    Combines two two-place constraints on the environment / monad pair.

--

--    For example, an advice which requires both @Ensure HasLogger@ and @Ensure

--    HasRepository@ might use this.

--

--    Useful to build the @cem@ type application argument of 'advise' and

--    'restrictEnv'.

--

--    For similar behavior with the @ar@ and @cr@ type arguments of 'advise' and

--    'restrictEnv', use 'And' from \"sop-core\".

type And2 ::
  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint) ->
  (((Type -> Type) -> Type) -> (Type -> Type) -> Constraint)
class (f e m, g e m) => (f `And2` g) e m

instance (f e m, g e m) => (f `And2` g) e m

infixl 7 `And2`

-- | A class synonym for @(~)@, the type equality constraint.

--

-- Poly-kinded, so it can be applied both to type constructors (like monads) and to concrete types.

--

-- It this library it will be used partially applied:

--

-- >>> type FooAdvice = Advice Top (MonadConstraint (MustBe IO)) Top

--

-- >>>  type FooAdvice = Advice Top Top2 (MustBe String)

type MustBe :: forall k. k -> k -> Constraint
class x ~ y => MustBe x y

instance x ~ y => MustBe x y

-- |

-- Pins both the environment type constructor and the base monad. Sometimes we

-- don't want to advise functions in some generic environment, but in a

-- concrete environment having access to all the fields, and in a concrete base

-- monad.

--

-- Useful to build the @cem@ type application argument of 'advise' and

-- 'restricEnv'.

--

-- For similar behavior with the @ar@ and @cr@ type arguments of 'advise'

-- and 'restrictEnv', use 'MustBe'.

--

-- It this library it will be used partially applied:

--

-- >>> type FooAdvice = Advice Top (MustBe2 NilEnv IO) Top

type MustBe2 :: ((Type -> Type) -> Type) -> (Type -> Type) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class (e' ~ e, m' ~ m) => MustBe2 e' m' e m

instance (e' ~ e, m' ~ m) => MustBe2 e' m' e m

-- |

--    Require a constraint only on the /unapplied/ environment type constructor, which has kind @(Type -> Type) -> Type@.

--

--    Can be used to build @cem@ type application argument of 'advise' and 'restrictEnv'.

--

--    Most of the time this is /not/ what you want. One exception is when

--    pinning the environment with a 'MustBe' equality constraint, while

--    leaving the base monad free:

--

--    >>> type FooAdvice = Advice Top (EnvConstraint (MustBe NilEnv)) Top

--

--    If what you want is to lift a two-parameter @HasX@-style typeclass to @cem@, use 'Ensure' instead.

type EnvConstraint :: (((Type -> Type) -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class c e => EnvConstraint c e m

instance c e => EnvConstraint c e m

-- |

--    Require a constraint only on the base monad, for example a base moonad with @MonadIO@.

--

--    Useful to build @cem@ type application argument of 'advise' and 'restrictEnv'.

--

--    >>> type FooAdvice = Advice Top (MonadConstraint MonadIO) Top

--

--    >>> type FooAdvice = Advice Top (MonadConstraint (MonadReader Int)) Top

type MonadConstraint :: ((Type -> Type) -> Constraint) -> ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
class c m => MonadConstraint c e m

instance c m => MonadConstraint c e m

-- $restrict

--

--    'Advice' values can be composed using the 'Monoid' instance, but only if

--    the have the same constraint parameters. It's unfortunate that—unlike with

--    normal functions—'Advice' constaints aren't automatically "collected"

--    during composition.

--

--    We need to harmonize the constraints on each 'Advice' by turning them

--    into the combination of all constraints. The functions in this section

--    help with that.

--

--    These functions take as parameter evidence of entailment between

--    constraints, using the type '(:-)' from the \"constraints\" package.  But

--    how to construct such evidence? By using the 'Sub' and the 'Dict'

--    constructors, with either an explicit type signature:

--

-- >>> :{

-- returnMempty' :: Advice ca cem (Monoid `And` Show)

-- returnMempty' = restrictResult (Sub Dict) returnMempty

-- :}

--

-- or with a type application to the restriction function:

--

-- >>> :{

-- returnMempty'' :: Advice ca cem (Monoid `And` Show)

-- returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty

-- :}

--

-- Another example:

--

-- >>> :{

--  type HasLogger :: Type -> (Type -> Type) -> Constraint

--  class HasLogger em m | em -> m where

--    logger :: em -> String -> m ()

--  doLogging :: Advice Show (Ensure HasLogger) cr

--  doLogging = undefined

--  type EnsureLoggerAndWriter :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint

--  type EnsureLoggerAndWriter = Ensure HasLogger `And2` MonadConstraint MonadIO

--  doLogging':: Advice Show EnsureLoggerAndWriter cr

--  doLogging'= restrictEnv (Sub Dict) doLogging

--  doLogging'' = restrictEnv @EnsureLoggerAndWriter (Sub Dict) doLogging

-- :}


-- | Makes the constraint on the arguments more restrictive.

restrictArgs ::
  forall more less cem cr.
  -- | Evidence that one constraint implies the other.

  (forall r. more r :- less r) ->
  -- | Advice with less restrictive constraint on the args.

  Advice less cem cr ->
  -- | Advice with more restrictive constraint on the args.

  Advice more cem cr
-- about the order of the type parameters... which is more useful?

-- A possible principle to follow:

-- We are likely to know the "less" constraint, because advices are likely to

-- come pre-packaged and having a type signature.

-- We arent' so sure about having a signature for a whole composed Advice,

-- because the composition might be done

-- on the fly, while constructing a record, without a top-level binding with a

-- type signature.  This seems to favor putting "more" first.

restrictArgs :: (forall r. more r :- less r)
-> Advice less cem cr -> Advice more cem cr
restrictArgs forall r. more r :- less r
evidence (Advice Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) =
  let captureExistential ::
        forall more less cem cr u.
        (forall r. more r :- less r) ->
        Proxy u ->
        ( forall as e m.
          (All less as, cem e m, Monad m) =>
          NP I as ->
          DepT e m (u, NP I as)
        ) ->
        ( forall e m r.
          (cem e m, Monad m, cr r) =>
          u ->
          DepT e m r ->
          DepT e m r
        ) ->
        Advice more cem cr
      captureExistential :: (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All less as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
captureExistential forall r. more r :- less r
evidence' Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' =
        Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All more as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
          (Proxy u
forall k (t :: k). Proxy t
Proxy @u)
          ( let tweakArgs'' :: forall as e m. (All more as, cem e m, Monad m) => NP I as -> DepT e m (u, NP I as)
                tweakArgs'' :: NP I as -> DepT e m (u, NP I as)
tweakArgs'' = case (forall a. Dict more a -> Dict less a)
-> Dict (All more) as -> Dict (All less) as
forall k (c :: k -> Constraint) (d :: k -> Constraint) (xs :: [k]).
(forall (a :: k). Dict c a -> Dict d a)
-> Dict (All c) xs -> Dict (All d) xs
SOP.mapAll @more @less ((forall r. more r :- less r) -> Dict more a -> Dict less a
forall k (more :: k -> Constraint) (less :: k -> Constraint)
       (a :: k).
(forall (x :: k). more x :- less x) -> Dict more a -> Dict less a
translateEvidence @more @less forall r. more r :- less r
evidence') of
                  Dict (All more) as -> Dict (All less) as
f -> case Dict (All more) as -> Dict (All less) as
f (All more as => Dict (All more) as
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
SOP.Dict @(All more) @as) of
                    Dict (All less) as
SOP.Dict -> \NP I as
args -> NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' @as @e @m NP I as
args
             in NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All more as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs''
          )
          forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution'
   in (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All less as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
forall (more :: * -> Constraint) (less :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint) u.
(forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All less as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice more cem cr
captureExistential forall r. more r :- less r
evidence Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All less as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution

-- |

--    Makes the constraint on the environment / monad more restrictive.

restrictEnv ::
  forall more ca less cr.
  -- | Evidence that one constraint implies the other.

  (forall e m. more e m :- less e m) ->
  -- | Advice with less restrictive constraint on the environment and base monad.

  Advice ca less cr ->
  -- | Advice with more restrictive constraint on the environment and base monad.

  Advice ca more cr
restrictEnv :: (forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Advice ca less cr -> Advice ca more cr
restrictEnv forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence (Advice Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) =
  let captureExistential ::
        forall more ca less cr u.
        (forall e m. more e m :- less e m) ->
        Proxy u ->
        ( forall as e m.
          (All ca as, less e m, Monad m) =>
          NP I as ->
          DepT e m (u, NP I as)
        ) ->
        ( forall e m r.
          (less e m, Monad m, cr r) =>
          u ->
          DepT e m r ->
          DepT e m r
        ) ->
        Advice ca more cr
      captureExistential :: (forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, less e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (less e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
captureExistential forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence' Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' =
        Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, more e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (more e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
          (Proxy u
forall k (t :: k). Proxy t
Proxy @u)
          ( let tweakArgs'' :: forall as e m. (All ca as, more e m, Monad m) => NP I as -> DepT e m (u, NP I as)
                tweakArgs'' :: NP I as -> DepT e m (u, NP I as)
tweakArgs'' = case more e m :- less e m
forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence' @e @m of Sub more e m => Dict (less e m)
Dict -> \NP I as
args -> NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' @as @e @m NP I as
args
             in NP I as -> DepT e m (u, NP I as)
forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, more e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs''
          )
          ( let tweakExecution'' :: forall e m r. (more e m, Monad m, cr r) => u -> DepT e m r -> DepT e m r
                tweakExecution'' :: u -> DepT e m r -> DepT e m r
tweakExecution'' = case more e m :- less e m
forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence' @e @m of Sub more e m => Dict (less e m)
Dict -> \u
u DepT e m r
action -> u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' @e @m @r u
u DepT e m r
action
             in u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(more e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution''
          )
   in (forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, less e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (less e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
forall (more :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (ca :: * -> Constraint)
       (less :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint) u.
(forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, less e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (less e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca more cr
captureExistential forall (e :: (* -> *) -> *) (m :: * -> *). more e m :- less e m
evidence Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, less e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(less e m, Monad m, cr r) =>
u -> DepT e m r -> DepT e m r
tweakExecution

-- |

--    Makes the constraint on the result more restrictive.

restrictResult ::
  forall more ca cem less.
  -- | Evidence that one constraint implies the other.

  (forall r. more r :- less r) ->
  -- | Advice with less restrictive constraint on the result.

  Advice ca cem less ->
  -- | Advice with more restrictive constraint on the result.

  Advice ca cem more
restrictResult :: (forall r. more r :- less r)
-> Advice ca cem less -> Advice ca cem more
restrictResult forall r. more r :- less r
evidence (Advice Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution) =
  let captureExistential ::
        forall more ca cem less u.
        (forall r. more r :- less r) ->
        Proxy u ->
        ( forall as e m.
          (All ca as, cem e m, Monad m) =>
          NP I as ->
          DepT e m (u, NP I as)
        ) ->
        ( forall e m r.
          (cem e m, Monad m, less r) =>
          u ->
          DepT e m r ->
          DepT e m r
        ) ->
        Advice ca cem more
      captureExistential :: (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, less r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
captureExistential forall r. more r :- less r
evidence' Proxy u
_ forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs' forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' =
        Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, more r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
forall u (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (cr :: * -> Constraint).
Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, cr r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem cr
Advice
          (Proxy u
forall k (t :: k). Proxy t
Proxy @u)
          forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs'
          ( let tweakExecution'' :: forall e m r. (cem e m, Monad m, more r) => u -> DepT e m r -> DepT e m r
                tweakExecution'' :: u -> DepT e m r -> DepT e m r
tweakExecution'' = case more r :- less r
forall r. more r :- less r
evidence' @r of Sub more r => Dict (less r)
Dict -> \u
u DepT e m r
action -> u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution' @e @m @r u
u DepT e m r
action
             in u -> DepT e m r -> DepT e m r
forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, more r) =>
u -> DepT e m r -> DepT e m r
tweakExecution''
          )
   in (forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, less r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
forall (more :: * -> Constraint) (ca :: * -> Constraint)
       (cem :: ((* -> *) -> *) -> (* -> *) -> Constraint)
       (less :: * -> Constraint) u.
(forall r. more r :- less r)
-> Proxy u
-> (forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
    (All ca as, cem e m, Monad m) =>
    NP I as -> DepT e m (u, NP I as))
-> (forall (e :: (* -> *) -> *) (m :: * -> *) r.
    (cem e m, Monad m, less r) =>
    u -> DepT e m r -> DepT e m r)
-> Advice ca cem more
captureExistential forall r. more r :- less r
evidence Proxy u
proxy forall (as :: [*]) (e :: (* -> *) -> *) (m :: * -> *).
(All ca as, cem e m, Monad m) =>
NP I as -> DepT e m (u, NP I as)
tweakArgs forall (e :: (* -> *) -> *) (m :: * -> *) r.
(cem e m, Monad m, less r) =>
u -> DepT e m r -> DepT e m r
tweakExecution

translateEvidence :: forall more less a. (forall x. more x :- less x) -> SOP.Dict more a -> SOP.Dict less a
translateEvidence :: (forall (x :: k). more x :- less x) -> Dict more a -> Dict less a
translateEvidence forall (x :: k). more x :- less x
evidence Dict more a
SOP.Dict =
  case more a :- less a
forall (x :: k). more x :- less x
evidence @a of
    Sub more a => Dict (less a)
Dict -> less a => Dict less a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
SOP.Dict @less @a

-- $sop

-- Some useful definitions re-exported the from \"sop-core\" package.

--

-- 'NP' is an n-ary product used to represent the arguments of advised functions.

--

-- 'I' is an identity functor. The arguments processed by an 'Advice' come wrapped in it.

--

-- 'cfoldMap_NP' is useful to construct homogeneous lists out of the 'NP' product, for example:

--

-- >>> cfoldMap_NP (Proxy @Show) (\(I a) -> [show a]) (I False :* I (1::Int) :* Nil)

-- ["False","1"]


-- $constraints

--

-- Some useful definitions re-exported the from \"constraints\" package.

--

-- 'Dict' and '(:-)' are GADTs used to capture and transform constraints. Used in the 'restrictArgs', 'restrictEnv' and 'restrictResult' functions.


-- $constrainthelpers

-- Some  <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ class synonyms>

-- to help create the constraints that parameterize the 'Advice' type.

--

-- This library also re-exports the 'Top', 'And' and 'All' helpers from \"sop-core\":

--

-- * 'Top' is the \"always satisfied\" constraint, useful when whe don't want to require anything specific in @ca@ or @cr@ (@cem@ requires 'Top2').

--

-- * 'And' combines constraints for @ca@ or @cr@ (@cem@ requires 'And2').

--

-- * 'All' says that some constraint is satisfied by all the components of an 'NP'

-- product. In this library, it's used to stipulate constraints on the

-- arguments of advised functions.


-- $invocation

-- There functions are helpers for running 'DepT' computations, beyond what 'runDepT' provides.

--

-- They aren't directly related to 'Advice's, but they require some of the same machinery, and that's why they are here.