diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Revision history for monad-actions
 
+## 2.0.0.0 -- 2026-02-22
+
+* This version adds a new record-based implementation of monad actions, meant to avoid overlapping instances.
+
 ## 1.0.0.0 -- 2026-01-27
 
 * For any monad m, m acts on every transformer stack whose base is m.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,10 @@
+Left or right actions of a monad on a functor.
+
+See [this blog post](https://stringdiagram.com/2023/04/23/monad-actions/) by Dan Marsden for an introduction to monad actions.
+
+This package provides two implementations of monad actions.
+The simpler one uses the `LeftModule`, `RightModule`, and `BiModule` classes defined in `Control.Monad.Action`,
+and can be used with the `QualifiedDo` extension by qualifying the `do` blocks with either `Control.Monad.Action.Right` or `Control.Monad.Action.Left`.
+However, it uses incoherent instances.
+The second implementation, designed to avoid incoherent and overlapping instances, is defined in `Control.Monad.Action.Records`, and uses the `LeftAction`, `RightAtion`, and `BiAction` types.
+It is meant to be used with `RecordWildCards` and `RebindableSyntax` and/or `OverloadedRecordDot`.
diff --git a/monad-actions.cabal b/monad-actions.cabal
--- a/monad-actions.cabal
+++ b/monad-actions.cabal
@@ -8,8 +8,8 @@
 --       +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 1.0.0.0
-synopsis: Left or right actions of a monad on a functor
+version: 2.0.0.0
+synopsis: Actions of monads on functors
 description:
   This package defines classes for left and right actions of
   monads on functors.  It also includes modules for using
@@ -26,6 +26,7 @@
 homepage: https://codeberg.org/noiioiu/monad-actions
 build-type: Simple
 extra-doc-files: CHANGELOG.md
+                 README.md
 
 common warnings
   ghc-options: -Wall
@@ -38,8 +39,10 @@
   import: warnings
   exposed-modules:
     Control.Monad.Action
+    Control.Monad.TransformerStack
     Control.Monad.Action.Left
     Control.Monad.Action.Right
+    Control.Monad.Action.Records
 
   other-modules: Control.Monad.Action.TH
   build-depends:
@@ -50,8 +53,9 @@
    mtl >= 2.3.1 && < 2.4,
    template-haskell >= 2.22.0 && < 2.23,
    transformers >= 0.6.1 && < 0.7,
+   constraints >= 0.14.4 && < 0.15,
 
-    
+
 
   hs-source-dirs: src
   default-language: GHC2021
diff --git a/src/Control/Monad/Action.hs b/src/Control/Monad/Action.hs
--- a/src/Control/Monad/Action.hs
+++ b/src/Control/Monad/Action.hs
@@ -1,12 +1,12 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | Given a monad \(M\) on a category \(\mathcal{D}\) with unit \(\eta\) and
 --     multiplication \(\mu\) and a functor \(F\) from \(\mathcal{C}\) to \(\mathcal{D}\),
---     a left monad action of \(M\) on \(F\) is a natural transformation \(\nu: M \circ F \to F\)
---     such that the following two laws hold:
+--     a left (or outer) monad action of \(M\) on \(F\) is a natural transformation
+--     \(\nu: M \circ F \to F\) such that the following two laws hold:
 --
 --     * \(\nu \cdot (\eta \circ F) = \mathrm{id}_F\)
 --     * \(\nu \cdot (\mu \circ F) = \nu \cdot (M \circ \nu)\)
@@ -14,12 +14,12 @@
 --     We also say that \(F\) is a left module over \(M\).  In the case
 --     \(\mathcal{C} = \mathcal{D}\), a left monad module is a left monoid module
 --     object in the category of endofunctors on \(\mathcal{C}\).  We may also
---     call \(\alpha\) the scalar multiplication of the module by the monad, by analogy
+--     call \(\nu\) the scalar multiplication of the module by the monad, by analogy
 --     with ring modules, which are monoid module objects in the category of abelian groups
 --     with tensor product as the monoidal product (rings are just monoid objects in this
 --     category).
 --
---     Right monad actions are defined similarly.
+--     Right (or inner) monad actions are defined similarly.
 --
 --     See [this blog post](https://stringdiagram.com/2023/04/23/monad-actions/) by Dan Marsden
 --     or the paper /Modules over monads and their algebras/ by Piróg, Wu, and Gibbons.
@@ -27,13 +27,10 @@
   ( LeftModule (..),
     RightModule (..),
     BiModule (..),
-    LiftStack (..),
   )
 where
 
 import Control.Monad (join)
-import Control.Monad.Action.TH
-import Control.Monad.Co ()
 import Control.Monad.Codensity (Codensity (..))
 import Control.Monad.Error.Class (MonadError (..), liftEither)
 import Control.Monad.IO.Class
@@ -41,21 +38,11 @@
 import Control.Monad.Reader.Class (MonadReader (..))
 import Control.Monad.State (State, runState)
 import Control.Monad.State.Class (MonadState (..))
-import Control.Monad.Trans ()
-import Control.Monad.Trans.Accum ()
-import Control.Monad.Trans.Compose ()
 import Control.Monad.Trans.Except (ExceptT (..), runExceptT)
-import Control.Monad.Trans.Free ()
-import Control.Monad.Trans.Iter ()
 import Control.Monad.Trans.Maybe (MaybeT (..))
 import Control.Monad.Trans.Reader (Reader, runReader)
-import Control.Monad.Trans.Select ()
-import Control.Monad.Trans.State.Lazy qualified as L ()
-import Control.Monad.Trans.State.Strict qualified as S ()
 import Control.Monad.Trans.Writer (Writer, runWriter)
-import Control.Monad.Trans.Writer.CPS qualified as C ()
-import Control.Monad.Trans.Writer.Lazy qualified as L ()
-import Control.Monad.Trans.Writer.Strict qualified as S ()
+import Control.Monad.TransformerStack
 import Control.Monad.Writer.Class (MonadWriter (..))
 import Data.Functor.Compose (Compose (..))
 import Data.List.NonEmpty qualified as NE (NonEmpty, toList)
@@ -103,149 +90,15 @@
     f a
   bijoin = rjoin . ljoin
 
--- | All @'LiftStack'@ instances are defined inductively using @'Control.Monad.Trans.Class.MonadTrans'@.
---   @'Control.Monad.Trans.Class.MonadTrans'@ instances are required to satisfy these laws, which state
---   that @'Control.Monad.Trans.Class.lift'@ is a monad homomorphism:
---
---   * @'Control.Monad.Trans.Class.lift' '.' 'pure' = 'pure'@
---
---   * @'Control.Monad.Trans.Class.lift' (m '>>=' f) = 'Control.Monad.Trans.Class.lift' m '>>=' ('Control.Monad.Trans.Class.lift' '.' f)@
---
---   Restating the second law in terms of @'join'@:
---
---   * @'Control.Monad.Trans.Class.lift' '.' 'join' = 'join' '.' 'fmap' 'Control.Monad.Trans.Class.lift' '.' 'Control.Monad.Trans.Class.lift'@
---
---   Because the composition of two monad homomorphisms is a monad homomorphism, @'liftStack'@ also satisfies these laws:
---
---   * @'liftStack' '.' 'pure' = 'pure'@
---
---   * @'liftStack' '.' 'join' = 'join' '.' 'fmap' 'liftStack' '.' 'liftStack'@
---
---   The left monad action laws can now be easily proved using string diagrams.
---   Functors compose from top to bottom, natural transformations from left to right,
---   @───@ represents @t m@, @┈┈┈@ represents @m@, @├@ represents @'pure'@ or
---   @'join'@ depending on the number of inputs, and @┈┈┈►───@ represents @'liftStack'@.
---   The @'LiftStack'@ laws as string diagrams are:
---
---   > ├┈┈┈►───  = ├──────
---
---   > ┈┈┈┐            ┈┈┈►───┐
---   >    ├┈┈┈►───  =         ├───
---   > ┈┈┈┘            ┈┈┈►───┘
---
---   and the diagram for @'ljoin'@ is:
---
---   > ┈┈►──┐
---   >      ├───
---   > ─────┘
---
---   To prove the identity law:
---
---   >   ├┈┈►──┐          ├─────┐
---   >         ├───  =          ├───  =  ──────
---   > ────────┘        ────────┘
---
---   In other words,
---
---   @   'ljoin' '.' 'pure'
---   = 'join' '.' 'liftStack' '.' 'pure'
---   = 'join' '.' 'pure'
---   = 'id'@
---
---   To prove associativity:
---
---   > ┈┈┈┐              ┈┈►──┐
---   >    ├┈┈►─┐              ├──┐         ┈┈┈┈┈┈┈►─┐
---   > ┈┈┈┘    ├────  =  ┈┈►──┘  ├────  =  ┈┈►──┐   ├────
---   > ────────┘         ────────┘              ├───┘
---   >                                     ─────┘
---
---   In other words,
---
---   @  'ljoin' '.' 'join'
---   = 'join' '.' 'liftStack' '.' 'join'
---   = 'join' '.' 'join' '.' 'fmap' 'liftStack' '.' 'liftStack'
---   = 'join' '.' 'fmap' 'join' '.' 'fmap' 'liftStack' '.' 'liftStack'
---   = 'join' '.' 'fmap' ('join' '.' 'liftStack') '.' 'liftStack'
---   = 'join' '.' 'liftStack' '.' 'fmap' ('join' '.' 'liftStack')
---   = 'ljoin' '.' 'fmap' 'ljoin'@
---
---   We can prove the right module laws using string diagrams in the same way.
---
---   The diagram for @'rjoin'@ is:
---
---   > ─────┐
---   >      ├───
---   > ┈┈►──┘
---
---   To prove the identity law:
---
---   > ────────┐        ────────┐
---   >         ├───  =          ├───  =  ──────
---   >   ├┈┈►──┘          ├─────┘
---
---   In other words,
---
---   @   'rjoin' '.' 'fmap' 'pure'
---   = 'join' '.' 'fmap' 'liftStack' , 'pure'
---   = 'join' '.' 'fmap' 'liftStack' , 'fmap' 'pure'
---   = 'join' '.' 'fmap' ('liftStack' , 'pure')
---   = 'join' '.' 'fmap' 'pure'
---   = 'id'@
---
---   To prove associativity:
---
---   >                                      ─────┐
---   > ────────┐         ─────────┐              ├───┐
---   > ┈┈┈┐    ├────  =  ┈┈►──┐   ├────  =  ┈┈►──┘   ├────
---   >    ├┈┈►─┘              ├───┘         ┈┈┈┈┈┈┈►─┘
---   > ┈┈┈┘              ┈┈►──┘
---
---   In other words,
---
---   @  'rjoin' '.' 'fmap' 'join'
---   = 'join' '.' 'fmap' 'liftStack' '.' 'fmap' 'join'
---   = 'join' '.' 'fmap' ('liftStack' '.' 'join')
---   = 'join' '.' 'fmap' ('join' '.' 'fmap' 'liftStack' '.' 'liftStack')
---   = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'liftStack' '.' 'liftStack')
---   = 'join' '.' 'join' '.' 'fmap' ('fmap' 'liftStack') '.' 'fmap' ('liftStack')
---   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'fmap' 'liftStack'
---   = 'rjoin' '.' 'rjoin'@
---
---   The bimodule law can be proved as follows:
---
---   > ┈┈┈►─┐             ┈┈►─┐
---   >      ├───┐             ├───┐          ┈┈┈┈┈┈►─┐
---   > ─────┘   ├────  =  ────┘   ├────  =   ────┐   ├────
---   > ┈►───────┘         ┈┈┈┈┈┈►─┘              ├───┘
---   >                                       ┈┈►─┘
---
---   In other words,
---
---   @  'bijoin'
---   = 'join' '.' 'join' '.' 'liftStack' '.' 'fmap' ('fmap' 'liftStack')
---   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'liftStack'
---   = 'rjoin' '.' 'ljoin'
---   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'liftStack'
---   = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'liftStack') '.' 'liftStack'
---   = 'join' '.' 'fmap' ('join' '.' 'fmap' 'liftStack') '.' 'liftStack'
---   = 'join' '.' 'fmap' 'rjoin' '.' 'liftStack'
---   = 'join' '.' 'liftStack' '.' 'fmap' 'rjoin'
---   = 'ljoin' '.' 'fmap' 'rjoin'@
-class LiftStack m n where
-  liftStack :: forall a. m a -> n a
-
-$mkLiftStackInstances
-
-instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => LeftModule m n where
+instance {-# OVERLAPS #-} (Monad n, Monad m, MonadTransStack m n) => LeftModule m n where
   ljoin = join . liftStack
   lbind = (>>=) . liftStack
 
-instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => RightModule m n where
+instance {-# OVERLAPS #-} (Monad n, Monad m, MonadTransStack m n) => RightModule m n where
   rjoin = (liftStack =<<)
   rbind = flip $ (=<<) . (liftStack .)
 
-instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => BiModule m m n
+instance {-# OVERLAPS #-} (Monad n, Monad m, MonadTransStack m n) => BiModule m m n
 
 instance {-# INCOHERENT #-} (Functor f) => LeftModule Identity f where ljoin = runIdentity
 
@@ -419,7 +272,7 @@
 instance {-# INCOHERENT #-} (MonadState s m) => BiModule (State s) (State s) m
 
 -- | Proof that @f@ is always a left module over @t'Codensity' f@:
--- 
+--
 --   * @   'ljoin' ('join' m)
 --       = 'ljoin' ('Codensity' (\\c -> 'runCodensity' m (\\a -> 'runCodensity' a c)))
 --       = (\\c -> 'runCodensity' m (\\a -> 'runCodensity' a c)) id
@@ -428,7 +281,7 @@
 --       = (\\k -> 'runCodensity' m (\\x -> k ('ljoin' x))) 'id'
 --       = 'ljoin' ('Codensity' (\\k -> 'runCodensity' m (\\x -> k ('ljoin' x))))
 --       = 'ljoin' ('fmap' 'ljoin' m)@
--- 
+--
 --   * @'ljoin' ('pure' x) = 'ljoin' ('Codensity' (\\x -> k x)) = (\\k -> k x) 'id' = x@
 instance (Functor f) => LeftModule (Codensity f) f where
   ljoin c = runCodensity c id
diff --git a/src/Control/Monad/Action/Records.hs b/src/Control/Monad/Action/Records.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Action/Records.hs
@@ -0,0 +1,323 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE NoFieldSelectors #-}
+
+-- | This module should be used with @OverloadedRecordDot@ and/or @RebindableSyntax@ (and @RecordWildCards@).
+module Control.Monad.Action.Records where
+
+import Control.Monad qualified as M (Monad (..), join, (=<<))
+import Control.Monad.Codensity (Codensity (..))
+import Control.Monad.Error.Class (MonadError, liftEither)
+import Control.Monad.IO.Class (MonadIO (..))
+import Control.Monad.RWS (MonadRWS, RWS, RWST (..), runRWS)
+import Control.Monad.Reader (MonadReader (..), Reader, ReaderT (..), runReader)
+import Control.Monad.State (MonadState (..), State, StateT (..), runState)
+import Control.Monad.Trans.Writer (WriterT (..))
+import Control.Monad.TransformerStack
+import Control.Monad.Writer (MonadWriter (..), Writer, runWriter)
+import Data.Bifunctor (second)
+import Data.Constraint (Dict (..))
+import Data.Functor.Compose (Compose (..))
+import Data.Kind (Constraint, Type)
+import Data.List.NonEmpty qualified as NE
+import Data.Maybe (maybeToList)
+import Prelude hiding ((<*>), (=<<), (>>), (>>=))
+import Prelude qualified as P
+
+infixl 1 >>=
+
+infixr 1 =<<
+
+infixl 1 >>
+
+infixr 1 >=>
+
+infixr 1 <=<
+
+infixl 4 <*>
+
+-- | Every @'LeftAction'@ @l@ should satisfy the following laws:
+--
+-- * @l.'join' '.' 'Control.Monad.join' = l.'join' '.' 'fmap' l.'join'@
+--
+-- * @l.'join' '.' 'pure' = 'id'@
+--
+-- All of the operators should match the default implementations in "Control.Monad.Action" and "Control.Monad.Left".
+data LeftAction (action :: (Type -> Type) -> (Type -> Type) -> Constraint) where
+  LeftAction ::
+    { -- | left monad action scalar multiplication
+      join :: forall m f a. (action m f) => m (f a) -> f a,
+      -- | left monad action bind
+      (>>=) :: forall m f a b. (action m f) => m a -> (a -> f b) -> f b,
+      -- | left monad action bind with arguments reversed
+      (=<<) :: forall m f a b. (action m f) => (a -> f b) -> m a -> f b,
+      -- | left to right Kleisli arrow scalar multiplication induced by a left monad action
+      (>=>) :: forall m f a b c. (action m f) => (a -> m b) -> (b -> f c) -> a -> f c,
+      -- | right to left Kleisli arrow scalar multiplication induced by a left monad action
+      (<=<) :: forall m f a b c. (action m f) => (b -> f c) -> (a -> m b) -> a -> f c,
+      -- | left monad action sequencing operator
+      (>>) :: forall m f a b. (action m f) => m a -> f b -> f b,
+      -- | scalar sequential application, used for desugaring applicative do blocks
+      (<*>) :: forall m f a b. (action m f) => m (a -> b) -> f a -> f b
+    } ->
+    LeftAction action
+
+-- | Every @'RightAction'@ @r@ should satisfy the following laws:
+--
+-- * @r.'join' '.' 'fmap' 'Control.Monad.join' = r.'join' '.' r.'join'@
+--
+-- * @r.'join' '.' 'fmap' 'pure' = 'id'@
+--
+-- All of the operators should match the default implementations in "Control.Monad.Action" and "Control.Monad.Right".
+data RightAction (action :: (Type -> Type) -> (Type -> Type) -> Constraint) where
+  RightAction ::
+    { -- | right monad action scalar multiplication
+      join :: forall m f a. (action m f) => f (m a) -> f a,
+      -- | right monad action bind
+      (>>=) :: forall m f a b. (action m f) => f a -> (a -> m b) -> f b,
+      -- | right monad action bind with arguments reversed
+      (=<<) :: forall m f a b. (action m f) => (a -> m b) -> f a -> f b,
+      -- | left to right Kleisli arrow scalar multiplication induced by a right monad action
+      (>=>) :: forall m f a b c. (action m f) => (a -> f b) -> (b -> m c) -> a -> f c,
+      -- | right to left Kleisli arrow scalar multiplication induced by a right monad action
+      (<=<) :: forall m f a b c. (action m f) => (b -> m c) -> (a -> f b) -> a -> f c,
+      -- | right monad action sequencing operator
+      (>>) :: forall m f a b. (action m f) => f a -> m b -> f b,
+      -- | scalar sequential application, used for desugaring applicative do blocks
+      (<*>) :: forall m f a b. (action m f) => f (a -> b) -> m a -> f b
+    } ->
+    RightAction action
+
+-- | Every @'BiAction'@ @b@ should satisfy the following laws, in addition to the laws for left and right actions:
+--
+-- * @b.'right'.'join' '.' b.'left'.'join' = b.'left'.'join' '.' 'fmap' b.'right'.'join'@
+data BiAction (action :: (Type -> Type) -> (Type -> Type) -> Constraint) where
+  BiAction ::
+    { left :: LeftAction action,
+      right :: RightAction action
+    } ->
+    BiAction action
+
+-- | @'MonadHomomorphism' c@ means that, whenever @c m n@, there is a monad homomorphism @'hom'@ from @m@ to @n@.
+class MonadHomomorphism (c :: (Type -> Type) -> (Type -> Type) -> Constraint) where
+  hom :: forall m n a. (c m n) => m a -> n a
+  mDict :: forall m n. (c m n) => (Dict (Monad m), Dict (Monad n))
+
+-- | Two-sided action induced by a monad homomorphism.
+monadMorphAction :: forall action. (MonadHomomorphism action) => BiAction action
+monadMorphAction =
+  let left =
+        let join :: forall m n a. (action m n) => m (n a) -> n a
+            join = case mDict @action @m @n of (_, Dict) -> M.join . hom @action
+            (>>=) :: forall m n a b. (action m n) => m a -> (a -> n b) -> n b
+            (>>=) = case mDict @action @m @n of (_, Dict) -> (P.>>=) . hom @action
+            (=<<) :: forall m n a b. (action m n) => (a -> n b) -> m a -> n b
+            (=<<) = flip (>>=)
+            (>=>) :: forall m n a b c. (action m n) => (a -> m b) -> (b -> n c) -> a -> n c
+            f >=> g = \x -> f x >>= g
+            (<=<) :: forall m n a b c. (action m n) => (b -> n c) -> (a -> m b) -> a -> n c
+            (<=<) = flip (>=>)
+            (>>) :: forall m n a b. (action m n) => m a -> n b -> n b
+            a >> b = a >>= const b
+            (<*>) :: forall m n a b. (action m n) => m (a -> b) -> n a -> n b
+            (<*>) = case mDict @action @m @n of (_, Dict) -> (P.<*>) . hom @action
+         in LeftAction {..} :: LeftAction action
+      right =
+        let join :: forall m n a. (action m n) => n (m a) -> n a
+            join = case mDict @action @m @n of (_, Dict) -> (hom @action M.=<<)
+            (>>=) :: forall m n a b. (action m n) => n a -> (a -> m b) -> n b
+            (>>=) = flip (=<<)
+            (=<<) :: forall m n a b. (action m n) => (a -> m b) -> n a -> n b
+            (=<<) = case mDict @action @m @n of (_, Dict) -> (M.=<<) . (hom @action .)
+            (>=>) :: forall m n a b c. (action m n) => (a -> n b) -> (b -> m c) -> a -> n c
+            f >=> g = \x -> f x >>= g
+            (<=<) :: forall m n a b c. (action m n) => (b -> m c) -> (a -> n b) -> a -> n c
+            (<=<) = flip (>=>)
+            (>>) :: forall m n a b. (action m n) => n a -> m b -> n b
+            a >> b = a >>= const b
+            (<*>) :: forall m n a b. (action m n) => n (a -> b) -> m a -> n b
+            f <*> x = case mDict @action @m @n of (_, Dict) -> f P.<*> hom @action x
+         in RightAction {..} :: RightAction action
+   in BiAction {..}
+
+instance MonadHomomorphism MonadTransStack where
+  hom = liftStack
+  mDict = (Dict, Dict)
+
+transformerStackAction :: BiAction MonadTransStack
+transformerStackAction = monadMorphAction
+
+-- | @m ':<:' n@ means that @m@ is a submonad of @n@. @'inject'@ must be a monic monad homomorphism.
+class (Monad m, Monad n) => m :<: n where
+  inject :: forall a. m a -> n a
+
+instance MonadHomomorphism (:<:) where
+  hom = inject
+  mDict = (Dict, Dict)
+
+submonadAction :: BiAction (:<:)
+submonadAction = monadMorphAction
+
+instance (Monad m) => m :<: m where
+  inject = id
+
+-- | A @'Maybe'@ is just a list of length at most 1.
+instance Maybe :<: [] where
+  inject = maybeToList
+
+-- | A @'Data.List.NonEmpty.NonEmpty'@ is just a list of length at least 1.
+instance NE.NonEmpty :<: [] where
+  inject = NE.toList
+
+-- | @'ReaderT'@ is just read-only @'StateT'@.
+instance (m :<: n) => ReaderT s m :<: StateT s n where
+  inject ReaderT {runReaderT} = StateT $ \s -> inject . fmap (,s) $ runReaderT s
+
+-- | @'WriterT'@ is just append-only @'StateT'@.
+instance (Monoid s, m :<: n) => WriterT s m :<: StateT s n where
+  inject WriterT {runWriterT} = StateT $ \s -> inject @m @n . fmap (second (s <>)) $ runWriterT
+
+-- | @'StateT'@ is just @'RWST'@ that ignores the read-only environment and doesn't append to the output.
+instance (Monoid w, m :<: n) => StateT s m :<: RWST r w s n where
+  inject StateT {runStateT} = RWST $ \_ s -> inject . fmap (\(a, t) -> (a, t, mempty)) $ runStateT s
+
+-- | @'ReaderT'@ is just @'RWST'@ that ignores the state and doesn't append to the output.
+--
+--   Note: @'inject' \@('ReaderT' s m) \@('StateT' s n) '.' 'inject' \@('StateT' s n) \@('RWST' s w s k) =/= 'inject' \@('ReaderT' s m) \@('RWST' s w s k)@
+instance (Monoid w, m :<: n) => ReaderT r m :<: RWST r w s n where
+  inject ReaderT {runReaderT} = RWST $ \r s -> inject . fmap (,s,mempty) $ runReaderT r
+
+-- | @'WriterT'@ is just @'RWST'@ that ignores the environment and state.
+--
+--   Note: @'inject' \@('WriterT' w m) \@('StateT' w n) '.' 'inject' \@('StateT' w n) \@('RWST' r w w k) =/= 'inject' \@('WriterT' w m) \@('RWST' r w w k)@
+instance (Monoid w, m :<: n) => WriterT w m :<: RWST r w s n where
+  inject WriterT {runWriterT} = RWST $ \_ s -> inject @m @n . fmap (\(a, w) -> (a, s, w)) $ runWriterT
+
+instance (MonadIO m) => IO :<: m where
+  inject = liftIO
+
+instance (MonadState s m) => (State s) :<: m where
+  inject = state . runState
+
+instance (MonadReader r m) => (Reader r) :<: m where
+  inject = reader . runReader
+
+instance (MonadWriter w m) => (Writer w) :<: m where
+  inject = writer . runWriter
+
+instance (MonadRWS r w s m) => (RWS r w s) :<: m where
+  inject t =
+    ask P.>>= \r ->
+      get P.>>= \s ->
+        let (a, s', w) = runRWS t r s
+         in put s'
+              M.>> tell w
+              M.>> pure a
+
+instance (MonadError e m) => (Either e) :<: m where
+  inject = liftEither
+
+class CodensityAction m f where
+  codensityJoin :: forall a. m (f a) -> f a
+  codensityBind :: forall a b. m a -> (a -> f b) -> f b
+  codensityApply :: forall a b. m (a -> b) -> f a -> f b
+
+codensityAction :: LeftAction CodensityAction
+codensityAction =
+  let join :: forall m f a. (CodensityAction m f) => m (f a) -> f a
+      join = codensityJoin
+      (>>=) :: forall m f a b. (CodensityAction m f) => m a -> (a -> f b) -> f b
+      (>>=) = codensityBind
+      (=<<) :: forall m f a b. (CodensityAction m f) => (a -> f b) -> m a -> f b
+      (=<<) = flip codensityBind
+      (>=>) :: forall m f a b c. (CodensityAction m f) => (a -> m b) -> (b -> f c) -> a -> f c
+      f >=> g = \x -> f x >>= g
+      (<=<) :: forall m f a b c. (CodensityAction m f) => (b -> f c) -> (a -> m b) -> a -> f c
+      (<=<) = flip (>=>)
+      (>>) :: forall m f a b. (CodensityAction m f) => m a -> f b -> f b
+      a >> b = a >>= const b
+      (<*>) :: forall m f a b. (CodensityAction m f) => m (a -> b) -> f a -> f b
+      (<*>) = codensityApply
+   in LeftAction {..}
+
+instance (Monad m) => CodensityAction m m where
+  codensityJoin = M.join
+  codensityBind = (P.>>=)
+  codensityApply = (P.<*>)
+
+instance (Functor f) => CodensityAction (Codensity f) f where
+  codensityJoin c = runCodensity c id
+  a `codensityBind` f = runCodensity (f P.<$> a) id
+  fs `codensityApply` xs = fs `codensityBind` flip fmap xs
+
+class (Monad m, Functor f) => LeftCompAction m f where
+  leftCompJoin :: forall a. m (f a) -> f a
+  leftCompBind :: forall a b. m a -> (a -> f b) -> f b
+  leftCompApply :: forall a b. m (a -> b) -> f a -> f b
+
+-- | Left action of any monad @m@ on any composition of functors with @m@ as the outermost component.
+leftCompAction :: LeftAction LeftCompAction
+leftCompAction =
+  let join :: forall m f a. (LeftCompAction m f) => m (f a) -> f a
+      join = leftCompJoin
+      (>>=) :: forall m f a b. (LeftCompAction m f) => m a -> (a -> f b) -> f b
+      (>>=) = leftCompBind
+      (=<<) :: forall m f a b. (LeftCompAction m f) => (a -> f b) -> m a -> f b
+      (=<<) = flip leftCompBind
+      (>=>) :: forall m f a b c. (LeftCompAction m f) => (a -> m b) -> (b -> f c) -> a -> f c
+      f >=> g = \x -> f x >>= g
+      (<=<) :: forall m f a b c. (LeftCompAction m f) => (b -> f c) -> (a -> m b) -> a -> f c
+      (<=<) = flip (>=>)
+      (>>) :: forall m f a b. (LeftCompAction m f) => m a -> f b -> f b
+      a >> b = a >>= const b
+      (<*>) :: forall m f a b. (LeftCompAction m f) => m (a -> b) -> f a -> f b
+      (<*>) = leftCompApply
+   in LeftAction {..}
+
+instance (Monad m) => LeftCompAction m m where
+  leftCompJoin = M.join
+  leftCompBind = (P.>>=)
+  leftCompApply = (P.<*>)
+
+instance (LeftCompAction m f, Functor g) => LeftCompAction m (Compose f g) where
+  leftCompJoin = Compose . leftCompJoin . fmap getCompose
+  a `leftCompBind` f = Compose $ a `leftCompBind` (getCompose . f)
+  fs `leftCompApply` xs = fs `leftCompBind` flip fmap xs
+
+class (Monad m, Functor f) => RightCompAction m f where
+  rightCompJoin :: forall a. f (m a) -> f a
+  rightCompBind :: forall a b. f a -> (a -> m b) -> f b
+  rightCompApply :: forall a b. f (a -> b) -> m a -> f b
+
+-- | Right action of any monad @m@ on any composition of functors with @m@ as the innermost component.
+rightCompAction :: RightAction RightCompAction
+rightCompAction =
+  let join :: forall m f a. (RightCompAction m f) => f (m a) -> f a
+      join = rightCompJoin
+      (>>=) :: forall m f a b. (RightCompAction m f) => f a -> (a -> m b) -> f b
+      (>>=) = rightCompBind
+      (=<<) :: forall m f a b. (RightCompAction m f) => (a -> m b) -> f a -> f b
+      (=<<) = flip rightCompBind
+      (>=>) :: forall m f a b c. (RightCompAction m f) => (a -> f b) -> (b -> m c) -> a -> f c
+      f >=> g = \x -> f x >>= g
+      (<=<) :: forall m f a b c. (RightCompAction m f) => (b -> m c) -> (a -> f b) -> a -> f c
+      (<=<) = flip (>=>)
+      (>>) :: forall m f a b. (RightCompAction m f) => f a -> m b -> f b
+      a >> b = a >>= const b
+      (<*>) :: forall m f a b. (RightCompAction m f) => f (a -> b) -> m a -> f b
+      (<*>) = rightCompApply
+   in RightAction {..}
+
+instance (Monad m) => RightCompAction m m where
+  rightCompJoin = M.join
+  rightCompBind = (P.>>=)
+  rightCompApply = (P.<*>)
+
+instance (RightCompAction m f, Functor g) => RightCompAction m (Compose g f) where
+  rightCompJoin = Compose . fmap rightCompJoin . getCompose
+  a `rightCompBind` f = Compose . fmap (`rightCompBind` f) $ getCompose a
+  fs `rightCompApply` xs = fs `rightCompBind` flip fmap xs
diff --git a/src/Control/Monad/Action/TH.hs b/src/Control/Monad/Action/TH.hs
--- a/src/Control/Monad/Action/TH.hs
+++ b/src/Control/Monad/Action/TH.hs
@@ -1,9 +1,11 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
+{-# LANGUAGE TypeData #-}
 
-module Control.Monad.Action.TH (mkLiftStackInstances) where
+module Control.Monad.Action.TH (mkLiftBy) where
 
 import Control.Monad.Trans
+import Data.Kind qualified as K
 import Language.Haskell.TH
 
 infixl 5 #
@@ -11,43 +13,62 @@
 (#) :: Type -> Type -> Type
 (#) = AppT
 
-mkLiftStackInstances :: Q [Dec]
-mkLiftStackInstances =
+(|->|) :: Type -> Type -> Type
+a |->| b = ArrowT # a # b
+
+mkLiftBy :: Q [Dec]
+mkLiftBy =
   reify ''MonadTrans
     >>= \case
       ClassI _ instances ->
         do
+          decs <-
+            [d|
+              type data Nat = Z | S Nat
+
+              class (Monad m, Monad n) => LiftBy (k :: Nat) (m :: K.Type -> K.Type) (n :: K.Type -> K.Type) | k n -> m where
+                liftBy :: m a -> n a
+
+              instance (Monad m) => LiftBy Z m m where
+                liftBy = id
+              |]
+          let famName = mkName "Steps"
           m <- newName "m"
           n <- newName "n"
-          let cName = mkName "LiftStack"
-          -- instance LiftStack m m where
-          --   liftStack = id
-          let baseInstance =
-                InstanceD
-                  (Just Incoherent)
-                  []
-                  (ConT cName # VarT m # VarT m)
-                  [ValD (VarP $ mkName "liftStack") (NormalB $ VarE 'id) []]
-              inductiveInstances =
+          k <- newName "k"
+          let famDec =
+                ClosedTypeFamilyD
+                  ( TypeFamilyHead
+                      famName
+                      [ KindedTV m BndrReq (StarT |->| StarT),
+                        KindedTV n BndrReq (StarT |->| StarT)
+                      ]
+                      (KindSig . ConT $ mkName "Nat")
+                      Nothing
+                  )
+                  $ TySynEqn Nothing (ConT famName # VarT m # VarT m) (ConT $ mkName "Z")
+                    : ( instances >>= \case
+                          InstanceD _ _ (AppT (ConT _) t) _ ->
+                            [ TySynEqn
+                                Nothing
+                                (ConT famName # VarT m # (t # VarT n))
+                                (ConT (mkName "S") # (ConT famName # VarT m # VarT n))
+                            ]
+                          _ -> []
+                      )
+          let inductiveInstances =
                 instances >>= \case
-                  InstanceD _ ct (AppT (ConT _) t) _ ->
-                    -- instance (Monad m, Monad n, LiftStack m n) => LiftStack m (t n) where
-                    --   liftStack = lift . liftStack
+                  InstanceD ov ct (AppT (ConT _) t) _ ->
                     pure $
                       InstanceD
-                        (Just Incoherent)
-                        ( [ ConT ''Monad # VarT m,
-                            ConT ''Monad # VarT n,
-                            ConT cName # VarT m # VarT n
-                          ]
-                            ++ ct
-                        )
-                        (ConT cName # VarT m # (t # VarT n))
+                        ov
+                        (ct ++ [ConT (mkName "LiftBy") # VarT k # VarT m # VarT n, ConT ''Monad # (t # VarT n)])
+                        (ConT (mkName "LiftBy") # (ConT (mkName "S") # VarT k) # VarT m # (t # VarT n))
                         [ ValD
-                            (VarP $ mkName "liftStack")
-                            (NormalB $ UInfixE (VarE 'lift) (VarE '(.)) (VarE $ mkName "liftStack"))
+                            (VarP $ mkName "liftBy")
+                            (NormalB $ UInfixE (VarE 'lift) (VarE '(.)) (AppTypeE (VarE $ mkName "liftBy") (VarT k)))
                             []
                         ]
                   _ -> []
-          pure $ baseInstance : inductiveInstances
+          pure $ decs ++ famDec : inductiveInstances
       _ -> pure []
diff --git a/src/Control/Monad/TransformerStack.hs b/src/Control/Monad/TransformerStack.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/TransformerStack.hs
@@ -0,0 +1,169 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeData #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Control.Monad.TransformerStack (MonadTransStack (..)) where
+
+import Control.Monad.Action.TH
+import Control.Monad.Co ()
+import Control.Monad.Trans ()
+import Control.Monad.Trans.Accum ()
+import Control.Monad.Trans.Compose ()
+import Control.Monad.Trans.Except ()
+import Control.Monad.Trans.Free ()
+import Control.Monad.Trans.Iter ()
+import Control.Monad.Trans.Maybe ()
+import Control.Monad.Trans.RWS ()
+import Control.Monad.Trans.RWS.CPS ()
+import Control.Monad.Trans.RWS.Lazy ()
+import Control.Monad.Trans.RWS.Strict ()
+import Control.Monad.Trans.Reader ()
+import Control.Monad.Trans.Select ()
+import Control.Monad.Trans.State.Lazy ()
+import Control.Monad.Trans.State.Strict ()
+import Control.Monad.Trans.Writer ()
+import Control.Monad.Trans.Writer.CPS ()
+import Control.Monad.Trans.Writer.Lazy ()
+import Control.Monad.Trans.Writer.Strict ()
+
+$mkLiftBy
+
+-- | @'MonadTransStack' m n@ means that @n@ is a stack of monad transformers over @m@.
+--
+--   All @'MonadTransStack'@ instances are defined inductively using @'Control.Monad.Trans.Class.MonadTrans'@.
+--   @'Control.Monad.Trans.Class.MonadTrans'@ instances are required to satisfy these laws, which state
+--   that @'Control.Monad.Trans.Class.lift'@ is a monad homomorphism:
+--
+--   * @'Control.Monad.Trans.Class.lift' '.' 'pure' = 'pure'@
+--
+--   * @'Control.Monad.Trans.Class.lift' (m '>>=' f) = 'Control.Monad.Trans.Class.lift' m '>>=' ('Control.Monad.Trans.Class.lift' '.' f)@
+--
+--   Restating the second law in terms of @'Control.Monad.join'@:
+--
+--   * @'Control.Monad.Trans.Class.lift' '.' 'Control.Monad.join' = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.Trans.Class.lift' '.' 'Control.Monad.Trans.Class.lift'@
+--
+--   Because the composition of two monad homomorphisms is a monad homomorphism, @'liftStack'@ also satisfies these laws:
+--
+--   * @'liftStack' '.' 'pure' = 'pure'@
+--
+--   * @'liftStack' '.' 'Control.Monad.join' = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack'@
+--
+--   The left monad action laws can now be easily proved using string diagrams.
+--   Functors compose from top to bottom, natural transformations from left to right,
+--   @───@ represents @t m@, @┈┈┈@ represents @m@, @├@ represents @'pure'@ or
+--   @'Control.Monad.join'@ depending on the number of inputs, and @┈┈┈►───@ represents @'liftStack'@.
+--   The @'MonadTransStack'@ laws as string diagrams are:
+--
+--   > ├┈┈┈►───  = ├──────
+--
+--   > ┈┈┈┐            ┈┈┈►───┐
+--   >    ├┈┈┈►───  =         ├───
+--   > ┈┈┈┘            ┈┈┈►───┘
+--
+--   and the diagram for @'Control.Monad.Action.ljoin'@ is:
+--
+--   > ┈┈►──┐
+--   >      ├───
+--   > ─────┘
+--
+--   To prove the identity law:
+--
+--   >   ├┈┈►──┐          ├─────┐
+--   >         ├───  =          ├───  =  ──────
+--   > ────────┘        ────────┘
+--
+--   In other words,
+--
+--   @   'Control.Monad.Action.ljoin' '.' 'pure'
+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'pure'
+--   = 'Control.Monad.join' '.' 'pure'
+--   = 'id'@
+--
+--   To prove associativity:
+--
+--   > ┈┈┈┐              ┈┈►──┐
+--   >    ├┈┈►─┐              ├──┐         ┈┈┈┈┈┈┈►─┐
+--   > ┈┈┈┘    ├────  =  ┈┈►──┘  ├────  =  ┈┈►──┐   ├────
+--   > ────────┘         ────────┘              ├───┘
+--   >                                     ─────┘
+--
+--   In other words,
+--
+--   @  'Control.Monad.Action.ljoin' '.' 'Control.Monad.join'
+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'Control.Monad.join'
+--   = 'Control.Monad.join' '.' 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'fmap' ('Control.Monad.join' '.' 'liftStack') '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'fmap' ('Control.Monad.join' '.' 'liftStack')
+--   = 'Control.Monad.Action.ljoin' '.' 'fmap' 'Control.Monad.Action.ljoin'@
+--
+--   We can prove the right module laws using string diagrams in the same way.
+--
+--   The diagram for @'Control.Monad.Action.rjoin'@ is:
+--
+--   > ─────┐
+--   >      ├───
+--   > ┈┈►──┘
+--
+--   To prove the identity law:
+--
+--   > ────────┐        ────────┐
+--   >         ├───  =          ├───  =  ──────
+--   >   ├┈┈►──┘          ├─────┘
+--
+--   In other words,
+--
+--   @   'Control.Monad.Action.rjoin' '.' 'fmap' 'pure'
+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' , 'pure'
+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' , 'fmap' 'pure'
+--   = 'Control.Monad.join' '.' 'fmap' ('liftStack' , 'pure')
+--   = 'Control.Monad.join' '.' 'fmap' 'pure'
+--   = 'id'@
+--
+--   To prove associativity:
+--
+--   >                                      ─────┐
+--   > ────────┐         ─────────┐              ├───┐
+--   > ┈┈┈┐    ├────  =  ┈┈►──┐   ├────  =  ┈┈►──┘   ├────
+--   >    ├┈┈►─┘              ├───┘         ┈┈┈┈┈┈┈►─┘
+--   > ┈┈┈┘              ┈┈►──┘
+--
+--   In other words,
+--
+--   @  'Control.Monad.Action.rjoin' '.' 'fmap' 'Control.Monad.join'
+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'fmap' 'Control.Monad.join'
+--   = 'Control.Monad.join' '.' 'fmap' ('liftStack' '.' 'Control.Monad.join')
+--   = 'Control.Monad.join' '.' 'fmap' ('Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'liftStack')
+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.join' '.' 'fmap' ('fmap' 'liftStack' '.' 'liftStack')
+--   = 'Control.Monad.join' '.' 'Control.Monad.join' '.' 'fmap' ('fmap' 'liftStack') '.' 'fmap' ('liftStack')
+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'Control.Monad.join' '.' 'fmap' 'liftStack'
+--   = 'Control.Monad.Action.rjoin' '.' 'Control.Monad.Action.rjoin'@
+--
+--   The bimodule law can be proved as follows:
+--
+--   > ┈┈┈►─┐             ┈┈►─┐
+--   >      ├───┐             ├───┐          ┈┈┈┈┈┈►─┐
+--   > ─────┘   ├────  =  ────┘   ├────  =   ────┐   ├────
+--   > ┈►───────┘         ┈┈┈┈┈┈►─┘              ├───┘
+--   >                                       ┈┈►─┘
+--
+--   In other words,
+--
+--   @  'Control.Monad.Action.bijoin'
+--   = 'Control.Monad.join' '.' 'Control.Monad.join' '.' 'liftStack' '.' 'fmap' ('fmap' 'liftStack')
+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'Control.Monad.join' '.' 'liftStack'
+--   = 'Control.Monad.Action.rjoin' '.' 'Control.Monad.Action.ljoin'
+--   = 'Control.Monad.join' '.' 'fmap' 'liftStack' '.' 'Control.Monad.join' '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.join' '.' 'fmap' ('fmap' 'liftStack') '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'fmap' ('Control.Monad.join' '.' 'fmap' 'liftStack') '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'fmap' 'Control.Monad.Action.rjoin' '.' 'liftStack'
+--   = 'Control.Monad.join' '.' 'liftStack' '.' 'fmap' 'Control.Monad.Action.rjoin'
+--   = 'Control.Monad.Action.ljoin' '.' 'fmap' 'Control.Monad.Action.rjoin'@
+class (LiftBy (Steps m n) m n) => MonadTransStack m n where
+  liftStack :: forall a. m a -> n a
+
+instance (LiftBy (Steps m n) m n) => MonadTransStack m n where
+  liftStack = liftBy @(Steps m n)
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -21,6 +21,7 @@
 import Control.Monad.Trans.Compose
 import Control.Monad.Trans.Free (FreeF (..), FreeT (..))
 import Control.Monad.Trans.Maybe
+import Control.Monad.TransformerStack
 import Control.Monad.Writer
 import Data.Functor.Classes (Eq1)
 import Data.Functor.Compose
@@ -130,7 +131,8 @@
     Arbitrary s,
     EqProp (m (a, s)),
     Arbitrary (m (m (m a), s)),
-    Show (m (m (m a), s))
+    Show (m (m (m a), s)),
+    MonadTransStack m (StateT s m)
   ) =>
   TestBatch
 rightmodulestate =
@@ -159,7 +161,8 @@
     EqProp (m (StateT s m a)),
     Show s,
     Arbitrary s,
-    EqProp (m (a, s))
+    EqProp (m (a, s)),
+    MonadTransStack m (StateT s m)
   ) =>
   TestBatch
 leftmodulestate =
@@ -185,7 +188,8 @@
     Show (m (Fun s (m (m a, s)))),
     Show s,
     Arbitrary s,
-    EqProp (m (a, s))
+    EqProp (m (a, s)),
+    MonadTransStack m (StateT s m)
   ) =>
   TestBatch
 bimodulestate =
@@ -216,7 +220,8 @@
     Show (m (m (m a))),
     Show s,
     Arbitrary s,
-    EqProp (m a)
+    EqProp (m a),
+    MonadTransStack m (ReaderT s m)
   ) =>
   TestBatch
 rightmodulereader =