dep-t-advice 0.1.0.0 → 0.2.0.0

raw patch · 7 files changed

+312/−375 lines, 7 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• README.md +2/−6
• dep-t-advice.cabal +15/−6
• lib/Control/Monad/Dep/Advice.hs +135/−339
• lib/Control/Monad/Dep/Advice/Basic.hs +75/−5
• test/tests.hs +31/−19
• test/weird-advice-tests.hs +46/−0

@@ -1,5 +1,13 @@ # Revision history for dep-t-advice
 
+## 0.2.0.0 
+
+* BREAKING CHANGE. The Advice type is no longer parameterized by the `cem` and
+  `cr` constraints. Instead, it's directly parameterized by the types @e@ of
+  the environment, @m@ of the base monad and @r@ of the result, which are left
+  polymorphic when needed. This simplifies a bunch of things. The `ca`
+  constraint paramter remains however.
+
 ## 0.1.0.0 -- YYYY-mm-dd
 
 * First version. Released on an unsuspecting world.

@@ -80,7 +80,7 @@ 
 Here's how a `printArgs` advice might be defined:
 
-    printArgs :: forall cr. Handle -> String -> Advice Show (BaseConstraint MonadIO) cr
+    printArgs :: forall e m r. MonadIO m => Handle -> String -> Advice Show e m r
     printArgs h prefix =
       makeArgsAdvice
         ( \args -> do
@@ -99,11 +99,7 @@ 
 The advice would be applied like this:
 
-    advise (printArgs @Top stdout "foo args: ") foo
-
-The `@Top` type application is necessary because `printArgs` is polymorphic on
-the `cr` constraint on the function results, and the `advise` function requires
-all the constraints to be "concrete" in order to apply the advice. 
+    advise (printArgs stdout "foo args: ") foo
 
 ## Advices should be applied at the composition root
 

@@ -1,7 +1,7 @@ cabal-version:       3.0
 
 name:                dep-t-advice
-version:             0.1.0.0
+version:             0.2.0.0
 synopsis:            Giving good advice to functions in a DepT environment.
 description:         Companion to the dep-t package. Easily add behaviour to functions living in a DepT environment, 
                      whatever the number of arguments they might have.
@@ -36,6 +36,14 @@                        mtl                ^>= 2.2,
                        template-haskell,
 
+
+common common-tasty
+  import:              common-tests
+  hs-source-dirs:      test
+  build-depends:       
+                       tasty              >= 1.3.1,
+                       tasty-hunit        >= 0.10.0.2,
+
 library
   import: common
   exposed-modules:     Control.Monad.Dep.Advice
@@ -43,13 +51,14 @@   hs-source-dirs:      lib 
 
 test-suite tests
-  import:              common-tests
+  import:              common-tasty
   type:                exitcode-stdio-1.0
-  hs-source-dirs:      test
   main-is:             tests.hs
-  build-depends:       
-                       tasty              >= 1.3.1,
-                       tasty-hunit        >= 0.10.0.2,
+
+test-suite weird-advice-tests
+  import:              common-tasty
+  type:                exitcode-stdio-1.0
+  main-is:             weird-advice-tests.hs
 
 -- VERY IMPORTANT for doctests to work: https://stackoverflow.com/a/58027909/1364288
 -- http://hackage.haskell.org/package/cabal-doctest

@@ -19,7 +19,7 @@ {-# LANGUAGE UndecidableSuperClasses #-}
 
 -- |
---    This package provices the 'Advice' datatype, along for functions for creating,
+--    This package provides 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
@@ -36,35 +36,38 @@ --
 -- They work for @DepT@-actions of zero arguments:
 --
--- >>> advise (printArgs @Top stdout "foo0") foo0 `runDepT` NilEnv
+-- >>> advise (printArgs 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
+-- >>> advise (printArgs stdout "foo1") foo1 False `runDepT` NilEnv
 -- foo1: False
 -- <BLANKLINE>
 -- Sum {getSum = 5}
 --
--- >>> advise (printArgs @Top stdout "foo2") foo2 'd' False `runDepT` NilEnv
+-- >>> advise (printArgs 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
+-- >>> advise (returnMempty @Top) 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):
+-- And they can be combined using @Advice@'s 'Monoid' instance before being
+-- applied:
 --
 -- >>> advise (printArgs stdout "foo2" <> returnMempty) foo2 'd' False `runDepT` NilEnv
 -- foo2: 'd' False
 -- <BLANKLINE>
 -- Sum {getSum = 0}
+--
+-- Although sometimes composition might require harmonizing the constraints
+-- each 'Advice' places on the arguments, if they differ.
 module Control.Monad.Dep.Advice
   ( -- * The Advice type
     Advice,
@@ -80,18 +83,10 @@     -- * Constraint helpers
     -- $constrainthelpers
     Ensure,
-    Top2,
-    And2,
-    MonadConstraint,
-    EnvConstraint,
-    MustBe,
-    MustBe2,
 
-    -- * Combining Advices by harmonizing their constraints
+    -- * Harmonizing Advice argument constraints
     -- $restrict
     restrictArgs,
-    restrictEnv,
-    restrictResult,
 
     -- * Invocation helpers
     -- $invocation
@@ -131,6 +126,7 @@ -- >>> :set -XTypeOperators
 -- >>> :set -XConstraintKinds
 -- >>> :set -XNamedFieldPuns
+-- >>> :set -XFlexibleContexts
 -- >>> import Control.Monad
 -- >>> import Control.Monad.Dep
 -- >>> import Control.Monad.Dep.Advice
@@ -143,51 +139,42 @@ -- >>> 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.
+-- | A generic transformation of 'DepT'-effectful functions with environment
+-- @e@ of kind @(Type -> Type) -> Type@, base monad @m@ and return type @r@,
+-- provided the functions satisfy certain constraint @ca@ of kind @Type ->
+-- Constraint@ on all of their arguments.
 --
--- 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@.
+-- Note that the environment @e@ must be parameterizable by a monad, and the type
+-- constructor is given unapplied. That is, @Advice Show NilEnv IO ()@
+-- kind-checks but @Advice Show (NilEnv IO) IO ()@ doesn't. See also 'Ensure'.
 --
--- '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'.
+-- 'Advice's that don't care about the @ca@ constraint (because they don't
+-- touch function arguments) can leave it polymorphic, and this facilitates
+-- 'Advice' composition, but then the constraint must be given the catch-all
+-- `Top` value (using a 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 -> Type) -> Type) ->
+  (Type -> Type) ->
+  Type ->
   Type
-data Advice ca cem cr where
+data Advice ca e m r where
   Advice ::
-    forall u ca cem cr.
+    forall u ca e m r.
     Proxy u ->
-    ( forall as e m.
-      (All ca as, cem e m, Monad m) =>
+    ( forall as.
+      All ca as =>
       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 ca e m r
 
 -- |
 --    Aspects compose \"sequentially\" when tweaking the arguments, and
@@ -195,65 +182,61 @@ --
 --    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
+instance Monad m => Semigroup (Advice ca e m r) where
   Advice outer tweakArgsOuter tweakExecutionOuter <> Advice inner tweakArgsInner tweakExecutionInner =
     let captureExistentials ::
-          forall ca cem cr outer inner.
+          forall ca e r outer inner.
           Proxy outer ->
-          ( forall as e m.
-            (All ca as, cem e m, Monad m) =>
+          ( forall as.
+            All ca as =>
             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) =>
+          ( forall as.
+            All ca as =>
             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
+          Advice ca e m r
         captureExistentials _ tweakArgsOuter' tweakExecutionOuter' _ tweakArgsInner' tweakExecutionInner' =
           Advice
             (Proxy @(Pair outer inner))
             ( let tweakArgs ::
-                    forall as e m.
-                    (All ca as, cem e m, Monad m) =>
+                    forall as.
+                    All ca as =>
                     NP I as ->
                     DepT e m (Pair outer inner, NP I as)
                   tweakArgs args =
                     do
-                      (uOuter, argsOuter) <- tweakArgsOuter' @as @e @m args
-                      (uInner, argsInner) <- tweakArgsInner' @as @e @m argsOuter
+                      (uOuter, argsOuter) <- tweakArgsOuter' @as args
+                      (uInner, argsInner) <- tweakArgsInner' @as argsOuter
                       pure (Pair uOuter uInner, argsInner)
                in 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 uOuter uInner) action ->
-                        tweakExecutionOuter' @e @m @r uOuter (tweakExecutionInner' @e @m @r uInner action)
+                        tweakExecutionOuter' uOuter (tweakExecutionInner' uInner action)
                     )
                in tweakExecution
             )
-     in captureExistentials @ca @cem @cr outer tweakArgsOuter tweakExecutionOuter inner tweakArgsInner tweakExecutionInner
+     in captureExistentials @ca @e outer tweakArgsOuter tweakExecutionOuter inner tweakArgsInner tweakExecutionInner
 
-instance Monoid (Advice ca cem cr) where
+instance Monad m => Monoid (Advice ca e m r) where
   mappend = (<>)
   mempty = Advice (Proxy @()) (\args -> pure (pure args)) (const id)
 
@@ -272,29 +255,28 @@ --    type @u@ calculated earlier.
 --
 -- >>> :{
---  doesNothing :: forall ca cem cr. Advice ca cem cr
+--  doesNothing :: forall ca e m r. Monad m => Advice ca e m r
 --  doesNothing = makeAdvice @() (\args -> pure (pure args)) (\() action -> action)
 -- :}
 --
---    __/IMPORTANT!/__ When invoking 'makeAdvice', you must always give the
+--    __/TYPE APPLICATION REQUIRED!/__ 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.
+  forall u ca e m r.
   -- | The function that tweaks the arguments.
-  ( forall as e m.
-    (All ca as, cem e m, Monad m) =>
+  ( forall as.
+    All ca as =>
     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
+  Advice ca e m r
 makeAdvice = Advice (Proxy @u)
 
 -- |
@@ -303,18 +285,19 @@ --    Notice that there's no @u@ parameter, unlike with 'makeAdvice'.
 --
 -- >>> :{
---  doesNothing :: forall ca cem cr. Advice ca cem cr
+--  doesNothing :: forall ca e m r. Monad m => Advice ca e m r
 --  doesNothing = makeArgsAdvice pure
 -- :}
 makeArgsAdvice ::
-  forall ca cem cr.
+  forall ca e m r.
+  Monad m => 
   -- | The function that tweaks the arguments.
-  ( forall as e m.
-    (All ca as, cem e m, Monad m) =>
+  ( forall as.
+    All ca as =>
     NP I as ->
     DepT e m (NP I as)
   ) ->
-  Advice ca cem cr
+  Advice ca e m r
 makeArgsAdvice tweakArgs =
   makeAdvice @()
     ( \args -> do
@@ -329,18 +312,18 @@ --    Notice that there's no @u@ parameter, unlike with 'makeAdvice'.
 --
 -- >>> :{
---  doesNothing :: forall ca cem cr. Advice ca cem cr
+--  doesNothing :: forall ca e m r. Monad m => Advice ca e m r
 --  doesNothing = makeExecutionAdvice id
 -- :}
 makeExecutionAdvice ::
-  forall ca cem cr.
+  forall ca e m r.
+  Applicative m =>
   -- | 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
+  Advice ca e m r
 makeExecutionAdvice tweakExecution = makeAdvice @() (\args -> pure (pure args)) (\() action -> tweakExecution action)
 
 data Pair a b = Pair !a !b
@@ -354,43 +337,51 @@ --    logger :: em -> String -> m ()
 -- :}
 --
--- To work as the @cem@ constraint, like this:
+-- To work as a constraints on the @e@ and @m@ parameters of an 'Advice', like this:
 --
--- >>> type FooAdvice = Advice Top (Ensure HasLogger) Top
+-- >>> :{ 
+--  requiresLogger :: forall e m r. (Ensure HasLogger e m, Monad m) => Advice Show e m r
+--  requiresLogger = mempty
+--  :}
 --
 -- 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.
+-- 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@.
+-- But the @e@ type parameter of 'Advice' has kind @(Type -> Type) -> Type@.
+-- That is: @NilEnv@ alone.
+--
+-- Furthermore, 'Advices' require @HasX@-style constraints to be placed on the
+-- @DepT@ transformer, not directly on the base monad @m@. @Ensure@ takes care
+-- of that as well.
 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
+type Ensure c e m = c (e (DepT e m)) (DepT 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:
+-- effects in 'DepT', and all of its arguments must satisfy the @ca@ constraint.
 --
 -- >>> :{
 --  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
+--  advisedFoo = advise (printArgs stdout "Foo args: ") foo
 -- :}
+--
+-- __/TYPE APPLICATION REQUIRED!/__ If the @ca@ constraint of the 'Advice' remains polymorphic,
+-- it must be supplied by means of a type application:
+--
+-- >>> :{
+--  bar :: Int -> DepT NilEnv IO String
+--  bar _ = pure "bar"
+--  advisedBar1 = advise (returnMempty @Top) bar
+--  advisedBar2 = advise @Top returnMempty bar
+-- :}
 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) =>
+  forall ca e m r as advisee.
+  (Multicurryable as e m r advisee, All ca as, Monad m) =>
   -- | The advice to apply.
-  Advice ca cem cr ->
+  Advice ca e m r ->
   -- | A function to be adviced.
   advisee ->
   advisee
@@ -409,13 +400,13 @@   Type ->
   Constraint
 class Multicurryable as e m r curried | curried -> as e m r where
-  type BaseMonadAtTheTip as e m r curried :: Type
+  type DownToBaseMonad 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
+  _runFromEnv :: m (e (DepT e m)) -> (e (DepT e m) -> curried) -> DownToBaseMonad 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
+  type DownToBaseMonad '[] e m r (DepT e m r) = m r
   multiuncurry action Nil = action
   multicurry f = f Nil
   _runFromEnv producer extractor = do
@@ -423,7 +414,7 @@     runDepT (extractor e) 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
+  type DownToBaseMonad (a ': as) e m r (a -> curried) = a -> DownToBaseMonad as e m r curried
   multiuncurry f (I a :* as) = multiuncurry @as @e @m @r @curried (f a) as
   multicurry f a = multicurry @as @e @m @r @curried (f . (:*) (I a))
   _runFromEnv producer extractor a = _runFromEnv @as @e @m @r @curried producer (\f -> extractor f a)
@@ -445,7 +436,7 @@   -- | function to invoke with effects in 'DepT'
   curried ->
   -- | a new function with effects in the base monad
-  BaseMonadAtTheTip as e m r curried
+  DownToBaseMonad as e m r curried
 runFinalDepT producer extractor = _runFromEnv producer (const extractor)
 
 -- | Given a base monad @m@ action that gets hold of the 'DepT' environment,
@@ -469,7 +460,7 @@ --      let foo' = runFromEnv (readIORef envRef) _foo
 --      do r <- foo' 7
 --         print r
---      modifyIORef envRef (\e -> e { _foo = advise @Top @Top2 returnMempty (_foo e) })
+--      modifyIORef envRef (\e -> e { _foo = advise @Top returnMempty (_foo e) })
 --      do r <- foo' 7
 --         print r
 -- :}
@@ -477,167 +468,51 @@ -- Sum {getSum = 0}
 runFromEnv ::
   forall as e m r curried.
-  (Multicurryable as e m r curried, Monad m) =>
+  Multicurryable as e m r curried =>
   -- | 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
+  DownToBaseMonad as e m r curried
 runFromEnv = _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.
+--    they have the same type parameters. It's unfortunate that—unlike with
+--    normal function constraints—the @ca@ constraints of an 'Advice' 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
+--    Instead, we need to harmonize the @ca@ constraints of each 'Advice' by turning them
+--    into the combination of all constraints. 'restrictArgs' help with that.
 --    help with that.
 --
---    These functions take as parameter evidence of entailment between
+--    'restrictArgs' takes as parameter evidence of entailment between @ca@
 --    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:
+--    constructors, either with an explicit type signature:
 --
 -- >>> :{
--- returnMempty' :: Advice ca cem (Monoid `And` Show)
--- returnMempty' = restrictResult (Sub Dict) returnMempty
+--  stricterPrintArgs :: forall e m r. MonadIO m => Advice (Show `And` Eq `And` Ord) NilEnv m r
+--  stricterPrintArgs = restrictArgs (Sub Dict) (printArgs stdout "foo")
 -- :}
 --
--- or with a type application to the restriction function:
+--    or with a type application to 'restrictArgs':
 --
--- >>> :{
--- returnMempty'' :: Advice ca cem (Monoid `And` Show)
--- returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty
--- :}
+-- >>> stricterPrintArgs = restrictArgs @(Show `And` Eq `And` Ord) (Sub Dict) (printArgs stdout "foo")
 --
--- 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.
+  forall more less e m r.
   -- | Evidence that one constraint implies the other.
-  (forall r. more r :- less r) ->
+  (forall x. more x :- less x) ->
   -- | Advice with less restrictive constraint on the args.
-  Advice less cem cr ->
+  Advice less e m r ->
   -- | Advice with more restrictive constraint on the args.
-  Advice more cem cr
+  Advice more e m r
 -- 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
@@ -648,110 +523,33 @@ -- type signature.  This seems to favor putting "more" first.
 restrictArgs evidence (Advice proxy tweakArgs tweakExecution) =
   let captureExistential ::
-        forall more less cem cr u.
-        (forall r. more r :- less r) ->
+        forall more less e m r u.
+        (forall x. more x :- less x) ->
         Proxy u ->
-        ( forall as e m.
-          (All less as, cem e m, Monad m) =>
+        ( forall as.
+          All less as =>
           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
+        Advice more e m r
       captureExistential evidence' _ tweakArgs' tweakExecution' =
         Advice
           (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)
+          ( let tweakArgs'' :: forall as. All more as => NP I as -> DepT e m (u, NP I as)
                 tweakArgs'' = case SOP.mapAll @more @less (translateEvidence @more @less evidence') of
                   f -> case f (SOP.Dict @(All more) @as) of
-                    SOP.Dict -> \args -> tweakArgs' @as @e @m args
+                    SOP.Dict -> \args -> tweakArgs' @as args
              in tweakArgs''
           )
           tweakExecution'
    in captureExistential evidence proxy tweakArgs 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 evidence (Advice proxy tweakArgs 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 evidence' _ tweakArgs' tweakExecution' =
-        Advice
-          (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'' = case evidence' @e @m of Sub Dict -> \args -> tweakArgs' @as @e @m args
-             in tweakArgs''
-          )
-          ( let tweakExecution'' :: forall e m r. (more e m, Monad m, cr r) => u -> DepT e m r -> DepT e m r
-                tweakExecution'' = case evidence' @e @m of Sub Dict -> \u action -> tweakExecution' @e @m @r u action
-             in tweakExecution''
-          )
-   in captureExistential evidence proxy tweakArgs 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 evidence (Advice proxy tweakArgs 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 evidence' _ tweakArgs' tweakExecution' =
-        Advice
-          (Proxy @u)
-          tweakArgs'
-          ( let tweakExecution'' :: forall e m r. (cem e m, Monad m, more r) => u -> DepT e m r -> DepT e m r
-                tweakExecution'' = case evidence' @r of Sub Dict -> \u action -> tweakExecution' @e @m @r u action
-             in tweakExecution''
-          )
-   in captureExistential evidence proxy tweakArgs tweakExecution
-
 translateEvidence :: forall more less a. (forall x. more x :- less x) -> SOP.Dict more a -> SOP.Dict less a
 translateEvidence evidence SOP.Dict =
   case evidence @a of
@@ -773,23 +571,21 @@ --
 -- 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.
+-- 'Dict' and '(:-)' are GADTs used to capture and transform constraints. Used in the 'restrictArgs' function.
 
 -- $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\":
+-- To help with the constraint @ca@ that parameterizes 'Advice', this library re-exports the following 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').
+-- * 'Top' is the \"always satisfied\" constraint, useful when whe don't want to require anything specific in @ca@.
 --
--- * 'And' combines constraints for @ca@ or @cr@ (@cem@ requires 'And2').
+-- * 'And' combines two constraints so that an 'Advice' can request them both, for example @Show \`And\` Eq@.
 --
--- * '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.
+-- Also, the 'All' constraint says that some constraint is satisfied by all the
+-- components of an 'NP' product. It's in scope when processing the function
+-- arguments inside an 'Advice'.
 
 -- $invocation
--- There functions are helpers for running 'DepT' computations, beyond what 'runDepT' provides.
+-- These 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.

@@ -18,6 +18,7 @@   ( -- * Basic advices
     returnMempty,
     printArgs,
+    doLocally,
     AnyEq (..),
     doCachingBadly,
     doAsyncBadly
@@ -35,16 +36,44 @@ import Type.Reflection
 import Control.Concurrent
 
+-- $setup
+--
+-- >>> :set -XTypeApplications
+-- >>> :set -XStandaloneKindSignatures
+-- >>> :set -XMultiParamTypeClasses
+-- >>> :set -XFunctionalDependencies
+-- >>> :set -XRankNTypes
+-- >>> :set -XTypeOperators
+-- >>> :set -XConstraintKinds
+-- >>> :set -XNamedFieldPuns
+-- >>> :set -XFlexibleContexts
+-- >>> :set -XFlexibleInstances
+-- >>> :set -XAllowAmbiguousTypes
+-- >>> :set -XBlockArguments
+-- >>> 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
+
+
+
 -- | Makes functions discard their result and always return 'mempty'.
 --
 -- Because it doesn't touch the arguments or require some effect from the
 -- environment, this 'Advice' is polymorphic on @ca@ and @cem@.
-returnMempty :: forall ca cem. Advice ca cem Monoid
+returnMempty :: forall ca e m r. (Monad m, Monoid r) => Advice ca e m r
 returnMempty =
   makeExecutionAdvice
     ( \action -> do
         _ <- action
-        pure mempty
+        pure (mempty :: r)
     )
 
 -- | Given a 'Handle' and a prefix string, makes functions print their
@@ -55,7 +84,7 @@ --
 -- Because it doesn't touch the return value of the advised function, this
 -- 'Advice' is polymorphic on @cr@.
-printArgs :: forall cr. Handle -> String -> Advice Show (MonadConstraint MonadIO) cr
+printArgs :: forall e m r. MonadIO m => Handle -> String -> Advice Show e m r
 printArgs h prefix =
   makeArgsAdvice
     ( \args -> do
@@ -66,6 +95,46 @@         pure args
     )
 
+-- | Use 'local' on the final 'DepT' action of a function.
+--
+-- Allows tweaking the environment that will be seen by the function and all of
+-- its sub-calls.
+--
+-- >>> :{
+--  type HasLogger :: Type -> (Type -> Type) -> Constraint
+--  class HasLogger em m | em -> m where
+--    logger :: em -> String -> m ()
+--  type Env :: (Type -> Type) -> Type
+--  data Env m = Env
+--    { _logger1 :: String -> m (),
+--      _logger2 :: String -> m (),
+--      _controllerA :: Int -> m (),
+--      _controllerB :: Int -> m ()
+--    }
+--  instance HasLogger (Env m) m where
+--    logger = _logger1
+--  envIO :: Env (DepT Env IO)
+--  envIO = Env 
+--    {
+--      _logger1 = \_ -> liftIO $ putStrLn "logger1 ran",
+--      _logger2 = \_ -> liftIO $ putStrLn "logger2 ran",
+--      _controllerA = \_ -> do e <- ask; logger e "foo",
+--      _controllerB = advise @Top 
+--                     (doLocally \e@Env{_logger2} -> e {_logger1 = _logger2}) 
+--                     \_ -> do e <- ask; logger e "foo" 
+--    }
+-- :}
+--
+--  >>> runFromEnv (pure envIO) _controllerA 0
+--  logger1 ran
+--
+--  >>> runFromEnv (pure envIO) _controllerB 0
+--  logger2 ran
+--
+doLocally :: forall ca e m r. Monad m => (forall n. e n -> e n) -> Advice ca e m r 
+doLocally transform = makeExecutionAdvice (local transform)  
+
+
 -- | A helper datatype for universal equality comparisons of existentialized values, used by 'doCachingBadly'.
 --
 -- For a more complete elaboration of this idea, see the the \"exinst\" package.
@@ -93,7 +162,7 @@ --
 -- A better implementation of this advice would likely use an @AnyHashable@
 -- helper datatype for the keys.
-doCachingBadly :: forall m r. (AnyEq -> m (Maybe r)) -> (AnyEq -> r -> m ()) -> Advice (Eq `And` Typeable) (MonadConstraint (MustBe m)) (MustBe r)
+doCachingBadly :: forall e m r. Monad m => (AnyEq -> m (Maybe r)) -> (AnyEq -> r -> m ()) -> Advice (Eq `And` Typeable) e m r
 doCachingBadly cacheLookup cachePut =
   makeAdvice @AnyEq
     ( \args ->
@@ -117,10 +186,11 @@ -- package instead of bare `forkIO`. 
 --
 -- And the @MustBe IO@ constraint could be relaxed to @MonadUnliftIO@.
-doAsyncBadly :: Advice ca (MonadConstraint (MustBe IO)) (MustBe ())
+doAsyncBadly :: forall ca e. Advice ca e IO ()
 doAsyncBadly = makeExecutionAdvice (\action -> do
         e <- ask 
         _ <- liftIO $ forkIO $ runDepT action e
         pure ()
     )
+
 

@@ -194,13 +194,7 @@ --
 -- Experiment about adding instrumetation
 
-emptyResult :: Advice ca cem Monoid
-emptyResult = makeAdvice @()
-    (\args -> pure ((), args))
-    (\() action -> do _ <- action
-                      pure mempty)
-
-doLogging :: Advice Show (Ensure HasLogger) cr
+doLogging :: forall e m r. (Ensure HasLogger e m, Monad m) => Advice Show e m r
 doLogging = makeAdvice @()
         (\args -> do
             e <- ask
@@ -216,7 +210,7 @@ advicedEnv :: Env (DepT Env (Writer TestTrace))
 advicedEnv =
    env {
-         _controller = advise (doLogging @Top) (_controller env)
+         _controller = advise doLogging (_controller env)
        }
 
 expectedAdviced :: TestTrace
@@ -226,28 +220,46 @@ weirdAdvicedEnv :: Env (DepT Env (Writer TestTrace))
 weirdAdvicedEnv =
    env {
-         _controller = advise (doLogging <> emptyResult) (_controller env), --,
+         _controller = advise (doLogging <> returnMempty) (_controller env), --,
          -- This advice below doesn't really do anything, I'm just experimenting with passing the constraints with type application
-         _logger = advise @(Show `And` Eq) @Top2 @Monoid (makeAdvice @() (\args -> pure (pure args)) (\_ -> id)) (_logger env)
+         _logger = advise @(Show `And` Eq) (makeAdvice @() (\args -> pure (pure args)) (\_ -> id)) (_logger env)
        }
 
-type EnsureLoggerAndWriter :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
-type EnsureLoggerAndWriter = Ensure HasLogger `And2` MonadConstraint (MonadWriter TestTrace)
+-- type EnsureLoggerAndWriter :: ((Type -> Type) -> Type) -> (Type -> Type) -> Constraint
+-- type EnsureLoggerAndWriter = Ensure HasLogger `And2` MonadConstraint (MonadWriter TestTrace)
 
 -- to ways to invoke restrict functions
-doLogging':: Advice Show EnsureLoggerAndWriter cr
-doLogging'= restrictEnv (Sub Dict) doLogging
+-- doLogging':: Advice Show EnsureLoggerAndWriter cr
+-- doLogging'= restrictEnv (Sub Dict) doLogging
+-- 
+-- doLogging'' = restrictEnv @EnsureLoggerAndWriter (Sub Dict) doLogging
+ 
+-- Checking that constraints on the environment and the monad are collected "automatically"
+doLogging' :: forall e m r . (Ensure HasLogger e m, Ensure HasRepository e m, MonadIO m) => Advice Show e m r
+doLogging' = doLogging 
 
-doLogging'' = restrictEnv @EnsureLoggerAndWriter (Sub Dict) doLogging
+justARepositoryConstraint :: forall ca e m r. (Ensure HasRepository e m, Monad m) => Advice ca e m r
+justARepositoryConstraint = mempty
 
-returnMempty' :: Advice ca cem (Monoid `And` Show)
-returnMempty' = restrictResult (Sub Dict) returnMempty
+doLogging'' :: forall e m r . (Ensure HasLogger e m, Ensure HasRepository e m, MonadIO m) => Advice Show e m r
+doLogging'' = doLogging <> justARepositoryConstraint
 
-returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty
+-- Checking that constraints on the results are collected "automatically"
+returnMempty' :: forall ca e m r. (Monad m, Monoid r, Show r, Read r) => Advice ca e m r
+returnMempty' = returnMempty
 
+justAResultConstraint :: forall ca e m r. (Monad m, Show r, Read r) => Advice ca e m r
+justAResultConstraint = mempty
+
+returnMempty'' :: forall ca e m r. (Monad m, Monoid r, Show r, Read r) => Advice ca e m r
+returnMempty'' = returnMempty <> justAResultConstraint
+
+-- 
+-- returnMempty'' = restrictResult @(Monoid `And` Show) (Sub Dict) returnMempty
+-- 
 -- does EnvConstraint compile?
 
-type FooAdvice = Advice Top (EnvConstraint (MustBe NilEnv)) Top
+-- type FooAdvice = Advice Top (EnvConstraint (MustBe NilEnv)) Top
 
 
 --

@@ -0,0 +1,46 @@+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ConstraintKinds #-}
+
+module Main (main) where
+
+import Control.Monad.Dep
+import Control.Monad.Dep.Advice
+import Control.Monad.Dep.Advice.Basic
+import Control.Monad.Reader
+import Control.Monad.Writer
+import Control.Monad.RWS
+import Data.Kind
+import Data.List (intercalate,lookup)
+import Rank2 qualified
+import Rank2.TH qualified
+import Test.Tasty
+import Test.Tasty.HUnit
+import Prelude hiding (log)
+import Data.Proxy
+
+
+--
+--
+--
+
+tests :: TestTree
+tests =
+  testGroup
+    "All"
+    [
+    ]
+
+main :: IO ()
+main = defaultMain tests