diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,20 +1,33 @@
 # Revision history for dep-t
 
-## 0.6.7
+## 0.6.8.0
 
+* Un-deprecated `HasAll`. Turns out that it's actually useful :facepalm:
+
+* Added `InjectsAll`.
+
+* Deprecated `DemotableFieldNames` `demoteFieldNames` `mapPhaseWithFieldNames`
+
+* Deprecated `skipPhase`. Instead of using both  `skipPhase` and `bindPhase`, it's 
+  better to use only the latter, for consistency.
+
+* Moved main `Phased` definitions to `Dep.Phased`, re-exporting them from `Dep.Env`.
+
+## 0.6.7.0
+
 * Deprecated `HasAll`.
 
 * Added `Call` pattern synonym to `Dep.Has`.
 
 * Added tuple instances for `Has` and `Injects`.
 
-## 0.6.6
+## 0.6.6.0
 
 * Added `Dep.Phases`. 
 
 * Added `Dep.Injects`.
 
-## 0.6.5
+## 0.6.5.0
 
 * Deprecated `Constructor`, `fixEnv` and the `Accum-` counterparts from `Dep.Env`.
   
@@ -30,7 +43,7 @@
 
 * Shifted `DepT`-specific parts of the readme to `Control.Monad.Dep`.
 
-## 0.6.4
+## 0.6.4.0
 
 * Added AccumConstructor, a generalization of Constructor that threads a
   monoidal summary along with the environment record.
@@ -45,7 +58,7 @@
   TraversableT and ApplicativeT from the "barbies" library to implement Phased.
   But most of the time you would use Phased's own generic deriving anyway.
 
-## 0.6.3
+## 0.6.3.0
 
 * Now the Bare typeclass doesn't recurse inside Identity or Const.
 
@@ -60,7 +73,7 @@
   functions did not compile. This led to unnecessary code duplication. Stopping
   at Identity means Bare never touches the type variable and doesn't get stuck.
 
-## 0.6.2
+## 0.6.2.0
 
 * Moved `fromBare` and `toBare` from dep-t-dynamic.
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -42,8 +42,8 @@
 ```mermaid
   graph TD;
       Dep.Env-->Dep.Has;
-      Dep.Constructor-->Dep.Env;
-      Dep.Tagged;
+      Dep.Env-->Dep.Phases;
+      Dep.Constructor-->Dep.Phases;
       Control.Monad.Dep.Class-->Control.Monad.Reader;
       Control.Monad.Dep-->Control.Monad.Reader;
       Control.Monad.Dep-->Control.Monad.Dep.Class;
@@ -52,8 +52,8 @@
 - __Dep.Has__ provides a generic `Has` typeclass for locating dependencies in an
 environment. Usually, component implementations import this module.
 - __Dep.Env__ complements __Dep.Has__ with helpers for building dependency injection environments. Usually, only the [composition root](https://stackoverflow.com/questions/6277771/what-is-a-composition-root-in-the-context-of-dependency-injection) of the application imports this module.
-- __Dep.Tagged__ is a helper for disambiguating dependencies in __Dep.Env__ environments.
-- __Dep.Constructor__ enables fixpoint-based dependency injection in __Dep.Env__ environments. See [this thread in the Haskell Discourse](https://discourse.haskell.org/t/dependency-injection-fixed-points-and-monoidal-accumulators/5557) for an example.
+- __Dep.Phases__ provides a `Phased` typeclass for DI environments which go through a sequence of `Applicative` phases during construction. Also a special [`QualifiedDo`](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/qualified_do.html#extension-QualifiedDo) notation for phases.
+- __Dep.Constructor__ enables fixpoint-based dependency injection in `Phased` environments. See [this thread in the Haskell Discourse](https://discourse.haskell.org/t/dependency-injection-fixed-points-and-monoidal-accumulators/5557) for an example.
 - __Control.Monad.Dep__ provides the `DepT` monad transformer, a variant of `ReaderT`. You either want to use this or __Dep.Constructor__ in your composition root, but not both.
 - __Control.Monad.Dep.Class__ is an extension of `MonadReader`, useful to program against both `ReaderT` and `DepT`.
 
diff --git a/dep-t.cabal b/dep-t.cabal
--- a/dep-t.cabal
+++ b/dep-t.cabal
@@ -1,7 +1,7 @@
 cabal-version:       3.0
 
 name:                dep-t
-version:             0.6.7.0
+version:             0.6.8.0
 synopsis:            Dependency injection for records-of-functions.
 description:         Put all your functions in the environment record! Let all
                      your functions read from the environment record! No favorites!
diff --git a/lib/Dep/Constructor.hs b/lib/Dep/Constructor.hs
--- a/lib/Dep/Constructor.hs
+++ b/lib/Dep/Constructor.hs
@@ -79,10 +79,11 @@
 import Data.Function (fix)
 import Data.Kind
 import Data.Typeable
-import Dep.Env hiding (AccumConstructor, Constructor, accumConstructor, constructor, fixEnv, fixEnvAccum)
+import Dep.Phases
 import Control.Category (Category)
 import Control.Category qualified
 import Control.Arrow
+import Data.Functor.Identity
 
 -- | A phase with the effect of \"constructing each component by reading its
 -- dependencies from a completed environment\". It should be the final phase.
diff --git a/lib/Dep/Env.hs b/lib/Dep/Env.hs
--- a/lib/Dep/Env.hs
+++ b/lib/Dep/Env.hs
@@ -128,6 +128,7 @@
 import GHC.Generics qualified as G
 import GHC.Records
 import GHC.TypeLits
+import Dep.Phases hiding ((>>=), (>>))
 
 -- $setup
 --
@@ -261,243 +262,10 @@
   WithLeftResult_ ('Just ls) right r = 'Just ls
   WithLeftResult_ Nothing right r = GFindFieldByType right r
 
---
---
--- Managing Phases
 
--- see also https://github.com/haskell/cabal/issues/7394#issuecomment-861767980
-
--- | Class of 2-parameter environments for which the first parameter @h@ wraps
--- each field and corresponds to phases in the construction of the environment,
--- and the second parameter @m@ is the effect monad used by each component.
---
--- @h@ will typically be a composition of applicative functors, each one
--- representing a phase. We advance through the phases by \"pulling out\" the
--- outermost phase and running it in some way, until we are are left with a
--- 'Constructor' phase, which we can remove using 'fixEnv'.
---
--- 'Phased' resembles [FunctorT, TraversableT and
--- ApplicativeT](https://hackage.haskell.org/package/barbies-2.0.3.0/docs/Data-Functor-Transformer.html)
--- from the [barbies](https://hackage.haskell.org/package/barbies) library,
--- although 'Phased' instances /can't/ be written in terms of them because of the extra 'Typeable' constraints.
-type Phased :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
-class Phased (env_ :: (Type -> Type) -> (Type -> Type) -> Type) where
-  -- | Used to implement 'pullPhase' and 'mapPhase',  typically you should use those functions instead.
-  traverseH ::
-    forall
-      (h :: Type -> Type)
-      (f :: Type -> Type)
-      (g :: Type -> Type)
-      (m :: Type -> Type).
-    ( 
-      Applicative f,
-      Typeable f,
-      Typeable g,
-      Typeable h,
-      Typeable m
-    ) =>
-    -- | Transform to be applied to each field.
-    (forall x. Typeable x => h x -> f (g x)) ->
-    env_ h m ->
-    f (env_ g m)
-  default traverseH ::
-    forall
-      (h :: Type -> Type)
-      (f :: Type -> Type)
-      (g :: Type -> Type)
-      (m :: Type -> Type).
-    ( Applicative f,
-      Typeable f,
-      Typeable g,
-      Typeable h,
-      Typeable m,
-      G.Generic (env_ h m),
-      G.Generic (env_ g m),
-      GTraverseH h g (G.Rep (env_ h m)) (G.Rep (env_ g m))
-    ) =>
-    -- | Transform to be applied to each field.
-    (forall x. Typeable x => h x -> f (g x)) ->
-    env_ h m ->
-    f (env_ g m)
-  traverseH t env = G.to <$> gTraverseH t (G.from env)
-
-  -- | Used to implement 'liftA2Phase', typically you should use that function instead.
-  liftA2H ::
-    forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) (m :: Type -> Type).
-    ( Typeable a,
-      Typeable f,
-      Typeable f',
-      Typeable m
-    ) =>
-    -- | Binary operation to combine corresponding fields.
-    (forall x. Typeable x => a x -> f x -> f' x) ->
-    env_ a m ->
-    env_ f m ->
-    env_ f' m
-  default liftA2H ::
-    forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) m.
-    ( Typeable a,
-      Typeable f,
-      Typeable f',
-      Typeable m,
-      G.Generic (env_ a m),
-      G.Generic (env_ f m),
-      G.Generic (env_ f' m),
-      GLiftA2Phase a f f' (G.Rep (env_ a m)) (G.Rep (env_ f m)) (G.Rep (env_ f' m))
-    ) =>
-    -- | Transform to be applied to each field.
-    (forall x. Typeable x => a x -> f x -> f' x) ->
-    env_ a m ->
-    env_ f m ->
-    env_ f' m
-  liftA2H f enva env = G.to (gLiftA2Phase f (G.from enva) (G.from env))
-
--- | Slightly less powerful version of 'traverseH'.
-liftAH ::
-  forall deps_ phases phases' m.
-  (Phased deps_, Typeable phases, Typeable phases', Typeable m) =>
-  (forall x. Typeable x => phases x -> phases' x) ->
-  deps_ phases m ->
-  deps_ phases' m
-liftAH tweak =
-  runIdentity . traverseH (Identity . tweak)
-
--- | Take the outermost phase wrapping each component and \"pull it outwards\",
--- aggregating the phase's applicative effects.
---
--- >>> :{
---  newtype Foo d = Foo {foo :: String -> d ()} deriving Generic
---  makeIOFoo :: MonadIO m => Foo m
---  makeIOFoo = Foo (liftIO . putStrLn)
---  env :: InductiveEnv '[Foo] (IO `Compose` Constructor (InductiveEnv '[Foo] Identity IO)) IO
---  env = EmptyEnv
---      & AddDep @Foo (putStrLn "io phase" `bindPhase` \() -> constructor (\_ -> makeIOFoo))
---  ioOutside :: IO (InductiveEnv '[Foo] (Constructor (InductiveEnv '[Foo] Identity IO)) IO)
---  ioOutside = pullPhase env
--- :}
-pullPhase ::
-  forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
-  (Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
-  env_ (Compose f g) m ->
-  -- Environment with the outer 'Applicative' layer pulled outward.
-  f (env_ g m)
--- f first to help annotate the phase
-pullPhase = traverseH @env_ getCompose
-
--- | Modify the outermost phase wrapping each component.
---
--- >>> :{
---  newtype Foo d = Foo {foo :: String -> d ()} deriving Generic
---  makeIOFoo :: MonadIO m => Foo m
---  makeIOFoo = Foo (liftIO . putStrLn)
---  env :: InductiveEnv '[Foo] ((,) Int `Compose` Constructor String) IO
---  env = EmptyEnv
---      & AddDep @Foo ((2,()) `bindPhase` \() -> constructor (\_ -> makeIOFoo))
---  env' :: InductiveEnv '[Foo] ((,) String `Compose` Constructor String) IO
---  env' = mapPhase (\(n,x) -> (show n,x)) env
--- :}
-mapPhase ::
-  forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
-  (Phased env_, Typeable f, Typeable f', Typeable g, Typeable m) =>
-  -- | Transform to be applied to each field.
-  (forall x. Typeable x => f x -> f' x) ->
-  env_ (Compose f g) m ->
-  env_ (Compose f' g) m
--- f' first to help annotate the *target* of the transform?
-mapPhase f env = runIdentity $ traverseH @env_ (\(Compose fg) -> Identity (Compose (f fg))) env
-
--- | Combine two environments with a function that works on their outermost phases.
-liftA2Phase ::
-  forall (a :: Type -> Type) (f' :: Type -> Type) (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
-  (Phased env_, Typeable a, Typeable f, Typeable f', Typeable g, Typeable m) =>
-  -- | Binary operation to combine corresponding fields.
-  (forall x. Typeable x => a x -> f x -> f' x) ->
-  env_ (Compose a g) m ->
-  env_ (Compose f g) m ->
-  env_ (Compose f' g) m
--- f' first to help annotate the *target* of the transform?
-liftA2Phase f = liftA2H @env_ (\(Compose fa) (Compose fg) -> Compose (f fa fg))
-
-class GTraverseH h g env env' | env -> h, env' -> g where
-  gTraverseH :: Applicative f => (forall x. Typeable x => h x -> f (g x)) -> env x -> f (env' x)
-
-instance
-  (GTraverseH h g fields fields') =>
-  GTraverseH
-    h
-    g
-    (G.D1 metaData (G.C1 metaCons fields))
-    (G.D1 metaData (G.C1 metaCons fields'))
-  where
-  gTraverseH t (G.M1 (G.M1 fields)) =
-    G.M1 . G.M1 <$> gTraverseH @h @g t fields
-
-instance
-  ( GTraverseH h g left left',
-    GTraverseH h g right right'
-  ) =>
-  GTraverseH h g (left G.:*: right) (left' G.:*: right')
-  where
-  gTraverseH t (left G.:*: right) =
-    let left' = gTraverseH @h @g t left
-        right' = gTraverseH @h @g t right
-     in liftA2 (G.:*:) left' right'
-
-instance
-  Typeable bean =>
-  GTraverseH
-    h
-    g
-    (G.S1 metaSel (G.Rec0 (h bean)))
-    (G.S1 metaSel (G.Rec0 (g bean)))
-  where
-  gTraverseH t (G.M1 (G.K1 hbean)) =
-    G.M1 . G.K1 <$> t hbean
-
---
---
-class GLiftA2Phase a f f' enva env env' | enva -> a, env -> f, env' -> f' where
-  gLiftA2Phase :: (forall r. Typeable r => a r -> f r -> f' r) -> enva x -> env x -> env' x
-
-instance
-  GLiftA2Phase a f f' fieldsa fields fields' =>
-  GLiftA2Phase
-    a
-    f
-    f'
-    (G.D1 metaData (G.C1 metaCons fieldsa))
-    (G.D1 metaData (G.C1 metaCons fields))
-    (G.D1 metaData (G.C1 metaCons fields'))
-  where
-  gLiftA2Phase f (G.M1 (G.M1 fieldsa)) (G.M1 (G.M1 fields)) =
-    G.M1 (G.M1 (gLiftA2Phase @a @f @f' f fieldsa fields))
-
-instance
-  ( GLiftA2Phase a f f' lefta left left',
-    GLiftA2Phase a f f' righta right right'
-  ) =>
-  GLiftA2Phase a f f' (lefta G.:*: righta) (left G.:*: right) (left' G.:*: right')
-  where
-  gLiftA2Phase f (lefta G.:*: righta) (left G.:*: right) =
-    let left' = gLiftA2Phase @a @f @f' f lefta left
-        right' = gLiftA2Phase @a @f @f' f righta right
-     in (G.:*:) left' right'
-
-instance
-  Typeable bean =>
-  GLiftA2Phase
-    a
-    f
-    f'
-    (G.S1 metaSel (G.Rec0 (a bean)))
-    (G.S1 metaSel (G.Rec0 (f bean)))
-    (G.S1 metaSel (G.Rec0 (f' bean)))
-  where
-  gLiftA2Phase f (G.M1 (G.K1 abean)) (G.M1 (G.K1 fgbean)) =
-    G.M1 (G.K1 (f abean fgbean))
-
 -- | Class of 2-parameter environments for which it's possible to obtain the
 -- names of each field as values.
+{-# DEPRECATED DemotableFieldNames "using the field names directly is usually a bad idea" #-}
 type DemotableFieldNames :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
 class DemotableFieldNames env_ where
   demoteFieldNamesH :: (forall x. String -> h String x) -> env_ (h String) m
@@ -511,6 +279,7 @@
 
 -- | Bring down the field names of the environment to the term level and store
 -- them in the accumulator of "Data.Functor.Constant".
+{-# DEPRECATED demoteFieldNames "using the field names directly is usually a bad idea" #-}
 demoteFieldNames :: forall env_ m. DemotableFieldNames env_ => env_ (Constant String) m
 demoteFieldNames = demoteFieldNamesH Constant
 
@@ -542,6 +311,7 @@
 -- A typical usage is modifying a \"parsing the configuration\" phase so that
 -- each component looks into a different section of the global configuration
 -- field.
+{-# DEPRECATED mapPhaseWithFieldNames "using the field names directly is usually a bad idea" #-}
 mapPhaseWithFieldNames ::
   forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
   ( Phased env_,
@@ -581,6 +351,10 @@
 --      pure 2 `bindPhase` \i2 ->
 --      Identity (i1 + i2)
 -- :}
+--
+--
+-- A possible alternative is 'Dep.Phases.>>=' from "Dep.Phases" used in
+-- combination with @-XQualifiedDo@.
 bindPhase :: forall f g a b. Functor f => f a -> (a -> g b) -> Compose f g b
 -- f as first type parameter to help annotate the current phase
 bindPhase f k = Compose (f <&> k)
@@ -595,6 +369,7 @@
 --      skipPhase $
 --      Identity 1
 -- :}
+{-# DEPRECATED skipPhase "use pure () in combination with bindPhase" #-}
 skipPhase :: forall f g a. Applicative f => g a -> Compose f g a
 -- f as first type parameter to help annotate the current phase
 skipPhase g = Compose (pure g)
diff --git a/lib/Dep/Has.hs b/lib/Dep/Has.hs
--- a/lib/Dep/Has.hs
+++ b/lib/Dep/Has.hs
@@ -18,66 +18,51 @@
 {-# LANGUAGE ViewPatterns #-}
 
 -- | This module provides a general-purpose 'Has' class favoring a style in
--- which the components of the environment, instead of being bare functions,
--- are themselves records or newtypes containing functions.
---
--- In this style, the functions that are \"invoked\" from the environment are
--- actually record field selectors. These selectors guide the 'Has' class to
--- find the correct records in the environment.
+-- which the components of the dependency injection environment, instead of
+-- being bare functions, are themselves records or newtypes containing
+-- functions:
 --
 -- >>> :{
 --  newtype Logger d = Logger {log :: String -> d ()}
---  instance Dep Logger where
---    type DefaultFieldName Logger = "logger"
---  --
---  data Repository d = Repository
---    { select :: String -> d [Int],
---      insert :: [Int] -> d ()
---    }
---  instance Dep Repository where
---    type DefaultFieldName Repository = "repository"
---  --
+--  data Repository d = Repository { select :: String -> d [Int], insert :: [Int] -> d () }
 --  newtype Controller d = Controller {serve :: Int -> d String}
---  instance Dep Controller where
---    type DefaultFieldName Controller = "controller"
---  --
+--  -- A dependency injection environment that contains the components.
 --  type Deps :: (Type -> Type) -> Type
 --  data Deps m = Deps
 --    { logger :: Logger m,
 --      repository :: Repository m,
 --      controller :: Controller m
 --    }
---  instance Has Logger m (Deps m)
---  instance Has Repository m (Deps m)
---  instance Has Controller m (Deps m)
+--  instance Has Logger m (Deps m) where dep Deps {logger} = logger
+--  instance Has Repository m (Deps m) where dep Deps {repository} = repository
+--  instance Has Controller m (Deps m) where dep Deps {controller} = controller
 --  :}
 --
--- 'Has' can be used in combination with 'MonadDep', like this:
 --
--- >>> :{
---  mkController :: MonadDep [Has Logger, Has Repository] d env m => Controller m
---  mkController =
---    Controller \url ->
---      useEnv \(asCall -> call) -> do
---        call log "I'm going to insert in the db!"
---        call select "select * from ..."
---        call insert [1, 2, 3, 4]
---        return "view"
--- :}
+-- In this style, the functions that are \"invoked\" from the environment are
+-- actually record field selectors. These selectors guide the 'Has' class to
+-- find the correct components in the environment:
 --
--- 'Has' can also be used independently of 'MonadReader' or 'MonadDep'. Here
--- for example the environment is passed as a plain function argument, and @m@
--- doesn't have any constraint other than 'Monad':
 --
 -- >>> :{
---  mkController' :: (Monad m, Has Logger m deps, Has Repository m deps) => deps -> Controller m
---  mkController' (asCall -> call) =
+--  makeController :: (Has Logger m deps, Has Repository m deps, Monad m) => deps -> Controller m
+--  makeController (asCall -> call) =
 --    Controller \url -> do
 --      call log "I'm going to insert in the db!"
 --      call select "select * from ..."
 --      call insert [1, 2, 3, 4]
 --      return "view"
 -- :}
+--
+--
+-- By convention, the DI environment parameter is usually called @deps@. Notice
+-- also the use of the (optional) 'asCall' helper.
+--
+-- If we regard @makeController@ above as a component constructor, 'Has' lets us
+-- avoid having to define separate positional parameters for each dependency of the 
+-- constructor. Not only that: it also avoids us having to give names to those 
+-- parameters, and even having to mention their types (because they are
+-- implicit in the record field selectors).
 module Dep.Has
   ( -- * A general-purpose Has
     Has (..),
@@ -121,8 +106,6 @@
 -- | When partially applied to a type-level list @rs_@ of parametrizable records-of-functions,
 -- produces a 2-place constraint saying that the environment @e@ has all the
 -- records @rs_@ with effect monad @m@.
-{-# DEPRECATED HasAll "Use All from sop-core along with separate Has applications" #-}
-
 type HasAll :: [(Type -> Type) -> Type] -> (Type -> Type) -> Type -> Constraint
 type family HasAll rs_ m e where
   HasAll '[] m e = ()
@@ -161,9 +144,9 @@
 -- Each function field is then a \"method\". And the record field selectors are functions
 -- which take the component and return the method corresponding to that field.
 --
--- Given a dependency injection context, 'asCall' produces a reusable helper
+-- Given a dependency injection environment, 'asCall' produces a reusable helper
 -- that returns the the method corresponding to a field selector, on the condition that
--- the required 'Has' instance exists for the selectors' record.
+-- the selector's record actually exists in the environment.
 --
 -- >>> :{
 --  data SomeRecord m = SomeRecord { someSelector :: String -> m () }
diff --git a/lib/Dep/Injects.hs b/lib/Dep/Injects.hs
--- a/lib/Dep/Injects.hs
+++ b/lib/Dep/Injects.hs
@@ -20,6 +20,7 @@
 module Dep.Injects
   ( -- * General-purpose injector.
     Injects (..),
+    InjectsAll
   )
 where
 
@@ -65,3 +66,10 @@
 
 instance (Monoid a, Monoid b, Monoid c) => Injects r_ m (a, b, c, r_ m) where
   inject r = (mempty, mempty, mempty, r)
+
+
+-- | Mirror image of 'Dep.Has.HasAll'.
+type InjectsAll :: [(Type -> Type) -> Type] -> (Type -> Type) -> Type -> Constraint
+type family InjectsAll rs_ m e where
+  InjectsAll '[] m e = ()
+  InjectsAll (r_ : rs_) m e = (Injects r_ m e, InjectsAll rs_ m e)
diff --git a/lib/Dep/Phases.hs b/lib/Dep/Phases.hs
--- a/lib/Dep/Phases.hs
+++ b/lib/Dep/Phases.hs
@@ -1,4 +1,29 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 module Dep.Phases (
+    -- * Managing phases
+    Phased (..),
+    liftAH,
+    pullPhase,
+    mapPhase,
+    liftA2Phase,
     -- * Qualified do-notation for building phases
     -- $warning
     (>>=), 
@@ -7,12 +32,286 @@
     Compose (..),
     ) where
 
+
+import Control.Applicative
+import Data.Coerce
+import Data.Function (fix)
+import Data.Functor (($>), (<&>))
+import Data.Functor.Identity
+import Data.Kind
+import Data.Proxy
+import Data.String
+import Data.Type.Equality (type (==))
+import Data.Typeable
+import GHC.Generics qualified as G
+import GHC.Records
+import GHC.TypeLits
 import Data.Functor.Compose
-import Prelude (Functor, (<$>), (<$))
+import Prelude (Functor, (<$>), (<$), ($), (.))
 
+--
+--
+-- Managing Phases
+
+-- see also https://github.com/haskell/cabal/issues/7394#issuecomment-861767980
+
+-- | Class of 2-parameter environments for which the first parameter @h@ wraps
+-- each field and corresponds to phases in the construction of the environment,
+-- and the second parameter @m@ is the effect monad used by each component.
+--
+-- @h@ will typically be a composition of applicative functors, each one
+-- representing a phase. We advance through the phases by \"pulling out\" the
+-- outermost phase and running it in some way, until we are are left with a
+-- 'Constructor' phase, which we can remove using 'fixEnv'.
+--
+-- 'Phased' resembles [FunctorT, TraversableT and
+-- ApplicativeT](https://hackage.haskell.org/package/barbies-2.0.3.0/docs/Data-Functor-Transformer.html)
+-- from the [barbies](https://hackage.haskell.org/package/barbies) library,
+-- although 'Phased' instances /can't/ be written in terms of them because of the extra 'Typeable' constraints.
+type Phased :: ((Type -> Type) -> (Type -> Type) -> Type) -> Constraint
+class Phased (env_ :: (Type -> Type) -> (Type -> Type) -> Type) where
+  -- | Used to implement 'pullPhase' and 'mapPhase',  typically you should use those functions instead.
+  traverseH ::
+    forall
+      (h :: Type -> Type)
+      (f :: Type -> Type)
+      (g :: Type -> Type)
+      (m :: Type -> Type).
+    ( 
+      Applicative f,
+      Typeable f,
+      Typeable g,
+      Typeable h,
+      Typeable m
+    ) =>
+    -- | Transform to be applied to each field.
+    (forall x. Typeable x => h x -> f (g x)) ->
+    env_ h m ->
+    f (env_ g m)
+  default traverseH ::
+    forall
+      (h :: Type -> Type)
+      (f :: Type -> Type)
+      (g :: Type -> Type)
+      (m :: Type -> Type).
+    ( Applicative f,
+      Typeable f,
+      Typeable g,
+      Typeable h,
+      Typeable m,
+      G.Generic (env_ h m),
+      G.Generic (env_ g m),
+      GTraverseH h g (G.Rep (env_ h m)) (G.Rep (env_ g m))
+    ) =>
+    -- | Transform to be applied to each field.
+    (forall x. Typeable x => h x -> f (g x)) ->
+    env_ h m ->
+    f (env_ g m)
+  traverseH t env = G.to <$> gTraverseH t (G.from env)
+
+  -- | Used to implement 'liftA2Phase', typically you should use that function instead.
+  liftA2H ::
+    forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) (m :: Type -> Type).
+    ( Typeable a,
+      Typeable f,
+      Typeable f',
+      Typeable m
+    ) =>
+    -- | Binary operation to combine corresponding fields.
+    (forall x. Typeable x => a x -> f x -> f' x) ->
+    env_ a m ->
+    env_ f m ->
+    env_ f' m
+  default liftA2H ::
+    forall (a :: Type -> Type) (f :: Type -> Type) (f' :: Type -> Type) m.
+    ( Typeable a,
+      Typeable f,
+      Typeable f',
+      Typeable m,
+      G.Generic (env_ a m),
+      G.Generic (env_ f m),
+      G.Generic (env_ f' m),
+      GLiftA2Phase a f f' (G.Rep (env_ a m)) (G.Rep (env_ f m)) (G.Rep (env_ f' m))
+    ) =>
+    -- | Transform to be applied to each field.
+    (forall x. Typeable x => a x -> f x -> f' x) ->
+    env_ a m ->
+    env_ f m ->
+    env_ f' m
+  liftA2H f enva env = G.to (gLiftA2Phase f (G.from enva) (G.from env))
+
+-- | Slightly less powerful version of 'traverseH'.
+liftAH ::
+  forall deps_ phases phases' m.
+  (Phased deps_, Typeable phases, Typeable phases', Typeable m) =>
+  -- | Transform to be applied to each field.
+  (forall x. Typeable x => phases x -> phases' x) ->
+  deps_ phases m ->
+  deps_ phases' m
+liftAH tweak =
+  runIdentity . traverseH (Identity . tweak)
+
+-- | Take the outermost phase wrapping each component and \"pull it outwards\",
+-- aggregating the phase's applicative effects.
+--
+-- >>> :{
+--  newtype Foo d = Foo {foo :: String -> d ()} deriving Generic
+--  makeIOFoo :: MonadIO m => Foo m
+--  makeIOFoo = Foo (liftIO . putStrLn)
+--  env :: InductiveEnv '[Foo] (IO `Compose` Constructor (InductiveEnv '[Foo] Identity IO)) IO
+--  env = EmptyEnv
+--      & AddDep @Foo (putStrLn "io phase" `bindPhase` \() -> constructor (\_ -> makeIOFoo))
+--  ioOutside :: IO (InductiveEnv '[Foo] (Constructor (InductiveEnv '[Foo] Identity IO)) IO)
+--  ioOutside = pullPhase env
+-- :}
+pullPhase ::
+  forall (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
+  (Phased env_, Applicative f, Typeable f, Typeable g, Typeable m) =>
+  env_ (Compose f g) m ->
+  -- | Environment with the outer 'Applicative' layer pulled outward.
+  f (env_ g m)
+-- f first to help annotate the phase
+pullPhase = traverseH @env_ getCompose
+
+-- | Modify the outermost phase wrapping each component.
+--
+-- >>> :{
+--  newtype Foo d = Foo {foo :: String -> d ()} deriving Generic
+--  makeIOFoo :: MonadIO m => Foo m
+--  makeIOFoo = Foo (liftIO . putStrLn)
+--  env :: InductiveEnv '[Foo] ((,) Int `Compose` Constructor String) IO
+--  env = EmptyEnv
+--      & AddDep @Foo ((2,()) `bindPhase` \() -> constructor (\_ -> makeIOFoo))
+--  env' :: InductiveEnv '[Foo] ((,) String `Compose` Constructor String) IO
+--  env' = mapPhase (\(n,x) -> (show n,x)) env
+-- :}
+mapPhase ::
+  forall (f :: Type -> Type) (f' :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
+  (Phased env_, Typeable f, Typeable f', Typeable g, Typeable m) =>
+  -- | Transform to be applied to each field.
+  (forall x. Typeable x => f x -> f' x) ->
+  env_ (Compose f g) m ->
+  env_ (Compose f' g) m
+-- f' first to help annotate the *target* of the transform?
+mapPhase f env = runIdentity $ traverseH @env_ (\(Compose fg) -> Identity (Compose (f fg))) env
+
+-- | Combine two environments with a function that works on their outermost phases.
+liftA2Phase ::
+  forall (a :: Type -> Type) (f' :: Type -> Type) (f :: Type -> Type) (g :: Type -> Type) (m :: Type -> Type) env_.
+  (Phased env_, Typeable a, Typeable f, Typeable f', Typeable g, Typeable m) =>
+  -- | Binary operation to combine corresponding fields.
+  (forall x. Typeable x => a x -> f x -> f' x) ->
+  env_ (Compose a g) m ->
+  env_ (Compose f g) m ->
+  env_ (Compose f' g) m
+-- f' first to help annotate the *target* of the transform?
+liftA2Phase f = liftA2H @env_ (\(Compose fa) (Compose fg) -> Compose (f fa fg))
+
+class GTraverseH h g env env' | env -> h, env' -> g where
+  gTraverseH :: Applicative f => (forall x. Typeable x => h x -> f (g x)) -> env x -> f (env' x)
+
+instance
+  (GTraverseH h g fields fields') =>
+  GTraverseH
+    h
+    g
+    (G.D1 metaData (G.C1 metaCons fields))
+    (G.D1 metaData (G.C1 metaCons fields'))
+  where
+  gTraverseH t (G.M1 (G.M1 fields)) =
+    G.M1 . G.M1 <$> gTraverseH @h @g t fields
+
+instance
+  ( GTraverseH h g left left',
+    GTraverseH h g right right'
+  ) =>
+  GTraverseH h g (left G.:*: right) (left' G.:*: right')
+  where
+  gTraverseH t (left G.:*: right) =
+    let left' = gTraverseH @h @g t left
+        right' = gTraverseH @h @g t right
+     in liftA2 (G.:*:) left' right'
+
+instance
+  Typeable bean =>
+  GTraverseH
+    h
+    g
+    (G.S1 metaSel (G.Rec0 (h bean)))
+    (G.S1 metaSel (G.Rec0 (g bean)))
+  where
+  gTraverseH t (G.M1 (G.K1 hbean)) =
+    G.M1 . G.K1 <$> t hbean
+
+--
+--
+class GLiftA2Phase a f f' enva env env' | enva -> a, env -> f, env' -> f' where
+  gLiftA2Phase :: (forall r. Typeable r => a r -> f r -> f' r) -> enva x -> env x -> env' x
+
+instance
+  GLiftA2Phase a f f' fieldsa fields fields' =>
+  GLiftA2Phase
+    a
+    f
+    f'
+    (G.D1 metaData (G.C1 metaCons fieldsa))
+    (G.D1 metaData (G.C1 metaCons fields))
+    (G.D1 metaData (G.C1 metaCons fields'))
+  where
+  gLiftA2Phase f (G.M1 (G.M1 fieldsa)) (G.M1 (G.M1 fields)) =
+    G.M1 (G.M1 (gLiftA2Phase @a @f @f' f fieldsa fields))
+
+instance
+  ( GLiftA2Phase a f f' lefta left left',
+    GLiftA2Phase a f f' righta right right'
+  ) =>
+  GLiftA2Phase a f f' (lefta G.:*: righta) (left G.:*: right) (left' G.:*: right')
+  where
+  gLiftA2Phase f (lefta G.:*: righta) (left G.:*: right) =
+    let left' = gLiftA2Phase @a @f @f' f lefta left
+        right' = gLiftA2Phase @a @f @f' f righta right
+     in (G.:*:) left' right'
+
+instance
+  Typeable bean =>
+  GLiftA2Phase
+    a
+    f
+    f'
+    (G.S1 metaSel (G.Rec0 (a bean)))
+    (G.S1 metaSel (G.Rec0 (f bean)))
+    (G.S1 metaSel (G.Rec0 (f' bean)))
+  where
+  gLiftA2Phase f (G.M1 (G.K1 abean)) (G.M1 (G.K1 fgbean)) =
+    G.M1 (G.K1 (f abean fgbean))
+
+
+-- | Examples without @-XQualifiedDo@:
+--
+-- >>> :{
+--  type Phases = IO `Compose` IO `Compose` Identity
+--  phased :: Phases Int
+--  phased =
+--      pure 1 Dep.Phases.>>= \i1 ->
+--      pure 2 Dep.Phases.>>= \i2 ->
+--      pure $ i1 + i2
+-- :}
+--
+--
+-- >>> :{
+-- type Phases = (IO `Compose` Maybe `Compose` Either Char) Int
+-- phases :: Phases
+-- phases = 
+--    pure () Dep.Phases.>>= \_ ->
+--    Just 5 Dep.Phases.>>= \_ ->
+--    Left 'e'
+-- :}
+--
+--
 (>>=) :: Functor f => f x -> (x -> g y) -> Compose f g y
 f >>= k = Compose (k <$> f)
 
+-- | Better not use this one without @-XQualifiedDo@
 (>>) :: Functor f => f x -> g y -> Compose f g y
 f >> g = Compose (g <$ f)
 
@@ -45,7 +344,7 @@
 -- It would indeed be useful (it would allow pre-packaging and sharing initial
 -- phases as do-blocks) but it isn't supported.
 --
--- __BEWARE__ #2! Do not use 'return' in this do-notation.
+-- __BEWARE#2__! Do not use 'return' in this do-notation.
 --
 -- Some valid examples:
 --
@@ -97,6 +396,7 @@
 -- >>> :set -fno-warn-deprecations
 -- >>> import Data.Kind
 -- >>> import Data.Function ((&))
+-- >>> import Control.Monad.IO.Class
 -- >>> import Dep.Env
 -- >>> import GHC.Generics (Generic)
 -- >>> import Prelude hiding ((>>=), (>>))
diff --git a/test/tests_has.hs b/test/tests_has.hs
--- a/test/tests_has.hs
+++ b/test/tests_has.hs
@@ -376,6 +376,12 @@
 acc2 :: Accumulator IO 
 acc2 = inject (Constant ())
 
+accAll :: (InjectsAll '[Activities, Constant ()] IO accum, Monoid accum) => accum
+accAll = inject (Activities []) <> inject (Constant ())
+
+acc3 :: Accumulator IO 
+acc3 = accAll
+
 --
 --
 --