diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,20 @@
 # Changelog for `cleff`
 
-## 0.1.0.0
+## 0.2.0.0 (2022-02-06)
+
+### Changed
+
+- **[BREAKING]** Changed parameter order of `Handling` class from `e es esSend` to `esSend e es`
+- **[BREAKING]** Relaxed fundep of `Handling` to `esSend -> e es` (HO combinators may require `TypeApplication` more often)
+- Moved `Data.*` modules to `Cleff.Internal.*` so as not to pollute common namespaces
+
+### Added
+
+- `Trustworthy` flags for non-internal modules
+- `sendVia` for sending an effect operation along a transformation between effect stacks
+- `raiseUnder`, `raiseNUnder`, `raiseUnderN`, `raiseNUnderN` for introducing effects under other effects in the effect stack
+- `runWriterBatch` as a more efficient `Writer` interpreter that writes `listen`ed values in batch instead of in real time
+
+## 0.1.0.0 (2022-01-31)
 
 - Initial API
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -7,11 +7,11 @@
 
 ## Overview
 
-Different from [many](`polysemy`) [previous](`fused-effects`) [libraries](`freer-simple`), `cleff` does not use techniques like Freer monads or monad transformers. Instead, the `Eff` monad is esentially a `ReaderT IO`, which provides predictable semantics and reliable performance. The only caveat is that `cleff` does not support nondeterminism and continuations in the `Eff` monad - but after all, [most effects libraries has broken nondeterminism support](https://github.com/polysemy-research/polysemy/issues/246), and we encourage users to wrap another monad transformer with support of nondeterminism (e.g. `ListT`) over the main `Eff` monad in such cases.
+Different from [many](`polysemy`) [previous](`fused-effects`) [libraries](`freer-simple`), `cleff` does not use techniques like Freer monads or monad transformers. Instead, the `Eff` monad is essentially a `ReaderT IO`, which provides predictable semantics and reliable performance. The only caveat is that `cleff` does not support nondeterminism and continuations in the `Eff` monad - but after all, [most effects libraries has broken nondeterminism support](https://github.com/polysemy-research/polysemy/issues/246), and we encourage users to wrap another monad transformer with support of nondeterminism (e.g. `ListT`) over the main `Eff` monad in such cases.
 
 ### Performance
 
-`cleff`'s `Eff` monad is esentially implemented as a `ReaderT IO`. This concrete formulation [allows more GHC optimizations to fire][alexis-talk], and brings lower performance overhead. This is first done by [`eff`], and then [`effectful`]; it proved to work, so we followed this path.
+`cleff`'s `Eff` monad is essentially implemented as a `ReaderT IO`. This concrete formulation [allows more GHC optimizations to fire][alexis-talk], and brings lower performance overhead. This is first done by [`eff`], and then [`effectful`]; it proved to work, so we followed this path.
 
 [In microbenchmarks](#benchmarks), `cleff` outperforms [`polysemy`], and is slightly behind [`effectful`]. However, note that `effectful` and `cleff` have very different design principles. While `effectful` prioritizes performance over anything else (by [providing static dispatch](https://github.com/arybczak/effectful/blob/master/effectful-core/src/Effectful/Reader/Static.hs)), `cleff` focuses on balancing expressivity and performance. If you would like minimal performance overhead, consider [`effectful`].
 
@@ -29,7 +29,7 @@
 
 ### Higher-order effects
 
-*Higher-order* effects are effects that take monadic computations. They are often useful in real world applications, as examples of higher-order effect operations include `local`, `catchError` and `mask`. Implementing higher-order effects is often tedious, or even not supported in some effect libraries. `polysemy` is the first library that aims to provide easy higher-order effects mechanicsm with its [`Tactics`](https://hackage.haskell.org/package/polysemy-1.7.1.0/docs/Polysemy.html#g:16) API. Following its path, `cleff` provides a set of combinators that can be used to implement higher-order effects. These combinators are as expressive as `polysemy`'s, and are also easier to use correctly.
+*Higher-order* effects are effects that take monadic computations. They are often useful in real world applications, as examples of higher-order effect operations include `local`, `catchError` and `mask`. Implementing higher-order effects is often tedious, or even not supported in some effect libraries. `polysemy` is the first library that aims to provide easy higher-order effects mechanism with its [`Tactics`](https://hackage.haskell.org/package/polysemy-1.7.1.0/docs/Polysemy.html#g:16) API. Following its path, `cleff` provides a set of combinators that can be used to implement higher-order effects. These combinators are as expressive as `polysemy`'s, and are also easier to use correctly.
 
 ## Example
 
@@ -91,7 +91,7 @@
 
 ## References
 
-These are the useful resourses that inspired this library's design and implementation.
+These are the useful resources that inspired this library's design and implementation.
 
 Papers:
 
diff --git a/cleff.cabal b/cleff.cabal
--- a/cleff.cabal
+++ b/cleff.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           cleff
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Fast and concise extensible effects
 description:    Please see the README on GitHub at <https://github.com/re-xyr/cleff#readme>
 category:       Control, Effect, Language
@@ -43,6 +43,7 @@
       Cleff.Fail
       Cleff.Fresh
       Cleff.Input
+      Cleff.Internal.Any
       Cleff.Internal.Base
       Cleff.Internal.Effect
       Cleff.Internal.Interpret
@@ -54,9 +55,6 @@
       Cleff.State
       Cleff.Trace
       Cleff.Writer
-      Data.Any
-      Data.Mem
-      Data.Rec
   other-modules:
       Paths_cleff
   hs-source-dirs:
@@ -99,6 +97,7 @@
     , microlens >=0.4.9 && <0.5
     , monad-control >=1 && <1.1
     , primitive >=0.6 && <0.8
+    , rec-smallarray ==0.1.*
     , template-haskell >=2.14 && <3
     , th-abstraction >=0.2.11 && <0.5
     , transformers >=0.5 && <0.7
@@ -159,6 +158,7 @@
     , microlens >=0.4.9 && <0.5
     , monad-control >=1 && <1.1
     , primitive >=0.6 && <0.8
+    , rec-smallarray ==0.1.*
     , template-haskell >=2.14 && <3
     , th-abstraction >=0.2.11 && <0.5
     , transformers >=0.5 && <0.7
@@ -177,7 +177,6 @@
       HigherOrderSpec
       InterposeSpec
       MaskSpec
-      RecSpec
       StateSpec
       ThSpec
       Paths_cleff
@@ -228,6 +227,7 @@
     , microlens >=0.4.9 && <0.5
     , monad-control >=1 && <1.1
     , primitive >=0.6 && <0.8
+    , rec-smallarray ==0.1.*
     , template-haskell >=2.14 && <3
     , th-abstraction >=0.2.11 && <0.5
     , transformers >=0.5 && <0.7
diff --git a/src/Cleff.hs b/src/Cleff.hs
--- a/src/Cleff.hs
+++ b/src/Cleff.hs
@@ -1,4 +1,12 @@
--- | This library implements an /extensible effects system/, where sets of monadic actions ("effects") are encoded as
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
+--
+-- This library implements an /extensible effects system/, where sets of monadic actions ("effects") are encoded as
 -- datatypes, tracked at the type level and can have multiple different implementations. This means you can swap out
 -- implementations of certain monadic actions in mock tests or in different environments. The notion of "effect" is
 -- general here: it can be an 'IO'-performing side effect, or just obtaining the value of a static global environment.
@@ -26,7 +34,7 @@
     runPure, runIOE
   , -- * Defining effects
     -- $definingEffects
-    send, makeEffect, makeEffect_
+    send, sendVia, makeEffect, makeEffect_
   , -- * Trivial effects handling
     raise, raiseN, inject, subsume, subsumeN, KnownList, Subset
   , -- * Interpreting effects
@@ -36,6 +44,8 @@
     HandlerIO, interpretIO
   , -- ** Translating effects
     Translator, transform, translate
+  , -- ** Transforming interpreters
+    raiseUnder, raiseNUnder, raiseUnderN, raiseNUnderN
   , -- * Combinators for interpreting higher order effects
     -- $higherOrderEffects
     Handling, toEff, toEffWith, withFromEff
diff --git a/src/Cleff/Error.hs b/src/Cleff/Error.hs
--- a/src/Cleff/Error.hs
+++ b/src/Cleff/Error.hs
@@ -1,4 +1,11 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE Trustworthy         #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Error
   ( -- * Effect
     Error (..)
@@ -10,9 +17,9 @@
   ) where
 
 import           Cleff
+import           Cleff.Internal.Any
 import           Cleff.Internal.Base
 import           Control.Exception   (Exception)
-import           Data.Any            (Any, fromAny, toAny)
 import           Data.Bool           (bool)
 import           Data.Unique         (Unique, hashUnique, newUnique)
 import qualified UnliftIO.Exception  as Exc
@@ -94,7 +101,7 @@
 instance Show ErrorExc where
   showsPrec _ (ErrorExc uid _) =
     ("Cleff.Error.runError: Escaped error (error UID hash: " <>) . shows (hashUnique uid) . ("). This is possibly due \
-    \to trying to 'throwError' in a forked thread, or trying to 'wait' on an error-throwing \'Async' computation out \
+    \to trying to 'throwError' in a forked thread, or trying to 'wait' on an error-throwing 'Async' computation out \
     \of the effect scope where it is created. Refer to the haddock of 'runError' for details on the caveats. If all \
     \those shenanigans mentioned or other similar ones seem unlikely, please report this as a bug." <>)
 
@@ -114,7 +121,7 @@
 
 -- | Run an 'Error' effect.
 --
--- __Caveat__: 'runError' is implemented with 'Exc.Exception's therefore inherits some of its unexpected behavoirs.
+-- __Caveat__: 'runError' is implemented with 'Exc.Exception's therefore inherits some of its unexpected behaviors.
 -- Errors thrown in forked threads will /not/ be directly caught by 'catchError's in the parent thread. Instead it will
 -- incur an exception, and we won't be quite able to display the details of that exception properly at that point.
 -- Therefore please properly handle the errors in the forked threads separately.
diff --git a/src/Cleff/Fail.hs b/src/Cleff/Fail.hs
--- a/src/Cleff/Fail.hs
+++ b/src/Cleff/Fail.hs
@@ -1,5 +1,11 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE Trustworthy #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Fail
   ( -- * Effect
     Fail (..)
diff --git a/src/Cleff/Fresh.hs b/src/Cleff/Fresh.hs
--- a/src/Cleff/Fresh.hs
+++ b/src/Cleff/Fresh.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Fresh
   ( -- * Effect
     Fresh (..)
diff --git a/src/Cleff/Input.hs b/src/Cleff/Input.hs
--- a/src/Cleff/Input.hs
+++ b/src/Cleff/Input.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Input
   ( -- * Effect
     Input (..)
diff --git a/src/Cleff/Internal/Any.hs b/src/Cleff/Internal/Any.hs
new file mode 100644
--- /dev/null
+++ b/src/Cleff/Internal/Any.hs
@@ -0,0 +1,26 @@
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- This module contains utility functions for 'Any'.
+--
+-- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
+-- extra careful if you're to depend on this module.
+module Cleff.Internal.Any (Any, fromAny, toAny) where
+
+import           GHC.Exts      (Any)
+import           Unsafe.Coerce (unsafeCoerce)
+
+-- | Coerce any boxed value into 'Any'.
+toAny :: a -> Any
+toAny = unsafeCoerce
+{-# INLINE toAny #-}
+
+-- | Coerce 'Any' to a boxed value. This is /generally unsafe/ and it is your responsibility to ensure that the type
+-- you're coercing into is the original type that the 'Any' is coerced from.
+fromAny :: Any -> a
+fromAny = unsafeCoerce
+{-# INLINE fromAny #-}
diff --git a/src/Cleff/Internal/Base.hs b/src/Cleff/Internal/Base.hs
--- a/src/Cleff/Internal/Base.hs
+++ b/src/Cleff/Internal/Base.hs
@@ -1,7 +1,14 @@
 {-# LANGUAGE CPP #-}
 {-# OPTIONS_HADDOCK not-home #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
--- | This module contains the 'IOE' effect together with a few primitives for using it, as well as interpretation
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- This module contains the 'IOE' effect together with a few primitives for using it, as well as interpretation
 -- combinators for 'IO'-related effects. It is not usually needed because safe functionalities are re-exported in the
 -- "Cleff" module.
 --
@@ -29,7 +36,6 @@
 import qualified Control.Monad.Catch         as Catch
 import           Control.Monad.Primitive     (PrimMonad (PrimState, primitive), RealWorld)
 import           Control.Monad.Trans.Control (MonadBaseControl (StM, liftBaseWith, restoreM))
-import qualified Data.Mem                    as Mem
 import           GHC.IO                      (IO (IO))
 import           System.IO.Unsafe            (unsafeDupablePerformIO)
 import           UnliftIO                    (MonadIO (liftIO), MonadUnliftIO (withRunInIO), throwIO)
@@ -139,7 +145,7 @@
 
 -- | Extract the 'IO' computation out of an 'Eff' given no effect remains on the stack.
 runEff :: Eff '[] a -> IO a
-runEff m = unEff m Mem.empty
+runEff m = unEff m emptyEnv
 {-# INLINE runEff #-}
 
 -- | Unwrap an 'Eff' computation with side effects into an 'IO' computation, given that all effects other than 'IOE' are
@@ -157,7 +163,7 @@
 
 -- | The type of an /'IO' effect handler/, which is a function that transforms an effect @e@ into 'IO' computations.
 -- This is used for 'interpretIO'.
-type HandlerIO e es = ∀ esSend. (Handling e es esSend) => e (Eff esSend) ~> IO
+type HandlerIO e es = ∀ esSend. Handling esSend e es => e (Eff esSend) ~> IO
 
 -- | Interpret an effect in terms of 'IO', by transforming an effect into 'IO' computations.
 --
@@ -172,10 +178,10 @@
 
 -- | Temporarily gain the ability to unlift an @'Eff' esSend@ computation into 'IO'. This is useful for dealing with
 -- higher-order effects that involves 'IO'.
-withToIO :: (Handling e es esSend, IOE :> es) => ((Eff esSend ~> IO) -> IO a) -> Eff es a
-withToIO f = Eff \es -> f \m -> unEff m (Mem.update es sendEnv)
+withToIO :: (Handling esSend e es, IOE :> es) => ((Eff esSend ~> IO) -> IO a) -> Eff es a
+withToIO f = Eff \es -> f \m -> unEff m (updateEnv es esSend)
 
 -- | Lift an 'IO' computation into @'Eff' esSend@. This is useful for dealing with effect operations with the monad type in
 -- the negative position within 'Cleff.IOE', like 'UnliftIO.mask'ing.
-fromIO :: (Handling e es esSend, IOE :> es) => IO ~> Eff esSend
+fromIO :: (Handling esSend e es, IOE :> es) => IO ~> Eff esSend
 fromIO = Eff . const
diff --git a/src/Cleff/Internal/Effect.hs b/src/Cleff/Internal/Effect.hs
--- a/src/Cleff/Internal/Effect.hs
+++ b/src/Cleff/Internal/Effect.hs
@@ -1,13 +1,20 @@
 {-# OPTIONS_HADDOCK not-home #-}
--- | This module contains definitions of some basic types related to effects. You won't need this module directly;
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- This module contains definitions of some basic types related to effects. You won't need this module directly;
 -- these functionalities are reexported in the "Cleff" module.
 --
 -- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
 -- extra careful if you're to depend on this module.
 module Cleff.Internal.Effect (Effect, (:>), (:>>), type (++), type (~>)) where
 
-import           Data.Kind (Constraint, Type)
-import           Data.Rec  (Elem, type (++), type (~>))
+import           Data.Kind           (Constraint, Type)
+import           Data.Rec.SmallArray (Elem, type (++), type (~>))
 
 -- | The type of effects. An effect @e m a@ takes an effect monad type @m :: 'Type' -> 'Type'@ and a result type
 -- @a :: 'Type'@.
diff --git a/src/Cleff/Internal/Interpret.hs b/src/Cleff/Internal/Interpret.hs
--- a/src/Cleff/Internal/Interpret.hs
+++ b/src/Cleff/Internal/Interpret.hs
@@ -1,16 +1,23 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE UnboxedTuples       #-}
 {-# OPTIONS_HADDOCK not-home #-}
--- | This module contains functions for interpreting effects. Most of the times you won't need to import this directly;
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- This module contains functions for interpreting effects. Most of the times you won't need to import this directly;
 -- the module "Cleff" reexports most of the functionalities.
 --
 -- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
 -- extra careful if you're to depend on this module.
 module Cleff.Internal.Interpret
   ( -- * Trivial handling
-    raise, raiseN, inject, subsume, subsumeN
+    adjust, raise, raiseN, inject, subsume, subsumeN, raiseUnder, raiseNUnder, raiseUnderN, raiseNUnderN
   , -- * Handler types
-    Handling, sendEnv, Handler, Translator
+    Handling, esSend, Handler, Translator
   , -- * Interpreting effects
     interpret, reinterpret, reinterpret2, reinterpret3, reinterpretN, interpose, impose, imposeN
   , -- * Translating effects
@@ -21,14 +28,18 @@
 
 import           Cleff.Internal.Effect
 import           Cleff.Internal.Monad
-import           Data.Mem              (MemPtr)
-import qualified Data.Mem              as Mem
-import           Data.Rec              (pattern (:++:))
-import qualified Data.Rec              as Env
+import           Data.Rec.SmallArray   (Rec, pattern (:++:))
+import qualified Data.Rec.SmallArray   as Rec
 import           Unsafe.Coerce         (unsafeCoerce)
 
 -- * Trivial handling
 
+-- | Adjust the effect stack by a contravariant transformation function over the stack. This function reveals the
+-- profunctorial nature of 'Eff'; in particular, 'Eff' is a profunctor @['Effect'] -> 'Data.Kind.Type'@, @lmap@ is
+-- 'adjust', and @rmap@ is 'fmap'.
+adjust :: ∀ es es'. (∀ f. Rec f es' -> Rec f es) -> Eff es ~> Eff es'
+adjust f m = Eff (unEff m . adjustEnv f)
+
 -- | Lift a computation into a bigger effect stack with one more effect. For a more general version see 'raiseN'.
 raise :: ∀ e es. Eff es ~> Eff (e ': es)
 raise = raiseN @'[e]
@@ -36,11 +47,50 @@
 -- | Lift a computation into a bigger effect stack with arbitrarily more effects. This function requires
 -- @TypeApplications@.
 raiseN :: ∀ es' es. KnownList es' => Eff es ~> Eff (es' ++ es)
-raiseN m = Eff (unEff m . Mem.adjust (Env.drop @es'))
+raiseN = adjust (Rec.drop @es')
 
+-- | Like 'raise', but adds the new effect under the top effect. This is useful for transforming an interpreter
+-- @e' ':>' es => 'Eff' (e ': es) '~>` 'Eff' es@ into a reinterpreter @'Eff' (e ': es) '~>' 'Eff' (e' ': es)@:
+--
+-- @
+-- myInterpreter :: Bar ':>' es => 'Eff' (Foo ': es) '~>' 'Eff' es
+-- myInterpreter = ...
+--
+-- myReinterpreter :: 'Eff' (Foo ': es) '~>' 'Eff' (Bar ': es)
+-- myReinterpreter = myInterpreter '.' 'raiseUnder'
+-- @
+--
+-- In other words,
+--
+-- @
+-- 'reinterpret' h == 'interpret' h . 'raiseUnder'
+-- @
+--
+-- However, note that this function is suited for transforming an existing interpreter into a reinterpreter; if you
+-- want to define a reinterpreter from scratch, you should still prefer 'reinterpret', which is both easier to use and
+-- more efficient.
+raiseUnder :: ∀ e' e es. Eff (e ': es) ~> Eff (e ': e' ': es)
+raiseUnder = raiseNUnder @'[e']
+
+-- | Like 'raiseUnder', but allows introducing multiple effects. This function requires @TypeApplications@.
+raiseNUnder :: ∀ es' e es. KnownList es' => Eff (e ': es) ~> Eff (e ': es' ++ es)
+raiseNUnder = raiseNUnderN @es' @'[e]
+
+-- | Like 'raiseUnder', but allows introducing the effect under multiple effects. This function requires
+-- @TypeApplications@.
+raiseUnderN :: ∀ e es' es. KnownList es' => Eff (es' ++ es) ~> Eff (es' ++ e ': es)
+raiseUnderN = raiseNUnderN @'[e] @es' @es
+
+-- | A generalization of both 'raiseUnderN' and 'raiseNUnder', allowing introducing multiple effects under multiple
+-- effects. This function requires @TypeApplications@ and is subject to serious type ambiguity; you most likely will
+-- need to supply all three type variables explicitly.
+raiseNUnderN :: ∀ es'' es' es. (KnownList es', KnownList es'') => Eff (es' ++ es) ~> Eff (es' ++ (es'' ++ es))
+raiseNUnderN = adjust \re -> Rec.concat
+  (Rec.take @es' @(es'' ++ es) re) (Rec.drop @es'' @es (Rec.drop @es' @(es'' ++ es) re))
+
 -- | Lift a computation with a fixed, known effect stack into some superset of the stack.
 inject :: ∀ es' es. Subset es' es => Eff es' ~> Eff es
-inject m = Eff (unEff m . Mem.adjust (Env.pick @es'))
+inject = adjust (Rec.pick @es')
 
 -- | Eliminate a duplicate effect from the top of the effect stack. For a more general version see 'subsumeN'.
 subsume :: ∀ e es. e :> es => Eff (e ': es) ~> Eff es
@@ -48,50 +98,53 @@
 
 -- | Eliminate several duplicate effects from the top of the effect stack. This function requires @TypeApplications@.
 subsumeN :: ∀ es' es. Subset es' es => Eff (es' ++ es) ~> Eff es
-subsumeN m = Eff (unEff m . Mem.adjust (\re -> Env.pick @es' re :++: re))
+subsumeN = adjust \re -> Rec.pick @es' re :++: re
 
 -- * Handler types
 
 -- | The send-site environment.
-data SendSite e esSend = SendSite
-  {-# UNPACK #-} !(MemPtr InternalHandler e) -- ^ The pointer to the effect handler of the effect being handled.
+data SendSite esSend e = SendSite
   {-# UNPACK #-} !(Env esSend) -- ^ The send-site 'Env'.
+  {-# UNPACK #-} !(HandlerPtr e) -- ^ The pointer to the current effect handler.
 
--- | The typeclass that indicates a handler scope, handling effect @e@ sent from the effect stack @esSend@ in the
+-- | The typeclass that denotes a handler scope, handling effect @e@ sent from the effect stack @esSend@ in the
 -- effect stack @es@.
 --
 -- You should not define instances for this typeclass whatsoever.
-class Handling e es esSend | e -> es esSend, es -> e esSend, esSend -> e es where
+class Handling esSend e es | esSend -> e es where
+  -- @esSend@ is existential so it uniquely determines the other two variables. As handling scopes can nest, the other
+  -- two variables cannot determine anything.
+
   -- | Obtain the send-site environment.
-  sendSite :: SendSite e esSend
+  sendSite :: SendSite esSend e
   sendSite = error
     "Cleff.Internal.Interpret.sendSite: Attempting to access the send site without a reflected value. This is perhaps \
     \because you are trying to define an instance for the 'Handling' typeclass, which you should not be doing \
     \whatsoever. If that or other shenanigans seem unlikely, please report this as a bug."
 
 -- | Get the pointer to the current effect handler itself.
-hdlPtr :: Handling e es esSend => MemPtr InternalHandler e
-hdlPtr = let SendSite ptr _ = sendSite in ptr
+hdlPtr :: ∀ esSend e es. Handling esSend e es => HandlerPtr e
+hdlPtr = let SendSite _ ptr = sendSite @esSend in ptr
 {-# INLINE hdlPtr #-}
 
 -- | Get the send-site 'Env'.
-sendEnv :: Handling e es esSend => Env esSend
-sendEnv = let SendSite _ env = sendSite in env
-{-# INLINE sendEnv #-}
+esSend :: Handling esSend e es => Env esSend
+esSend = let SendSite env _ = sendSite in env
+{-# INLINE esSend #-}
 
 -- | Newtype wrapper for instantiating the 'Handling' typeclass locally, a la the reflection trick. We do not use
 -- the @reflection@ library directly so as not to expose this piece of implementation detail to the user.
-newtype InstHandling e es esSend a = InstHandling (Handling e es esSend => a)
+newtype InstHandling esSend e es a = InstHandling (Handling esSend e es => a)
 
 -- | Instantiate an 'Handling' typeclass, i.e. pass an implicit send-site environment in. This function shouldn't
 -- be directly used anyhow.
-instHandling :: ∀ e es esSend a. (Handling e es esSend => a) -> SendSite e esSend -> a
-instHandling x = unsafeCoerce (InstHandling x :: InstHandling e es esSend a)
+instHandling :: ∀ esSend e es a. (Handling esSend e es => a) -> SendSite esSend e -> a
+instHandling x = unsafeCoerce (InstHandling x :: InstHandling esSend e es a)
 {-# INLINE instHandling #-}
 
 -- | The type of an /effect handler/, which is a function that transforms an effect @e@ from an arbitrary effect stack
 -- into computations in the effect stack @es@.
-type Handler e es = ∀ esSend. Handling e es esSend => e (Eff esSend) ~> Eff es
+type Handler e es = ∀ esSend. Handling esSend e es => e (Eff esSend) ~> Eff es
 
 -- | The type of a simple transformation function from effect @e@ to @e'@.
 type Translator e e' = ∀ esSend. e (Eff esSend) ~> e' (Eff esSend)
@@ -100,9 +153,9 @@
 
 -- | Transform a 'Handler' into an 'InternalHandler' given a pointer that is going to point to the 'InternalHandler'
 -- and the current 'Env'.
-mkInternalHandler :: MemPtr InternalHandler e -> Env es -> Handler e es -> InternalHandler e
-mkInternalHandler ptr es handle = InternalHandler \eff -> Eff \esSend ->
-  unEff (instHandling handle (SendSite ptr esSend) eff) (Mem.update esSend es)
+mkInternalHandler :: HandlerPtr e -> Env es -> Handler e es -> InternalHandler e
+mkInternalHandler ptr es handle = InternalHandler \e -> Eff \ess ->
+  unEff (instHandling handle (SendSite ess ptr) e) (updateEnv ess es)
 
 -- | Interpret an effect @e@ in terms of effects in the effect stack @es@ with an effect handler.
 interpret :: ∀ e es. Handler e es -> Eff (e ': es) ~> Eff es
@@ -123,8 +176,9 @@
 -- | Like 'reinterpret', but adds arbitrarily many new effects. This function requires @TypeApplications@.
 reinterpretN :: ∀ es' e es. KnownList es' => Handler e (es' ++ es) -> Eff (e ': es) ~> Eff (es' ++ es)
 reinterpretN handle m = Eff \es ->
-  let (# ptr, es' #) = Mem.alloca es
-  in unEff m $ Mem.append ptr (mkInternalHandler ptr es' handle) $ Mem.adjust (Env.drop @es') es'
+  let (# ptr, es' #) = allocaEnv es
+  in unEff m $ appendEnv ptr (mkInternalHandler ptr es' handle) $ adjustEnv (Rec.drop @es') es'
+{-# INLINE reinterpretN #-}
 
 -- | Respond to an effect while being able to leave it unhandled (i.e. you can resend the effects in the handler).
 interpose :: ∀ e es. e :> es => Handler e es -> Eff es ~> Eff es
@@ -137,26 +191,27 @@
 -- | Like 'impose', but allows introducing arbitrarily many effects. This requires @TypeApplications@.
 imposeN :: ∀ es' e es. (KnownList es', e :> es) => Handler e (es' ++ es) -> Eff es ~> Eff (es' ++ es)
 imposeN handle m = Eff \es ->
-  let (# ptr, es' #) = Mem.alloca es
-  in unEff m $ Mem.replace ptr (mkInternalHandler ptr es' handle) $ Mem.adjust (Env.drop @es') es'
+  let (# ptr, es' #) = allocaEnv es
+  in unEff m $ replaceEnv ptr (mkInternalHandler ptr es' handle) $ adjustEnv (Rec.drop @es') es'
+{-# INLINE imposeN #-}
 
 -- * Translating effects
 
 -- | Interpret an effect in terms of another effect in the stack via a simple 'Translator'.
-transform :: ∀ e' e es. e' :> es => Translator e e' -> Eff (e ': es) ~> Eff es
-transform = translateN @'[]
+--
+-- @
+-- 'transform' trans = 'interpret' ('sendVia' 'toEff' '.' trans)
+-- @
+transform :: ∀ e e' es. e' :> es => Translator e e' -> Eff (e ': es) ~> Eff es
+transform trans = interpret (sendVia toEff . trans)
 
 -- | Like 'transform', but instead of using an effect in stack, add a new one to the top of it.
-translate :: ∀ e' e es. Translator e e' -> Eff (e ': es) ~> Eff (e' ': es)
-translate = translateN @'[e']
-
--- | Common implementation of 'transform' and 'translate'. It is overly general on its own so it is not exported in
--- "Cleff".
-translateN :: ∀ es' e' e es. (KnownList es', e' :> es' ++ es) => Translator e e' -> Eff (e ': es) ~> Eff (es' ++ es)
-translateN trans m = Eff \es ->
-  let (# ptr, es' #) = Mem.alloca es
-  in let handler = InternalHandler (runHandler (Mem.read es') . trans)
-  in unEff m $ Mem.append ptr handler $ Mem.adjust (Env.drop @es') es'
+--
+-- @
+-- 'translate' trans = 'reinterpret' ('sendVia' 'toEff' '.' trans)
+-- @
+translate :: ∀ e e' es. Translator e e' -> Eff (e ': es) ~> Eff (e' ': es)
+translate trans = reinterpret (sendVia toEff . trans)
 
 -- * Combinators for interpreting higher effects
 
@@ -175,8 +230,8 @@
 --     ('toEff' . dealloc)
 --     ('toEff' . use)
 -- @
-toEff :: Handling e es esSend => Eff esSend ~> Eff es
-toEff m = Eff \es -> unEff m (Mem.update es sendEnv)
+toEff :: Handling esSend e es => Eff esSend ~> Eff es
+toEff m = Eff \es -> unEff m (updateEnv es esSend)
 
 -- | Run a computation in the current effect stack, but handles the current effect inside the computation differently
 -- by providing a new 'Handler'. This is useful for interpreting effects with local contexts, like 'Cleff.Reader.Local':
@@ -190,12 +245,14 @@
 --       'Cleff.Reader.Ask'       -> 'pure' r
 --       'Cleff.Reader.Local' f m -> 'toEffWith' (handle $ f r) m
 -- @
-toEffWith :: Handling e es esSend => Handler e es -> Eff esSend ~> Eff es
+toEffWith :: ∀ esSend e es. Handling esSend e es => Handler e es -> Eff esSend ~> Eff es
 toEffWith handle m = Eff \es -> unEff m $
-  Mem.write hdlPtr (mkInternalHandler hdlPtr es handle) $ Mem.update es sendEnv
+  -- The 'Handling' constraint of 'handle' will NOT be prematurely initialized here because that will make 'handle'
+  -- monomorphic. Therefore this usage is safe.
+  writeEnv (hdlPtr @esSend) (mkInternalHandler (hdlPtr @esSend) es handle) $ updateEnv es esSend
 
 -- | Temporarily gain the ability to lift some @'Eff' es@ actions into @'Eff' esSend@. This is useful for dealing with
 -- effect operations with the monad type in the negative position, which means it's unlikely that you need to use this
 -- function in implementing your effects.
-withFromEff :: Handling e es esSend => ((Eff es ~> Eff esSend) -> Eff esSend a) -> Eff es a
-withFromEff f = Eff \es -> unEff (f \m -> Eff \esSend -> unEff m (Mem.update esSend es)) (Mem.update es sendEnv)
+withFromEff :: Handling esSend e es => ((Eff es ~> Eff esSend) -> Eff esSend a) -> Eff es a
+withFromEff f = Eff \es -> unEff (f \m -> Eff \ess -> unEff m (updateEnv ess es)) (updateEnv es esSend)
diff --git a/src/Cleff/Internal/Monad.hs b/src/Cleff/Internal/Monad.hs
--- a/src/Cleff/Internal/Monad.hs
+++ b/src/Cleff/Internal/Monad.hs
@@ -1,25 +1,38 @@
+{-# LANGUAGE UnboxedTuples #-}
 {-# OPTIONS_HADDOCK not-home #-}
--- | This module contains the definition of the 'Eff' monad, which is basically an @'Env' es -> 'IO' a@, as well as
--- functions for manipulating the effect environment type 'Env'. Most of the times, you won't need to use this module
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- This module contains the definition of the 'Eff' monad. Most of the times, you won't need to use this module
 -- directly; user-facing functionalities are all exported via the "Cleff" module.
 --
 -- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
 -- extra careful if you're to depend on this module.
 module Cleff.Internal.Monad
-  ( -- * Core types
-    InternalHandler (InternalHandler, runHandler), Env, Eff (Eff, unEff)
+  ( -- * The 'Eff' monad
+    InternalHandler (InternalHandler, runHandler), Eff (Eff, unEff)
+  , -- * Effect environment
+    Env, HandlerPtr, emptyEnv, adjustEnv, allocaEnv, readEnv, writeEnv, replaceEnv, appendEnv, updateEnv
   , -- * Performing effect operations
-    KnownList, Subset, send
+    KnownList, Subset, send, sendVia
   ) where
 
+import           Cleff.Internal.Any
 import           Cleff.Internal.Effect
 import           Control.Monad.Fix          (MonadFix)
 import           Control.Monad.Trans.Reader (ReaderT (ReaderT))
-import           Data.Mem                   (Mem)
-import qualified Data.Mem                   as Mem
-import           Data.Rec                   (KnownList, Subset)
+import           Data.IntMap.Strict         (IntMap)
+import qualified Data.IntMap.Strict         as Map
+import           Data.Rec.SmallArray        (KnownList, Rec, Subset, pattern (:~:))
+import qualified Data.Rec.SmallArray        as Rec
 import           Type.Reflection            (Typeable, typeRep)
 
+-- * The 'Eff' monad
+
 -- | The internal representation of effect handlers. This is just a natural transformation from the effect type
 -- @e ('Eff' es)@ to the effect monad @'Eff' es@ for any effect stack @es@.
 --
@@ -34,9 +47,6 @@
 instance Typeable e => Show (InternalHandler e) where
   showsPrec p _ = ("Handler " ++) . showsPrec p (typeRep @e)
 
--- | The effect memironment that stores handlers of any effect present in the stack @es@.
-type Env = Mem InternalHandler
-
 -- | The extensible effect monad. A monad @'Eff' es@ is capable of performing any effect in the /effect stack/ @es@,
 -- which is a type-level list that holds all effects available. However, most of the times, for flexibility, @es@
 -- should be a polymorphic type variable, and you should use the '(:>)' and '(:>>)' operators in constraints to
@@ -50,10 +60,85 @@
 -- effect in a computation returning an 'Integer'.
 type role Eff nominal representational
 newtype Eff es a = Eff { unEff :: Env es -> IO a }
+  -- ^ The effect monad receives an effect environment 'Env' that contains all effect handlers and produces an 'IO'
+  -- action.
   deriving newtype (Semigroup, Monoid)
   deriving (Functor, Applicative, Monad, MonadFix) via (ReaderT (Env es) IO)
 
+-- * Effect environment
+
+-- | The /effect environment/ that corresponds effects in the stack to their respective 'InternalHandler's. This
+-- structure simulates memory: handlers are retrieved via pointers ('HandlerPtr's), and for each effect in the stack
+-- we can either change what pointer it uses or change the handler the pointer points to. The former is used for global
+-- effect interpretation ('Cleff.reinterpretN') and the latter for local interpretation ('Cleff.toEffWith') in order to
+-- retain correct HO semantics. For more details on this see https://github.com/re-xyr/cleff/issues/5.
+type role Env nominal
+data Env (es :: [Effect]) = Env
+  {-# UNPACK #-} !(Rec HandlerPtr es) -- ^ The array.
+  {-# UNPACK #-} !Int -- ^ The next memory address to allocate.
+  !(IntMap Any) -- ^ The simulated memory.
+
+-- | A pointer to 'InternalHandler' in an 'Env'.
+type role HandlerPtr nominal
+newtype HandlerPtr (e :: Effect) = HandlerPtr { unHandlerPtr :: Int }
+  deriving newtype
+    ( Eq  -- ^ Pointer equality.
+    , Ord -- ^ An arbitrary total order on the pointers.
+    )
+
+-- | Create an empty 'Env' with no address allocated.
+emptyEnv :: Env '[]
+emptyEnv = Env Rec.empty 0 Map.empty
+{-# INLINE emptyEnv #-}
+
+-- | Adjust the effect stack via an function over 'Rec'.
+adjustEnv :: ∀ es' es. (Rec HandlerPtr es -> Rec HandlerPtr es') -> Env es -> Env es'
+adjustEnv f (Env re n mem) = Env (f re) n mem
+{-# INLINE adjustEnv #-}
+
+-- | Allocate a new, empty address for a handler. \( O(1) \).
+allocaEnv :: ∀ e es. Env es -> (# HandlerPtr e, Env es #)
+allocaEnv (Env re n mem) = (# HandlerPtr n, Env re (succ n) mem #)
+{-# INLINE allocaEnv #-}
+
+-- | Read the handler a pointer points to. \( O(1) \).
+readEnv :: ∀ e es. Rec.Elem e es => Env es -> InternalHandler e
+readEnv (Env re _ mem) = fromAny $ mem Map.! unHandlerPtr (Rec.index @e re)
+{-# INLINE readEnv #-}
+
+-- | Overwrite the handler a pointer points to. \( O(1) \).
+writeEnv :: ∀ e es. HandlerPtr e -> InternalHandler e -> Env es -> Env es
+writeEnv (HandlerPtr m) x (Env re n mem) = Env re n (Map.insert m (toAny x) mem)
+{-# INLINE writeEnv #-}
+
+-- | Replace the handler pointer of an effect in the stack. \( O(n) \).
+replaceEnv :: ∀ e es. Rec.Elem e es => HandlerPtr e -> InternalHandler e -> Env es -> Env es
+replaceEnv (HandlerPtr m) x (Env re n mem) = Env (Rec.update @e (HandlerPtr m) re) n (Map.insert m (toAny x) mem)
+{-# INLINE replaceEnv #-}
+
+-- | Add a new effect to the stack with its corresponding handler pointer. \( O(n) \).
+appendEnv :: ∀ e es. HandlerPtr e -> InternalHandler e -> Env es -> Env (e ': es)
+appendEnv (HandlerPtr m) x (Env re n mem) = Env (HandlerPtr m :~: re) n (Map.insert m (toAny x) mem)
+{-# INLINE appendEnv #-}
+
+-- | Use the state of LHS as a newer version for RHS. \( O(1) \).
+updateEnv :: ∀ es es'. Env es' -> Env es -> Env es
+updateEnv (Env _ n mem) (Env re' _ _) = Env re' n mem
+{-# INLINE updateEnv #-}
+
+-- * Performing effect operations
+
 -- | Perform an effect operation, /i.e./ a value of an effect type @e :: 'Effect'@. This requires @e@ to be in the
 -- effect stack.
 send :: e :> es => e (Eff es) ~> Eff es
-send eff = Eff \handlers -> unEff (runHandler (Mem.read handlers) eff) handlers
+send = sendVia id
+
+-- | Perform an action in another effect stack via a transformation to that stack; in other words, this function "maps"
+-- the effect operation from effect stack @es@ to @es'@. This is a generalization of 'send'; end users most likely
+-- won't need to use this.
+--
+-- @
+-- 'send' = 'sendVia' 'id'
+-- @
+sendVia :: e :> es' => (Eff es ~> Eff es') -> e (Eff es) ~> Eff es'
+sendVia f e = Eff \es -> unEff (f (runHandler (readEnv es) e)) es
diff --git a/src/Cleff/Internal/TH.hs b/src/Cleff/Internal/TH.hs
--- a/src/Cleff/Internal/TH.hs
+++ b/src/Cleff/Internal/TH.hs
@@ -1,6 +1,13 @@
 {-# LANGUAGE CPP #-}
 {-# OPTIONS_HADDOCK not-home #-}
--- | This module contains Template Haskell functions for generating definitions of functions that send effect
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- This module contains Template Haskell functions for generating definitions of functions that send effect
 -- operations. You mostly won't want to import this module directly; The "Cleff" module reexports the main
 -- functionalities of this module.
 --
diff --git a/src/Cleff/Mask.hs b/src/Cleff/Mask.hs
--- a/src/Cleff/Mask.hs
+++ b/src/Cleff/Mask.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Mask
   ( -- * Effect
     Mask (..)
diff --git a/src/Cleff/Output.hs b/src/Cleff/Output.hs
--- a/src/Cleff/Output.hs
+++ b/src/Cleff/Output.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Output
   ( -- * Effect
     Output (..)
diff --git a/src/Cleff/Reader.hs b/src/Cleff/Reader.hs
--- a/src/Cleff/Reader.hs
+++ b/src/Cleff/Reader.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Reader
   ( -- * Effect
     Reader (..)
diff --git a/src/Cleff/State.hs b/src/Cleff/State.hs
--- a/src/Cleff/State.hs
+++ b/src/Cleff/State.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.State
   ( -- * Effect
     State (..)
diff --git a/src/Cleff/Trace.hs b/src/Cleff/Trace.hs
--- a/src/Cleff/Trace.hs
+++ b/src/Cleff/Trace.hs
@@ -1,3 +1,10 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Trace
   ( -- * Effect
     Trace (..)
diff --git a/src/Cleff/Writer.hs b/src/Cleff/Writer.hs
--- a/src/Cleff/Writer.hs
+++ b/src/Cleff/Writer.hs
@@ -1,10 +1,17 @@
+{-# LANGUAGE Trustworthy #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: experimental
+-- Portability: non-portable (GHC only)
 module Cleff.Writer
   ( -- * Effect
     Writer (..)
   , -- * Operations
     tell, listen, listens
   , -- * Interpretations
-    runWriter
+    runWriter, runWriterBatch
   ) where
 
 import           Cleff
@@ -59,10 +66,37 @@
         pure (x, w')
 {-# INLINE runWriter #-}
 
--- f :: Writer String :> es => Int -> Eff es [String]
--- f 0 = tell "0" >> pure []
--- f n = do
---   tell (show n) >> uncurry (flip (:)) <$> listen (f $ n - 1)
-
--- >>> runPure $ runWriter @String $ f 10
--- (["9876543210","876543210","76543210","6543210","543210","43210","3210","210","10","0"],"109876543210")
+-- | Run a monoidal 'Writer' effect, but appends the listened output to the parent value only when the listen operation
+-- finishes. This means that when you run two 'listen's on two threads, the values 'tell'ed inside will not be appended
+-- to the parent value in real time, but only after the thread finishes 'listen'ing. For example, this code
+--
+-- @
+-- 'UnliftIO.concurrently_'
+--   ('listen' '$' 'tell' "1" '>>' 'tell' "2" '>>' 'tell' "3")
+--   ('listen' '$' 'tell' "4" '>>' 'tell' "5" '>>' 'tell' "6")
+-- @
+--
+-- will produce either @"123456"@ or @"456123"@ with 'runWriterBatch', but may produce these digits in any order with
+-- 'runWriter'.
+--
+-- This version of interpreter can be faster than 'runWriter' in 'listen'-intense code. It is subject to all caveats
+-- of 'runWriter'.
+--
+-- @since 0.2.0.0
+runWriterBatch :: ∀ w es a. Monoid w => Eff (Writer w ': es) a -> Eff es (a, w)
+runWriterBatch m = thisIsPureTrustMe do
+  rw <- newIORef mempty
+  x <- reinterpret (h rw) m
+  w' <- readIORef rw
+  pure (x, w')
+  where
+    h :: IORef w -> Handler (Writer w) (IOE ': es)
+    h rw = \case
+      Tell w' -> liftIO $ atomicModifyIORefCAS_ rw (<> w')
+      Listen m' -> do
+        rw' <- newIORef mempty
+        x <- toEffWith (h rw') m'
+        w' <- readIORef rw'
+        liftIO $ atomicModifyIORefCAS_ rw (<> w')
+        pure (x, w')
+{-# INLINE runWriterBatch #-}
diff --git a/src/Data/Any.hs b/src/Data/Any.hs
deleted file mode 100644
--- a/src/Data/Any.hs
+++ /dev/null
@@ -1,19 +0,0 @@
--- | This module contains utility functions for 'Any'.
---
--- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
--- extra careful if you're to depend on this module.
-module Data.Any (Any, fromAny, toAny) where
-
-import           GHC.Exts      (Any)
-import           Unsafe.Coerce (unsafeCoerce)
-
--- | Coerce any boxed value into 'Any'.
-toAny :: a -> Any
-toAny = unsafeCoerce
-{-# INLINE toAny #-}
-
--- | Coerce 'Any' to a boxed value. This is /generally unsafe/ and it is your responsibility to ensure that the type
--- you're coercing into is the original type that the 'Any' is coerced from.
-fromAny :: Any -> a
-fromAny = unsafeCoerce
-{-# INLINE fromAny #-}
diff --git a/src/Data/Mem.hs b/src/Data/Mem.hs
deleted file mode 100644
--- a/src/Data/Mem.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE UnboxedTuples #-}
--- | 'Mem' is a data structure that is a simulation of an array of thread-local pointers. This structure supports:
---
--- * \( O(n) \) creation of a new pointer;
--- * \( O(n) \) changing the pointer in an array cell;
--- * \( O(1) \) modification of the memory a pointer points to;
--- * \( O(1) \) read.
---
--- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
--- extra careful if you're to depend on this module.
-module Data.Mem (Mem, MemPtr, empty, adjust, alloca, read, write, replace, append, update) where
-
-import           Data.Any
-import           Data.IntMap.Strict (IntMap)
-import qualified Data.IntMap.Strict as Map
-import           Data.Kind          (Type)
-import           Data.Rec           (Rec, pattern (:~:))
-import qualified Data.Rec           as Rec
-import           Prelude            hiding (read)
-
--- | The representation of a pointer in a 'Mem'.
-type role MemPtr representational nominal
-newtype MemPtr (f :: k -> Type) (a :: k) = MemPtr { unMemPtr :: Int }
-  deriving newtype
-    ( Eq  -- ^ Pointer equality.
-    , Ord -- ^ An arbitrary total order on the pointers.
-    )
-
--- | A simulated array of thread-local pointers. This means for each array cell, you can either change the pointer or
--- change the memory the pointer points to.
---
--- Note that like real memory, any of the operations provided is not generally safe and it is your responsibility to
--- ensure the correctness of your calls.
-type role Mem representational nominal
-data Mem (f :: k -> Type) (es :: [k]) = Mem
-  {-# UNPACK #-} !(Rec (MemPtr f) es) -- ^ The array.
-  {-# UNPACK #-} !Int -- ^ The next memory address to allocate.
-  !(IntMap Any) -- ^ The simulated memory.
-
--- | Create a 'Mem' with no pointers.
-empty :: Mem f '[]
-empty = Mem Rec.empty 0 Map.empty
-{-# INLINE empty #-}
-
--- | Adjust the array of pointers.
-adjust :: ∀ es' es f. (Rec (MemPtr f) es -> Rec (MemPtr f) es') -> Mem f es -> Mem f es'
-adjust f (Mem re n mem) = Mem (f re) n mem
-{-# INLINE adjust #-}
-
--- | Allocate a new address. \( O(1) \).
-alloca :: ∀ e es f. Mem f es -> (# MemPtr f e, Mem f es #)
-alloca (Mem re n mem) = (# MemPtr n, Mem re (succ n) mem #)
-{-# INLINE alloca #-}
-
--- | Read a pointer. \( O(1) \).
-read :: ∀ e es f. Rec.Elem e es => Mem f es -> f e
-read (Mem re _ mem) = fromAny $ mem Map.! unMemPtr (Rec.index @e re)
-{-# INLINE read #-}
-
--- | Write to the memory a pointer points to. \( O(1) \).
-write :: ∀ e es f. MemPtr f e -> f e -> Mem f es -> Mem f es
-write (MemPtr m) x (Mem re n mem) = Mem re n (Map.insert m (toAny x) mem)
-{-# INLINE write #-}
-
--- | Replace a pointer with a new one. \( O(n) \).
-replace :: ∀ e es f. Rec.Elem e es => MemPtr f e -> f e -> Mem f es -> Mem f es
-replace (MemPtr m) x (Mem re n mem) = Mem (Rec.modify @e (MemPtr m) re) n (Map.insert m (toAny x) mem)
-{-# INLINE replace #-}
-
--- | Add a new pointer to the array. \( O(n) \).
-append :: ∀ e es f. MemPtr f e -> f e -> Mem f es -> Mem f (e ': es)
-append (MemPtr m) x (Mem re n mem) = Mem (MemPtr m :~: re) n (Map.insert m (toAny x) mem)
-{-# INLINE append #-}
-
--- | Use the memory of LHS as a newer version for the memory of RHS. \( O(1) \).
-update :: ∀ es es' f. Mem f es' -> Mem f es -> Mem f es
-update (Mem _ n mem) (Mem re' _ _) = Mem re' n mem
-{-# INLINE update #-}
diff --git a/src/Data/Rec.hs b/src/Data/Rec.hs
deleted file mode 100644
--- a/src/Data/Rec.hs
+++ /dev/null
@@ -1,390 +0,0 @@
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# OPTIONS_HADDOCK not-home #-}
--- | This module defines an immutable extensible record type, similar to @vinyl@ and @data-diverse@. However this
--- implementation focuses on fast reads, hence has very different performance characteristics from other libraries:
---
--- * Lookup: Amortized \( O(1) \).
--- * Update: \( O(n) \).
--- * Shrink: \( O(1) \).
--- * Append: \( O(n) \).
---
--- __This is an /internal/ module and its API may change even between minor versions.__ Therefore you should be
--- extra careful if you're to depend on this module.
-module Data.Rec
-  ( Rec, length
-  , -- * Construction
-    empty, singleton
-  , -- * Addition
-    cons, pattern (:~:), type (++), concat, pattern (:++:)
-  , -- * Deletion
-    tail, KnownList, drop
-  , -- * Retrieval
-    head, take, Elem, index, Subset, pick
-  , -- * Modification
-    modify, (/~/), batch, (/++/)
-  , -- * Mapping
-    type (~>), natural, (<#>), zipWith, all, any, degenerate, extract
-  , -- * Debugging
-    invariant, sizeInvariant, allAccessible
-  ) where
-
-import           Control.Arrow             ((&&&))
-import           Control.Monad.Primitive   (PrimMonad (PrimState))
-import           Data.Any
-import           Data.Functor.Const        (Const (Const, getConst))
-import           Data.Kind                 (Type)
-import           Data.List                 (intersperse)
-import           Data.Primitive.SmallArray (SmallArray, SmallMutableArray, copySmallArray, indexSmallArray,
-                                            newSmallArray, runSmallArray, sizeofSmallArray, writeSmallArray)
-import           GHC.TypeLits              (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
-import           Prelude                   hiding (all, any, concat, drop, head, length, tail, take, zipWith)
-import           Text.Read                 (readPrec)
-import qualified Text.Read                 as R
-import qualified Text.Read.Lex             as RL
-
--- | Extensible record type supporting efficient \( O(1) \) reads. The underlying implementation is 'SmallArray'
--- slices, therefore suits small numbers of entries (/i.e./ less than 128).
-type role Rec representational nominal
-data Rec (f :: k -> Type) (es :: [k]) = Rec
-  {-# UNPACK #-} !Int -- ^ The offset.
-  {-# UNPACK #-} !Int -- ^ The length.
-  {-# UNPACK #-} !(SmallArray Any) -- ^ The array content.
-
-instance Eq (Rec f '[]) where
-  _ == _ = True
-
-instance (Eq (Rec f xs), Eq (f x)) => Eq (Rec f (x ': xs)) where
-  x :~: xs == y :~: ys = x == y && xs == ys
-
-instance {-# OVERLAPPABLE #-} (∀ x. Eq (f x)) => Eq (Rec f xs) where
-  xs == ys = all (== Const True) $ zipWith (\x y -> Const $ x == y) xs ys
-
--- | @
--- 'show' 'empty' == "empty"
--- @
-instance Show (Rec f '[]) where
-  show _ = "empty"
-
--- | @
--- 'read' \"empty\" == 'empty'
--- @
-instance Read (Rec f '[]) where
-  readPrec = R.parens $ R.prec appPrec $
-    empty <$ R.lift (RL.expect (R.Ident "empty"))
-    where appPrec = 10
-
--- | @
--- 'show' ('Data.Functor.Identity.Identity' 'True' ':~:' 'Data.Functor.Identity.Identity' \"Hi\" ':~:' 'empty')
--- == "Identity True :~: Identity \\"Hi\\" :~: empty"
--- @
-instance (Show (f x), Show (Rec f xs)) => Show (Rec f (x ': xs)) where
-  showsPrec p (x :~: xs) = showParen (p > consPrec) $
-    showsPrec (consPrec + 1) x . showString " :~: " . showsPrec consPrec xs
-
--- | @
--- 'read' "Identity True :~: Identity \\"Hi\\" :~: empty"
--- == 'Data.Functor.Identity.Identity' 'True' ':~:' 'Data.Functor.Identity.Identity' \"Hi\" ':~:' 'empty'
--- @
-instance (Read (f x), Read (Rec f xs)) => Read (Rec f (x ': xs)) where
-  readPrec = R.parens $ R.prec consPrec $
-    cons <$> R.step (readPrec @(f x)) <* R.lift (RL.expect (R.Symbol ":~:")) <*> readPrec @(Rec f xs)
-
--- | @
--- 'show' ('Const' 'False' ':~:' 'Const' 'True' ':~:' 'empty')
--- == "Const False :~: Const True :~: empty"
--- @
-instance {-# OVERLAPPABLE #-} (∀ x. Show (f x)) => Show (Rec f xs) where
-  showsPrec p xs = showParen (p > consPrec) $
-    foldr (.) id $ intersperse (showString " :~: ") $ extract (showsPrec (consPrec + 1)) xs
-
-instance Semigroup (Rec f '[]) where
-  xs <> _ = xs
-
--- | One-by-one semigroup operation instead of concatenation.
---
--- @
--- (x ':~:' xs) '<>' (y ':~:' ys) == x '<>' y ':~:' xs '<>' ys
--- @
-instance (Semigroup (f x), Semigroup (Rec f xs)) => Semigroup (Rec f (x ': xs)) where
-  (x :~: xs) <> (y :~: ys) = x <> y :~: xs <> ys
-
-instance {-# OVERLAPPABLE #-} (∀ x. Semigroup (f x)) => Semigroup (Rec f xs) where
-  xs <> ys = zipWith (<>) xs ys
-
--- | @
--- 'mempty' == 'empty'
--- @
-instance Monoid (Rec f '[]) where
-  mempty = empty
-
--- | The unit of a record type are the units of its element types:
---
--- @
--- 'mempty' == 'mempty' ':~:' 'mempty'
--- @
-instance (Monoid (f x), Monoid (Rec f xs)) => Monoid (Rec f (x ': xs)) where
-  mempty = mempty :~: mempty
-
--- | Get the length of the record.
-length :: Rec f es -> Int
-length (Rec _ len _) = len
-
--- | Create a new 'SmallMutableArray' with no contents.
-newArr :: PrimMonad m => Int -> m (SmallMutableArray (PrimState m) a)
-newArr len = newSmallArray len $ error
-  "Data.Rec.newArr: Attempting to read an element of the underlying array of a 'Rec'. Please report this as a bug."
-
--- | Create an empty record. \( O(1) \).
-empty :: Rec f '[]
-empty = Rec 0 0 $ runSmallArray $ newArr 0
-
--- | Create a record with one entry. \( O(1) \).
-singleton :: f e -> Rec f '[e]
-singleton x = Rec 0 1 $ runSmallArray do
-  marr <- newArr 1
-  writeSmallArray marr 0 (toAny x)
-  pure marr
-
--- | Prepend one entry to the record. \( O(n) \).
-cons :: f e -> Rec f es -> Rec f (e ': es)
-cons x (Rec off len arr) = Rec 0 (len + 1) $ runSmallArray do
-  marr <- newArr (len + 1)
-  writeSmallArray marr 0 (toAny x)
-  copySmallArray marr 1 arr off len
-  pure marr
-
--- | Infix version of 'cons' that also supports destructuring.
-pattern (:~:) :: f e -> Rec f es -> Rec f (e ': es)
-pattern x :~: xs <- (head &&& tail -> (x, xs))
-  where (:~:) = cons
-infixr 5 :~:
-{-# COMPLETE (:~:) #-}
-
--- | @infixr 5 :~:@
-consPrec :: Int
-consPrec = 5
-
--- | Type level list concatenation.
-type family xs ++ ys where
-  '[] ++ ys = ys
-  (x ': xs) ++ ys = x ': (xs ++ ys)
-infixr 5 ++
-
--- | Concatenate two records. \( O(m+n) \).
-concat :: Rec f es -> Rec f es' -> Rec f (es ++ es')
-concat (Rec off len arr) (Rec off' len' arr') = Rec 0 (len + len') $ runSmallArray do
-  marr <- newArr (len + len')
-  copySmallArray marr 0 arr off len
-  copySmallArray marr len arr' off' len'
-  pure marr
-
--- | Infix version of 'concat' that also supports destructuring.
-pattern (:++:) :: ∀ es es' f. KnownList es => Rec f es -> Rec f es' -> Rec f (es ++ es')
-pattern xs :++: xs' <- (take @es @es' &&& drop @es @es' -> (xs, xs'))
-  where (:++:) = concat
-infixr 5 :++:
-{-# COMPLETE (:++:) #-}
-
--- | Slice off one entry from the top of the record. \( O(1) \).
-tail :: Rec f (e ': es) -> Rec f es
-tail (Rec off len arr) = Rec (off + 1) (len - 1) arr
-
-unreifiable :: String -> String -> String -> a
-unreifiable clsName funName comp = error $
-  funName <> ": Attempting to access " <> comp <> " without a reflected value. This is perhaps because you are trying \
-  \to define an instance for the '" <> clsName <> "' typeclass, which you should not be doing whatsoever. If that or \
-  \other shenanigans seem unlikely, please report this as a bug."
-
--- | The list @es@ list is concrete, i.e. is of the form @'[a1, a2, ..., an]@, i.e. is not a type variable.
-class KnownList (es :: [k]) where
-  -- | Get the length of the list.
-  reifyLen :: Int
-  reifyLen = unreifiable "KnownList" "Data.Rec.reifyLen" "the length of a type-level list"
-
-instance KnownList '[] where
-  reifyLen = 0
-
-instance KnownList es => KnownList (e ': es) where
-  reifyLen = 1 + reifyLen @_ @es
-
--- | Slice off several entries from the top of the record. \( O(1) \).
-drop :: ∀ es es' f. KnownList es => Rec f (es ++ es') -> Rec f es'
-drop (Rec off len arr) = Rec (off + len') (len - len') arr
-  where len' = reifyLen @_ @es
-
--- | Get the head of the record. \( O(1) \).
-head :: Rec f (e ': es) -> f e
-head (Rec off _ arr) = fromAny $ indexSmallArray arr off
-
--- | Take elements from the top of the record. \( O(m) \).
-take :: ∀ es es' f. KnownList es => Rec f (es ++ es') -> Rec f es
-take (Rec off _ arr) = Rec 0 len $ runSmallArray do
-  marr <- newArr len
-  copySmallArray marr 0 arr off (off + len)
-  pure marr
-  where len = reifyLen @_ @es
-
--- | The element @e@ is present in the list @es@.
-class Elem (e :: k) (es :: [k]) where
-  -- | Get the index of the element.
-  reifyIndex :: Int
-  reifyIndex = unreifiable "Elem" "Data.Rec.reifyIndex" "the index of an element of a type-level list"
-
-instance {-# OVERLAPPING #-} Elem e (e ': es) where
-  reifyIndex = 0
-
-instance Elem e es => Elem e (e' ': es) where
-  reifyIndex = 1 + reifyIndex @_ @e @es
-
-type ElemNotFound e = 'Text "The element '" ':<>: 'ShowType e ':<>: 'Text "' is not present in the constraint"
-
-instance TypeError (ElemNotFound e) => Elem e '[] where
-  reifyIndex = error "Data.Rec.reifyIndex: Attempting to refer to a nonexistent member. Please report this as a bug."
-
--- | Get an element in the record. Amortized \( O(1) \).
-index :: ∀ e es f. Elem e es => Rec f es -> f e
-index (Rec off _ arr) = fromAny $ indexSmallArray arr (off + reifyIndex @_ @e @es)
-
--- | @es@ is a subset of @es'@.
-class KnownList es => Subset (es :: [k]) (es' :: [k]) where
-  -- | Get a list of indices of the elements.
-  reifyIndices :: [Int]
-  reifyIndices = unreifiable "Subset" "Data.Rec.reifyIndices" "the index of multiple elements of a type-level list"
-
-instance Subset '[] es where
-  reifyIndices = []
-
-instance (Subset es es', Elem e es') => Subset (e ': es) es' where
-  reifyIndices = reifyIndex @_ @e @es' : reifyIndices @_ @es @es'
-
--- | Get a subset of the record. Amortized \( O(m) \).
-pick :: ∀ es es' f. Subset es es' => Rec f es' -> Rec f es
-pick (Rec off _ arr) = Rec 0 (reifyLen @_ @es) $ runSmallArray do
-  marr <- newArr (reifyLen @_ @es)
-  go marr 0 (reifyIndices @_ @es @es')
-  pure marr
-  where
-    go :: PrimMonad m => SmallMutableArray (PrimState m) Any -> Int -> [Int] -> m ()
-    go _ _ [] = pure ()
-    go marr newIx (ix : ixs) = do
-      writeSmallArray marr newIx (indexSmallArray arr (off + ix))
-      go marr (newIx + 1) ixs
-
--- | Modify an entry in the record. \( O(n) \).
-modify :: ∀ e es f. Elem e es => f e -> Rec f es -> Rec f es
-modify x (Rec off len arr) = Rec 0 len $ runSmallArray do
-  marr <- newArr len
-  copySmallArray marr 0 arr off len
-  writeSmallArray marr (reifyIndex @_ @e @es) (toAny x)
-  pure marr
-
--- | Infix version of 'modify'.
-(/~/) :: Elem e es => f e -> Rec f es -> Rec f es
-(/~/) = modify
-infixl 9 /~/
-
--- | Merge a subset into the original record, updating several entries at once. \( O(m+n) \).
-batch :: ∀ es es' f. Subset es es' => Rec f es -> Rec f es' -> Rec f es'
-batch (Rec off _ arr) (Rec off' len' arr') = Rec 0 len' $ runSmallArray do
-  marr <- newArr len'
-  copySmallArray marr 0 arr' off' len'
-  go marr 0 (reifyIndices @_ @es @es')
-  pure marr
-  where
-    go :: PrimMonad m => SmallMutableArray (PrimState m) Any -> Int -> [Int] -> m ()
-    go _ _ [] = pure ()
-    go marr updIx (ix : ixs) = do
-      writeSmallArray marr ix (indexSmallArray arr (off + updIx))
-      go marr (updIx + 1) ixs
-
--- | Infix version of 'batch'.
-(/++/) :: Subset es es' => Rec f es -> Rec f es' -> Rec f es'
-(/++/) = batch
-infixl 9 /++/
-
--- | The type of natural transformations from functor @f@ to @g@.
-type f ~> g = ∀ a. f a -> g a
-infixr 0 ~>
-
--- | Apply a natural transformation to the record. \( O(n) \).
-natural :: (f ~> g) -> Rec f es -> Rec g es
-natural f (Rec off len arr) = Rec 0 len $ runSmallArray do
-  marr <- newArr len
-  go marr 0
-  pure marr
-  where
-    go :: PrimMonad m => SmallMutableArray (PrimState m) Any -> Int -> m ()
-    go marr n
-      | n == len = pure ()
-      | otherwise = do
-        writeSmallArray marr n (toAny $ f $ fromAny $ indexSmallArray arr (off + n))
-        go marr (n + 1)
-
--- | Infix version of 'natural'.
-(<#>) :: (f ~> g) -> Rec f es -> Rec g es
-(<#>) = natural
-infixl 4 <#>
-
--- | Zip two records with a natural transformation. \( O(n) \).
-zipWith :: (∀ x. f x -> g x -> h x) -> Rec f es -> Rec g es -> Rec h es
-zipWith f (Rec off len arr) (Rec off' _ arr') = Rec 0 len $ runSmallArray do
-  marr <- newArr len
-  go marr (0 :: Int)
-  pure marr
-  where
-    go :: PrimMonad m => SmallMutableArray (PrimState m) Any -> Int -> m ()
-    go marr n
-      | n == len = pure ()
-      | otherwise = do
-        writeSmallArray marr n
-          (toAny $ f (fromAny $ indexSmallArray arr (off + n)) (fromAny $ indexSmallArray arr' (off' + n)))
-        go marr (n + 1)
-
--- | Check if a predicate is true on all elements. \( O(n) \).
-all :: (∀ x. f x -> Bool) -> Rec f es -> Bool
-all f (Rec off len arr) = go 0
-  where
-    go n
-      | n == len = True
-      | otherwise = f (fromAny $ indexSmallArray arr (off + n)) && go (n + 1)
-
--- | Check if a predicate is true on at least one element. \( O(n) \).
-any :: (∀ x. f x -> Bool) -> Rec f es -> Bool
-any f (Rec off len arr) = go 0
-  where
-    go n
-      | n == len = False
-      | otherwise = f (fromAny $ indexSmallArray arr (off + n)) || go (n + 1)
-
--- | Convert a record that effectively contains a fixed type into a list of the fixed type. \( O(n) \).
-degenerate :: Rec (Const a) es -> [a]
-degenerate (Rec off len arr) = go 0
-  where
-    go n
-      | n == len = []
-      | otherwise = getConst (fromAny $ indexSmallArray arr (off + n)) : go (n + 1)
-
--- | Map each element to a fixed type. \( O(n) \).
-extract :: (∀ x. f x -> a) -> Rec f es -> [a]
-extract f xs = degenerate $ natural (Const . f) xs
-
--- | Test the size invariant of 'Rec'.
-sizeInvariant :: Rec f es -> Rec f es
-sizeInvariant xs@(Rec off len arr)
-  | tracked == actual = xs
-  | otherwise = error $ "Data.Rec.sizeInvariant: tracked size " <> show tracked <> ", actual size " <> show actual
-  where
-    tracked = len + off
-    actual = sizeofSmallArray arr
-
--- | Test whether all fields of 'Rec' are really set.
-allAccessible :: Rec f es -> Rec f es
-allAccessible xs@(Rec off len arr) = go 0
-  where
-    go n
-      | n == len = xs
-      | otherwise = indexSmallArray arr (off + n) `seq` go (n + 1)
-
--- | Test all invariants.
-invariant :: Rec f es -> Rec f es
-invariant = allAccessible . sizeInvariant
diff --git a/test/RecSpec.hs b/test/RecSpec.hs
deleted file mode 100644
--- a/test/RecSpec.hs
+++ /dev/null
@@ -1,100 +0,0 @@
-module RecSpec where
-
-import           Data.Functor.Identity (Identity (Identity))
-import           Data.Rec              (Rec, invariant, pattern (:++:), pattern (:~:), (/++/), (/~/), (<#>))
-import qualified Data.Rec              as Rec
-import           Data.Typeable         (cast)
-import           Test.Hspec
-
-type I = Identity
-i :: a -> Identity a
-i = Identity
-
-spec :: Spec
-spec = parallel do
-  it "is Typeable" do
-    let
-      x = i (5 :: Int) :~: i False :~: Rec.empty
-      y = cast x :: Maybe (Rec I '[Int, String])
-      z = cast x :: Maybe (Rec I '[Int, Bool])
-    y `shouldBe` Nothing
-    z `shouldBe` Just x
-
-  it "is Read & Show" do
-    let
-      s = "Identity 5 :~: Identity False :~: Identity 'X' :~: Identity (Just 'O') :~: empty"
-      s' = "Identity 5 :~: Identity False :~: Identity 'X' :~: (Identity (Just 'O') :~: (empty))"
-      x = invariant $ read s :: Rec Identity '[Int, Bool, Char, Maybe Char]
-      x' = invariant $ read s' :: Rec Identity '[Int, Bool, Char, Maybe Char]
-    show x `shouldBe` s
-    show x' `shouldBe` s
-
-  it "is Eq" do
-    let
-      x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-      y = invariant $ id <#> x
-      z = invariant $ read "Identity 5 :~: Identity False :~: Identity 'X' :~: Identity (Just 'O') :~: empty"
-        :: Rec Identity '[Int, Bool, Char, Maybe Char]
-    x `shouldBe` y
-    y `shouldBe` z
-
-  it "can be constructed with 'empty', 'singleton', 'cons', 'concat'" do
-    let
-      x = invariant $ i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-      y = invariant $ Rec.singleton (i (5 :: Int)) :++: Rec.singleton (i False)
-        :++: Rec.singleton (i 'X') :++: Rec.singleton (i (Just 'O'))
-      a = invariant $ i (5 :: Int) :~: Rec.singleton (i False)
-      b = invariant $  Rec.singleton (i 'X') :++: Rec.singleton (i (Just 'O'))
-    x `shouldBe` y
-    invariant (a :++: b) `shouldBe` x
-
-  it "can contain multiple fields of the same type" do
-    let
-      x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-      y = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: i (6 :: Int) :~: i (Just 'A') :~: Rec.empty
-    invariant (x :++: 6 :~: i (Just 'A') :~: Rec.empty) `shouldBe` y
-
-  it "can be destructed via 'head', 'tail', 'take', 'drop'" do
-    let
-      a = (x :~: y) :++: Rec.singleton z
-      x = i (5 :: Int)
-      y = i (Rec.singleton $ i False) :~: i 'X' :~: Rec.empty
-      z = i (Just 'O')
-    Rec.head a `shouldBe` x
-    invariant (Rec.drop @'[Int, Rec I '[Bool], Char] a) `shouldBe` Rec.singleton z
-    invariant (Rec.tail a) `shouldBe` invariant (y :++: Rec.singleton z)
-    invariant (Rec.take @'[Int, Rec I '[Bool], Char] a) `shouldBe` (x :~: y)
-
-  it "can get elements via 'index'" do
-    let x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    Rec.index @Int x `shouldBe` 5
-    Rec.index @Bool x `shouldBe` i False
-    Rec.index @Char x `shouldBe` i 'X'
-    Rec.index @(Maybe Char) x `shouldBe` i (Just 'O')
-
-  it "can get the topmost element among the duplicate ones" do
-    let y = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: i (6 :: Int) :~: i (Just 'A') :~: Rec.empty
-    Rec.index @Int y `shouldBe` 5
-    Rec.index @Bool y `shouldBe` i False
-    Rec.index @Char y `shouldBe` i 'X'
-    Rec.index @(Maybe Char) y `shouldBe` i (Just 'O')
-
-  it "can set elements via 'modify'" do
-    let x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    invariant (Rec.modify @Int 6 x) `shouldBe` 6 :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    invariant (i True /~/ x) `shouldBe` 5 :~: i True :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    invariant (i 'O' /~/ x) `shouldBe` 5 :~: i False :~: i 'O' :~: i (Just 'O') :~: Rec.empty
-    invariant (i (Just 'P') /~/ x) `shouldBe` 5 :~: i False :~: i 'X' :~: i (Just 'P') :~: Rec.empty
-
-  it "can get multiple elements via 'pick'" do
-    let x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    invariant (Rec.pick @'[Int, Maybe Char] x) `shouldBe` 5 :~: i (Just 'O') :~: Rec.empty
-
-  it "can reorder elements via 'pick'" do
-    let x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    invariant (Rec.pick @'[Bool, Int, Maybe Char] x) `shouldBe` i False :~: 5 :~: i (Just 'O') :~: Rec.empty
-
-  it "can set multiple fields via 'batch'" do
-    let x = i (5 :: Int) :~: i False :~: i 'X' :~: i (Just 'O') :~: Rec.empty
-    invariant ((i (6 :: Int) :~: i (Just 'X') :~: Rec.empty) /++/ x)
-      `shouldBe` 6 :~: i False :~: i 'X' :~: i (Just 'X') :~: Rec.empty