diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,15 @@
 # Changelog for `cleff`
 
+## 0.3.0.1 (2022-02-28)
+
+### Added
+
+- `makeEffect` is now capable of generating sending functions for operations using concrete `Eff`s for the monad type
+
+### Removed
+
+- Dependency on `rec-smallarray`
+
 ## 0.3.0.1 (2022-02-21)
 
 Clarify changelog: new features that are listed "Unreleased" in 0.3.0.0 changelog are in fact *released*
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -49,13 +49,13 @@
 makeEffect ''Teletype
 
 -- Effect Interpretation via IO
-runTeletypeIO :: IOE :> es => Eff (Teletype ': es) a -> Eff es a
+runTeletypeIO :: IOE :> es => Eff (Teletype : es) a -> Eff es a
 runTeletypeIO = interpretIO \case
   ReadTTY    -> getLine
   WriteTTY s -> putStrLn s
 
 -- Effect interpretation via other pure effects
-runTeletypePure :: [String] -> Eff (Teletype ': es) w -> Eff es [String]
+runTeletypePure :: [String] -> Eff (Teletype : es) w -> Eff es [String]
 runTeletypePure tty = fmap (reverse . snd)
   . runState [] . outputToListState
   . runState tty . inputToListState
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.3.0.1
+version:        0.3.1.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
@@ -48,6 +48,7 @@
       Cleff.Internal.Instances
       Cleff.Internal.Interpret
       Cleff.Internal.Monad
+      Cleff.Internal.Rec
       Cleff.Internal.TH
       Cleff.Mask
       Cleff.Output
@@ -76,7 +77,6 @@
       KindSignatures
       LambdaCase
       NoStarIsType
-      PatternSynonyms
       PolyKinds
       RankNTypes
       RoleAnnotations
@@ -89,7 +89,7 @@
       TypeOperators
       UndecidableInstances
       UnicodeSyntax
-  ghc-options: -Wall -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wpartial-fields -Wunused-type-patterns -Wmissing-export-lists
+  ghc-options: -Wall -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wno-unticked-promoted-constructors -Wpartial-fields -Wunused-type-patterns -Wmissing-export-lists
   build-depends:
       atomic-primops ==0.8.*
     , base >=4.12 && <4.17
@@ -97,14 +97,15 @@
     , exceptions ==0.10.*
     , microlens >=0.1 && <0.5
     , monad-control >=1 && <1.1
-    , primitive >=0.6 && <0.8
-    , rec-smallarray ==0.1.*
+    , primitive >=0.6.4 && <0.8
     , template-haskell >=2.14 && <2.19
     , th-abstraction >=0.2 && <0.5
-    , transformers-base >=0.1 && <0.5
+    , transformers-base ==0.4.*
     , unliftio >=0.2.4 && <0.3
   if flag(dynamic-ioe)
     cpp-options: -DDYNAMIC_IOE
+  if impl(ghc >= 8.8)
+    ghc-options: -Wmissing-deriving-strategies
   default-language: Haskell2010
 
 test-suite cleff-example
@@ -134,7 +135,6 @@
       KindSignatures
       LambdaCase
       NoStarIsType
-      PatternSynonyms
       PolyKinds
       RankNTypes
       RoleAnnotations
@@ -147,7 +147,7 @@
       TypeOperators
       UndecidableInstances
       UnicodeSyntax
-  ghc-options: -Wall -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -Wall -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wno-unticked-promoted-constructors -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       atomic-primops ==0.8.*
     , base >=4.12 && <4.17
@@ -157,14 +157,15 @@
     , extra
     , microlens >=0.1 && <0.5
     , monad-control >=1 && <1.1
-    , primitive >=0.6 && <0.8
-    , rec-smallarray ==0.1.*
+    , primitive >=0.6.4 && <0.8
     , template-haskell >=2.14 && <2.19
     , th-abstraction >=0.2 && <0.5
-    , transformers-base >=0.1 && <0.5
+    , transformers-base ==0.4.*
     , unliftio >=0.2.4 && <0.3
   if flag(dynamic-ioe)
     cpp-options: -DDYNAMIC_IOE
+  if impl(ghc >= 8.8)
+    ghc-options: -Wmissing-deriving-strategies
   default-language: Haskell2010
 
 test-suite cleff-test
@@ -176,6 +177,7 @@
       HigherOrderSpec
       InterposeSpec
       MaskSpec
+      RecSpec
       StateSpec
       ThSpec
       Paths_cleff
@@ -198,7 +200,6 @@
       KindSignatures
       LambdaCase
       NoStarIsType
-      PatternSynonyms
       PolyKinds
       RankNTypes
       RoleAnnotations
@@ -211,7 +212,7 @@
       TypeOperators
       UndecidableInstances
       UnicodeSyntax
-  ghc-options: -Wall -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-deriving-strategies -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
+  ghc-options: -Wall -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wno-unticked-promoted-constructors -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       atomic-primops ==0.8.*
     , base >=4.12 && <4.17
@@ -223,12 +224,13 @@
     , lifted-base
     , microlens >=0.1 && <0.5
     , monad-control >=1 && <1.1
-    , primitive >=0.6 && <0.8
-    , rec-smallarray ==0.1.*
+    , primitive >=0.6.4 && <0.8
     , template-haskell >=2.14 && <2.19
     , th-abstraction >=0.2 && <0.5
-    , transformers-base >=0.1 && <0.5
+    , transformers-base ==0.4.*
     , unliftio >=0.2.4 && <0.3
   if flag(dynamic-ioe)
     cpp-options: -DDYNAMIC_IOE
+  if impl(ghc >= 8.8)
+    ghc-options: -Wmissing-deriving-strategies
   default-language: Haskell2010
diff --git a/example/Filesystem.hs b/example/Filesystem.hs
--- a/example/Filesystem.hs
+++ b/example/Filesystem.hs
@@ -30,7 +30,7 @@
   deriving anyclass (Exception)
 
 -- | Run the 'Filesystem' effect with actual file IO.
-runFilesystemIO :: '[IOE, Error FsError] :>> es => Eff (Filesystem ': es) a -> Eff es a
+runFilesystemIO :: '[IOE, Error FsError] :>> es => Eff (Filesystem : es) a -> Eff es a
 runFilesystemIO = interpret \case
   ReadFile path           -> adapt $ IO.readFile path
   WriteFile path contents -> adapt $ IO.writeFile path contents
@@ -38,7 +38,7 @@
     adapt m = liftIO m `catch` \(e :: IOException) -> throwError $ FsError $ show e
 
 -- | Run the 'Filesystem' effect with a faked filesystem.
-runFilesystemPure :: Error FsError :> es => Map FilePath String -> Eff (Filesystem ': es) a -> Eff es a
+runFilesystemPure :: Error FsError :> es => Map FilePath String -> Eff (Filesystem : es) a -> Eff es a
 runFilesystemPure fs = fmap fst . runState fs . reinterpret \case
   ReadFile path -> maybeM (throwError $ FsError $ "File not found: " ++ show path) pure $ gets (M.lookup path)
   WriteFile path contents -> modify $ M.insert path contents
diff --git a/example/Teletype.hs b/example/Teletype.hs
--- a/example/Teletype.hs
+++ b/example/Teletype.hs
@@ -26,13 +26,13 @@
 -- * Interpretations
 
 -- | Run 'Teletype' via stdio.
-runTeletypeIO :: IOE :> es => Eff (Teletype ': es) a -> Eff es a
+runTeletypeIO :: IOE :> es => Eff (Teletype : es) a -> Eff es a
 runTeletypeIO = interpretIO \case
   ReadTTY    -> getLine
   WriteTTY s -> putStrLn s
 
 -- | Run 'Teletype' from a fixed input list.
-runTeletypePure :: [String] -> Eff (Teletype ': es) w -> Eff es [String]
+runTeletypePure :: [String] -> Eff (Teletype : es) w -> Eff es [String]
 runTeletypePure tty = fmap (reverse . snd)
   . runState [] . outputToListState
   . runState tty . inputToListState
diff --git a/src/Cleff.hs b/src/Cleff.hs
--- a/src/Cleff.hs
+++ b/src/Cleff.hs
@@ -101,7 +101,7 @@
 -- To run an effect @T@, we should use an /interpreter/ of @T@, which is a function that has a type like this:
 --
 -- @
--- runT :: 'Eff' (T ': es) a -> 'Eff' es a
+-- runT :: 'Eff' (T : es) a -> 'Eff' es a
 -- @
 --
 -- Such an interpreter provides an implementation of @T@ and eliminates @T@ from the effect stack. All builtin effects
@@ -116,7 +116,7 @@
 
 -- $definingEffects
 -- An effect should be defined as a GADT and have the kind 'Effect'. Each operation in the effect is a constructor of
--- the effect type. For example, an effect supporting reading/writing files can be as following:
+-- the effect type. For example, an effect supporting reading and writing files can be like this:
 --
 -- @
 -- data Filesystem :: 'Effect' where
@@ -124,32 +124,22 @@
 --   WriteFile :: 'FilePath' -> 'String' -> Filesystem m ()
 -- @
 --
+-- Here, @ReadFile@ is an operation that takes a 'FilePath' and returns a 'String', presumably the content of the file;
+-- @WriteFile@ is an operation that takes a 'FilePath' and a 'String' and returns @()@, meaning it only performs
+-- side effects - presumably writing the 'String' to the file specified.
+--
 -- Operations constructed with these constructors can be performed via the 'send' function. You can also use the
 -- Template Haskell function 'makeEffect' to automatically generate definitions of functions that perform the effects.
--- For example,
---
--- @
--- 'makeEffect' ''Filesystem
--- @
---
--- generates the following definitions:
---
--- @
--- readFile      :: Filesystem ':>' es => 'FilePath' -> 'Eff' es 'String'
--- readFile  x   =  'send' (ReadFile x)
--- writeFile     :: Filesystem ':>' es => 'FilePath' -> 'String' -> 'Eff' es ()
--- writeFile x y =  'send' (WriteFile x y)
--- @
 
 -- $interpretingEffects
--- An effect can be understood as the "grammar" (or /syntax/) of a small language; however we also need to define the
--- "meaning" (or /semantics/) of the language. In other words, we need to specify the implementation of effects.
+-- An effect can be understood as the /syntax/ of a tiny language; however we also need to define the /meaning/ (or
+-- /semantics/) of the language. In other words, we need to specify the implementations of effects.
 --
 -- In an extensible effects system, this is achieved by writing /effect handlers/, which are functions that transforms
 -- operations of one effect into other "more primitive" effects. These handlers can then be used to make interpreters
 -- with library functions that we'll now see.
 --
--- This is very easy to do. For example, for the @Filesystem@ effect
+-- For example, for the @Filesystem@ effect:
 --
 -- @
 -- data Filesystem :: 'Effect' where
@@ -161,26 +151,51 @@
 -- constructors:
 --
 -- @
--- runFilesystemIO :: 'IOE' ':>' es => 'Eff' (Filesystem ': es) a -> 'Eff' es a
+-- runFilesystemIO :: 'IOE' ':>' es => 'Eff' (Filesystem : es) a -> 'Eff' es a
 -- runFilesystemIO = 'interpretIO' \\case
 --   ReadFile path           -> 'readFile' path
 --   WriteFile path contents -> 'writeFile' path contents
 -- @
 --
--- Alternatively, we can also construct an in-memory filesystem in terms of the 'Cleff.State.State' effect via
--- the 'reinterpret' function.
+-- Specifically, a @ReadFile@ operation is mapped to a real 'readFile' IO computation, and similarly a @WriteFile@
+-- operation is mapped to a 'writeFile' computation.
 --
+-- An effect is a set of abstract operations, and naturally, they can have more than one interpretations. Therefore,
+-- here we can also construct an in-memory filesystem that reads from and writes into a 'Cleff.State.State' effect, via
+-- the 'reinterpret' function that adds another effect to the stack for the effect handler to use:
+--
 -- @
--- runFilesystemPure :: 'Cleff.Fail.Fail' ':>' es => 'Data.Map.Map' 'FilePath' 'String' -> 'Eff' (Filesystem ': es) a -> 'Eff' es a
--- runFilesystemPure fs = 'fmap' 'fst' '.' 'Cleff.State.runState' fs '.' 'reinterpret' \\case
+-- filesystemToState
+--   :: 'Cleff.Fail.Fail' ':>' es
+--   => 'Eff' (Filesystem : es) a
+--   -> 'Eff' ('Cleff.State.State' ('Data.Map.Map' 'FilePath' 'String') : es) a
+-- filesystemToState = 'reinterpret' \\case
 --   ReadFile path -> 'Cleff.State.gets' ('Data.Map.lookup' path) >>= \\case
 --     'Nothing'       -> 'fail' ("File not found: " ++ 'show' path)
 --     'Just' contents -> 'pure' contents
 --   WriteFile path contents -> 'Cleff.State.modify' ('Data.Map.insert' path contents)
 -- @
 --
--- These interpreters can then be applied to computations with the @Filesystem@ effect to give different implementations
--- to the effect.
+-- Here, we used the 'reinterpret' function to introduce a @'Cleff.State.State' ('Data.Map.Map' 'FilePath' 'String')@ as
+-- the in-memory filesystem, making 'filesystemToState' a /reinterpreter/ that "maps" an effect into another effect.
+-- We also added a @'Cleff.Fail.Fail' ':>' es@ constraint to our reinterpreter so that we're able to report errors.
+-- To make an /interpreter/ out of this is simple, as we just need to interpret the remaining 'Cleff.State.State'
+-- effect:
+--
+-- @
+-- runFilesystemPure
+--   :: 'Cleff.Fail.Fail' ':>' es
+--   => 'Data.Map.Map' 'FilePath' 'String'
+--   -> 'Eff' (Filesystem : es) a
+--   -> 'Eff' es a
+-- runFilesystemPure fs
+--   = 'fmap' 'fst'           -- runState returns (Eff es (a, s)), so we need to extract the first component to get (Eff es a)
+--   . 'Cleff.State.runState' fs        -- (State (Map FilePath String) : es) ==> es
+--   . 'filesystemToState'  -- (Filesystem : es) ==> (State (Map FilePath String) : es)
+-- @
+--
+-- Both of these interpreters can then be applied to computations with the @Filesystem@ effect to give different
+-- implementations to the effect.
 
 -- $higherOrderEffects
 -- /Higher order effects/ are effects whose operations take other effect computations as arguments. For example, the
@@ -196,9 +211,9 @@
 -- More literally, an high order effect makes use of the monad type paramenter @m@, while a first order effect, like
 -- 'Cleff.State.State', does not.
 --
--- It is harder to write interpreters for higher order effects, because we need to transform computations from
--- arbitrary effect stacks into a specific stack that the effect is currently interpreted into. In other words, they
--- need to thread other effects through themselves. This is why Cleff also provides convenient combinators for doing so.
+-- It is harder to write interpreters for higher order effects, because the operations of these effects carry
+-- computations from arbitrary effect stacks, and we'll need to convert the to the current effect stack that the effect
+-- is being interpreted into. Fortunately, Cleff provides convenient combinators for doing so.
 --
 -- In a 'Handler', you can temporarily "unlift" a computation from an arbitrary effect stack into the current stack via
 -- 'toEff', explicitly change the current effect interpretation in the computation via 'toEffWith', or directly express
diff --git a/src/Cleff/Error.hs b/src/Cleff/Error.hs
--- a/src/Cleff/Error.hs
+++ b/src/Cleff/Error.hs
@@ -150,7 +150,7 @@
 newExcUid = incrCounter 1 excUidSource
 {-# INLINE newExcUid #-}
 
-errorHandler :: ExcUid -> Handler (Error e) (IOE ': es)
+errorHandler :: ExcUid -> Handler (Error e) (IOE : es)
 errorHandler eid = \case
   ThrowError e     -> Exc.throwIO $ ErrorExc eid (toAny e)
   CatchError m' h' -> withToIO \toIO -> liftIO $ catch' eid (toIO m') (toIO . h')
@@ -169,14 +169,14 @@
 -- the same 'runError' handler), the error /will/ be caught in the parent thread even if you don't deal with it in the
 -- forked thread. But if you passed the @Async@ value out of the effect scope and @wait@ed for it elsewhere, the error
 -- will again not be caught. The best choice is /not to pass @Async@ values around randomly/.
-runError :: ∀ e es a. Eff (Error e ': es) a -> Eff es (Either e a)
+runError :: ∀ e es a. Eff (Error e : es) a -> Eff es (Either e a)
 runError m = thisIsPureTrustMe do
   eid <- liftIO newExcUid
   try' eid $ reinterpret (errorHandler eid) m
 {-# INLINE runError #-}
 
 -- | Transform an 'Error' into another. This is useful for aggregating multiple errors into one type.
-mapError :: ∀ e e' es. Error e' :> es => (e -> e') -> Eff (Error e ': es) ~> Eff es
+mapError :: ∀ e e' es. Error e' :> es => (e -> e') -> Eff (Error e : es) ~> Eff es
 mapError f = thisIsPureTrustMe . reinterpret \case
   ThrowError e   -> throwError $ f e
   CatchError m h -> do
diff --git a/src/Cleff/Fail.hs b/src/Cleff/Fail.hs
--- a/src/Cleff/Fail.hs
+++ b/src/Cleff/Fail.hs
@@ -30,13 +30,13 @@
 -- * Interpretations
 
 -- | Run a 'Fail' effect in terms of 'Error'.
-runFail :: Eff (Fail ': es) a -> Eff es (Either String a)
+runFail :: Eff (Fail : es) a -> Eff es (Either String a)
 runFail = runError . reinterpret \case
   Fail msg -> throwError msg
 {-# INLINE runFail #-}
 
 -- | Run a 'Fail' effect in terms of throwing exceptions in 'IO'.
-runFailIO :: IOE :> es => Eff (Fail ': es) ~> Eff es
+runFailIO :: IOE :> es => Eff (Fail : es) ~> Eff es
 runFailIO = interpret \case
   Fail msg -> liftIO $ Fail.fail msg
 {-# INLINE runFailIO #-}
diff --git a/src/Cleff/Fresh.hs b/src/Cleff/Fresh.hs
--- a/src/Cleff/Fresh.hs
+++ b/src/Cleff/Fresh.hs
@@ -42,14 +42,14 @@
 -- value.
 --
 -- @since 0.2.1.0
-freshEnumToState :: Enum a => Eff (Fresh a ': es) ~> Eff (State a ': es)
+freshEnumToState :: Enum a => Eff (Fresh a : es) ~> Eff (State a : es)
 freshEnumToState = reinterpret \case
   Fresh -> state \s -> (s, succ s)
 {-# INLINE freshEnumToState #-}
 
 -- | Interpret a @'Fresh' 'Int'@ effect in terms of @'State' 'Int'@. This is a specialized version of
 -- 'freshEnumToState'.
-freshIntToState :: Eff (Fresh Int ': es) ~> Eff (State Int ': es)
+freshIntToState :: Eff (Fresh Int : es) ~> Eff (State Int : es)
 freshIntToState = freshEnumToState
 {-# INLINE freshIntToState #-}
 
@@ -57,7 +57,7 @@
 -- than 'runFreshUnique'.
 --
 -- @since 0.2.1.0
-runFreshAtomicCounter :: Eff (Fresh Int ': es) ~> Eff es
+runFreshAtomicCounter :: Eff (Fresh Int : es) ~> Eff es
 runFreshAtomicCounter m = thisIsPureTrustMe do
   counter <- liftIO $ newCounter minBound
   reinterpret (\case
@@ -66,7 +66,7 @@
 
 -- | Interpret a @'Fresh' 'Unique'@ effect in terms of IO actions. This is slower than 'runFreshAtomicCounter', but it
 -- won't overflow on @'maxBound' :: 'Int'@.
-runFreshUnique :: IOE :> es => Eff (Fresh Unique ': es) ~> Eff es
+runFreshUnique :: IOE :> es => Eff (Fresh Unique : es) ~> Eff es
 runFreshUnique = interpret \case
   Fresh -> liftIO newUnique
 {-# INLINE runFreshUnique #-}
diff --git a/src/Cleff/Input.hs b/src/Cleff/Input.hs
--- a/src/Cleff/Input.hs
+++ b/src/Cleff/Input.hs
@@ -44,13 +44,13 @@
 -- * Interpretations
 
 -- | Run an 'Input' effect by giving a constant input value.
-runInputConst :: i -> Eff (Input i ': es) ~> Eff es
+runInputConst :: i -> Eff (Input i : es) ~> Eff es
 runInputConst x = interpret \case
   Input -> pure x
 {-# INLINE runInputConst #-}
 
 -- | Run an 'Input' effect by going through a list of values.
-inputToListState :: Eff (Input (Maybe i) ': es) ~> Eff (State [i] ': es)
+inputToListState :: Eff (Input (Maybe i) : es) ~> Eff (State [i] : es)
 inputToListState = reinterpret \case
   Input -> state \case
     []     -> (Nothing, [])
@@ -60,13 +60,13 @@
 -- | Run an 'Input' in terms of a 'Reader'.
 --
 -- @since 0.2.1.0
-inputToReader :: Eff (Input i ': es) ~> Eff (Reader i ': es)
+inputToReader :: Eff (Input i : es) ~> Eff (Reader i : es)
 inputToReader = reinterpret \case
   Input -> ask
 {-# INLINE inputToReader #-}
 
 -- | Run an 'Input' effect by performing a computation for each input request.
-runInputEff :: Eff es i -> Eff (Input i ': es) ~> Eff es
+runInputEff :: Eff es i -> Eff (Input i : es) ~> Eff es
 runInputEff m = interpret \case
   Input -> m
 {-# INLINE runInputEff #-}
@@ -74,7 +74,7 @@
 -- | Transform an 'Input' effect into another one already in the effect stack, by a pure function.
 --
 -- @since 0.2.1.0
-mapInput :: Input i' :> es => (i' -> i) -> Eff (Input i ': es) ~> Eff es
+mapInput :: Input i' :> es => (i' -> i) -> Eff (Input i : es) ~> Eff es
 mapInput f = interpret \case
   Input -> f <$> input
 {-# INLINE mapInput #-}
@@ -82,7 +82,7 @@
 -- | Transform an 'Input' effect into another one already in the effect stack, by an effectful computation.
 --
 -- @since 0.2.1.0
-bindInput :: Input i' :> es => (i' -> Eff es i) -> Eff (Input i ': es) ~> Eff es
+bindInput :: Input i' :> es => (i' -> Eff es i) -> Eff (Input i : es) ~> Eff es
 bindInput f = interpret \case
   Input -> f =<< input
 {-# INLINE bindInput #-}
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
@@ -141,7 +141,7 @@
 -- | Unsafely eliminate an 'IOE' effect from the top of the effect stack. This is mainly for implementing effects that
 -- uses 'IO' but does not do anything really /impure/ (i.e. can be safely used 'unsafeDupablePerformIO' on), such as a
 -- State effect.
-thisIsPureTrustMe :: Eff (IOE ': es) ~> Eff es
+thisIsPureTrustMe :: Eff (IOE : es) ~> Eff es
 thisIsPureTrustMe = interpret \case
 #ifdef DYNAMIC_IOE
   Lift m   -> primLiftIO m
@@ -171,18 +171,53 @@
 -- @
 -- 'interpretIO' f = 'interpret' ('liftIO' '.' f)
 -- @
-interpretIO :: IOE :> es => HandlerIO e es -> Eff (e ': es) ~> Eff es
+interpretIO :: IOE :> es => HandlerIO e es -> Eff (e : es) ~> Eff es
 interpretIO f = interpret (liftIO . f)
 {-# INLINE interpretIO #-}
 
 -- * Combinators for interpreting higher-order effects
 
--- | Temporarily gain the ability to unlift an @'Eff' esSend@ computation into 'IO'. This is useful for dealing with
--- higher-order effects that involves 'IO'.
+-- | Temporarily gain the ability to unlift an @'Eff' esSend@ computation into 'IO'. This is analogous to
+-- 'withRunInIO', and is useful in dealing with higher-order effects that involves 'IO'. For example, the @Resource@
+-- effect that supports bracketing:
+--
+-- @
+-- data Resource m a where
+--   Bracket :: m a -> (a -> m ()) -> (a -> m b) -> Resource m b
+-- @
+--
+-- can be interpreted into 'Control.Exception.bracket' actions in 'IO', by converting all effect computations into
+-- 'IO' computations via 'withToIO':
+--
+-- @
+-- runResource :: 'IOE' ':>' es => 'Eff' (Resource : es) a -> 'Eff' es a
+-- runResource = 'interpret' \\case
+--   Bracket alloc dealloc use -> 'withToIO' $ \\toIO ->
+--     'Control.Exception.bracket' (toIO alloc) (toIO . dealloc) (toIO . use)
+-- @
 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.
+-- | Lift an 'IO' computation into @'Eff' esSend@. This is analogous to 'liftIO', and is only useful in dealing with
+-- effect operations with the monad type in the negative position, for example 'Control.Exception.mask'ing:
+--
+-- @
+-- data Mask :: 'Effect' where
+--   Mask :: ((m '~>' m) -> m a) -> Mask m a
+--                  ^ this "m" is in negative position
+-- @
+--
+-- See how the @restore :: IO a -> IO a@ from 'Control.Exception.mask' is "wrapped" into
+-- @'Eff' esSend a -> 'Eff' esSend a@:
+--
+-- @
+-- runMask :: 'IOE' ':>' es => 'Eff' (Mask : es) a -> 'Eff' es a
+-- runMask = 'interpret' \\case
+--   Mask f -> 'withToIO' $ \\toIO -> 'Control.Exception.mask' $
+--     \\restore -> f ('fromIO' . restore . toIO)
+-- @
+--
+-- Here, @toIO@ from 'withToIO' takes an @'Eff' esSend@ to 'IO', where it can be passed into the @restore@ function,
+-- and the returned 'IO' computation is recovered into 'Eff' with 'fromIO'.
 fromIO :: (Handling esSend e es, IOE :> es) => IO ~> Eff esSend
 fromIO = Eff . const
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
@@ -49,8 +49,8 @@
   ) where
 
 import           Cleff.Internal.Monad
-import           Data.Rec.SmallArray  (Rec, pattern (:++:))
-import qualified Data.Rec.SmallArray  as Rec
+import           Cleff.Internal.Rec   (Rec)
+import qualified Cleff.Internal.Rec   as Rec
 import           Unsafe.Coerce        (unsafeCoerce)
 
 -- * Trivial handling
@@ -62,7 +62,7 @@
 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 :: ∀ e es. Eff es ~> Eff (e : es)
 raise = raiseN @'[e]
 
 -- | Lift a computation into a bigger effect stack with arbitrarily more effects. This function requires
@@ -71,13 +71,13 @@
 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)@:
+-- @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 :: Bar ':>' es => 'Eff' (Foo : es) '~>' 'Eff' es
 -- myInterpreter = ...
 --
--- myReinterpreter :: 'Eff' (Foo ': es) '~>' 'Eff' (Bar ': es)
+-- myReinterpreter :: 'Eff' (Foo : es) '~>' 'Eff' (Bar : es)
 -- myReinterpreter = myInterpreter '.' 'raiseUnder'
 -- @
 --
@@ -92,20 +92,20 @@
 -- more efficient.
 --
 -- @since 0.2.0.0
-raiseUnder :: ∀ e' e es. Eff (e ': es) ~> Eff (e ': e' ': es)
+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@.
 --
 -- @since 0.2.0.0
-raiseNUnder :: ∀ es' e es. KnownList es' => Eff (e ': es) ~> Eff (e ': es' ++ es)
+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@.
 --
 -- @since 0.2.0.0
-raiseUnderN :: ∀ e es' es. KnownList es' => Eff (es' ++ es) ~> Eff (es' ++ e ': es)
+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
@@ -122,12 +122,12 @@
 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
+subsume :: ∀ e es. e :> es => Eff (e : es) ~> Eff es
 subsume = subsumeN @'[e]
 
 -- | 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 = adjust \re -> Rec.pick @es' re :++: re
+subsumeN = adjust \re -> Rec.concat (Rec.pick @es' re) re
 
 -- * Handler types
 
@@ -187,34 +187,36 @@
   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
+interpret :: ∀ e es. Handler e es -> Eff (e : es) ~> Eff es
 interpret = reinterpretN @'[]
 
--- | Like 'interpret', but adds a new effect @e'@ that can be used in the handler.
-reinterpret :: ∀ e' e es. Handler e (e' ': es) -> Eff (e ': es) ~> Eff (e' ': es)
+-- | Like 'interpret', but adds a new effect @e'@ to the stack that can be used in the handler.
+reinterpret :: ∀ e' e es. Handler e (e' : es) -> Eff (e : es) ~> Eff (e' : es)
 reinterpret = reinterpretN @'[e']
 
 -- | Like 'reinterpret', but adds two new effects.
-reinterpret2 :: ∀ e' e'' e es. Handler e (e' ': e'' ': es) -> Eff (e ': es) ~> Eff (e' ': e'' ': es)
+reinterpret2 :: ∀ e' e'' e es. Handler e (e' : e'' : es) -> Eff (e : es) ~> Eff (e' : e'' : es)
 reinterpret2 = reinterpretN @'[e', e'']
 
 -- | Like 'reinterpret', but adds three new effects.
-reinterpret3 :: ∀ e' e'' e''' e es. Handler e (e' ': e'' ': e''' ': es) -> Eff (e ': es) ~> Eff (e' ': e'' ': e''' ': es)
+reinterpret3 :: ∀ e' e'' e''' e es. Handler e (e' : e'' : e''' : es) -> Eff (e : es) ~> Eff (e' : e'' : e''' : es)
 reinterpret3 = reinterpretN @'[e', e'', e''']
 
 -- | 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 :: ∀ es' e es. KnownList es' => Handler e (es' ++ es) -> Eff (e : es) ~> Eff (es' ++ es)
 reinterpretN handle m = Eff \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).
+-- | Respond to an effect, but does not eliminate it from the stack. This means you can re-send the operations in the
+-- effect handler; it is often useful when you need to "intercept" operations so you can add extra behaviors like
+-- logging.
 interpose :: ∀ e es. e :> es => Handler e es -> Eff es ~> Eff es
 interpose = imposeN @'[]
 
 -- | Like 'interpose', but allows to introduce one new effect to use in the handler.
-impose :: ∀ e' e es. e :> es => Handler e (e' ': es) -> Eff es ~> Eff (e' ': es)
+impose :: ∀ e' e es. e :> es => Handler e (e' : es) -> Eff es ~> Eff (e' : es)
 impose = imposeN @'[e']
 
 -- | Like 'impose', but allows introducing arbitrarily many effects. This requires @TypeApplications@.
@@ -231,7 +233,7 @@
 -- @
 -- 'transform' trans = 'interpret' ('sendVia' 'toEff' '.' trans)
 -- @
-transform :: ∀ e e' es. e' :> es => Translator e e' -> Eff (e ': es) ~> Eff es
+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.
@@ -239,22 +241,37 @@
 -- @
 -- 'translate' trans = 'reinterpret' ('sendVia' 'toEff' '.' trans)
 -- @
-translate :: ∀ e e' es. Translator e e' -> Eff (e ': es) ~> Eff (e' ': es)
+translate :: ∀ e e' es. Translator e e' -> Eff (e : es) ~> Eff (e' : es)
 translate trans = reinterpret (sendVia toEff . trans)
 
 -- * Combinators for interpreting higher effects
 
--- | Run a computation in the current effect stack. This is useful for interpreting higher-order effects, like a
--- bracketing effect:
+-- | Run a computation in the current effect stack; this is useful for interpreting higher-order effects. For example,
+-- if you want to interpret a bracketing effects in terms of 'IO':
 --
 -- @
 -- data Resource m a where
 --   Bracket :: m a -> (a -> m ()) -> (a -> m b) -> Resource m b
 -- @
 --
+-- You will not be able to simply write this for the effect:
+--
 -- @
--- Bracket alloc dealloc use ->
---   'UnliftIO.bracket'
+-- runBracket :: IOE ':>' es => 'Eff' (Resource : es) a -> 'Eff' es a
+-- runBracket = 'interpret' \\case
+--   Bracket alloc dealloc use -> UnliftIO.'UnliftIO.bracket' alloc dealloc use
+-- @
+--
+-- This is because effects are sended from all kinds of stacks that has @Resource@ in it, so effect handlers received
+-- the effect as @Resource esSend a@, where @esSend@ is an arbitrary stack with @Resource@, instead of
+-- @Resource es a@. This means @alloc@, @dealloc@ and @use@ are of type @'Eff' esSend a@, while 'UnliftIO.bracket' can
+-- only take and return @'Eff' es a@. So we need to use 'toEff', which converts an @'Eff' esSend a@ into
+-- an @'Eff' es a@:
+--
+-- @
+-- runBracket :: IOE ':>' es => 'Eff' (Resource : es) a -> 'Eff' es a
+-- runBracket = 'interpret' \\case
+--   Bracket alloc dealloc use -> UnliftIO.'UnliftIO.bracket'
 --     ('toEff' alloc)
 --     ('toEff' . dealloc)
 --     ('toEff' . use)
@@ -262,11 +279,12 @@
 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':
+-- | Run a computation in the current effect stack, just like 'toEff', but takes a 'Handler' of the current effect
+-- being interpreted, so that inside the computation being ran, the effect is interpreted differently. This is useful
+-- for interpreting effects with local contexts, like 'Cleff.Reader.Local':
 --
 -- @
--- runReader :: r -> 'Eff' ('Cleff.Reader.Reader' r ': es) '~>' 'Eff' es
+-- runReader :: r -> 'Eff' ('Cleff.Reader.Reader' r : es) '~>' 'Eff' es
 -- runReader x = 'interpret' (handle x)
 --   where
 --     handle :: r -> 'Handler' ('Cleff.Reader.Reader' r) es
@@ -280,8 +298,8 @@
   -- 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.
+-- | Temporarily gain the ability to lift some @'Eff' es@ actions into @'Eff' esSend@. This is only 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 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
@@ -40,14 +40,14 @@
   , sendVia
   ) where
 
-import           Cleff.Internal.Any
+import           Cleff.Internal.Any  (Any, fromAny, toAny)
+import           Cleff.Internal.Rec  (Elem, KnownList, Rec, Subset, type (++))
+import qualified Cleff.Internal.Rec  as Rec
 import           Control.Applicative (Applicative (liftA2))
 import           Control.Monad.Fix   (MonadFix (mfix))
 import           Data.IntMap.Strict  (IntMap)
 import qualified Data.IntMap.Strict  as Map
 import           Data.Kind           (Constraint, Type)
-import           Data.Rec.SmallArray (Elem, KnownList, Rec, Subset, pattern (:~:), type (++), type (~>))
-import qualified Data.Rec.SmallArray as Rec
 
 -- * Basic types
 
@@ -64,9 +64,22 @@
 -- alias for @(e1 ':>' es, ..., en ':>' es)@.
 type family xs :>> es :: Constraint where
   '[] :>> _ = ()
-  (x ': xs) :>> es = (x :> es, xs :>> es)
+  (x : xs) :>> es = (x :> es, xs :>> es)
 infix 0 :>>
 
+-- | A natural transformation from @f@ to @g@. With this, instead of writing
+--
+-- @
+-- runSomeEffect :: 'Eff' (SomeEffect : es) a -> 'Eff' es a
+-- @
+--
+-- you can write:
+--
+-- @
+-- runSomeEffect :: 'Eff' (SomeEffect : es) ~> 'Eff' es
+-- @
+type f ~> g = ∀ a. f a -> g a
+
 -- * The 'Eff' monad
 
 -- | The internal representation of effect handlers. This is just a natural transformation from the effect type
@@ -77,16 +90,21 @@
 newtype InternalHandler e = InternalHandler { runHandler :: ∀ es. e (Eff es) ~> Eff es }
 
 -- | The extensible effects monad. The 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
--- indicate what effects are in the stack. For example,
+-- which is a type-level list that holds all effects available.
 --
+-- The best practice is to always use a polymorphic type variable for the effect stack @es@, and then use the type
+-- operators '(:>)' and '(:>>)' in constraints to indicate what effects are available in the stack. For example,
+--
 -- @
 -- ('Cleff.Reader.Reader' 'String' ':>' es, 'Cleff.State.State' 'Bool' ':>' es) => 'Eff' es 'Integer'
 -- @
 --
 -- means you can perform operations of the @'Cleff.Reader.Reader' 'String'@ effect and the @'Cleff.State.State' 'Bool'@
--- effect in a computation returning an 'Integer'.
+-- effect in a computation returning an 'Integer'. The reason why you should always use a polymorphic effect stack as
+-- opposed to a concrete list of effects are that
+--
+-- * it can contain other effects that are used by computations other than the current one, and
+-- * it does not require you to run the effects in any particular order.
 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'
@@ -129,7 +147,10 @@
 -- 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 #-} !Int {-# UNPACK #-} !(Rec HandlerPtr es) !(IntMap Any)
+data Env (es :: [Effect]) = Env
+  {-# UNPACK #-} !Int
+  {-# UNPACK #-} !(Rec HandlerPtr es)
+  !(IntMap Any)
 
 -- | A pointer to 'InternalHandler' in an 'Env'.
 type role HandlerPtr nominal
@@ -166,8 +187,8 @@
 {-# 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 n re mem) = Env n (HandlerPtr m :~: re) (Map.insert m (toAny x) mem)
+appendEnv :: ∀ e es. HandlerPtr e -> InternalHandler e -> Env es -> Env (e : es)
+appendEnv (HandlerPtr m) x (Env n re mem) = Env n (Rec.cons (HandlerPtr m) re) (Map.insert m (toAny x) mem)
 {-# INLINE appendEnv #-}
 
 -- | Use the state of LHS as a newer version for RHS. \( O(1) \).
diff --git a/src/Cleff/Internal/Rec.hs b/src/Cleff/Internal/Rec.hs
new file mode 100644
--- /dev/null
+++ b/src/Cleff/Internal/Rec.hs
@@ -0,0 +1,183 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# OPTIONS_HADDOCK not-home #-}
+-- |
+-- Copyright: (c) 2021 Xy Ren
+-- License: BSD3
+-- Maintainer: xy.r@outlook.com
+-- Stability: unstable
+-- Portability: non-portable (GHC only)
+--
+-- 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 Cleff.Internal.Rec
+  ( Rec (Rec)
+  , type (++)
+    -- * Construction
+  , empty
+  , cons
+  , concat
+    -- * Deconstruction
+  , KnownList
+  , head
+  , take
+  , tail
+  , drop
+    -- * Retrieval and updating
+  , Elem
+  , Subset
+  , index
+  , pick
+  , update
+    -- * Helpers
+  , newArr
+  ) where
+
+import           Cleff.Internal.Any        (Any, fromAny, toAny)
+import           Control.Monad.ST          (ST)
+import           Data.Kind                 (Type)
+import           Data.Primitive.SmallArray (SmallArray, SmallMutableArray, cloneSmallArray, copySmallArray,
+                                            indexSmallArray, newSmallArray, runSmallArray, thawSmallArray,
+                                            writeSmallArray)
+import           GHC.TypeLits              (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
+import           Prelude                   hiding (all, any, concat, drop, head, length, tail, take, zipWith)
+
+-- | 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.
+
+-- | Create a new 'SmallMutableArray' with no contents.
+newArr :: Int -> ST s (SmallMutableArray s Any)
+newArr len = newSmallArray len $ error
+  "Cleff.Internal.Rec.newArr: Attempting to read an element of the underlying array of a 'Rec'. Please report this \
+  \as a bug."
+
+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."
+
+-- | Create an empty record. \( O(1) \).
+empty :: Rec f '[]
+empty = Rec 0 0 $ runSmallArray $ newArr 0
+
+-- | 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
+
+-- | 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
+
+-- | 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
+
+-- | @'KnownList' es@ means the list @es@ is concrete, i.e. is of the form @'[a1, a2, ..., an]@ instead of a type
+-- variable.
+class KnownList (es :: [k]) where
+  -- | Get the length of the list.
+  reifyLen :: Int
+  reifyLen = unreifiable "KnownList" "Cleff.Internal.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 $ cloneSmallArray arr off len
+  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" "Cleff.Internal.Rec.reifyIndex" "the index of an element of a type-level list"
+
+-- | The element closer to the head takes priority.
+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
+    "Cleff.Internal.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'@, i.e. all elements of @es@ are in @es'@.
+class KnownList es => Subset (es :: [k]) (es' :: [k]) where
+  -- | Get a list of indices of the elements.
+  reifyIndices :: [Int]
+  reifyIndices = unreifiable
+    "Subset" "Cleff.Internal.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 :: SmallMutableArray s Any -> Int -> [Int] -> ST s ()
+    go _ _ [] = pure ()
+    go marr newIx (ix : ixs) = do
+      writeSmallArray marr newIx $ indexSmallArray arr (off + ix)
+      go marr (newIx + 1) ixs
+
+-- | Update an entry in the record. \( O(n) \).
+update :: ∀ e es f. Elem e es => f e -> Rec f es -> Rec f es
+update x (Rec off len arr) = Rec 0 len $ runSmallArray do
+  marr <- thawSmallArray arr off len
+  writeSmallArray marr (reifyIndex @_ @e @es) (toAny x)
+  pure marr
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
@@ -28,22 +28,29 @@
 import           Prelude                      hiding ((<>))
 
 -- | For a datatype @T@ representing an effect, @'makeEffect' T@ generates functions defintions for performing the
--- operations of @T@ via 'send'. The naming rule is changing the first uppercase letter in the constructor name to
--- lowercase or removing the @:@ symbol in the case of operator constructors. Also, this function will preserve any
--- fixity declarations defined on the constructors.
+-- operations of @T@ via 'send'. For example,
 --
--- Because of the limitations of Template Haskell, all constructors of @T@ should be /polymorphic in the monad type/,
--- if they are to be used by 'makeEffect'. For example, this is not OK:
+-- @
+-- 'makeEffect' ''Filesystem
+-- @
 --
+-- generates the following definitions:
+--
 -- @
--- data Limited :: 'Effect' where
---   Noop :: Limited ('Eff' es) ()
+-- readFile      :: Filesystem ':>' es => 'FilePath' -> 'Eff' es 'String'
+-- readFile  x   =  'send' (ReadFile x)
+-- writeFile     :: Filesystem ':>' es => 'FilePath' -> 'String' -> 'Eff' es ()
+-- writeFile x y =  'send' (WriteFile x y)
 -- @
 --
--- because the monad type @'Eff' es@ is not a fully polymorphic type variable.
+-- The naming rule is changing the first uppercase letter in the constructor name to lowercase or removing the @:@
+-- symbol in the case of operator constructors. Also, this function will preserve any fixity declarations defined on
+-- the constructors.
 --
+-- === Technical details
+--
 -- This function is also "weaker" than @polysemy@'s @makeSem@, because this function cannot properly handle some
--- cases involving complex higher order effects. Those cases are rare, though. See the tests for more details.
+-- cases involving ambiguous types. Those cases are rare, though. See the @ThSpec@ test spec for more details.
 makeEffect :: Name -> Q [Dec]
 makeEffect = makeSmartCons True
 
@@ -66,67 +73,87 @@
 -- | This is the function underlying 'makeEffect' and 'makeEffect_'. You can switch between the behavior of two by
 -- changing the 'Bool' parameter to 'True' (generating signatures) or 'False' (not generating signatures).
 makeSmartCons :: Bool -> Name -> Q [Dec]
-makeSmartCons makeSig effName = do
+makeSmartCons shouldMakeSig effName = do
   info <- reifyDatatype effName
-  join <$> traverse (makeCon makeSig) (constructorName <$> reverse (datatypeCons info))
+  join <$> traverse (makeCon shouldMakeSig) (constructorName <$> reverse (datatypeCons info))
 
 -- | Make a single function definition of a certain effect operation.
 makeCon :: Bool -> Name -> Q [Dec]
-makeCon makeSig name = do
+makeCon shouldMakeSig name = do
   fixity <- reifyFixity name
-  typ <- reify name >>= \case
-    DataConI _ typ _ -> pure typ
-    _ -> fail $ show
-      $ text "'" <> ppr name <> text "' is not a constructor"
+  ctorTy <- reify name >>= \case
+    DataConI _ ty _ -> pure ty
+    _               -> fail $ show $ text "'" <> ppr name <> text "' is not a constructor"
 
-  effVar <- VarT <$> newName "es"
+  operationCtx' <- extractCtx ctorTy
+  (operationParams', (effTy, effMonad, resTy')) <- extractParams ctorTy
 
-  let actionCtx = extractCtx typ
-  (actionPar, (effTy, monadVar, resTy)) <- extractPar typ
+  (esVar, maybeMndVar) <- case effMonad of
+    Right m -> do
+      fresh <- VarT <$> newName "es"
+      pure (fresh, Just m)
+    Left v -> pure (VarT v, Nothing)
 
+  let operationCtx = substMnd maybeMndVar esVar <$> operationCtx'
+  let operationParams = substMnd maybeMndVar esVar <$> operationParams'
+  let resTy = substMnd maybeMndVar esVar resTy'
+
   let fnName = mkName $ toSmartConName $ nameBase name
-  fnArgs <- traverse (const $ newName "x") actionPar
+  fnArgs <- traverse (const $ newName "x") operationParams
 
   let
     fnBody = VarE 'send `AppE` foldl' (\f -> AppE f . VarE) (ConE name) fnArgs
-    fnSig = ForallT [] (UInfixT effTy ''(:>) effVar : actionCtx)
-      (makeTyp actionPar effVar effTy monadVar resTy)
+    fnSig = ForallT [] (UInfixT effTy ''(:>) esVar : operationCtx)
+      (makeTyp operationParams esVar effTy resTy)
 
   pure $
     maybeToList ((`InfixD` name) <$> fixity) ++
-    [ SigD fnName fnSig | makeSig ] ++
+    [ SigD fnName fnSig | shouldMakeSig ] ++
     [ FunD fnName [Clause (VarP <$> fnArgs) (NormalB fnBody) []] ]
 
   where
+    -- Uncapitalize the first letter / remove the ':' in operator constructors
+    toSmartConName :: String -> String
     toSmartConName (':' : xs) = xs
     toSmartConName (x : xs)   = toLower x : xs
     toSmartConName _          = error "Cleff.makeEffect: Empty constructor name. Please report this as a bug."
 
-    extractCtx (ForallT _ ctx t) = ctx ++ extractCtx t
-    extractCtx _                 = []
+    -- Extract constraints for the constructor (the type is normalized so we don't need to extract recursively)
+    extractCtx :: Type -> Q Cxt
+    extractCtx (ForallT _ ctx _) = pure ctx
+    extractCtx ty = fail $ show $ text "The constructor with type'" <> ppr ty <> text "' does not construct an effect"
 
-    extractPar (ForallT _ _ t) = extractPar t
-    extractPar (SigT t _) = extractPar t
-    extractPar (ParensT t) = extractPar t
-    extractPar (ArrowT `AppT` a `AppT` t) = do
-      (args, ret) <- extractPar t
+    -- Extract (parameter types, (effect type, Eff es / m variable, return type))
+    extractParams :: Type -> Q ([Type], (Type, Either Name Name, Type))
+    extractParams (ForallT _ _ t) = extractParams t
+    extractParams (SigT t _) = extractParams t
+    extractParams (ParensT t) = extractParams t
+    extractParams (ArrowT `AppT` a `AppT` t) = do
+      (args, ret) <- extractParams t
       pure (a : args, ret)
 #if MIN_VERSION_template_haskell(2,17,0)
-    extractPar (MulArrowT `AppT` _ `AppT` a `AppT` t) = do
-      (args, ret) <- extractPar t
+    extractParams (MulArrowT `AppT` _ `AppT` a `AppT` t) = do
+      (args, ret) <- extractParams t
       pure (a : args, ret)
 #endif
-
-    extractPar (effTy `AppT` VarT monadVar `AppT` resTy) = pure ([], (effTy, monadVar, resTy))
-    extractPar ty@(_ `AppT` m `AppT` _) = fail $ show
+    extractParams (effTy `AppT` VarT mndVar `AppT` resTy) = pure ([], (effTy, Right mndVar, resTy))
+    extractParams (effTy `AppT` (ConT eff `AppT` VarT esVar) `AppT` resTy)
+      | eff == ''Eff = pure ([], (effTy, Left esVar, resTy))
+    extractParams ty@(_ `AppT` m `AppT` _) = fail $ show
       $ text "The effect monad argument '" <> ppr m
-      <> text "' in the effect '" <> ppr ty <> text "' is not a type variable"
-    extractPar t = fail $ show
+      <> text "' in the effect '" <> ppr ty <> text "' is not a type variable nor in shape 'Eff es'"
+    extractParams t = fail $ show
       $ text "The type '" <> ppr t
       <> text "' does not have the shape of an effect (i.e. has a polymorphic monad type and a result type)"
 
-    makeTyp [] effVar _ _ resTy = ConT ''Eff `AppT` effVar `AppT` resTy
-    makeTyp (parTy : pars) effVar effTy monadVar resTy =
-      ArrowT `AppT` substMnd monadVar effVar parTy `AppT` makeTyp pars effVar effTy monadVar resTy
+    -- Make the type of the smart constructor from params, effect row variable, effect type and result type
+    -- Example: a -> m b -> c -> MyEffect m d ==> a -> Eff es b -> c -> Eff es d
+    makeTyp :: [Type] -> Type -> Type -> Type -> Type
+    makeTyp [] esVar _ resTy = ConT ''Eff `AppT` esVar `AppT` resTy
+    makeTyp (parTy : pars) esVar effTy resTy =
+      ArrowT `AppT` parTy `AppT` makeTyp pars esVar effTy resTy
 
-    substMnd monadVar effVar = applySubstitution (Map.singleton monadVar $ ConT ''Eff `AppT` effVar)
+    -- Substitute in 'Eff es' for the 'm' variable
+    substMnd :: Maybe Name -> Type -> Type -> Type
+    substMnd Nothing _           = id
+    substMnd (Just mndVar) esVar = applySubstitution (Map.singleton mndVar $ ConT ''Eff `AppT` esVar)
diff --git a/src/Cleff/Mask.hs b/src/Cleff/Mask.hs
--- a/src/Cleff/Mask.hs
+++ b/src/Cleff/Mask.hs
@@ -135,7 +135,7 @@
 -- * Interpretations
 
 -- | Interpret the 'Mask' effect in terms of primitive 'IO' actions.
-runMask :: Eff (Mask ': es) ~> Eff es
+runMask :: Eff (Mask : es) ~> Eff es
 runMask = thisIsPureTrustMe . reinterpret \case
   Mask f -> withToIO \toIO -> Exc.mask \restore -> toIO $ f (fromIO . restore . toIO)
   UninterruptibleMask f -> withToIO \toIO -> Exc.uninterruptibleMask \restore -> toIO $ f (fromIO . restore . toIO)
diff --git a/src/Cleff/Output.hs b/src/Cleff/Output.hs
--- a/src/Cleff/Output.hs
+++ b/src/Cleff/Output.hs
@@ -40,25 +40,25 @@
 
 -- | Run an 'Output' effect by accumulating a list. Note that outputs are being prepended to the head of the list, so
 -- in many cases you would want to 'reverse' the result.
-outputToListState :: Eff (Output o ': es) ~> Eff (State [o] ': es)
+outputToListState :: Eff (Output o : es) ~> Eff (State [o] : es)
 outputToListState = reinterpret \case
   Output x -> modify (x :)
 {-# INLINE outputToListState #-}
 
 -- | Run an 'Output' effect by translating it into a 'Writer'.
-outputToWriter :: (o -> o') -> Eff (Output o ': es) ~> Eff (Writer o' ': es)
+outputToWriter :: (o -> o') -> Eff (Output o : es) ~> Eff (Writer o' : es)
 outputToWriter f = reinterpret \case
   Output x -> tell $ f x
 {-# INLINE outputToWriter #-}
 
 -- | Ignore outputs of an 'Output' effect altogether.
-ignoreOutput :: Eff (Output o ': es) ~> Eff es
+ignoreOutput :: Eff (Output o : es) ~> Eff es
 ignoreOutput = interpret \case
   Output _ -> pure ()
 {-# INLINE ignoreOutput #-}
 
 -- | Run an 'Output' effect by performing a computation for each output.
-runOutputEff :: (o -> Eff es ()) -> Eff (Output o ': es) ~> Eff es
+runOutputEff :: (o -> Eff es ()) -> Eff (Output o : es) ~> Eff es
 runOutputEff m = interpret \case
   Output x -> m x
 {-# INLINE runOutputEff #-}
@@ -66,7 +66,7 @@
 -- | Transform an 'Output' effect into another one already in the effect stack, by a pure function.
 --
 -- @since 0.2.1.0
-mapOutput :: Output o' :> es => (o -> o') -> Eff (Output o ': es) ~> Eff es
+mapOutput :: Output o' :> es => (o -> o') -> Eff (Output o : es) ~> Eff es
 mapOutput f = interpret \case
   Output x -> output $ f x
 {-# INLINE mapOutput #-}
@@ -74,7 +74,7 @@
 -- | Transform an 'Output' effect into another one already in the effect stack, by an effectful computation.
 --
 -- @since 0.2.1.0
-bindOutput :: Output o' :> es => (o -> Eff es o') -> Eff (Output o ': es) ~> Eff es
+bindOutput :: Output o' :> es => (o -> Eff es o') -> Eff (Output o : es) ~> Eff es
 bindOutput f = interpret \case
   Output x -> output =<< f x
 {-# INLINE bindOutput #-}
diff --git a/src/Cleff/Reader.hs b/src/Cleff/Reader.hs
--- a/src/Cleff/Reader.hs
+++ b/src/Cleff/Reader.hs
@@ -48,7 +48,7 @@
 -- * Interpretations
 
 -- | Run a 'Reader' effect with a given environment value.
-runReader :: r -> Eff (Reader r ': es) ~> Eff es
+runReader :: r -> Eff (Reader r : es) ~> Eff es
 runReader x = interpret (h x)
   where
     h :: r -> Handler (Reader r) es
@@ -58,7 +58,7 @@
 {-# INLINE runReader #-}
 
 -- | Run a 'Reader' effect in terms of a larger 'Reader' via a 'Lens''.
-magnify :: Reader t :> es => Lens' t r -> Eff (Reader r ': es) ~> Eff es
+magnify :: Reader t :> es => Lens' t r -> Eff (Reader r : es) ~> Eff es
 magnify field = interpret \case
   Ask       -> asks (^. field)
   Local f m -> local (& field %~ f) $ toEff m
diff --git a/src/Cleff/State.hs b/src/Cleff/State.hs
--- a/src/Cleff/State.hs
+++ b/src/Cleff/State.hs
@@ -86,7 +86,7 @@
 --
 -- 'runState' will stop taking care of state operations done on forked threads as soon as the main thread finishes its
 -- computation. Any state operation done /before main thread finishes/ is still taken into account.
-runState :: s -> Eff (State s ': es) a -> Eff es (a, s)
+runState :: s -> Eff (State s : es) a -> Eff es (a, s)
 runState s m = thisIsPureTrustMe do
   rs <- newIORef s
   x <- reinterpret (handleIORef rs) m
@@ -97,14 +97,14 @@
 -- | Run the 'State' effect in terms of operations on a supplied 'IORef'. The 'state' operation is atomic.
 --
 -- @since 0.2.1.0
-runStateIORef :: IOE :> es => IORef s -> Eff (State s ': es) a -> Eff es a
+runStateIORef :: IOE :> es => IORef s -> Eff (State s : es) a -> Eff es a
 runStateIORef rs = interpret $ handleIORef rs
 {-# INLINE runStateIORef #-}
 
 -- | Run the 'State' effect in terms of operations on a supplied 'MVar'.
 --
 -- @since 0.2.1.0
-runStateMVar :: IOE :> es => MVar s -> Eff (State s ': es) a -> Eff es a
+runStateMVar :: IOE :> es => MVar s -> Eff (State s : es) a -> Eff es a
 runStateMVar rs = interpret \case
   Get     -> readMVar rs
   Put s'  -> void $ swapMVar rs s'
@@ -114,7 +114,7 @@
 -- | Run the 'State' effect in terms of operations on a supplied 'TVar'.
 --
 -- @since 0.2.1.0
-runStateTVar :: IOE :> es => TVar s -> Eff (State s ': es) a -> Eff es a
+runStateTVar :: IOE :> es => TVar s -> Eff (State s : es) a -> Eff es a
 runStateTVar rs = interpret \case
   Get -> readTVarIO rs
   Put s' -> atomically $ writeTVar rs s'
@@ -126,7 +126,7 @@
 {-# INLINE runStateTVar #-}
 
 -- | Run a 'State' effect in terms of a larger 'State' via a 'Lens''.
-zoom :: State t :> es => Lens' t s -> Eff (State s ': es) ~> Eff es
+zoom :: State t :> es => Lens' t s -> Eff (State s : es) ~> Eff es
 zoom field = interpret \case
   Get     -> gets (^. field)
   Put s   -> modify (& field .~ s)
diff --git a/src/Cleff/Trace.hs b/src/Cleff/Trace.hs
--- a/src/Cleff/Trace.hs
+++ b/src/Cleff/Trace.hs
@@ -38,29 +38,29 @@
 -- * Interpretations
 
 -- | Run the 'Trace' effect by writing to a 'Handle'.
-runTraceHandle :: IOE :> es => Handle -> Eff (Trace ': es) a -> Eff es a
+runTraceHandle :: IOE :> es => Handle -> Eff (Trace : es) a -> Eff es a
 runTraceHandle h = interpretIO \case
   Trace s -> hPutStrLn h s
 {-# INLINE runTraceHandle #-}
 
 -- | Run the 'Trace' effect by writing to 'stdout'.
-runTraceStdout :: IOE :> es => Eff (Trace ': es) ~> Eff es
+runTraceStdout :: IOE :> es => Eff (Trace : es) ~> Eff es
 runTraceStdout = runTraceHandle stdout
 {-# INLINE runTraceStdout #-}
 
 -- | Run the 'Trace' effect by writing to 'stderr'.
-runTraceStderr :: IOE :> es => Eff (Trace ': es) ~> Eff es
+runTraceStderr :: IOE :> es => Eff (Trace : es) ~> Eff es
 runTraceStderr = runTraceHandle stderr
 {-# INLINE runTraceStderr #-}
 
 -- | Run the 'Trace' effect by ignoring all outputs altogether.
-ignoreTrace :: Eff (Trace ': es) ~> Eff es
+ignoreTrace :: Eff (Trace : es) ~> Eff es
 ignoreTrace = interpret \case
   Trace _ -> pure ()
 {-# INLINE ignoreTrace #-}
 
 -- | Transform the 'Trace' effect into an @'Output' 'String'@ effect.
-traceToOutput :: Eff (Trace ': es) ~> Eff (Output String ': es)
+traceToOutput :: Eff (Trace : es) ~> Eff (Output String : es)
 traceToOutput = reinterpret \case
   Trace s -> output s
 {-# INLINE traceToOutput #-}
diff --git a/src/Cleff/Writer.hs b/src/Cleff/Writer.hs
--- a/src/Cleff/Writer.hs
+++ b/src/Cleff/Writer.hs
@@ -60,14 +60,14 @@
 -- Both 'runWriter' and 'listen's under 'runWriter' will stop taking care of writer operations done on
 -- forked threads as soon as the main thread finishes its computation. Any writer operation done
 -- /before main thread finishes/ is still taken into account.
-runWriter :: ∀ w es a. Monoid w => Eff (Writer w ': es) a -> Eff es (a, w)
+runWriter :: ∀ w es a. Monoid w => Eff (Writer w : es) a -> Eff es (a, w)
 runWriter 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 :: [IORef w] -> Handler (Writer w) (IOE : es)
     h rws = \case
       Tell w' -> traverse_ (\rw -> liftIO $ atomicModifyIORefCAS_ rw (<> w')) rws
       Listen m' -> do
@@ -94,14 +94,14 @@
 -- of 'runWriter'.
 --
 -- @since 0.2.0.0
-runWriterBatch :: ∀ w es a. Monoid w => Eff (Writer w ': es) a -> Eff es (a, w)
+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 :: IORef w -> Handler (Writer w) (IOE : es)
     h rw = \case
       Tell w' -> liftIO $ atomicModifyIORefCAS_ rw (<> w')
       Listen m' -> do
diff --git a/test/RecSpec.hs b/test/RecSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/RecSpec.hs
@@ -0,0 +1,130 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+module RecSpec where
+
+import           Cleff.Internal.Rec        (Elem, Rec (Rec), type (++))
+import qualified Cleff.Internal.Rec        as Rec
+import           Data.Functor.Identity     (Identity (Identity))
+import           Data.Primitive.SmallArray (indexSmallArray, sizeofSmallArray)
+import           Data.Typeable             (cast)
+import           Test.Hspec
+
+type I = Identity
+i :: a -> Identity a
+i = Identity
+
+-- | Test the size invariant of 'Rec'.
+sizeInvariant :: Rec f es -> Rec f es
+sizeInvariant xs@(Rec off len arr)
+  | tracked == actual = xs
+  | otherwise = error $
+    "Cleff.Internal.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
+
+singleton :: f e -> Rec f '[e]
+singleton x = x <:> Rec.empty
+
+(<:>) :: f e -> Rec f es -> Rec f (e : es)
+(<:>) = Rec.cons
+infixr 5 <:>
+
+(<++>) :: Rec f es -> Rec f es' -> Rec f (es ++ es')
+(<++>) = Rec.concat
+infixr 5 <++>
+
+(<//>) :: Elem e es => f e -> Rec f es -> Rec f es
+(<//>) = Rec.update
+infixr 9 <//>
+
+instance Eq (Rec f '[]) where
+  _ == _ = True
+
+instance (Eq (Rec f xs), Eq (f x)) => Eq (Rec f (x : xs)) where
+  xs == ys = Rec.head xs == Rec.head ys && Rec.tail xs == Rec.tail ys
+
+instance Show (Rec f '[]) where
+  show _ = "empty"
+
+instance (Show (f x), Show (Rec f xs)) => Show (Rec f (x : xs)) where
+  showsPrec p xs = showParen (p > consPrec) $
+    showsPrec (consPrec + 1) (Rec.head xs) . showString " <:> " . showsPrec consPrec (Rec.tail xs)
+    where consPrec = 5
+
+spec :: Spec
+spec = describe "Rec (SmallArray)" $ 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 "can be constructed with 'empty', 'cons', 'concat'" do
+    let
+      x = invariant $ i (5 :: Int) <:> i False <:> i 'X' <:> i (Just 'O') <:> Rec.empty
+      y = invariant $ singleton (i (5 :: Int)) <++> singleton (i False)
+        <++> singleton (i 'X') <++> singleton (i (Just 'O'))
+      a = invariant $ i (5 :: Int) <:> singleton (i False)
+      b = invariant $  singleton (i 'X') <++> 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) <++> singleton z
+      x = i (5 :: Int)
+      y = i (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` singleton z
+    invariant (Rec.tail a) `shouldBe` invariant (y <++> 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 'update'" do
+    let x = i (5 :: Int) <:> i False <:> i 'X' <:> i (Just 'O') <:> Rec.empty
+    invariant (Rec.update @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
diff --git a/test/ThSpec.hs b/test/ThSpec.hs
--- a/test/ThSpec.hs
+++ b/test/ThSpec.hs
@@ -1,11 +1,10 @@
-
 -- | This module is adapted from https://github.com/arybczak/effectful/blob/master/effectful/tests/ThEffectSpec.hs,
 -- originally BSD3 license, authors Andrzej Rybczak et al.
 module ThSpec where
 
 import           Cleff
 import           Data.Kind    (Type)
-import           GHC.TypeLits
+import           GHC.TypeLits (KnownNat, Nat, type (+))
 import           Test.Hspec
 
 spec :: Spec
@@ -70,8 +69,8 @@
   MMIC1 :: f m -> Family 'MMI m (f m)
   MMIC2 :: (∀ x. m x -> m (f m)) -> Family 'MMI m (f m)
 
--- TODO(daylily): This cannot produce desired result.
--- makeEffect 'MMIC1
+-- Generates correctly since 0.3.1.0
+makeEffect 'MMIC1
 
 data Complex m a where
   Mono            :: Int -> Complex m Bool
@@ -127,3 +126,9 @@
   ByFieldC :: { byFieldCF :: Int } -> ByField m Int
 
 makeEffect 'byFieldCF
+
+data PartialMonad m a where
+  ImpartialMonad :: Int -> PartialMonad m ()
+  PartialMonad :: IOE :> es => Int -> Eff es () -> PartialMonad (Eff es) ()
+
+makeEffect ''PartialMonad