diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Revision history for monad-actions
 
+## 1.0.0.0 -- 2026-01-27
+
+* For any monad m, m acts on every transformer stack whose base is m.
+* Known bugs: Still requires overlapping and incoherent instances.
+
 ## 0.1.0.0 -- 2026-01-22
 
 * First version. Released on an unsuspecting world.
diff --git a/monad-actions.cabal b/monad-actions.cabal
--- a/monad-actions.cabal
+++ b/monad-actions.cabal
@@ -8,10 +8,10 @@
 --       +-+------- breaking API changes
 --       | | +----- non-breaking API additions
 --       | | | +--- code changes with no API change
-version: 0.1.0.0
+version: 1.0.0.0
 synopsis: Left or right actions of a monad on a functor
 description:
-  This package defines classes for left and rght actions of
+  This package defines classes for left and right actions of
   monads on functors.  It also includes modules for using
   monad actions with qualified do notation.
 
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,9 +1,12 @@
+{-# 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\) such that
---     the following two laws hold:
+--     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:
 --
 --     * \(\nu \cdot (\eta \circ F) = \mathrm{id}_F\)
 --     * \(\nu \cdot (\mu \circ F) = \nu \cdot (M \circ \nu)\)
@@ -24,9 +27,7 @@
   ( LeftModule (..),
     RightModule (..),
     BiModule (..),
-    monadTransLScale,
-    monadTransRScale,
-    monadTransBiScale,
+    LiftStack (..),
   )
 where
 
@@ -34,9 +35,12 @@
 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
 import Control.Monad.Identity (Identity (..))
-import Control.Monad.Morph
+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 ()
@@ -44,16 +48,19 @@
 import Control.Monad.Trans.Free ()
 import Control.Monad.Trans.Iter ()
 import Control.Monad.Trans.Maybe (MaybeT (..))
-import Control.Monad.Trans.Reader ()
+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.Writer.Class (MonadWriter (..))
 import Data.Functor.Compose (Compose (..))
 import Data.List.NonEmpty qualified as NE (NonEmpty, toList)
 import Data.Maybe (catMaybes, mapMaybe)
+import Data.Tuple (swap)
 
 -- | Instances must satisfy the following laws:
 --
@@ -96,23 +103,29 @@
     f a
   bijoin = rjoin . ljoin
 
--- | Default left scalar multiplication for monad transformers.
---
---   @'MonadTrans'@ instances are required to satisfy these laws, which state that @'lift'@ is a monad homomorphism:
+-- | 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:
 --
---   * @'lift' '.' 'pure' = 'pure'@
+--   * @'Control.Monad.Trans.Class.lift' '.' 'pure' = 'pure'@
 --
---   * @'lift' (m '>>=' f) = 'lift' m '>>=' ('lift' '.' f)@
+--   * @'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'@:
 --
---   * @'lift' '.' 'join' = 'join' '.' 'fmap' 'lift' '.' 'lift'@
+--   * @'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 @'lift'@.
---   The @'MonadTrans'@ laws as string diagrams are:
+--   @'join'@ depending on the number of inputs, and @┈┈┈►───@ represents @'liftStack'@.
+--   The @'LiftStack'@ laws as string diagrams are:
 --
 --   > ├┈┈┈►───  = ├──────
 --
@@ -135,7 +148,7 @@
 --   In other words,
 --
 --   @   'ljoin' '.' 'pure'
---   = 'join' '.' 'lift' '.' 'pure'
+--   = 'join' '.' 'liftStack' '.' 'pure'
 --   = 'join' '.' 'pure'
 --   = 'id'@
 --
@@ -150,19 +163,14 @@
 --   In other words,
 --
 --   @  'ljoin' '.' 'join'
---   = 'join' '.' 'lift' '.' 'join'
---   = 'join' '.' 'join' '.' 'fmap' 'lift' '.' 'lift'
---   = 'join' '.' 'fmap' 'join' '.' 'fmap' 'lift' '.' 'lift'
---   = 'join' '.' 'fmap' ('join' '.' 'lift') '.' 'lift'
---   = 'join' '.' 'lift' '.' 'fmap' ('join' '.' 'lift')
+--   = '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'@
-monadTransLScale :: (Monad m, MonadTrans t, Monad (t m)) => m (t m a) -> t m a
-monadTransLScale = join . lift
-
--- | Default right scalar multiplication for monad transformers.
 --
---   We prove the right module laws using string diagrams, just as in the case
---   of the left module laws.
+--   We can prove the right module laws using string diagrams in the same way.
 --
 --   The diagram for @'rjoin'@ is:
 --
@@ -179,9 +187,9 @@
 --   In other words,
 --
 --   @   'rjoin' '.' 'fmap' 'pure'
---   = 'join' '.' 'fmap' 'lift' , 'pure'
---   = 'join' '.' 'fmap' 'lift' , 'fmap' 'pure'
---   = 'join' '.' 'fmap' ('lift' , 'pure')
+--   = 'join' '.' 'fmap' 'liftStack' , 'pure'
+--   = 'join' '.' 'fmap' 'liftStack' , 'fmap' 'pure'
+--   = 'join' '.' 'fmap' ('liftStack' , 'pure')
 --   = 'join' '.' 'fmap' 'pure'
 --   = 'id'@
 --
@@ -196,20 +204,15 @@
 --   In other words,
 --
 --   @  'rjoin' '.' 'fmap' 'join'
---   = 'join' '.' 'fmap' 'lift' '.' 'fmap' 'join'
---   = 'join' '.' 'fmap' ('lift' '.' 'join')
---   = 'join' '.' 'fmap' ('join' '.' 'fmap' 'lift' '.' 'lift')
---   = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'lift' '.' 'lift')
---   = 'join' '.' 'join' '.' 'fmap' ('fmap' 'lift') '.' 'fmap' ('lift')
---   = 'join' '.' 'fmap' 'lift' '.' 'join' '.' 'fmap' 'lift'
+--   = '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'@
-monadTransRScale :: (Monad m, MonadTrans t, Monad (t m)) => t m (m a) -> t m a
-monadTransRScale = (lift =<<)
-
--- | Default two-sided scalar multiplication for monad transformers.
 --
---   We prove the bimodule law using string diagrams, just as in the case
---   of the left and right module laws:
+--   The bimodule law can be proved as follows:
 --
 --   > ┈┈┈►─┐             ┈┈►─┐
 --   >      ├───┐             ├───┐          ┈┈┈┈┈┈►─┐
@@ -220,25 +223,29 @@
 --   In other words,
 --
 --   @  'bijoin'
---   = 'join' '.' 'join' '.' 'lift' '.' 'fmap' ('fmap' 'lift')
---   = 'join' '.' 'fmap' 'lift' '.' 'join' '.' 'lift'
+--   = 'join' '.' 'join' '.' 'liftStack' '.' 'fmap' ('fmap' 'liftStack')
+--   = 'join' '.' 'fmap' 'liftStack' '.' 'join' '.' 'liftStack'
 --   = 'rjoin' '.' 'ljoin'
---   = 'join' '.' 'fmap' 'lift' '.' 'join' '.' 'lift'
---   = 'join' '.' 'fmap' 'join' '.' 'fmap' ('fmap' 'lift') '.' 'lift'
---   = 'join' '.' 'fmap' ('join' '.' 'fmap' 'lift') '.' 'lift'
---   = 'join' '.' 'fmap' 'rjoin' '.' 'lift'
---   = 'join' '.' 'lift' '.' 'fmap' 'rjoin'
+--   = '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'@
-monadTransBiScale :: (Monad m, MonadTrans t, Monad (t m)) => m (t m (m a)) -> t m a
-monadTransBiScale = join . join . lift . fmap (fmap lift)
+class LiftStack m n where
+  liftStack :: forall a. m a -> n a
 
-$mkMonadTransModuleInstances
+$mkLiftStackInstances
 
-instance {-# OVERLAPPING #-} (Monad m) => LeftModule m m where ljoin = join; lbind = (>>=)
+instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => LeftModule m n where
+  ljoin = join . liftStack
+  lbind = (>>=) . liftStack
 
-instance {-# OVERLAPPING #-} (Monad m) => RightModule m m where rjoin = join; rbind = (>>=)
+instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => RightModule m n where
+  rjoin = (liftStack =<<)
+  rbind = flip $ (=<<) . (liftStack .)
 
-instance {-# OVERLAPPING #-} (Monad m) => BiModule m m m
+instance {-# OVERLAPS #-} (Monad n, Monad m, LiftStack m n) => BiModule m m n
 
 instance {-# INCOHERENT #-} (Functor f) => LeftModule Identity f where ljoin = runIdentity
 
@@ -246,21 +253,21 @@
 
 instance {-# INCOHERENT #-} (Functor f) => BiModule Identity Identity f
 
-instance RightModule Maybe [] where rjoin = catMaybes; rbind = flip mapMaybe
+instance {-# INCOHERENT #-} RightModule Maybe [] where rjoin = catMaybes; rbind = flip mapMaybe
 
-instance LeftModule Maybe [] where ljoin = concat; lbind = flip concatMap
+instance {-# INCOHERENT #-} LeftModule Maybe [] where ljoin = concat; lbind = flip concatMap
 
-instance LeftModule NE.NonEmpty [] where ljoin = concat; lbind = flip concatMap
+instance {-# INCOHERENT #-} LeftModule NE.NonEmpty [] where ljoin = concat; lbind = flip concatMap
 
-instance RightModule NE.NonEmpty [] where rjoin = (>>= NE.toList)
+instance {-# INCOHERENT #-} RightModule NE.NonEmpty [] where rjoin = (>>= NE.toList)
 
-instance BiModule Maybe Maybe []
+instance {-# INCOHERENT #-} BiModule Maybe Maybe []
 
-instance BiModule Maybe [] []
+instance {-# INCOHERENT #-} BiModule Maybe [] []
 
 instance BiModule [] Maybe []
 
-instance BiModule NE.NonEmpty NE.NonEmpty []
+instance {-# INCOHERENT #-} BiModule NE.NonEmpty NE.NonEmpty []
 
 instance BiModule [] NE.NonEmpty []
 
@@ -270,11 +277,11 @@
 
 instance BiModule NE.NonEmpty Maybe []
 
-instance RightModule (Either e) Maybe where
+instance {-# INCOHERENT #-} RightModule (Either e) Maybe where
   rjoin (Just (Right x)) = Just x
   rjoin _ = Nothing
 
-instance LeftModule (Either e) Maybe where
+instance {-# INCOHERENT #-} LeftModule (Either e) Maybe where
   ljoin (Right (Just x)) = Just x
   ljoin _ = Nothing
 
@@ -312,12 +319,6 @@
 instance {-# INCOHERENT #-} (Monoid e, Monad m) => RightModule Maybe (ExceptT e m) where
   rjoin = ExceptT . fmap (maybe (Left mempty) Right =<<) . runExceptT
 
-instance {-# INCOHERENT #-} (Monad m) => LeftModule (Either e) (ExceptT e m) where
-  ljoin = join . ExceptT . pure
-
-instance {-# INCOHERENT #-} (Monoid e, Monad m) => RightModule (Either e) (ExceptT e m) where
-  rjoin = ExceptT . fmap join . runExceptT
-
 instance {-# INCOHERENT #-} (Monad m) => BiModule Maybe Maybe (MaybeT m)
 
 instance {-# INCOHERENT #-} (Monad m) => BiModule (Either e) Maybe (MaybeT m)
@@ -332,28 +333,103 @@
 
 instance {-# INCOHERENT #-} (Monoid e, Monad m) => BiModule Maybe (Either e) (ExceptT e m)
 
-instance {-# INCOHERENT #-} (Monoid e, Monad m) => BiModule (Either e) (Either e) (ExceptT e m)
-
 -- | @'liftIO'@ is a monad homomorphism, so the proof that every monad with a lawful @'MonadIO'@
 --   instance is a {left,right,bi} module over @'IO'@ is the same as the proof for monad transformers.
 instance {-# INCOHERENT #-} (MonadIO m) => LeftModule IO m where
   ljoin = join . liftIO
+  a `lbind` f = liftIO a >>= f
 
 instance {-# INCOHERENT #-} (MonadIO m) => RightModule IO m where
   rjoin = (>>= liftIO)
+  a `rbind` f = a >>= liftIO . f
 
 instance {-# INCOHERENT #-} (MonadIO m) => BiModule IO IO m
 
--- | Proof that @f@ is always a left module over @'Codensity' f@:
---   - @   'ljoin' ('join' m)
---       = 'ljoin' ('Codensity' (\c -> 'runCodensity' m (\a -> 'runCodensity' a c)))
---       = (\c -> 'runCodensity' m (\a -> 'runCodensity' a c)) id
---       = 'runCodensity' m (\a -> 'runCodensity' a 'id')
---       = 'runCodensity' m 'ljoin' 'runCodensity' m (\x -> 'ljoin' x)
---       = (\k -> 'runCodensity' m (\x -> k ('ljoin' x))) 'id'
---       = 'ljoin' (Codensity (\k -> 'runCodensity' m (\x -> k ('ljoin' x))))
+-- | No laws are given in the documentation for @'MonadError'@, but we assume
+--   @'liftEither'@ is a monad homomorphism.
+instance {-# INCOHERENT #-} (MonadError e m) => LeftModule (Either e) m where
+  ljoin = join . liftEither
+  a `lbind` f = liftEither a >>= f
+
+instance {-# INCOHERENT #-} (MonadError e m) => RightModule (Either e) m where
+  rjoin = (>>= liftEither)
+  a `rbind` f = a >>= liftEither . f
+
+instance {-# INCOHERENT #-} (MonadError e m) => BiModule (Either e) (Either e) m
+
+-- | For every @'MonadReader'@ instance defined in "Control.Monad.Reader.Class", @'reader'@ is a monad homomorphism.
+instance {-# INCOHERENT #-} (MonadReader r m) => LeftModule ((->) r) m where
+  ljoin = join . reader
+  a `lbind` f = reader a >>= f
+
+instance {-# INCOHERENT #-} (MonadReader r m) => RightModule ((->) r) m where
+  rjoin = (>>= reader)
+  a `rbind` f = a >>= reader . f
+
+instance {-# INCOHERENT #-} (MonadReader r m) => BiModule ((->) r) ((->) r) m
+
+instance {-# INCOHERENT #-} (MonadReader r m) => LeftModule (Reader r) m where
+  ljoin = join . reader . runReader
+  a `lbind` f = reader (runReader a) >>= f
+
+instance {-# INCOHERENT #-} (MonadReader r m) => RightModule (Reader r) m where
+  rjoin = (>>= reader . runReader)
+  a `rbind` f = a >>= reader . runReader . f
+
+instance {-# INCOHERENT #-} (MonadReader r m) => BiModule (Reader r) (Reader r) m
+
+instance {-# INCOHERENT #-} (MonadReader r m) => BiModule ((->) r) (Reader r) m
+
+instance {-# INCOHERENT #-} (MonadReader r m) => BiModule (Reader r) ((->) r) m
+
+-- | For every @'MonadWriter'@ instance defined in "Control.Monad.Writer.Class", @'writer'@ is a monad homomorphism.
+instance {-# INCOHERENT #-} (MonadWriter w m) => LeftModule ((,) w) m where
+  ljoin = join . writer . swap
+  a `lbind` f = writer (swap a) >>= f
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => RightModule ((,) w) m where
+  rjoin = (>>= writer . swap)
+  a `rbind` f = a >>= writer . swap . f
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => BiModule ((,) w) ((,) w) m
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => LeftModule (Writer w) m where
+  ljoin = join . writer . runWriter
+  a `lbind` f = writer (runWriter a) >>= f
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => RightModule (Writer w) m where
+  rjoin = (>>= writer . runWriter)
+  a `rbind` f = a >>= writer . runWriter . f
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => BiModule (Writer w) (Writer w) m
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => BiModule ((,) w) (Writer w) m
+
+instance {-# INCOHERENT #-} (MonadWriter w m) => BiModule (Writer w) ((,) w) m
+
+-- | For every @'MonadState'@ instance defined in "Control.Monad.State.Class", @'state'@ is a monad homomorphism.
+instance {-# INCOHERENT #-} (MonadState s m) => LeftModule (State s) m where
+  ljoin = join . state . runState
+  a `lbind` f = state (runState a) >>= f
+
+instance {-# INCOHERENT #-} (MonadState s m) => RightModule (State s) m where
+  rjoin = (>>= (state . runState))
+  a `rbind` f = a >>= state . runState . f
+
+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
+--       = 'runCodensity' m (\\a -> 'runCodensity' a 'id')
+--       = 'runCodensity' m 'ljoin' 'runCodensity' m (\\x -> 'ljoin' x)
+--       = (\\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@
+-- 
+--   * @'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
   a `lbind` f = runCodensity (f <$> a) id
diff --git a/src/Control/Monad/Action/Left.hs b/src/Control/Monad/Action/Left.hs
--- a/src/Control/Monad/Action/Left.hs
+++ b/src/Control/Monad/Action/Left.hs
@@ -1,48 +1,82 @@
--- | This module should be imported qualified, and can be used with the @QualifiedDo@ extension.
-module Control.Monad.Action.Left ((>>=), (>>), (=<<), (>=>), (<=<), (<*>), fmap, pure, return, fail, join) where
+-- | Operators for left monad actions.
+--   This module should be imported qualified, and can be used with the @QualifiedDo@ extension.
+module Control.Monad.Action.Left
+  ( (>>=),
+    (>>),
+    (=<<),
+    (>=>),
+    (<=<),
+    (<*>),
+    fmap,
+    pure,
+    return,
+    fail,
+    join,
+    mfix,
+  )
+where
 
 import Control.Monad.Action
-import Prelude hiding (fmap, pure, return, (<*>), (=<<), (>>), (>>=))
+import Control.Monad.Fix qualified as F
+import Prelude hiding (fail, fmap, pure, return, (<*>), (=<<), (>>), (>>=))
 import Prelude qualified as P
 
 infixl 1 >>=
 
+-- | @'lbind'@ in operator form.
 (>>=) :: (LeftModule m f) => m a -> (a -> f b) -> f b
 (>>=) = lbind
 
 infixr 1 =<<
 
+-- | @'lbind'@ with arguments swapped.
 (=<<) :: (LeftModule m f) => (a -> f b) -> m a -> f b
 (=<<) = flip lbind
 
 infixl 1 >>
 
+-- | Sequencing operator induced by a left monad action.
 (>>) :: (LeftModule m f) => m a -> f b -> f b
 (>>) = (. const) . lbind
 
 infixr 1 >=>
 
+-- | Left to right Kleisli arrow scalar multiplication induced by a left monad action.
 (>=>) :: (LeftModule m f) => (a -> m b) -> (b -> f c) -> a -> f c
 (>=>) = flip $ (.) . (=<<)
 
 infixr 1 <=<
 
+-- | Right to left Kleisli arrow scalar multiplication induced by a left monad action.
 (<=<) :: (LeftModule m f) => (b -> f c) -> (a -> m b) -> a -> f c
 (<=<) = (.) . (=<<)
 
+-- | Alias for @'ljoin'@.
+join :: (LeftModule m f) => m (f a) -> f a
+join = ljoin
+
+-- | Re-export from "Prelude".
 fmap :: (Functor f) => (a -> b) -> f a -> f b
 fmap = P.fmap
 
+-- | Re-export from "Prelude".
 pure :: (Applicative f) => a -> f a
 pure = P.pure
 
+-- | Re-export from "Prelude".
+fail :: (MonadFail m) => String -> m a
+fail = P.fail
+
+-- | Re-export from "Control.Monad.Fix".
+mfix :: (F.MonadFix m) => (a -> m a) -> m a
+mfix = F.mfix
+
+-- | Alias for @'pure'@.
 return :: (Applicative f) => a -> f a
 return = pure
 
-join :: (LeftModule m f) => m (f a) -> f a
-join = ljoin
-
 infixl 4 <*>
 
+-- | Used for desugaring qualified @do@ blocks when @ApplicativeDo@ is enabled.
 (<*>) :: (LeftModule m f) => m (a -> b) -> f a -> f b
 fs <*> xs = fs >>= flip fmap xs
diff --git a/src/Control/Monad/Action/Right.hs b/src/Control/Monad/Action/Right.hs
--- a/src/Control/Monad/Action/Right.hs
+++ b/src/Control/Monad/Action/Right.hs
@@ -1,48 +1,84 @@
--- | This module should be imported qualified, and can be used with the @QualifiedDo@ extension.
-module Control.Monad.Action.Right ((>>=), (>>), (=<<), (>=>), (<=<), (<*>), fmap, pure, return, fail, join) where
+{-# LANGUAGE MonoLocalBinds #-}
 
+-- | Operators for right monad actions.
+--   This module should be imported qualified, and can be used with the @QualifiedDo@ extension.
+module Control.Monad.Action.Right
+  ( (>>=),
+    (>>),
+    (=<<),
+    (>=>),
+    (<=<),
+    (<*>),
+    fmap,
+    pure,
+    return,
+    fail,
+    join,
+    mfix,
+  )
+where
+
 import Control.Monad.Action
-import Prelude hiding (fmap, pure, return, (<*>), (=<<), (>>), (>>=))
+import Control.Monad.Fix qualified as F
+import Prelude hiding (fail, fmap, pure, return, (<*>), (=<<), (>>), (>>=))
 import Prelude qualified as P
 
 infixl 1 >>=
 
+-- | @'rbind'@ in operator form.
 (>>=) :: (RightModule m f) => f a -> (a -> m b) -> f b
 (>>=) = rbind
 
 infixr 1 =<<
 
+-- | @'rbind'@ with arguments swapped.
 (=<<) :: (RightModule m f) => (a -> m b) -> f a -> f b
 (=<<) = flip rbind
 
 infixl 1 >>
 
+-- | Sequencing operator induced by a right monad action.
 (>>) :: (RightModule m f) => f a -> m b -> f b
 (>>) = (. const) . rbind
 
 infixr 1 >=>
 
+-- | Left to right Kleisli arrow scalar multiplication induced by a right monad action.
 (>=>) :: (RightModule m f) => (a -> f b) -> (b -> m c) -> a -> f c
 (>=>) = flip $ (.) . (=<<)
 
 infixr 1 <=<
 
+-- | Right to left Kleisli arrow scalar multiplication induced by a right monad action.
 (<=<) :: (RightModule m f) => (b -> m c) -> (a -> f b) -> a -> f c
 (<=<) = (.) . (=<<)
 
+-- | Alias for @'rjoin'@.
+join :: (RightModule m f) => f (m a) -> f a
+join = rjoin
+
+-- | Re-export from "Prelude".
 fmap :: (Functor f) => (a -> b) -> f a -> f b
 fmap = P.fmap
 
+-- | Re-export from "Prelude".
 pure :: (Applicative f) => a -> f a
 pure = P.pure
 
+-- | Re-export from "Prelude".
+fail :: (MonadFail m) => String -> m a
+fail = P.fail
+
+-- | Re-export from "Control.Monad.Fix".
+mfix :: (F.MonadFix m) => (a -> m a) -> m a
+mfix = F.mfix
+
+-- | Alias for @'pure'@.
 return :: (Applicative f) => a -> f a
 return = pure
 
-join :: (RightModule m f) => f (m a) -> f a
-join = rjoin
-
 infixl 4 <*>
 
+-- | Used for desugaring qualified @do@ blocks when @ApplicativeDo@ is enabled.
 (<*>) :: (RightModule m f) => f (a -> b) -> m a -> f b
 fs <*> xs = fs >>= 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,61 +1,53 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TemplateHaskellQuotes #-}
 
-module Control.Monad.Action.TH (mkMonadTransModuleInstances) where
+module Control.Monad.Action.TH (mkLiftStackInstances) where
 
-import Control.Monad
 import Control.Monad.Trans
 import Language.Haskell.TH
 
-uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
-uncurry3 f (a, b, c) = f a b c
+infixl 5 #
 
-mkMonadTransModuleInstances :: Q [Dec]
-mkMonadTransModuleInstances =
+(#) :: Type -> Type -> Type
+(#) = AppT
+
+mkLiftStackInstances :: Q [Dec]
+mkLiftStackInstances =
   reify ''MonadTrans
     >>= \case
       ClassI _ instances ->
-        fmap join . forM instances $ \case
-          InstanceD _ ct (AppT (ConT _) ty) _ ->
-            do
-              m <- VarT <$> newName "m"
-              let ct' = ct ++ [AppT (ConT ''Monad) m]
-              let ctB =
-                    ct
-                      ++ [ AppT (ConT ''Monad) m,
-                           AppT (AppT (ConT $ mkName "LeftModule") m) (AppT ty m),
-                           AppT (AppT (ConT $ mkName "RightModule") m) (AppT ty m)
-                         ]
-              let tyL = AppT (AppT (ConT $ mkName "LeftModule") m) (AppT ty m)
-              let tyR = AppT (AppT (ConT $ mkName "RightModule") m) (AppT ty m)
-              let tyB = AppT (AppT (AppT (ConT $ mkName "BiModule") m) m) (AppT ty m)
-              pure $
-                fmap
-                  (uncurry3 $ InstanceD (Just Overlaps))
-                  [ ( ct',
-                      tyL,
-                      [ ValD
-                          (VarP $ mkName "ljoin")
-                          (NormalB (VarE $ mkName "monadTransLScale"))
-                          []
-                      ]
-                    ),
-                    ( ct',
-                      tyR,
-                      [ ValD
-                          (VarP $ mkName "rjoin")
-                          (NormalB (VarE $ mkName "monadTransRScale"))
-                          []
-                      ]
-                    ),
-                    ( ctB,
-                      tyB,
-                      [ ValD
-                          (VarP $ mkName "bijoin")
-                          (NormalB (VarE $ mkName "monadTransBiScale"))
-                          []
-                      ]
-                    )
-                  ]
-          _ -> fail "Not an instance"
+        do
+          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 =
+                instances >>= \case
+                  InstanceD _ ct (AppT (ConT _) t) _ ->
+                    -- instance (Monad m, Monad n, LiftStack m n) => LiftStack m (t n) where
+                    --   liftStack = lift . liftStack
+                    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))
+                        [ ValD
+                            (VarP $ mkName "liftStack")
+                            (NormalB $ UInfixE (VarE 'lift) (VarE '(.)) (VarE $ mkName "liftStack"))
+                            []
+                        ]
+                  _ -> []
+          pure $ baseInstance : inductiveInstances
       _ -> pure []
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE MonoLocalBinds #-}
 {-# LANGUAGE QualifiedDo #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -172,7 +173,7 @@
     assocP :: m (m (Fun s (m (a, s)))) -> Property
 
     leftP a = ljoin (pure @m (StateT . applyFun <$> a)) =-= (StateT . applyFun <$> a)
-    assocP a = ljoin (join (fmap (StateT . applyFun) <$> a)) =-= ljoin (fmap ljoin (fmap (StateT . applyFun) <$> a))
+    assocP a = ljoin (a >>= fmap (StateT . applyFun)) =-= ljoin (fmap ljoin (fmap (StateT . applyFun) <$> a))
 
 bimodulestate ::
   forall m s a.
@@ -303,10 +304,13 @@
                   -- , bimodule @[] @Maybe @[] @Int
                   -- , bimodule @[] @[] @[] @Int
                   leftmodule @Maybe @(MaybeT Maybe) @Int,
-                  -- leftmodule @[] @(MaybeT (MaybeT [])) @Int, -- this would require undecidable instances
+                  leftmodule @[] @(MaybeT (MaybeT [])) @Int,
                   leftmodule @(Either String) @(MaybeT (ExceptT String [])) @Int,
                   leftmodule @Identity @Identity @Int,
                   leftmodule @Maybe @(FreeT Maybe Maybe) @Int,
+                  leftmodule @((,) (Sum Int)) @(MaybeT (WriterT (Sum Int) Maybe)) @Int,
+                  rightmodule @((,) (Sum Int)) @(MaybeT (WriterT (Sum Int) Maybe)) @Int,
+                  bimodule @((,) (Sum Int)) @((,) (Sum Int)) @(MaybeT (WriterT (Sum Int) Maybe)) @Int,
                   rightmodulestate @(WriterT (Product Int) (Either Double)) @Int @Char
                   -- , rightmodulereader @(WriterT (Product Int) (Either Double)) @Int @Char
                   -- , rightmodulereader @(Either Bool) @Char @Int