diff --git a/README.md b/README.md
index dffc1bc..da017e9 100644
--- a/README.md
+++ b/README.md
@@ -264,7 +264,7 @@ This results in minimal surprise to the mental model of the code reader.
 * Since the representation of effectful programs in Heftia is simply a monad (`Eff`), it can be used as the base monad for transformers.
     This means you can stack any transformer on top of it.
 
-* The `Eff` monad is an instance of `MonadIO`, `MonadUnliftIO`, `Alternative`, etc., and these behave as the senders for the embedded `IO` or the effect GADTs defined in [data-effects](https://github.com/sayo-hs/data-effects).
+* The `Eff` monad is an instance of `MonadIO`, `MonadError`, `MonadRWS`, `MonadUnliftIO`, `Alternative`, etc., and these behave as the senders for the embedded `IO` or the effect GADTs defined in [data-effects](https://github.com/sayo-hs/data-effects).
 
 ## Future Plans
 * Enriching the documentation and tests
diff --git a/cabal.project b/cabal.project
index 782b750..d402e84 100644
--- a/cabal.project
+++ b/cabal.project
@@ -5,7 +5,7 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/sayo-hs/data-effects
-    tag: 7c4aec97857fd0a98e2bd1f628280c677c723a57
+    tag: 7090527d2f44e1f7243ed3b4310713e8b77ddc98
     subdir: data-effects-core
     subdir: data-effects-th
     subdir: data-effects
diff --git a/heftia-effects/heftia-effects.cabal b/heftia-effects/heftia-effects.cabal
index 5e92f6e..b3abead 100644
--- a/heftia-effects/heftia-effects.cabal
+++ b/heftia-effects/heftia-effects.cabal
@@ -56,6 +56,11 @@ common common-base
         base >= 4.16 && < 4.21,
         data-effects ^>= 0.1.2,
         heftia ^>= 0.4,
+        time,
+        unliftio,
+        unbounded-delays,
+        ghc-typelits-knownnat,
+        containers,
 
     ghc-options: -Wall -fplugin GHC.TypeLits.KnownNat.Solver
 
@@ -72,8 +77,6 @@ library
         Control.Effect.Interpreter.Heftia.Coroutine
         Control.Effect.Interpreter.Heftia.Input
         Control.Effect.Interpreter.Heftia.Output
-        Control.Effect.Interpreter.Heftia.Provider
-        Control.Effect.Interpreter.Heftia.Provider.Implicit
         Control.Effect.Interpreter.Heftia.Resource
         Control.Effect.Interpreter.Heftia.Unlift
         Control.Effect.Interpreter.Heftia.KVStore
@@ -167,7 +170,7 @@ executable Logging
     build-depends:
         heftia-effects,
         text >= 2.0 && < 2.2,
-        time ^>= 1.11.1,
+        time,
 
 executable Continuation
     import: common-base
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Concurrent/Timer.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Concurrent/Timer.hs
index c36cd93..d2db9a0 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Concurrent/Timer.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Concurrent/Timer.hs
@@ -1,30 +1,26 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 module Control.Effect.Interpreter.Heftia.Concurrent.Timer where
 
 import Control.Concurrent.Thread.Delay qualified as Thread
 import Control.Effect (sendIns, type (~>))
-import Control.Effect.ExtensibleFinal (type (:!!))
-import Control.Effect.Hefty (interposeRec, interpret, interpretRec, raise, raiseUnder)
 import Control.Effect.Interpreter.Heftia.Coroutine (runCoroutine)
 import Control.Effect.Interpreter.Heftia.State (evalState)
-import Data.Effect.Concurrent.Timer (CyclicTimer (Wait), LCyclicTimer, LTimer, Timer (..), clock, cyclicTimer)
+import Control.Monad.Hefty (interposeRec, interpret, interpretRec, raiseN, raiseNUnder, (:!!), type (<|))
+import Data.Effect.Concurrent.Timer (CyclicTimer (Wait), Timer (..), clock, cyclicTimer)
 import Data.Effect.Coroutine (Status (Coroutine, Done))
 import Data.Effect.State (get, put)
 import Data.Function ((&))
-import Data.Hefty.Extensible (ForallHFunctor, type (<|))
 import Data.Time (DiffTime)
 import Data.Time.Clock (diffTimeToPicoseconds, picosecondsToDiffTime)
 import Data.Void (Void, absurd)
 import GHC.Clock (getMonotonicTimeNSec)
 import UnliftIO (liftIO)
 
-runTimerIO ::
-    forall eh ef.
-    (IO <| ef, ForallHFunctor eh) =>
-    eh :!! LTimer ': ef ~> eh :!! ef
+runTimerIO
+    :: forall eh ef
+     . (IO <| ef)
+    => eh :!! Timer ': ef ~> eh :!! ef
 runTimerIO =
     interpretRec \case
         Clock -> do
@@ -33,18 +29,19 @@ runTimerIO =
         Sleep t ->
             Thread.delay (diffTimeToPicoseconds t `quot` 1000_000) & liftIO
 
-runCyclicTimer :: forall ef. Timer <| ef => '[] :!! LCyclicTimer ': ef ~> '[] :!! ef
+runCyclicTimer :: forall ef. (Timer <| ef) => '[] :!! CyclicTimer ': ef ~> '[] :!! ef
 runCyclicTimer a = do
     timer0 :: Status ('[] :!! ef) () DiffTime Void <- runCoroutine cyclicTimer
-    a & raiseUnder
+    a
+        & raiseNUnder @1 @1
         & interpret \case
             Wait delta ->
                 get @(Status ('[] :!! ef) () DiffTime Void) >>= \case
                     Done x -> absurd x
-                    Coroutine () k -> put =<< raise (k delta)
+                    Coroutine () k -> put =<< raiseN @1 (k delta)
         & evalState timer0
 
-restartClock :: (Timer <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
+restartClock :: (Timer <| ef) => eh :!! ef ~> eh :!! ef
 restartClock a = do
     t0 <- clock
     a & interposeRec \case
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Coroutine.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Coroutine.hs
index 187ede0..2ad26e8 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Coroutine.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Coroutine.hs
@@ -1,17 +1,13 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 module Control.Effect.Interpreter.Heftia.Coroutine where
 
-import Control.Effect.Hefty (Eff, interpretK)
-import Control.Monad.Freer (MonadFreer)
-import Data.Effect.Coroutine (LYield, Status (Coroutine, Done), Yield (Yield))
-import Data.Hefty.Union (Union)
+import Control.Monad.Hefty.Interpret (interpretBy)
+import Control.Monad.Hefty.Types (Eff)
+import Data.Effect.Coroutine (Status (Coroutine, Done), Yield (Yield))
 
-runCoroutine ::
-    forall a b r er fr u c.
-    (MonadFreer c fr, Union u, c (Eff u fr '[] er)) =>
-    Eff u fr '[] (LYield a b ': er) r ->
-    Eff u fr '[] er (Status (Eff u fr '[] er) a b r)
-runCoroutine = interpretK (pure . Done) (\kk (Yield a) -> pure $ Coroutine a kk)
+runCoroutine
+    :: forall a b ans r
+     . Eff '[] (Yield a b ': r) ans
+    -> Eff '[] r (Status (Eff '[] r) a b ans)
+runCoroutine = interpretBy (pure . Done) (\(Yield a) k -> pure $ Coroutine a k)
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Except.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Except.hs
index a800754..373be5c 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Except.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Except.hs
@@ -9,127 +9,47 @@ Maintainer  :  ymdfield@outlook.jp
 Stability   :  experimental
 Portability :  portable
 
-Interpreter and elaborator for the t'Data.Effect.Except.Throw' / t'Data.Effect.Except.Catch' effect
-classes.
+Interpreters for the t'Data.Effect.Except.Throw' / t'Data.Effect.Except.Catch' effects.
 -}
 module Control.Effect.Interpreter.Heftia.Except where
 
-import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (
-    Eff,
-    Elab,
-    interposeK,
-    interposeT,
-    interpretK,
-    interpretRec,
-    interpretRecH,
-    interpretT,
- )
 import Control.Exception (Exception)
-import Control.Monad.Freer (MonadFreer)
-import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
-import Data.Effect.Except (Catch (Catch), LThrow, Throw (Throw))
-import Data.Effect.HFunctor (HFunctor)
+import Control.Monad.Hefty.Interpret (interposeBy, interpretBy, interpretRec, interpretRecH)
+import Control.Monad.Hefty.Types (Eff, Elab, Interpreter)
+import Data.Effect.Except (Catch (Catch), Throw (Throw))
+import Data.Effect.OpenUnion.Internal.FO (type (<|))
+import Data.Effect.OpenUnion.Internal.HO (type (<<|))
 import Data.Effect.Unlift (UnliftIO)
 import Data.Function ((&))
-import Data.Hefty.Extensible (ForallHFunctor, type (<<|), type (<|))
-import Data.Hefty.Extensible qualified as Ex
-import Data.Hefty.Union (Member, Union)
 import UnliftIO (throwIO)
 import UnliftIO qualified as IO
 
--- | Interpret the "Data.Effect.Except" effects using the 'ExceptT' monad transformer internally.
-runExcept ::
-    forall e a ef fr u c.
-    ( Member u (Throw e) (LThrow e ': ef)
-    , MonadFreer c fr
-    , Union u
-    , c (Eff u fr '[] (LThrow e ': ef))
-    , c (ExceptT e (Eff u fr '[] (LThrow e ': ef)))
-    , HFunctor (u '[Catch e])
-    , c (Eff u fr '[] ef)
-    , c (ExceptT e (Eff u fr '[] ef))
-    , HFunctor (u '[])
-    ) =>
-    Eff u fr '[Catch e] (LThrow e ': ef) a ->
-    Eff u fr '[] ef (Either e a)
-runExcept = runCatch >>> runThrow
-{-# INLINE runExcept #-}
+runExcept :: Eff '[Catch e] (Throw e ': r) a -> Eff '[] r (Either e a)
+runExcept = runThrow . runCatch
 
--- | Elaborate the t'Catch' effect using the 'ExceptT' monad transformer internally.
-runCatch ::
-    forall e ef fr u c.
-    ( Member u (Throw e) ef
-    , MonadFreer c fr
-    , Union u
-    , c (Eff u fr '[] ef)
-    , c (ExceptT e (Eff u fr '[] ef))
-    , HFunctor (u '[Catch e])
-    , HFunctor (u '[])
-    ) =>
-    Eff u fr '[Catch e] ef ~> Eff u fr '[] ef
+runThrow :: Eff '[] (Throw e ': r) a -> Eff '[] r (Either e a)
+runThrow = interpretBy (pure . Right) handleThrow
+
+runCatch :: (Throw e <| ef) => Eff '[Catch e] ef ~> Eff '[] ef
 runCatch = interpretRecH elabCatch
-{-# INLINE runCatch #-}
 
-elabCatch ::
-    forall e ef fr u c.
-    ( Member u (Throw e) ef
-    , MonadFreer c fr
-    , Union u
-    , c (Eff u fr '[] ef)
-    , c (ExceptT e (Eff u fr '[] ef))
-    ) =>
-    Elab (Catch e) (Eff u fr '[] ef)
-elabCatch (Catch action hdl) = do
-    r <- runExceptT $ action & interposeT \(Throw e) -> throwE e
-    case r of
-        Left e -> hdl e
-        Right a -> pure a
+handleThrow :: Interpreter (Throw e) (Eff '[] r) (Either e a)
+handleThrow (Throw e) _ = pure $ Left e
+{-# INLINE handleThrow #-}
 
--- | Elaborate the 'Catch' effect using a delimited continuation.
-elabCatchK ::
-    forall e ef fr u c.
-    (Member u (Throw e) ef, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
-    Elab (Catch e) (Eff u fr '[] ef)
-elabCatchK (Catch action hdl) =
-    action & interposeK pure \_ (Throw e) -> hdl e
+elabCatch :: (Throw e <| ef) => Elab (Catch e) (Eff '[] ef)
+elabCatch (Catch action hdl) = action & interposeBy pure \(Throw e) _ -> hdl e
+{-# INLINE elabCatch #-}
 
--- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
-runThrow ::
-    forall e r a fr u c.
-    (MonadFreer c fr, Union u, c (Eff u fr '[] r), c (ExceptT e (Eff u fr '[] r))) =>
-    Eff u fr '[] (LThrow e ': r) a ->
-    Eff u fr '[] r (Either e a)
-runThrow = runExceptT . runThrowT
-{-# INLINE runThrow #-}
-
--- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
-runThrowT ::
-    forall e r fr u c.
-    (MonadFreer c fr, Union u, c (Eff u fr '[] r), c (ExceptT e (Eff u fr '[] r))) =>
-    Eff u fr '[] (LThrow e ': r) ~> ExceptT e (Eff u fr '[] r)
-runThrowT = interpretT \(Throw e) -> throwE e
-{-# INLINE runThrowT #-}
-
--- | Interpret the 'Throw' effect using a delimited continuation.
-runThrowK ::
-    forall e r a fr u c.
-    (MonadFreer c fr, Union u, c (Eff u fr '[] r)) =>
-    Eff u fr '[] (LThrow e ': r) a ->
-    Eff u fr '[] r (Either e a)
-runThrowK = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e
-
-runThrowIO ::
-    forall e eh ef fr c.
-    (MonadFreer c fr, IO <| ef, ForallHFunctor eh, Exception e) =>
-    Ex.Eff fr eh (LThrow e ': ef) ~> Ex.Eff fr eh ef
+runThrowIO
+    :: forall e eh ef
+     . (IO <| ef, Exception e)
+    => Eff eh (Throw e ': ef) ~> Eff eh ef
 runThrowIO = interpretRec \(Throw e) -> throwIO e
-{-# INLINE runThrowIO #-}
 
-runCatchIO ::
-    forall e eh ef fr c.
-    (MonadFreer c fr, UnliftIO <<| eh, IO <| ef, ForallHFunctor eh, Exception e) =>
-    Ex.Eff fr (Catch e ': eh) ef ~> Ex.Eff fr eh ef
+runCatchIO
+    :: forall e eh ef
+     . (UnliftIO <<| eh, IO <| ef, Exception e)
+    => Eff (Catch e ': eh) ef ~> Eff eh ef
 runCatchIO = interpretRecH \(Catch action hdl) -> IO.catch action hdl
-{-# INLINE runCatchIO #-}
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fail.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fail.hs
index c09e1cc..c9a9c46 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fail.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fail.hs
@@ -11,16 +11,12 @@ Portability :  portable
 -}
 module Control.Effect.Interpreter.Heftia.Fail where
 
-import Control.Effect (sendIns, type (~>))
-import Control.Effect.Hefty (Eff, interpret)
-import Control.Freer (Freer)
-import Data.Effect.Fail (Fail (Fail), LFail)
-import Data.Effect.HFunctor (HFunctor)
-import Data.Hefty.Union (Member, Union)
+import Control.Effect (type (~>))
+import Control.Monad.Hefty.Interpret (interpretRec)
+import Control.Monad.Hefty.Types (Eff)
+import Control.Monad.IO.Class (liftIO)
+import Data.Effect.Fail (Fail (Fail))
+import Data.Effect.OpenUnion.Internal.FO (type (<|))
 
-runFailAsIO
-    :: forall r fr u c
-     . (Freer c fr, Union u, HFunctor (u '[]), Member u IO r)
-    => Eff u fr '[] (LFail ': r) ~> Eff u fr '[] r
-runFailAsIO = interpret \(Fail s) -> sendIns @IO $ fail s
-{-# INLINE runFailAsIO #-}
+runFailIO :: (IO <| r) => Eff eh (Fail ': r) ~> Eff eh r
+runFailIO = interpretRec \(Fail s) -> liftIO $ fail s
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fresh.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fresh.hs
index b17595e..9cdd6fb 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fresh.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Fresh.hs
@@ -13,42 +13,21 @@ module Control.Effect.Interpreter.Heftia.Fresh where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (Eff, interpret, raiseUnder)
 import Control.Effect.Interpreter.Heftia.State (runState)
-import Control.Freer (Freer)
-import Control.Monad.State (StateT)
-import Data.Effect.Fresh (Fresh (Fresh), LFresh)
-import Data.Effect.HFunctor (HFunctor)
-import Data.Effect.State (LState, State, get, modify)
-import Data.Hefty.Union (Member, Union)
+import Control.Monad.Hefty.Interpret (interpretRec)
+import Control.Monad.Hefty.Transform (raiseUnder)
+import Control.Monad.Hefty.Types (Eff)
+import Data.Effect.Fresh (Fresh (Fresh))
+import Data.Effect.OpenUnion.Internal.FO (type (<|))
+import Data.Effect.State (State, get, modify)
 import Numeric.Natural (Natural)
 
-runFreshNatural
-    :: ( Freer c fr
-       , Union u
-       , HFunctor (u '[])
-       , Member u (State Natural) (LState Natural ': r)
-       , c (Eff u fr '[] r)
-       , c (StateT Natural (Eff u fr '[] r))
-       , Monad (Eff u fr '[] r)
-       , Monad (Eff u fr '[] (LState Natural ': r))
-       )
-    => Eff u fr '[] (LFresh Natural ': r) a
-    -> Eff u fr '[] r (Natural, a)
+runFreshNatural :: Eff '[] (Fresh Natural ': r) a -> Eff '[] r (Natural, a)
 runFreshNatural =
-    raiseUnder
-        >>> runFreshNaturalAsState
-        >>> runState 0
-{-# INLINE runFreshNatural #-}
+    raiseUnder >>> runFreshNaturalAsState >>> runState 0
 
 runFreshNaturalAsState
-    :: forall r fr u c
-     . ( Freer c fr
-       , Union u
-       , Member u (State Natural) r
-       , Monad (Eff u fr '[] r)
-       , HFunctor (u '[])
-       )
-    => Eff u fr '[] (LFresh Natural ': r) ~> Eff u fr '[] r
+    :: (State Natural <| r)
+    => Eff eh (Fresh Natural ': r) ~> Eff eh r
 runFreshNaturalAsState =
-    interpret \Fresh -> get @Natural <* modify @Natural (+ 1)
+    interpretRec \Fresh -> get @Natural <* modify @Natural (+ 1)
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Input.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Input.hs
index 629ce5d..450eabc 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Input.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Input.hs
@@ -13,50 +13,27 @@ module Control.Effect.Interpreter.Heftia.Input where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (Eff, interpret, interpretRec, raiseUnder)
 import Control.Effect.Interpreter.Heftia.State (evalState)
-import Control.Freer (Freer)
-import Control.Monad.State (StateT)
-import Data.Effect.HFunctor (HFunctor)
-import Data.Effect.Input (Input (Input), LInput)
-import Data.Effect.State (LState, State, gets, put)
-import Data.Hefty.Union (Member, Union)
+import Control.Monad.Hefty.Interpret (interpret, interpretRec)
+import Control.Monad.Hefty.Transform (raiseUnder)
+import Control.Monad.Hefty.Types (Eff)
+import Data.Effect.Input (Input (Input))
+import Data.Effect.State (gets, put)
 import Data.List (uncons)
 
-runInputEff
-    :: forall i r eh fr u c
-     . (Freer c fr, Union u, Applicative (Eff u fr eh r), HFunctor (u eh))
-    => Eff u fr eh r i
-    -> Eff u fr eh (LInput i ': r) ~> Eff u fr eh r
+runInputEff :: forall i r eh. Eff eh r i -> Eff eh (Input i ': r) ~> Eff eh r
 runInputEff a = interpretRec \Input -> a
-{-# INLINE runInputEff #-}
 
-runInputConst
-    :: forall i r eh fr u c
-     . (Freer c fr, Union u, Applicative (Eff u fr eh r), HFunctor (u eh))
-    => i
-    -> Eff u fr eh (LInput i ': r) ~> Eff u fr eh r
+runInputConst :: forall i r eh. i -> Eff eh (Input i ': r) ~> Eff eh r
 runInputConst i = interpretRec \Input -> pure i
-{-# INLINE runInputConst #-}
 
-runInputList
-    :: forall i r fr u c
-     . ( Freer c fr
-       , Union u
-       , Applicative (Eff u fr '[] r)
-       , Monad (Eff u fr '[] (LState [i] ': r))
-       , c (Eff u fr '[] r)
-       , c (StateT [i] (Eff u fr '[] r))
-       , Member u (State [i]) (LState [i] ': r)
-       , HFunctor (u '[])
-       )
-    => [i]
-    -> Eff u fr '[] (LInput (Maybe i) ': r) ~> Eff u fr '[] r
+runInputList :: forall i r. [i] -> Eff '[] (Input (Maybe i) ': r) ~> Eff '[] r
 runInputList is =
     raiseUnder
-        >>> ( interpret \Input -> do
-                is' <- gets @[i] uncons
-                mapM_ (put . snd) is'
-                pure $ fst <$> is'
-            )
+        >>> int
         >>> evalState is
+  where
+    int = interpret \Input -> do
+        is' <- gets @[i] uncons
+        mapM_ (put . snd) is'
+        pure $ fst <$> is'
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/KVStore.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/KVStore.hs
index b3db660..84b5205 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/KVStore.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/KVStore.hs
@@ -17,49 +17,32 @@ module Control.Effect.Interpreter.Heftia.KVStore where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (Eff, interpret, raiseUnder)
 import Control.Effect.Interpreter.Heftia.State (runState)
-import Control.Freer (Freer)
-import Control.Monad.State (StateT)
-import Data.Effect.HFunctor (HFunctor)
-import Data.Effect.KVStore (KVStore (LookupKV, UpdateKV), LKVStore)
-import Data.Effect.State (LState, State, get, modify)
+import Control.Monad.Hefty.Interpret (interpret)
+import Control.Monad.Hefty.Transform (raiseUnder)
+import Control.Monad.Hefty.Types (Eff)
+import Data.Effect.KVStore (KVStore (LookupKV, UpdateKV))
+import Data.Effect.OpenUnion.Internal.FO (type (<|))
+import Data.Effect.State (State, get, modify)
 import Data.Functor ((<&>))
-import Data.Hefty.Union (Member, Union)
 import Data.Map (Map)
 import Data.Map qualified as Map
 
-runKVStorePure ::
-    forall k v r a fr u c.
-    ( Ord k
-    , Freer c fr
-    , Union u
-    , HFunctor (u '[])
-    , Member u (State (Map k v)) (LState (Map k v) ': r)
-    , c (Eff u fr '[] r)
-    , c (StateT (Map k v) (Eff u fr '[] r))
-    , Monad (Eff u fr '[] r)
-    , Monad (Eff u fr '[] (LState (Map k v) ': r))
-    ) =>
-    Map k v ->
-    Eff u fr '[] (LKVStore k v ': r) a ->
-    Eff u fr '[] r (Map k v, a)
+runKVStorePure
+    :: forall k v r a
+     . (Ord k)
+    => Map k v
+    -> Eff '[] (KVStore k v ': r) a
+    -> Eff '[] r (Map k v, a)
 runKVStorePure initial =
     raiseUnder
         >>> runKVStoreAsState
         >>> runState initial
-{-# INLINE runKVStorePure #-}
 
-runKVStoreAsState ::
-    forall k v r fr u c.
-    ( Ord k
-    , Freer c fr
-    , Union u
-    , Member u (State (Map k v)) r
-    , Monad (Eff u fr '[] r)
-    , HFunctor (u '[])
-    ) =>
-    Eff u fr '[] (LKVStore k v ': r) ~> Eff u fr '[] r
+runKVStoreAsState
+    :: forall k v r
+     . (Ord k, State (Map k v) <| r)
+    => Eff '[] (KVStore k v ': r) ~> Eff '[] r
 runKVStoreAsState = interpret \case
     LookupKV k -> get <&> Map.lookup k
     UpdateKV k v -> modify $ Map.update (const v) k
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/NonDet.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/NonDet.hs
index 0b29d2a..370e2dc 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/NonDet.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/NonDet.hs
@@ -11,96 +11,63 @@ Portability :  portable
 -}
 module Control.Effect.Interpreter.Heftia.NonDet where
 
-import Control.Applicative (Alternative ((<|>)), empty, liftA2, (<|>))
+import Control.Applicative (Alternative ((<|>)), empty, (<|>))
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (Eff, injectF, interpretFin, interpretFinH, interpretK, interpretRecH)
-import Control.Freer (Freer)
-import Control.Monad.Freer (MonadFreer)
-import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
+import Control.Monad.Hefty
 import Data.Bool (bool)
-import Data.Effect.HFunctor (HFunctor)
-import Data.Effect.NonDet (Choose (Choose), ChooseH (ChooseH), Empty (Empty), LChoose, LEmpty, choose)
-import Data.Functor.Compose (Compose (Compose), getCompose)
-import Data.Hefty.Union (ForallHFunctor, HFunctorUnion, Member, Union)
+import Data.Effect.NonDet (Choose (Choose), ChooseH (ChooseH), Empty (Empty), choose)
 
--- | 'NonDet' effects handler for Monad use.
+-- | 'NonDet' effects handler for alternative answer type.
 runNonDet
-    :: forall f ef a fr u c
-     . ( Alternative f
-       , MonadFreer c fr
-       , Union u
-       , c (Eff u fr '[] ef)
-       , c (Eff u fr '[] (LEmpty : ef))
-       )
-    => Eff u fr '[] (LChoose ': LEmpty ': ef) a
-    -> Eff u fr '[] ef (f a)
+    :: forall f r a
+     . (Alternative f)
+    => Eff '[] (Choose ': Empty ': r) a
+    -> Eff '[] r (f a)
 runNonDet =
-    runChoose >>> interpretK pure \_ Empty -> pure empty
-{-# INLINE runNonDet #-}
+    runChoose
+        >>> interpretBy pure \Empty _ -> pure empty
 
--- | 'NonDet' effects handler for Monad use.
-runNonDetK
-    :: forall r ef a fr u c
-     . ( Monoid r
-       , MonadFreer c fr
-       , Union u
-       , c (Eff u fr '[] ef)
-       , c (Eff u fr '[] (LEmpty ': ef))
-       , HFunctor (u '[])
-       )
-    => (a -> Eff u fr '[] (LEmpty ': ef) r)
-    -> Eff u fr '[] (LChoose ': LEmpty ': ef) a
-    -> Eff u fr '[] ef r
-runNonDetK f =
-    runChooseK f >>> interpretK pure \_ Empty -> pure mempty
-{-# INLINE runNonDetK #-}
+-- | 'NonDet' effects handler for monoidal answer type.
+runNonDetMonoid
+    :: forall ans r a
+     . (Monoid ans)
+    => (a -> Eff '[] (Empty ': r) ans)
+    -> Eff '[] (Choose ': Empty ': r) a
+    -> Eff '[] r ans
+runNonDetMonoid f =
+    runChooseMonoid f
+        >>> interpretBy pure \Empty _ -> pure mempty
 
--- | 'Choose' effect handler for Monad use.
+-- | 'Choose' effect handler for alternative answer type.
 runChoose
-    :: forall f ef a fr u c
-     . ( Alternative f
-       , MonadFreer c fr
-       , Union u
-       , c (Eff u fr '[] ef)
-       )
-    => Eff u fr '[] (LChoose ': ef) a
-    -> Eff u fr '[] ef (f a)
+    :: forall f ef a
+     . (Alternative f)
+    => Eff '[] (Choose ': ef) a
+    -> Eff '[] ef (f a)
 runChoose =
-    interpretK (pure . pure) \k Choose ->
+    interpretBy (pure . pure) \Choose k ->
         liftA2 (<|>) (k False) (k True)
 
--- | 'Choose' effect handler for Monad use.
-runChooseK
-    :: forall r ef a fr u c
-     . ( Semigroup r
-       , MonadFreer c fr
-       , Union u
-       , c (Eff u fr '[] ef)
-       )
-    => (a -> Eff u fr '[] ef r)
-    -> Eff u fr '[] (LChoose ': ef) a
-    -> Eff u fr '[] ef r
-runChooseK f =
-    interpretK f \k Choose ->
+-- | 'Choose' effect handler for monoidal answer type.
+runChooseMonoid
+    :: forall ans r a
+     . (Semigroup ans)
+    => (a -> Eff '[] r ans)
+    -> Eff '[] (Choose ': r) a
+    -> Eff '[] r ans
+runChooseMonoid f =
+    interpretBy f \Choose k ->
         liftA2 (<>) (k False) (k True)
 
--- | 'Empty' effect handler for Monad use.
-runEmpty
-    :: forall a r fr u c
-     . ( Freer c fr
-       , Union u
-       , Applicative (Eff u fr '[] r)
-       , c (MaybeT (Eff u fr '[] r))
-       )
-    => Eff u fr '[] (LEmpty ': r) a
-    -> Eff u fr '[] r (Maybe a)
+-- | 'Empty' effect handler.
+runEmpty :: forall a r. Eff '[] (Empty ': r) a -> Eff '[] r (Maybe a)
 runEmpty =
-    runMaybeT . interpretFin
-        (MaybeT . fmap Just . injectF)
-        \Empty -> MaybeT $ pure Nothing
+    interpretBy
+        (pure . Just)
+        \Empty _ -> pure Nothing
 
-{- | 'ChooseH' effect handler for Monad use.
+{- | 'ChooseH' effect elaborator.
 
     Convert a higher-order effect of the form
 
@@ -110,49 +77,8 @@ runEmpty =
 
         @choose :: m Bool@
 -}
-runChooseH
-    :: ( Freer c fr
-       , HFunctorUnion u
-       , Member u Choose ef
-       , ForallHFunctor u eh
-       , Monad (Eff u fr eh ef)
-       )
-    => Eff u fr (ChooseH ': eh) ef ~> Eff u fr eh ef
+runChooseH :: (Choose <| ef) => Eff (ChooseH ': eh) ef ~> Eff eh ef
 runChooseH =
     interpretRecH \(ChooseH a b) -> do
         world <- choose
         bool a b world
-
--- | 'NonDet' effect handler for Applicative use.
-runNonDetA
-    :: forall f ef a fr u c
-     . ( Alternative f
-       , Freer c fr
-       , Union u
-       , Applicative (Eff u fr '[] ef)
-       , c (Compose (Eff u fr '[] ef) f)
-       )
-    => Eff u fr '[ChooseH] (LEmpty ': ef) a
-    -> Eff u fr '[] ef (f a)
-runNonDetA =
-    getCompose
-        . interpretFinH
-            (Compose . runEmptyA . injectF)
-            (\(ChooseH a b) -> Compose $ liftA2 (<|>) (runNonDetA a) (runNonDetA b))
-
--- | 'Empty' effect handler for Applicative use.
-runEmptyA
-    :: forall f a r fr u c
-     . ( Alternative f
-       , Freer c fr
-       , Union u
-       , Applicative (Eff u fr '[] r)
-       , c (Compose (Eff u fr '[] r) f)
-       )
-    => Eff u fr '[] (LEmpty ': r) a
-    -> Eff u fr '[] r (f a)
-runEmptyA =
-    getCompose
-        . interpretFin
-            (Compose . fmap pure . injectF)
-            \Empty -> Compose $ pure empty
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Output.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Output.hs
index 8b5f7d1..dc5f387 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Output.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Output.hs
@@ -13,45 +13,39 @@ module Control.Effect.Interpreter.Heftia.Output where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (Eff, interpret, interpretRec, raiseUnder, send0)
 import Control.Effect.Interpreter.Heftia.State (runState)
 import Control.Effect.Interpreter.Heftia.Writer (runTell, runTellA)
-import Control.Freer (Freer)
-import Control.Monad.Trans.State (StateT)
-import Control.Monad.Trans.Writer.CPS qualified as CPS
-import Control.Monad.Trans.Writer.Strict qualified as Strict
 import Data.Effect.HFunctor (HFunctor)
 import Data.Effect.Output (LOutput, Output (Output))
 import Data.Effect.State (LState, State, modify)
 import Data.Effect.Writer (Tell (Tell))
-import Data.Hefty.Union (Member, Union)
 
-runOutputEff ::
-    (Freer c fr, Union u, HFunctor (u eh)) =>
-    (o -> Eff u fr eh r ()) ->
-    Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
+runOutputEff
+    :: (Freer c fr, Union u, HFunctor (u eh))
+    => (o -> Eff u fr eh r ())
+    -> Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
 runOutputEff f = interpretRec \(Output o) -> f o
 {-# INLINE runOutputEff #-}
 
-ignoreOutput ::
-    (Freer c fr, Union u, HFunctor (u eh), Applicative (Eff u fr eh r)) =>
-    Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
+ignoreOutput
+    :: (Freer c fr, Union u, HFunctor (u eh), Applicative (Eff u fr eh r))
+    => Eff u fr eh (LOutput o ': r) ~> Eff u fr eh r
 ignoreOutput = runOutputEff $ const $ pure ()
 {-# INLINE ignoreOutput #-}
 
-runOutputList ::
-    forall o a r fr u c.
-    ( Freer c fr
-    , Union u
-    , c (Eff u fr '[] r)
-    , c (StateT [o] (Eff u fr '[] r))
-    , Applicative (Eff u fr '[] r)
-    , Monad (Eff u fr '[] (LState [o] ': r))
-    , Member u (State [o]) (LState [o] ': r)
-    , HFunctor (u '[])
-    ) =>
-    Eff u fr '[] (LOutput o ': r) a ->
-    Eff u fr '[] r ([o], a)
+runOutputList
+    :: forall o a r fr u c
+     . ( Freer c fr
+       , Union u
+       , c (Eff u fr '[] r)
+       , c (StateT [o] (Eff u fr '[] r))
+       , Applicative (Eff u fr '[] r)
+       , Monad (Eff u fr '[] (LState [o] ': r))
+       , Member u (State [o]) (LState [o] ': r)
+       , HFunctor (u '[])
+       )
+    => Eff u fr '[] (LOutput o ': r) a
+    -> Eff u fr '[] r ([o], a)
 runOutputList =
     raiseUnder
         >>> interpret (\(Output o) -> modify (o :))
@@ -60,18 +54,18 @@ runOutputList =
 {- | Run an `Output` effect by transforming into a monoid.
      The carrier is required to be a monad.
 -}
-runOutputMonoid ::
-    forall o m a r fr u c.
-    ( Monoid m
-    , Freer c fr
-    , Union u
-    , Monad (Eff u fr '[] r)
-    , c (CPS.WriterT m (Eff u fr '[] r))
-    , HFunctor (u '[])
-    ) =>
-    (o -> m) ->
-    Eff u fr '[] (LOutput o ': r) a ->
-    Eff u fr '[] r (m, a)
+runOutputMonoid
+    :: forall o m a r fr u c
+     . ( Monoid m
+       , Freer c fr
+       , Union u
+       , Monad (Eff u fr '[] r)
+       , c (CPS.WriterT m (Eff u fr '[] r))
+       , HFunctor (u '[])
+       )
+    => (o -> m)
+    -> Eff u fr '[] (LOutput o ': r) a
+    -> Eff u fr '[] r (m, a)
 runOutputMonoid f =
     raiseUnder
         >>> interpret (\(Output o) -> send0 $ Tell $ f o)
@@ -80,18 +74,18 @@ runOutputMonoid f =
 {- | Strict version of `runOutputMonoid`.
      The constraint on the carrier has been weakened to applicative.
 -}
-runOutputMonoidA ::
-    forall o m a r fr u c.
-    ( Monoid m
-    , Freer c fr
-    , Union u
-    , Applicative (Eff u fr '[] r)
-    , c (Strict.WriterT m (Eff u fr '[] r))
-    , HFunctor (u '[])
-    ) =>
-    (o -> m) ->
-    Eff u fr '[] (LOutput o ': r) a ->
-    Eff u fr '[] r (m, a)
+runOutputMonoidA
+    :: forall o m a r fr u c
+     . ( Monoid m
+       , Freer c fr
+       , Union u
+       , Applicative (Eff u fr '[] r)
+       , c (Strict.WriterT m (Eff u fr '[] r))
+       , HFunctor (u '[])
+       )
+    => (o -> m)
+    -> Eff u fr '[] (LOutput o ': r) a
+    -> Eff u fr '[] r (m, a)
 runOutputMonoidA f =
     raiseUnder
         >>> interpret (\(Output o) -> send0 $ Tell $ f o)
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Provider.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Provider.hs
deleted file mode 100644
index 61279e2..0000000
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Provider.hs
+++ /dev/null
@@ -1,39 +0,0 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
-
-{- |
-Copyright   :  (c) 2023 Sayo Koyoneda
-License     :  MPL-2.0 (see the LICENSE file)
-Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
-
-Elaborator for the t'Control.Effect.Class.Provider.Provider' effect class.
--}
-module Control.Effect.Interpreter.Heftia.Provider where
-
-import Control.Effect (type (~>))
-import Control.Effect.Hefty (Elab)
-import Control.Monad.Trans (MonadTrans, lift)
-import Data.Effect.Provider (Provider' (Provide))
-
--- | Elaborate the t'Control.Effect.Class.Provider.Provider' effect using the given interpreter.
-runProvider
-    :: (c g, e g)
-    => (f ~> g)
-    -> (i -> forall x. g x -> f (ctx x))
-    -> Elab (Provider' c i ctx e) f
-runProvider iLower run (Provide i f) = run i $ f iLower
-{-# INLINE runProvider #-}
-
-{- |
-Elaborate the t'Control.Effect.Class.Provider.Provider' effect using the given interpreter for some
-monad transformer.
--}
-runProviderT
-    :: (Monad m, MonadTrans t, c (t m), e (t m))
-    => (i -> forall x. t m x -> m (ctx x))
-    -> Elab (Provider' c i ctx e) m
-runProviderT = runProvider lift
-{-# INLINE runProviderT #-}
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Provider/Implicit.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Provider/Implicit.hs
deleted file mode 100644
index d69fedd..0000000
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Provider/Implicit.hs
+++ /dev/null
@@ -1,44 +0,0 @@
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
-
-{- |
-Copyright   :  (c) 2023 Sayo Koyoneda
-License     :  MPL-2.0 (see the LICENSE file)
-Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
-
-Elaborator for the t'Control.Effect.Class.Provider.Implicit.ImplicitProvider' effect class.
--}
-module Control.Effect.Interpreter.Heftia.Provider.Implicit where
-
-import Control.Effect (type (~>))
-import Control.Effect.Hefty (Eff, Elab, raise)
-import Control.Effect.Interpreter.Heftia.Reader (runAsk)
-import Control.Freer (Freer)
-import Data.Effect.HFunctor (HFunctor)
-import Data.Effect.Provider.Implicit (ImplicitProvider' (WithImplicit))
-import Data.Effect.Reader (LAsk)
-import Data.Hefty.Union (Union)
-
--- | Elaborate the t'ImplicitProvider'' effect using the given interpreter.
-elaborateImplicitProvider
-    :: (c g, e g)
-    => (f ~> g)
-    -> (i -> forall x. g x -> f x)
-    -> Elab (ImplicitProvider' c i e) f
-elaborateImplicitProvider iLower run (WithImplicit i f) = run i $ f iLower
-{-# INLINE elaborateImplicitProvider #-}
-
-runImplicitProvider
-    :: ( e (Eff u fr eh (LAsk i ': ef))
-       , c (Eff u fr eh (LAsk i ': ef))
-       , Freer c fr
-       , Union u
-       , HFunctor (u eh)
-       , Applicative (Eff u fr eh ef)
-       )
-    => Elab (ImplicitProvider' c i e) (Eff u fr eh ef)
-runImplicitProvider (WithImplicit i f) = runAsk i $ f raise
-{-# INLINE runImplicitProvider #-}
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Resource.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Resource.hs
index 52b25b7..561ebb5 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Resource.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Resource.hs
@@ -15,12 +15,21 @@ An elaborator for the t'Control.Effect.Class.Resource.Resource' effect class.
 -}
 module Control.Effect.Interpreter.Heftia.Resource where
 
-import Control.Effect.Hefty (Elab)
+import Control.Effect (type (~>))
+import Control.Monad.Hefty.Interpret (interpretRecH)
+import Control.Monad.Hefty.Types (Eff, Elab)
+import Data.Effect.OpenUnion.Internal.FO (type (<|))
+import Data.Effect.OpenUnion.Internal.HO (type (<<|))
 import Data.Effect.Resource (Resource (Bracket, BracketOnExcept))
+import Data.Effect.Unlift (UnliftIO)
 import UnliftIO (MonadUnliftIO, bracket, bracketOnError)
 
 -- | Elaborates the `Resource` effect under the `MonadUnliftIO` context.
-resourceToIO :: (MonadUnliftIO m) => Elab Resource m
-resourceToIO = \case
+runResourceIO :: (UnliftIO <<| eh, IO <| ef) => Eff (Resource ': eh) ef ~> Eff eh ef
+runResourceIO = interpretRecH elabResourceIO
+
+elabResourceIO :: (MonadUnliftIO m) => Elab Resource m
+elabResourceIO = \case
     Bracket acquire release thing -> bracket acquire release thing
     BracketOnExcept acquire onError thing -> bracketOnError acquire onError thing
+{-# INLINE elabResourceIO #-}
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/ShiftReset.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/ShiftReset.hs
index bd7b8f3..b51911a 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/ShiftReset.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/ShiftReset.hs
@@ -4,67 +4,26 @@
 
 module Control.Effect.Interpreter.Heftia.ShiftReset where
 
-import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (
-    Eff,
-    injectH,
-    interpretKAllH,
-    interpretKH,
-    interpretRecH,
-    raiseH,
-    runEff,
- )
-import Control.Freer (Freer)
-import Control.Monad ((<=<))
-import Control.Monad.Freer (MonadFreer)
-import Data.Effect (LiftIns)
-import Data.Effect.HFunctor (HFunctor, hfmap)
-import Data.Effect.Key (KeyH (KeyH))
-import Data.Effect.ShiftReset (Reset (Reset), Shift, Shift' (Shift), Shift_ (Shift_))
-import Data.Hefty.Union (HFunctorUnion, HFunctorUnion_ (ForallHFunctor), Union ((|+:)))
+import Control.Monad.Hefty.Interpret (interpretRecH, iterAllEffHFBy)
+import Control.Monad.Hefty.Transform (raiseH)
+import Control.Monad.Hefty.Types (Eff, sendUnionBy, sendUnionHBy)
+import Data.Effect.HFunctor.HCont (HCont (HCont))
+import Data.Effect.OpenUnion.Internal.HO (hfmapUnion, (!!+))
+import Data.Effect.ShiftReset (Reset (Reset), Shift_ (Shift_))
 
-evalShift ::
-    (MonadFreer c fr, Union u, c (Eff u fr '[] ef), HFunctor (u '[])) =>
-    Eff u fr '[Shift r] ef r ->
-    Eff u fr '[] ef r
-evalShift = runShift pure
-{-# INLINE evalShift #-}
-
-runShift ::
-    forall r a ef fr u c.
-    (MonadFreer c fr, Union u, c (Eff u fr '[] ef), HFunctor (u '[])) =>
-    (a -> Eff u fr '[] ef r) ->
-    Eff u fr '[Shift r] ef a ->
-    Eff u fr '[] ef r
-runShift f =
-    interpretKH f \k ->
-        let k' = raiseH . k
-         in evalShift . \case
-                KeyH (Shift g) -> g k'
-
-withShift ::
-    ( MonadFreer c fr
-    , Union u
-    , c (Eff u fr '[] '[LiftIns (Eff u fr eh ef)])
-    , c (Eff u fr eh ef)
-    , HFunctor (u '[])
-    ) =>
-    Eff u fr '[Shift r] '[LiftIns (Eff u fr eh ef)] r ->
-    Eff u fr eh ef r
-withShift = evalShift >>> runEff
-{-# INLINE withShift #-}
-
-runShift_ ::
-    (MonadFreer c fr, Union u, c (Eff u fr eh ef), HFunctor (u eh)) =>
-    Eff u fr (Shift_ ': eh) ef ~> Eff u fr eh ef
+runShift_ :: forall r ef. Eff (HCont Shift_ (Eff r ef) ': r) ef ~> Eff r ef
 runShift_ =
-    interpretKAllH pure \k ->
-        (\(Shift_ f) -> runShift_ $ f $ raiseH . k)
-            |+: (k <=< injectH . hfmap runShift_)
+    iterAllEffHFBy
+        pure
+        ( ( \(HCont g) k ->
+                case g runShift_ of
+                    Shift_ f -> runShift_ $ raiseH $ f k
+          )
+            !!+ (flip sendUnionHBy . hfmapUnion runShift_)
+        )
+        (flip sendUnionBy)
 
-runReset ::
-    (Freer c fr, HFunctorUnion u, ForallHFunctor u eh) =>
-    Eff u fr (Reset ': eh) ef ~> Eff u fr eh ef
+runReset :: forall r ef. Eff (Reset ': r) ef ~> Eff r ef
 runReset = interpretRecH \(Reset a) -> a
 {-# INLINE runReset #-}
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/State.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/State.hs
index bae71e1..4f05f52 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/State.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/State.hs
@@ -1,8 +1,6 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 
--- This Source Code Form is subject to the terms of the Mozilla Public
--- License, v. 2.0. If a copy of the MPL was not distributed with this
--- file, You can obtain one at https://mozilla.org/MPL/2.0/.
+-- SPDX-License-Identifier: MPL-2.0
 
 {- |
 Copyright   :  (c) 2023 Sayo Koyoneda
@@ -11,119 +9,61 @@ Maintainer  :  ymdfield@outlook.jp
 Stability   :  experimental
 Portability :  portable
 
-Interpreter for the t'Control.Effect.Class.State.State' effect class.
+Interpreter for the t'Data.Effect.State.State' effect.
 -}
 module Control.Effect.Interpreter.Heftia.State where
 
-import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (
-    Eff,
-    injectF,
-    interpose,
-    interposeT,
-    interpretFin,
-    interpretK,
-    interpretRec,
-    raiseUnder,
+import Control.Monad.Hefty.Interpret (interpretRec)
+import Control.Monad.Hefty.Interpret.State (
+    StateInterpreter,
+    interposeStateBy,
+    interpretStateBy,
+    interpretStateRecWith,
  )
-import Control.Effect.Interpreter.Heftia.Reader (runAsk)
-import Control.Freer (Freer)
-import Control.Monad.Freer (MonadFreer)
-import Control.Monad.State (StateT)
-import Control.Monad.Trans.State qualified as T
-import Data.Effect.HFunctor (HFunctor)
-import Data.Effect.Reader (Ask (Ask), LAsk, ask)
-import Data.Effect.State (LState, State (Get, Put), get, put)
+import Control.Monad.Hefty.Types (Eff)
+import Data.Effect.OpenUnion.Internal.FO (type (<|))
+import Data.Effect.State (State (Get, Put), get, put)
 import Data.Function ((&))
 import Data.Functor ((<&>))
-import Data.Hefty.Union (Member, Union)
-import Data.Tuple (swap)
-import UnliftIO (MonadIO, newIORef, readIORef, writeIORef)
+import UnliftIO (newIORef, readIORef, writeIORef)
 
--- | Interpret the 'Get'/'Put' effects using the 'StateT' monad transformer.
-runState ::
-    forall s r a fr u c.
-    (Freer c fr, Union u, c (Eff u fr '[] r), c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
-    s ->
-    Eff u fr '[] (LState s ': r) a ->
-    Eff u fr '[] r (s, a)
-runState s a = swap <$> T.runStateT (runStateT a) s
-{-# INLINE runState #-}
+-- | Interpret the 'Get'/'Put' effects.
+runState :: forall s r a. s -> Eff '[] (State s ': r) a -> Eff '[] r (s, a)
+runState s0 = interpretStateBy s0 (curry pure) handleState
 
-evalState ::
-    forall s r fr u c.
-    (Freer c fr, Union u, c (Eff u fr '[] r), c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
-    s ->
-    Eff u fr '[] (LState s ': r) ~> Eff u fr '[] r
-evalState s a = snd <$> runState s a
-{-# INLINE evalState #-}
+evalState :: forall s r a. s -> Eff '[] (State s ': r) a -> Eff '[] r a
+evalState s0 = interpretStateBy s0 (const pure) handleState
 
-execState ::
-    forall s r a fr u c.
-    (Freer c fr, Union u, c (Eff u fr '[] r), c (StateT s (Eff u fr '[] r)), Applicative (Eff u fr '[] r)) =>
-    s ->
-    Eff u fr '[] (LState s ': r) a ->
-    Eff u fr '[] r s
-execState s a = fst <$> runState s a
-{-# INLINE execState #-}
+execState :: forall s r a. s -> Eff '[] (State s ': r) a -> Eff '[] r s
+execState s0 = interpretStateBy s0 (\s _ -> pure s) handleState
 
--- | Interpret the 'Get'/'Put' effects using the 'StateT' monad transformer.
-runStateT ::
-    forall s r fr u c.
-    (Freer c fr, Union u, c (StateT s (Eff u fr '[] r)), c (Eff u fr '[] r), Applicative (Eff u fr '[] r)) =>
-    Eff u fr '[] (LState s ': r) ~> StateT s (Eff u fr '[] r)
-runStateT =
-    interpretFin (\u -> T.StateT \s -> (,s) <$> injectF u) fuseStateEffect
+runStateRec :: forall s r. s -> Eff '[] (State s ': r) ~> Eff '[] r
+runStateRec s0 = interpretStateRecWith s0 handleState
 
--- | Interpret the 'Get'/'Put' effects using delimited continuations.
-runStateK ::
-    forall s r a fr u c.
-    ( MonadFreer c fr
-    , Union u
-    , HFunctor (u '[])
-    , Member u (Ask s) (LAsk s ': r)
-    , c (Eff u fr '[] (LAsk s ': r))
-    , Applicative (Eff u fr '[] r)
-    ) =>
-    s ->
-    Eff u fr '[] (LState s ': r) a ->
-    Eff u fr '[] r (s, a)
-runStateK initialState =
-    raiseUnder
-        >>> interpretK
-            (\a -> ask <&> (,a))
-            ( \k -> \case
-                Get -> k =<< ask
-                Put s -> k () & interpose @(Ask s) \Ask -> pure s
-            )
-        >>> runAsk initialState
+handleState :: StateInterpreter s (State s) (Eff '[] r) ans
+handleState = \case
+    Put s -> \_ k -> k s ()
+    Get -> \s k -> k s s
+{-# INLINE handleState #-}
 
-runStateIORef ::
-    forall s r eh a fr u c.
-    (Freer c fr, Union u, HFunctor (u eh), MonadIO (Eff u fr eh r)) =>
-    s ->
-    Eff u fr eh (LState s ': r) a ->
-    Eff u fr eh r (s, a)
-runStateIORef s m = do
-    ref <- newIORef s
+runStateIORef
+    :: forall s r eh a
+     . (IO <| r)
+    => s
+    -> Eff eh (State s ': r) a
+    -> Eff eh r (s, a)
+runStateIORef s0 m = do
+    ref <- newIORef s0
     a <-
         m & interpretRec \case
             Get -> readIORef ref
-            Put s' -> writeIORef ref s'
+            Put s -> writeIORef ref s
     readIORef ref <&> (,a)
 
-transactState ::
-    forall s r fr u c.
-    (Freer c fr, Union u, Member u (State s) r, Monad (Eff u fr '[] r), c (StateT s (Eff u fr '[] r))) =>
-    Eff u fr '[] r ~> Eff u fr '[] r
+transactState :: forall s ef. (State s <| ef) => Eff '[] ef ~> Eff '[] ef
 transactState m = do
     pre <- get @s
-    (a, post) <- T.runStateT (interposeT fuseStateEffect m) pre
+    (post, a) <- interposeStateBy pre (curry pure) handleState m
     put post
     pure a
-
-fuseStateEffect :: Applicative f => State s ~> StateT s f
-fuseStateEffect = \case
-    Get -> T.StateT \s -> pure (s, s)
-    Put s -> T.StateT \_ -> pure ((), s)
diff --git a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs
index fd4c66c..555b044 100644
--- a/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs
+++ b/heftia-effects/src/Control/Effect/Interpreter/Heftia/Writer.hs
@@ -18,263 +18,245 @@ module Control.Effect.Interpreter.Heftia.Writer where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Hefty (
-    Eff,
-    Elab,
-    injectF,
-    interposeFin,
-    interposeT,
-    interpretFin,
-    interpretK,
-    interpretRecH,
-    interpretT,
-    rewrite,
- )
-import Control.Freer (Freer)
-import Control.Monad.Freer (MonadFreer)
-import Control.Monad.Trans (lift)
-import Control.Monad.Trans.Writer.CPS qualified as CPS
-import Control.Monad.Trans.Writer.Strict qualified as Strict
 import Data.Effect.HFunctor (HFunctor)
 import Data.Effect.Writer (LTell, Tell (Tell), WriterH (Censor, Listen), tell)
 import Data.Function ((&))
-import Data.Hefty.Union (Member, Union)
 import Data.Tuple (swap)
 
 -- | 'Writer' effect handler with post-applying censor semantics for Monad use.
-runWriterPost ::
-    forall w a r fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] r)
-    , c (CPS.WriterT w (Eff u fr '[] r))
-    , Member u (Tell w) (LTell w ': r)
-    , Monad (Eff u fr '[] (LTell w ': r))
-    , c (CPS.WriterT w (Eff u fr '[] (LTell w ': r)))
-    , HFunctor (u '[WriterH w])
-    ) =>
-    Eff u fr '[WriterH w] (LTell w ': r) a ->
-    Eff u fr '[] r (w, a)
+runWriterPost
+    :: forall w a r fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] r)
+       , c (CPS.WriterT w (Eff u fr '[] r))
+       , Member u (Tell w) (LTell w ': r)
+       , Monad (Eff u fr '[] (LTell w ': r))
+       , c (CPS.WriterT w (Eff u fr '[] (LTell w ': r)))
+       , HFunctor (u '[WriterH w])
+       )
+    => Eff u fr '[WriterH w] (LTell w ': r) a
+    -> Eff u fr '[] r (w, a)
 runWriterPost = elaborateWriterPost >>> runTell
 {-# INLINE runWriterPost #-}
 
-elaborateWriterPost ::
-    forall w ef fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) ef
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] ef)
-    , c (CPS.WriterT w (Eff u fr '[] ef))
-    , HFunctor (u '[WriterH w])
-    ) =>
-    Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
+elaborateWriterPost
+    :: forall w ef fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) ef
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] ef)
+       , c (CPS.WriterT w (Eff u fr '[] ef))
+       , HFunctor (u '[WriterH w])
+       )
+    => Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
 elaborateWriterPost = interpretRecH elabWriterPost
 {-# INLINE elaborateWriterPost #-}
 
-elabWriterPost ::
-    forall w ef fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) ef
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] ef)
-    , c (CPS.WriterT w (Eff u fr '[] ef))
-    ) =>
-    Elab (WriterH w) (Eff u fr '[] ef)
+elabWriterPost
+    :: forall w ef fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) ef
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] ef)
+       , c (CPS.WriterT w (Eff u fr '[] ef))
+       )
+    => Elab (WriterH w) (Eff u fr '[] ef)
 elabWriterPost = \case
     Listen m -> listenT m
     Censor f m -> postCensor f m
 
-postCensor ::
-    forall w es fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Member u (Tell w) es
-    , Union u
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] es)
-    , c (CPS.WriterT w (Eff u fr '[] es))
-    ) =>
-    (w -> w) ->
-    Eff u fr '[] es ~> Eff u fr '[] es
+postCensor
+    :: forall w es fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Member u (Tell w) es
+       , Union u
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] es)
+       , c (CPS.WriterT w (Eff u fr '[] es))
+       )
+    => (w -> w)
+    -> Eff u fr '[] es ~> Eff u fr '[] es
 postCensor f m = do
     (a, w) <- CPS.runWriterT $ confiscateT m
     tell $ f w
     pure a
 
 -- | 'Writer' effect handler with pre-applying censor semantics for Monad use.
-runWriterPre ::
-    forall w a r fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] r)
-    , c (CPS.WriterT w (Eff u fr '[] r))
-    , Member u (Tell w) (LTell w ': r)
-    , Monad (Eff u fr '[] (LTell w ': r))
-    , c (CPS.WriterT w (Eff u fr '[] (LTell w ': r)))
-    , HFunctor (u '[WriterH w])
-    ) =>
-    Eff u fr '[WriterH w] (LTell w ': r) a ->
-    Eff u fr '[] r (w, a)
+runWriterPre
+    :: forall w a r fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] r)
+       , c (CPS.WriterT w (Eff u fr '[] r))
+       , Member u (Tell w) (LTell w ': r)
+       , Monad (Eff u fr '[] (LTell w ': r))
+       , c (CPS.WriterT w (Eff u fr '[] (LTell w ': r)))
+       , HFunctor (u '[WriterH w])
+       )
+    => Eff u fr '[WriterH w] (LTell w ': r) a
+    -> Eff u fr '[] r (w, a)
 runWriterPre = elaborateWriterPre >>> runTell
 {-# INLINE runWriterPre #-}
 
-elaborateWriterPre ::
-    forall w ef fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) ef
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] ef)
-    , c (CPS.WriterT w (Eff u fr '[] ef))
-    , HFunctor (u '[WriterH w])
-    ) =>
-    Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
+elaborateWriterPre
+    :: forall w ef fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) ef
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] ef)
+       , c (CPS.WriterT w (Eff u fr '[] ef))
+       , HFunctor (u '[WriterH w])
+       )
+    => Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
 elaborateWriterPre = interpretRecH elabWriterPre
 {-# INLINE elaborateWriterPre #-}
 
-elabWriterPre ::
-    forall w ef fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) ef
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] ef)
-    , c (CPS.WriterT w (Eff u fr '[] ef))
-    ) =>
-    Elab (WriterH w) (Eff u fr '[] ef)
+elabWriterPre
+    :: forall w ef fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) ef
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] ef)
+       , c (CPS.WriterT w (Eff u fr '[] ef))
+       )
+    => Elab (WriterH w) (Eff u fr '[] ef)
 elabWriterPre = \case
     Listen m -> listenT m
     Censor f m -> preCensor f m
 
 -- | 'Writer' effect handler with pre-applying censor semantics for Applicative use.
-runWriterPreA ::
-    forall w a r fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , HFunctor (u '[])
-    , Monad (Eff u fr '[] r)
-    , c (Strict.WriterT w (Eff u fr '[] r))
-    , Member u (Tell w) (LTell w ': r)
-    , Monad (Eff u fr '[] (LTell w ': r))
-    , c (Strict.WriterT w (Eff u fr '[] (LTell w ': r)))
-    , HFunctor (u '[WriterH w])
-    ) =>
-    Eff u fr '[WriterH w] (LTell w ': r) a ->
-    Eff u fr '[] r (w, a)
+runWriterPreA
+    :: forall w a r fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , HFunctor (u '[])
+       , Monad (Eff u fr '[] r)
+       , c (Strict.WriterT w (Eff u fr '[] r))
+       , Member u (Tell w) (LTell w ': r)
+       , Monad (Eff u fr '[] (LTell w ': r))
+       , c (Strict.WriterT w (Eff u fr '[] (LTell w ': r)))
+       , HFunctor (u '[WriterH w])
+       )
+    => Eff u fr '[WriterH w] (LTell w ': r) a
+    -> Eff u fr '[] r (w, a)
 runWriterPreA = elaborateWriterPreA >>> runTellA
 {-# INLINE runWriterPreA #-}
 
-elaborateWriterPreA ::
-    forall w ef fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) ef
-    , HFunctor (u '[])
-    , Applicative (Eff u fr '[] ef)
-    , c (Strict.WriterT w (Eff u fr '[] ef))
-    , HFunctor (u '[WriterH w])
-    ) =>
-    Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
+elaborateWriterPreA
+    :: forall w ef fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) ef
+       , HFunctor (u '[])
+       , Applicative (Eff u fr '[] ef)
+       , c (Strict.WriterT w (Eff u fr '[] ef))
+       , HFunctor (u '[WriterH w])
+       )
+    => Eff u fr '[WriterH w] ef ~> Eff u fr '[] ef
 elaborateWriterPreA = interpretRecH elabWriterPre'
 {-# INLINE elaborateWriterPreA #-}
 
-elabWriterPre' ::
-    forall w ef fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) ef
-    , HFunctor (u '[])
-    , Applicative (Eff u fr '[] ef)
-    , c (Strict.WriterT w (Eff u fr '[] ef))
-    ) =>
-    Elab (WriterH w) (Eff u fr '[] ef)
+elabWriterPre'
+    :: forall w ef fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) ef
+       , HFunctor (u '[])
+       , Applicative (Eff u fr '[] ef)
+       , c (Strict.WriterT w (Eff u fr '[] ef))
+       )
+    => Elab (WriterH w) (Eff u fr '[] ef)
 elabWriterPre' = \case
     Listen m -> listenTA m
     Censor f m -> preCensor f m
 
-preCensor ::
-    forall w es fr u c.
-    (Freer c fr, Member u (Tell w) es, Union u, HFunctor (u '[])) =>
-    (w -> w) ->
-    Eff u fr '[] es ~> Eff u fr '[] es
+preCensor
+    :: forall w es fr u c
+     . (Freer c fr, Member u (Tell w) es, Union u, HFunctor (u '[]))
+    => (w -> w)
+    -> Eff u fr '[] es ~> Eff u fr '[] es
 preCensor f = rewrite @(Tell w) \(Tell w) -> Tell $ f w
 
-listenT ::
-    forall w es a fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) es
-    , Monad (Eff u fr '[] es)
-    , c (CPS.WriterT w (Eff u fr '[] es))
-    ) =>
-    Eff u fr '[] es a ->
-    Eff u fr '[] es (w, a)
+listenT
+    :: forall w es a fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) es
+       , Monad (Eff u fr '[] es)
+       , c (CPS.WriterT w (Eff u fr '[] es))
+       )
+    => Eff u fr '[] es a
+    -> Eff u fr '[] es (w, a)
 listenT m =
     swap <$> CPS.runWriterT do
         m & interposeT @(Tell w) \(Tell w) -> do
             lift $ tell w
             CPS.tell w
 
-listenTA ::
-    forall w es a fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) es
-    , Applicative (Eff u fr '[] es)
-    , c (Strict.WriterT w (Eff u fr '[] es))
-    ) =>
-    Eff u fr '[] es a ->
-    Eff u fr '[] es (w, a)
+listenTA
+    :: forall w es a fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) es
+       , Applicative (Eff u fr '[] es)
+       , c (Strict.WriterT w (Eff u fr '[] es))
+       )
+    => Eff u fr '[] es a
+    -> Eff u fr '[] es (w, a)
 listenTA m =
     swap <$> Strict.runWriterT do
         m & interposeFin @(Tell w) (liftStrictWriterT . injectF) \(Tell w) -> do
             liftStrictWriterT (tell w) *> tellStrictWriterT w
 
-runTell ::
-    (Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r), c (CPS.WriterT w (Eff u fr '[] r))) =>
-    Eff u fr '[] (LTell w ': r) a ->
-    Eff u fr '[] r (w, a)
+runTell
+    :: (Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r), c (CPS.WriterT w (Eff u fr '[] r)))
+    => Eff u fr '[] (LTell w ': r) a
+    -> Eff u fr '[] r (w, a)
 runTell = fmap swap . CPS.runWriterT . runTellT
 {-# INLINE runTell #-}
 
-runTellT ::
-    (Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r), c (CPS.WriterT w (Eff u fr '[] r))) =>
-    Eff u fr '[] (LTell w ': r) ~> CPS.WriterT w (Eff u fr '[] r)
+runTellT
+    :: (Monoid w, Freer c fr, Union u, Monad (Eff u fr '[] r), c (CPS.WriterT w (Eff u fr '[] r)))
+    => Eff u fr '[] (LTell w ': r) ~> CPS.WriterT w (Eff u fr '[] r)
 runTellT = interpretT \(Tell w) -> CPS.tell w
 {-# INLINE runTellT #-}
 
-runTellA ::
-    (Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r), c (Strict.WriterT w (Eff u fr '[] r))) =>
-    Eff u fr '[] (LTell w ': r) a ->
-    Eff u fr '[] r (w, a)
+runTellA
+    :: (Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r), c (Strict.WriterT w (Eff u fr '[] r)))
+    => Eff u fr '[] (LTell w ': r) a
+    -> Eff u fr '[] r (w, a)
 runTellA = fmap swap . Strict.runWriterT . runTellTA
 {-# INLINE runTellA #-}
 
-runTellTA ::
-    (Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r), c (Strict.WriterT w (Eff u fr '[] r))) =>
-    Eff u fr '[] (LTell w ': r) ~> Strict.WriterT w (Eff u fr '[] r)
+runTellTA
+    :: (Monoid w, Freer c fr, Union u, Applicative (Eff u fr '[] r), c (Strict.WriterT w (Eff u fr '[] r)))
+    => Eff u fr '[] (LTell w ': r) ~> Strict.WriterT w (Eff u fr '[] r)
 runTellTA = interpretFin (liftStrictWriterT . injectF) \(Tell w) -> tellStrictWriterT w
 {-# INLINE runTellTA #-}
 
-runTellK ::
-    (Monoid w, MonadFreer c fr, Union u, c (Eff u fr '[] r)) =>
-    Eff u fr '[] (LTell w ': r) a ->
-    Eff u fr '[] r (w, a)
+runTellK
+    :: (Monoid w, MonadFreer c fr, Union u, c (Eff u fr '[] r))
+    => Eff u fr '[] (LTell w ': r) a
+    -> Eff u fr '[] r (w, a)
 runTellK =
     interpretK (pure . (mempty,)) \k (Tell w) -> do
         (w', r) <- k ()
@@ -284,36 +266,36 @@ liftStrictWriterT :: forall w f. (Monoid w, Functor f) => f ~> Strict.WriterT w
 liftStrictWriterT = Strict.WriterT . ((,mempty) <$>)
 {-# INLINE liftStrictWriterT #-}
 
-tellStrictWriterT :: forall w f. Applicative f => w -> Strict.WriterT w f ()
+tellStrictWriterT :: forall w f. (Applicative f) => w -> Strict.WriterT w f ()
 tellStrictWriterT = Strict.WriterT . pure . ((),)
 {-# INLINE tellStrictWriterT #-}
 
-transactWriter ::
-    forall w es a fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) es
-    , Monad (Eff u fr '[] es)
-    , c (CPS.WriterT w (Eff u fr '[] es))
-    ) =>
-    Eff u fr '[] es a ->
-    Eff u fr '[] es a
+transactWriter
+    :: forall w es a fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) es
+       , Monad (Eff u fr '[] es)
+       , c (CPS.WriterT w (Eff u fr '[] es))
+       )
+    => Eff u fr '[] es a
+    -> Eff u fr '[] es a
 transactWriter m = do
     (a, w) <- CPS.runWriterT $ confiscateT m
     tell @w w
     pure a
 
-confiscateT ::
-    forall w es a fr u c.
-    ( Monoid w
-    , Freer c fr
-    , Union u
-    , Member u (Tell w) es
-    , Monad (Eff u fr '[] es)
-    , c (CPS.WriterT w (Eff u fr '[] es))
-    ) =>
-    Eff u fr '[] es a ->
-    CPS.WriterT w (Eff u fr '[] es) a
+confiscateT
+    :: forall w es a fr u c
+     . ( Monoid w
+       , Freer c fr
+       , Union u
+       , Member u (Tell w) es
+       , Monad (Eff u fr '[] es)
+       , c (CPS.WriterT w (Eff u fr '[] es))
+       )
+    => Eff u fr '[] es a
+    -> CPS.WriterT w (Eff u fr '[] es) a
 confiscateT m =
     m & interposeT @(Tell w) \(Tell w) -> CPS.tell w
diff --git a/heftia/heftia.cabal b/heftia/heftia.cabal
index c57ae50..48b80d0 100644
--- a/heftia/heftia.cabal
+++ b/heftia/heftia.cabal
@@ -91,6 +91,8 @@ library
         base                          >= 4.16 && < 4.21,
         data-effects                  ^>= 0.1.2,
         freer-simple                  ^>= 1.2.1.2,
+        mtl,
+        unliftio
 
     hs-source-dirs:   src
     ghc-options:      -Wall
diff --git a/heftia/src/Control/Monad/Hefty.hs b/heftia/src/Control/Monad/Hefty.hs
index 1c7fee0..acb4f45 100644
--- a/heftia/src/Control/Monad/Hefty.hs
+++ b/heftia/src/Control/Monad/Hefty.hs
@@ -5,6 +5,7 @@ module Control.Monad.Hefty (
     module Control.Monad.Hefty.Interpret,
     module Control.Monad.Hefty.Interpret.State,
     module Control.Monad.Hefty.Transform,
+    module Data.Effect.OpenUnion,
 ) where
 
 import Control.Monad.Hefty.Interpret (
@@ -58,6 +59,7 @@ import Control.Monad.Hefty.Interpret (
 import Control.Monad.Hefty.Interpret.State (
     StateElaborator,
     StateInterpreter,
+    interposeStateBy,
     interpretStateBy,
     iterStateAllEffHFBy,
     reinterpretStateBy,
@@ -70,18 +72,27 @@ import Control.Monad.Hefty.Transform (
     bundleN,
     bundleUnder,
     bundleUnderH,
+    raise,
+    raiseH,
     raiseN,
     raiseNH,
     raiseNUnder,
     raiseNUnderH,
+    raiseUnder,
+    raiseUnderH,
     raises,
     raisesH,
+    raisesUnder,
     rewrite,
     rewriteH,
+    subsume,
+    subsumeH,
     subsumeN,
     subsumeNH,
     subsumeNUnder,
     subsumeNUnderH,
+    subsumeUnder,
+    subsumeUnderH,
     subsumes,
     subsumesH,
     subsumesUnder,
@@ -117,3 +128,4 @@ import Control.Monad.Hefty.Types (
     type ($$),
     type (:!!),
  )
+import Data.Effect.OpenUnion
diff --git a/heftia/src/Control/Monad/Hefty/Interpret.hs b/heftia/src/Control/Monad/Hefty/Interpret.hs
index 69bcb69..2e75149 100644
--- a/heftia/src/Control/Monad/Hefty/Interpret.hs
+++ b/heftia/src/Control/Monad/Hefty/Interpret.hs
@@ -24,7 +24,7 @@ import Data.Effect.OpenUnion.Internal.FO (
     weakenN,
     weakens,
     (!+),
-    type (<!),
+    type (<|),
  )
 import Data.Effect.OpenUnion.Internal.HO (
     MemberH (prjH),
@@ -35,7 +35,7 @@ import Data.Effect.OpenUnion.Internal.HO (
     weakenNH,
     weakensH,
     (!!+),
-    type (<!!),
+    type (<<|),
  )
 import Data.FTCQueue (FTCQueue, ViewL (TOne, (:|)), tviewl, (><))
 
@@ -265,7 +265,7 @@ reinterpretRecWith
 reinterpretRecWith hdl = loop
   where
     loop :: Eff eh (e ': ef) ~> Eff eh ef'
-    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmap loop) (hdl !+ flip sendUnionBy . weakens)
+    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmapUnion loop) (hdl !+ flip sendUnionBy . weakens)
 {-# INLINE reinterpretRecWith #-}
 
 reinterpretRecNWith
@@ -277,7 +277,7 @@ reinterpretRecNWith
 reinterpretRecNWith hdl = loop
   where
     loop :: Eff eh (e ': ef) ~> Eff eh ef'
-    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmap loop) (hdl !+ flip sendUnionBy . weakenN @n)
+    loop = iterAllEffHFBy pure (flip sendUnionHBy . hfmapUnion loop) (hdl !+ flip sendUnionBy . weakenN @n)
 {-# INLINE reinterpretRecNWith #-}
 
 reinterpretRec :: forall e ef' ef eh. (ef `IsSuffixOf` ef') => (e ~> Eff eh ef') -> Eff eh (e ': ef) ~> Eff eh ef'
@@ -392,7 +392,7 @@ reinterpretRecNH elb = reinterpretRecNHWith @n (plain elb)
 
 interposeBy
     :: forall e ef ans a
-     . (e <! ef)
+     . (e <| ef)
     => (a -> Eff '[] ef ans)
     -> Interpreter e (Eff '[] ef) ans
     -> Eff '[] ef a
@@ -402,7 +402,7 @@ interposeBy ret f = iterAllEffHFBy ret nilH \u -> maybe (`sendUnionBy` u) f (prj
 
 interposeWith
     :: forall e ef a
-     . (e <! ef)
+     . (e <| ef)
     => Interpreter e (Eff '[] ef) a
     -> Eff '[] ef a
     -> Eff '[] ef a
@@ -411,7 +411,7 @@ interposeWith = interposeBy pure
 
 interpose
     :: forall e ef
-     . (e <! ef)
+     . (e <| ef)
     => (e ~> Eff '[] ef)
     -> Eff '[] ef ~> Eff '[] ef
 interpose f = interposeWith (plain f)
@@ -419,7 +419,7 @@ interpose f = interposeWith (plain f)
 
 interposeRecWith
     :: forall e ef eh a
-     . (e <! ef)
+     . (e <| ef)
     => (forall ans. Interpreter e (Eff eh ef) ans)
     -> Eff eh ef a
     -> Eff eh ef a
@@ -434,7 +434,7 @@ interposeRecWith f = loop
 
 interposeRec
     :: forall e ef eh
-     . (e <! ef)
+     . (e <| ef)
     => (e ~> Eff eh ef)
     -> Eff eh ef ~> Eff eh ef
 interposeRec f = interposeRecWith (plain f)
@@ -442,7 +442,7 @@ interposeRec f = interposeRecWith (plain f)
 
 interposeRecHWith
     :: forall e eh ef a
-     . (e <!! eh, HFunctor e)
+     . (e <<| eh, HFunctor e)
     => (forall ans. Elaborator e (Eff eh ef) ans)
     -> Eff eh ef a
     -> Eff eh ef a
@@ -458,7 +458,7 @@ interposeRecHWith f = loop
 
 interposeRecH
     :: forall e eh ef
-     . (e <!! eh, HFunctor e)
+     . (e <<| eh, HFunctor e)
     => Elab e (Eff eh ef)
     -> Eff eh ef ~> Eff eh ef
 interposeRecH f = interposeRecHWith (plain f)
diff --git a/heftia/src/Control/Monad/Hefty/Interpret/State.hs b/heftia/src/Control/Monad/Hefty/Interpret/State.hs
index e959338..6dbb72b 100644
--- a/heftia/src/Control/Monad/Hefty/Interpret/State.hs
+++ b/heftia/src/Control/Monad/Hefty/Interpret/State.hs
@@ -2,11 +2,12 @@
 
 module Control.Monad.Hefty.Interpret.State where
 
+import Control.Effect (type (~>))
 import Control.Monad.Hefty.Interpret (qApp)
-import Control.Monad.Hefty.Types (Eff (Op, Val), sendUnionBy)
+import Control.Monad.Hefty.Types (Eff (Op, Val), sendUnionBy, sendUnionHBy)
 import Data.Effect.OpenUnion.Internal (IsSuffixOf)
-import Data.Effect.OpenUnion.Internal.FO (Union, weakens, (!+))
-import Data.Effect.OpenUnion.Internal.HO (UnionH, nilH)
+import Data.Effect.OpenUnion.Internal.FO (Union, prj, weakens, (!+), type (<|))
+import Data.Effect.OpenUnion.Internal.HO (UnionH, hfmapUnion, nilH)
 import Data.Kind (Type)
 
 type StateInterpreter s e m (ans :: Type) = forall x. e x -> s -> (s -> x -> m ans) -> m ans
@@ -50,7 +51,47 @@ reinterpretStateBy
     -> Eff '[] (e ': ef) a
     -> Eff '[] ef' ans
 reinterpretStateBy s0 ret hdl =
-    iterStateAllEffHFBy s0 ret nilH (hdl !+ \e s k -> sendUnionBy (k s) (weakens e))
+    iterStateAllEffHFBy s0 ret nilH (hdl !+ \u s k -> sendUnionBy (k s) (weakens u))
 {-# INLINE reinterpretStateBy #-}
 
+interpretStateRecWith
+    :: forall s e ef eh a
+     . s
+    -> (forall ans. StateInterpreter s e (Eff eh ef) ans)
+    -> Eff eh (e ': ef) a
+    -> Eff eh ef a
+interpretStateRecWith = reinterpretStateRecWith
+{-# INLINE interpretStateRecWith #-}
+
+reinterpretStateRecWith
+    :: forall s e ef' ef eh a
+     . (ef `IsSuffixOf` ef')
+    => s
+    -> (forall ans. StateInterpreter s e (Eff eh ef') ans)
+    -> Eff eh (e ': ef) a
+    -> Eff eh ef' a
+reinterpretStateRecWith s0 hdl = loop s0
+  where
+    loop :: s -> Eff eh (e ': ef) ~> Eff eh ef'
+    loop s =
+        iterStateAllEffHFBy
+            s
+            (const pure)
+            (\u s' k -> sendUnionHBy (k s') $ hfmapUnion (loop s') u)
+            (hdl !+ \u s' k -> sendUnionBy (k s') (weakens u))
+{-# INLINE reinterpretStateRecWith #-}
+
+interposeStateBy
+    :: forall s e ef ans a
+     . (e <| ef)
+    => s
+    -> (s -> a -> Eff '[] ef ans)
+    -> StateInterpreter s e (Eff '[] ef) ans
+    -> Eff '[] ef a
+    -> Eff '[] ef ans
+interposeStateBy s0 ret f =
+    iterStateAllEffHFBy s0 ret nilH \u s k ->
+        maybe (sendUnionBy (k s) u) (\e -> f e s k) (prj @e u)
+{-# INLINE interposeStateBy #-}
+
 -- TODO: add other pattern functions.
diff --git a/heftia/src/Control/Monad/Hefty/Transform.hs b/heftia/src/Control/Monad/Hefty/Transform.hs
index 7ec1361..2b40c3c 100644
--- a/heftia/src/Control/Monad/Hefty/Transform.hs
+++ b/heftia/src/Control/Monad/Hefty/Transform.hs
@@ -20,6 +20,7 @@ import Data.Effect.OpenUnion.Internal (
     Take,
     WeakenN,
     WeakenNUnder,
+    WeakenUnder,
  )
 import Data.Effect.OpenUnion.Internal.FO (
     Union,
@@ -30,18 +31,23 @@ import Data.Effect.OpenUnion.Internal.FO (
     decomp,
     inj,
     prj,
+    strengthen,
     strengthenN,
     strengthenNUnder,
+    strengthenUnder,
     strengthens,
     strengthensUnder,
     unbundleAllUnion,
     unbundleUnion,
     unbundleUnionN,
     unbundleUnionUnder,
+    weaken,
     weakenN,
     weakenNUnder,
+    weakenUnder,
     weakens,
-    type (<!),
+    weakensUnder,
+    type (<|),
  )
 import Data.Effect.OpenUnion.Internal.HO (
     UnionH,
@@ -52,8 +58,10 @@ import Data.Effect.OpenUnion.Internal.HO (
     hfmapUnion,
     injH,
     prjH,
+    strengthenH,
     strengthenNH,
     strengthenNUnderH,
+    strengthenUnderH,
     strengthensH,
     unbundleAllUnionH,
     unbundleUnionH,
@@ -61,8 +69,9 @@ import Data.Effect.OpenUnion.Internal.HO (
     weakenH,
     weakenNH,
     weakenNUnderH,
+    weakenUnderH,
     weakensH,
-    type (<!!),
+    type (<<|),
  )
 import GHC.TypeNats (KnownNat)
 
@@ -78,30 +87,34 @@ transformH
 transformH f = transEffH (either weakenH (injH . f) . decompH)
 {-# INLINE transformH #-}
 
-translate :: forall e e' ef eh. (e' <! ef) => (e ~> e') -> Eff eh (e ': ef) ~> Eff eh ef
+translate :: forall e e' ef eh. (e' <| ef) => (e ~> e') -> Eff eh (e ': ef) ~> Eff eh ef
 translate f = transEff (either id (inj . f) . decomp)
 {-# INLINE translate #-}
 
 translateH
     :: forall e e' eh ef
-     . (e' <!! eh, HFunctor e)
+     . (e' <<| eh, HFunctor e)
     => (e (Eff eh ef) ~> e' (Eff eh ef))
     -> Eff (e ': eh) ef ~> Eff eh ef
 translateH f = transEffH (either id (injH . f) . decompH)
 {-# INLINE translateH #-}
 
-rewrite :: forall e ef eh. (e <! ef) => (e ~> e) -> Eff eh ef ~> Eff eh ef
+rewrite :: forall e ef eh. (e <| ef) => (e ~> e) -> Eff eh ef ~> Eff eh ef
 rewrite f = transEff \u -> maybe u (inj . f) $ prj @e u
 {-# INLINE rewrite #-}
 
 rewriteH
     :: forall e eh ef
-     . (e <!! eh, HFunctor e)
+     . (e <<| eh, HFunctor e)
     => (e (Eff eh ef) ~> e (Eff eh ef))
     -> Eff eh ef ~> Eff eh ef
 rewriteH f = transEffH \u -> maybe u (injH . f) $ prjH @e u
 {-# INLINE rewriteH #-}
 
+raise :: forall e ef eh. Eff eh ef ~> Eff eh (e ': ef)
+raise = transEff weaken
+{-# INLINE raise #-}
+
 raises :: (ef `IsSuffixOf` ef') => Eff eh ef ~> Eff eh ef'
 raises = transEff weakens
 {-# INLINE raises #-}
@@ -110,6 +123,17 @@ raiseN :: forall len ef ef' eh. (WeakenN len ef ef') => Eff eh ef ~> Eff eh ef'
 raiseN = transEff (weakenN @len)
 {-# INLINE raiseN #-}
 
+raiseUnder :: forall e1 e2 ef eh. Eff eh (e1 ': ef) ~> Eff eh (e1 ': e2 ': ef)
+raiseUnder = transEff weakenUnder
+{-# INLINE raiseUnder #-}
+
+raisesUnder
+    :: forall offset ef ef' eh
+     . (WeakenUnder offset ef ef')
+    => Eff eh ef ~> Eff eh ef'
+raisesUnder = transEff (weakensUnder @offset)
+{-# INLINE raisesUnder #-}
+
 raiseNUnder
     :: forall len offset ef ef' eh
      . (WeakenNUnder len offset ef ef')
@@ -117,6 +141,10 @@ raiseNUnder
 raiseNUnder = transEff (weakenNUnder @len @offset)
 {-# INLINE raiseNUnder #-}
 
+raiseH :: forall e eh ef. Eff eh ef ~> Eff (e ': eh) ef
+raiseH = transEffH weakenH
+{-# INLINE raiseH #-}
+
 raisesH :: (eh `IsSuffixOf` eh') => Eff eh ef ~> Eff eh' ef
 raisesH = transEffH weakensH
 {-# INLINE raisesH #-}
@@ -125,6 +153,10 @@ raiseNH :: forall len eh eh' ef. (WeakenN len eh eh') => Eff eh ef ~> Eff eh' ef
 raiseNH = transEffH (weakenNH @len)
 {-# INLINE raiseNH #-}
 
+raiseUnderH :: forall e1 e2 eh ef. Eff (e1 ': eh) ef ~> Eff (e1 ': e2 ': eh) ef
+raiseUnderH = transEffH weakenUnderH
+{-# INLINE raiseUnderH #-}
+
 raiseNUnderH
     :: forall len offset eh eh' ef
      . (WeakenNUnder len offset eh eh')
@@ -132,6 +164,10 @@ raiseNUnderH
 raiseNUnderH = transEffH (weakenNUnderH @len @offset)
 {-# INLINE raiseNUnderH #-}
 
+subsume :: forall e ef eh. (e <| ef) => Eff eh (e ': ef) ~> Eff eh ef
+subsume = transEff strengthen
+{-# INLINE subsume #-}
+
 subsumes :: forall ef ef' eh. (Strengthen ef ef') => Eff eh ef ~> Eff eh ef'
 subsumes = transEff strengthens
 {-# INLINE subsumes #-}
@@ -140,6 +176,10 @@ subsumeN :: forall len ef ef' eh. (StrengthenN len ef ef') => Eff eh ef ~> Eff e
 subsumeN = transEff (strengthenN @len)
 {-# INLINE subsumeN #-}
 
+subsumeUnder :: forall e2 e1 ef eh. (e2 <| ef) => Eff eh (e1 ': e2 ': ef) ~> Eff eh (e1 ': ef)
+subsumeUnder = transEff strengthenUnder
+{-# INLINE subsumeUnder #-}
+
 subsumesUnder
     :: forall offset ef ef' eh
      . (StrengthenUnder offset ef ef')
@@ -154,6 +194,10 @@ subsumeNUnder
 subsumeNUnder = transEff (strengthenNUnder @len @offset)
 {-# INLINE subsumeNUnder #-}
 
+subsumeH :: forall e eh ef. (e <<| eh) => Eff (e ': eh) ef ~> Eff eh ef
+subsumeH = transEffH strengthenH
+{-# INLINE subsumeH #-}
+
 subsumesH :: forall eh eh' ef. (Strengthen eh eh') => Eff eh ef ~> Eff eh' ef
 subsumesH = transEffH strengthensH
 {-# INLINE subsumesH #-}
@@ -162,6 +206,10 @@ subsumeNH :: forall len eh eh' ef. (StrengthenN len eh eh') => Eff eh ef ~> Eff
 subsumeNH = transEffH (strengthenNH @len)
 {-# INLINE subsumeNH #-}
 
+subsumeUnderH :: forall e2 e1 eh ef. (e2 <<| eh) => Eff (e1 ': e2 ': eh) ef ~> Eff (e1 ': eh) ef
+subsumeUnderH = transEffH strengthenUnderH
+{-# INLINE subsumeUnderH #-}
+
 subsumeNUnderH
     :: forall len offset eh eh' ef
      . (StrengthenNUnder len offset eh eh')
@@ -169,8 +217,6 @@ subsumeNUnderH
 subsumeNUnderH = transEffH (strengthenNUnderH @len @offset)
 {-# INLINE subsumeNUnderH #-}
 
--- TODO: add raiseUnder(H), subsume(H), subsumeUnder(H)
-
 bundle
     :: forall ef bundle rest eh
      . (Split ef bundle rest)
diff --git a/heftia/src/Control/Monad/Hefty/Types.hs b/heftia/src/Control/Monad/Hefty/Types.hs
index 24cb98f..d6fe94b 100644
--- a/heftia/src/Control/Monad/Hefty/Types.hs
+++ b/heftia/src/Control/Monad/Hefty/Types.hs
@@ -1,12 +1,38 @@
 -- SPDX-License-Identifier: MPL-2.0
+{-# LANGUAGE UndecidableInstances #-}
 
 module Control.Monad.Hefty.Types where
 
-import Control.Effect (type (~>))
-import Data.Effect.OpenUnion.Internal.FO (Union, inj, type (<!))
-import Data.Effect.OpenUnion.Internal.HO (UnionH, injH, type (<!!))
+import Control.Applicative (Alternative, empty, (<|>))
+import Control.Effect (SendIns, SendSig, sendIns, sendSig, type (~>))
+import Control.Effect.Key (ByKey (ByKey), SendInsBy, SendSigBy, key, sendInsBy, sendSigBy)
+import Control.Monad (MonadPlus)
+import Control.Monad.Error.Class (MonadError, catchError, throwError)
+import Control.Monad.Fix (MonadFix, mfix)
+import Control.Monad.IO.Class (MonadIO, liftIO)
+import Control.Monad.RWS (MonadRWS)
+import Control.Monad.Reader.Class (MonadReader, ask, local)
+import Control.Monad.State.Class (MonadState, get, put)
+import Control.Monad.Writer.Class (MonadWriter, listen, pass, tell)
+import Data.Effect.Except
+import Data.Effect.Fail (Fail)
+import Data.Effect.Fail qualified as E
+import Data.Effect.Fix (Fix)
+import Data.Effect.Fix qualified as E
+import Data.Effect.NonDet (ChooseH, Empty, chooseH)
+import Data.Effect.NonDet qualified as E
+import Data.Effect.OpenUnion.Internal.FO (Lookup, MemberBy, Union, inj, type (<|))
+import Data.Effect.OpenUnion.Internal.HO (LookupH, MemberHBy, UnionH, injH, type (<<|))
+import Data.Effect.Reader (Ask, Local, ask'', local'')
+import Data.Effect.State (State, get'', put'')
+import Data.Effect.Unlift (UnliftIO)
+import Data.Effect.Unlift qualified as E
+import Data.Effect.Writer (Tell, WriterH, listen'', tell'')
 import Data.FTCQueue (FTCQueue, tsingleton, (|>))
+import Data.Function ((&))
 import Data.Kind (Type)
+import Data.Tuple (swap)
+import UnliftIO (MonadUnliftIO, withRunInIO)
 
 {- | The 'Eff' monad represents computations with effects.
 It supports higher-order effects @eh@ and first-order effects @ef@.
@@ -48,6 +74,107 @@ instance Monad (Eff eh ef) where
         Op e q -> Op e (q |> k)
     {-# INLINE (>>=) #-}
 
+instance (e <| ef) => SendIns e (Eff eh ef) where
+    sendIns = send
+    {-# INLINE sendIns #-}
+
+instance (e <<| eh) => SendSig e (Eff eh ef) where
+    sendSig = sendH
+    {-# INLINE sendSig #-}
+
+instance (MemberBy key ef, e ~ Lookup key ef) => SendInsBy key e (Eff eh ef) where
+    sendInsBy = send
+    {-# INLINE sendInsBy #-}
+
+instance (MemberHBy key eh, e ~ LookupH key eh) => SendSigBy key e (Eff eh ef) where
+    sendSigBy = sendH
+    {-# INLINE sendSigBy #-}
+
+instance
+    ( SendInsBy ReaderKey (Ask r) (Eff eh ef)
+    , SendSigBy ReaderKey (Local r) (Eff eh ef)
+    )
+    => MonadReader r (Eff eh ef)
+    where
+    ask = ask'' @ReaderKey
+    local = local'' @ReaderKey
+    {-# INLINE ask #-}
+    {-# INLINE local #-}
+
+data ReaderKey
+
+instance
+    ( SendInsBy WriterKey (Tell w) (Eff eh ef)
+    , SendSigBy WriterKey (WriterH w) (Eff eh ef)
+    , Monoid w
+    )
+    => MonadWriter w (Eff eh ef)
+    where
+    tell = tell'' @WriterKey
+    listen = fmap swap . listen'' @WriterKey
+    pass m = pass (ByKey m) & key @WriterKey
+    {-# INLINE tell #-}
+    {-# INLINE listen #-}
+
+data WriterKey
+
+instance
+    (SendInsBy StateKey (State s) (Eff eh ef))
+    => MonadState s (Eff eh ef)
+    where
+    get = get'' @StateKey
+    put = put'' @StateKey
+    {-# INLINE get #-}
+    {-# INLINE put #-}
+
+data StateKey
+
+instance
+    ( SendInsBy ErrorKey (Throw e) (Eff eh ef)
+    , SendSigBy ErrorKey (Catch e) (Eff eh ef)
+    )
+    => MonadError e (Eff eh ef)
+    where
+    throwError = throw'' @ErrorKey
+    catchError = catch'' @ErrorKey
+    {-# INLINE throwError #-}
+    {-# INLINE catchError #-}
+
+data ErrorKey
+
+instance
+    ( SendInsBy ReaderKey (Ask r) (Eff eh ef)
+    , SendSigBy ReaderKey (Local r) (Eff eh ef)
+    , SendInsBy WriterKey (Tell w) (Eff eh ef)
+    , SendSigBy WriterKey (WriterH w) (Eff eh ef)
+    , SendInsBy StateKey (State s) (Eff eh ef)
+    , Monoid w
+    )
+    => MonadRWS r w s (Eff eh ef)
+
+instance (Empty <| ef, ChooseH <<| eh) => Alternative (Eff eh ef) where
+    empty = E.empty
+    a <|> b = chooseH a b
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
+
+instance (Empty <| ef, ChooseH <<| eh) => MonadPlus (Eff eh ef)
+
+instance (IO <| ef) => MonadIO (Eff eh ef) where
+    liftIO = send
+    {-# INLINE liftIO #-}
+
+instance (Fail <| ef) => MonadFail (Eff eh ef) where
+    fail = E.fail
+    {-# INLINE fail #-}
+
+instance (Fix <<| eh) => MonadFix (Eff eh ef) where
+    mfix = E.mfix
+
+instance (UnliftIO <<| eh, IO <| ef) => MonadUnliftIO (Eff eh ef) where
+    withRunInIO = E.withRunInIO
+    {-# INLINE withRunInIO #-}
+
 infixr 3 $
 infixr 4 $$
 
@@ -88,11 +215,11 @@ sendUnionHBy :: (a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
 sendUnionHBy k u = Op (Left u) (tsingleton k)
 {-# INLINE sendUnionHBy #-}
 
-send :: (e <! ef) => e ~> Eff eh ef
+send :: (e <| ef) => e ~> Eff eh ef
 send = sendUnion . inj
 {-# INLINE send #-}
 
-sendH :: (e <!! eh) => e (Eff eh ef) ~> Eff eh ef
+sendH :: (e <<| eh) => e (Eff eh ef) ~> Eff eh ef
 sendH = sendUnionH . injH
 {-# INLINE sendH #-}
 
diff --git a/heftia/src/Data/Effect/OpenUnion.hs b/heftia/src/Data/Effect/OpenUnion.hs
index 2512909..4da44e2 100644
--- a/heftia/src/Data/Effect/OpenUnion.hs
+++ b/heftia/src/Data/Effect/OpenUnion.hs
@@ -27,11 +27,14 @@ import Data.Effect.OpenUnion.Internal (
     Take,
     WeakenN,
     WeakenNUnder,
+    WeakenUnder,
     type (++),
  )
 import Data.Effect.OpenUnion.Internal.FO (
     EffectF,
+    Lookup,
     Member,
+    MemberBy,
     Union,
     bundleAllUnion,
     bundleUnion,
@@ -47,8 +50,10 @@ import Data.Effect.OpenUnion.Internal.FO (
     prefixUnion,
     prefixUnionUnder,
     prj,
+    strengthen,
     strengthenN,
     strengthenNUnder,
+    strengthenUnder,
     suffixUnion,
     suffixUnionOverN,
     unbundleAllUnion,
@@ -57,13 +62,17 @@ import Data.Effect.OpenUnion.Internal.FO (
     weaken,
     weakenN,
     weakenNUnder,
+    weakenUnder,
     weakens,
+    weakensUnder,
     (!+),
-    type (<!),
+    type (<|),
  )
 import Data.Effect.OpenUnion.Internal.HO (
     EffectH,
+    LookupH,
     MemberH,
+    MemberHBy,
     UnionH,
     bundleAllUnionH,
     bundleUnionH,
@@ -90,9 +99,11 @@ import Data.Effect.OpenUnion.Internal.HO (
     weakenH,
     weakenNH,
     weakenNUnderH,
+    weakenUnderH,
     weakensH,
+    weakensUnderH,
     (!!+),
-    type (<!!),
+    type (<<|),
  )
 
 -- TODO: add injN/prjN/move/swap/insert/rotate functions.
diff --git a/heftia/src/Data/Effect/OpenUnion/Internal.hs b/heftia/src/Data/Effect/OpenUnion/Internal.hs
index 7316b65..bfef577 100644
--- a/heftia/src/Data/Effect/OpenUnion/Internal.hs
+++ b/heftia/src/Data/Effect/OpenUnion/Internal.hs
@@ -98,6 +98,14 @@ lexi-lambda/freer-simple#3, which describes the motivation in more detail.
 -}
 instance {-# INCOHERENT #-} IfNotFound e r w
 
+type LookupError (key :: kk) (w :: [ke]) =
+    TypeError
+        ( 'Text "The key ‘"
+            ':<>: 'ShowType key
+            ':<>: 'Text "’ does not exist in the type-level list"
+            ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"
+        )
+
 infixr 5 ++
 type family xs ++ ys where
     '[] ++ ys = ys
@@ -107,6 +115,15 @@ wordVal :: forall n. (KnownNat n) => Word
 wordVal = fromIntegral $ natVal @n Proxy
 {-# INLINE wordVal #-}
 
+class IsSuffixOf es es' where
+    prefixLen :: Word
+
+instance IsSuffixOf es es where
+    prefixLen = 0
+
+instance {-# INCOHERENT #-} (IsSuffixOf es es') => IsSuffixOf es (e ': es') where
+    prefixLen = prefixLen @es @es' + 1
+
 type family Length es where
     Length '[] = 0
     Length (e ': es) = 1 + Length es
@@ -124,16 +141,11 @@ type family PrefixLength es es' where
 
 -- fixme: Use type class with functional dependencies instaed of type family for readable compile error and compile speed.
 
-type IsSuffixOf_ es es' = KnownNat (PrefixLength es es')
-class (IsSuffixOf_ es es') => IsSuffixOf es es'
-instance (IsSuffixOf_ es es') => IsSuffixOf es es'
-
-prefixLen :: forall es es'. (es `IsSuffixOf` es') => Word
-prefixLen = wordVal @(PrefixLength es es')
-{-# INLINE prefixLen #-}
-
 type WeakenN len es es' = (es ~ Drop len es', KnownNat len)
 
+type WeakenUnder offset es es' =
+    (WeakenNUnder (PrefixLength es es') offset es es', KnownNat (PrefixLength es es'))
+
 type WeakenNUnder len offset es es' =
     (WeakenN len (Drop offset es) (Drop offset es'), KnownNat offset)
 
@@ -165,7 +177,7 @@ instance
     => StrengthenMap_ 'False len (e ': es) es'
     where
     strengthenMap = \case
-        0 -> unP $ elemNo @e @es
+        0 -> wordVal @(ElemIndex e es)
         n -> strengthenMap @_ @_ @(len - 1) @es @es' $ n - 1
     {-# INLINE strengthenMap #-}
 
diff --git a/heftia/src/Data/Effect/OpenUnion/Internal/FO.hs b/heftia/src/Data/Effect/OpenUnion/Internal/FO.hs
index f73222f..9acad2a 100644
--- a/heftia/src/Data/Effect/OpenUnion/Internal/FO.hs
+++ b/heftia/src/Data/Effect/OpenUnion/Internal/FO.hs
@@ -57,14 +57,17 @@ Based on [the open union in freer-simple](https://hackage.haskell.org/package/fr
 module Data.Effect.OpenUnion.Internal.FO where
 
 import Data.Coerce (coerce)
+import Data.Effect.Key (type (#>))
 import Data.Effect.OpenUnion.Internal (
     BundleUnder,
     Drop,
+    ElemIndex,
     FindElem,
     IfNotFound,
     IsSuffixOf,
     KnownLength,
     Length,
+    LookupError,
     P (unP),
     PrefixLength,
     Reverse,
@@ -76,6 +79,7 @@ import Data.Effect.OpenUnion.Internal (
     Take,
     WeakenN,
     WeakenNUnder,
+    WeakenUnder,
     elemNo,
     prefixLen,
     reifyLength,
@@ -181,8 +185,17 @@ instance (FindElem e es, IfNotFound e es es) => Member e es where
     prj = unsafePrj $ unP (elemNo :: P e es)
     {-# INLINE prj #-}
 
-infix 3 <!
-type (<!) = Member
+infix 3 <|
+type (<|) = Member
+
+type MemberBy key es = Lookup key es <| es
+
+type Lookup key es = Lookup_ key es es
+
+type family Lookup_ (key :: k) r w :: EffectF where
+    Lookup_ key (key #> e ': _) w = key #> e
+    Lookup_ key (_ ': r) w = Lookup_ key r w
+    Lookup_ key '[] w = LookupError key w
 
 {- | Orthogonal decomposition of a @'Union' (e ': es) :: 'EffectF'@. 'Right' value
 is returned if the @'Union' (e ': es) :: 'EffectF'@ contains @e :: 'EffectF'@, and
@@ -230,7 +243,7 @@ more summand.
 
 /O(1)/
 -}
-weaken :: Union es a -> Union (any ': es) a
+weaken :: forall any es a. Union es a -> Union (any ': es) a
 weaken (Union n a) = Union (n + 1) a
 {-# INLINE weaken #-}
 
@@ -242,6 +255,16 @@ weakenN :: forall len es es' a. (WeakenN len es es') => Union es a -> Union es'
 weakenN (Union n a) = Union (n + wordVal @len) a
 {-# INLINE weakenN #-}
 
+weakenUnder :: forall any e es a. Union (e ': es) a -> Union (e ': any ': es) a
+weakenUnder u@(Union n a)
+    | n == 0 = coerce u
+    | otherwise = Union (n + 1) a
+{-# INLINE weakenUnder #-}
+
+weakensUnder :: forall offset es es' a. (WeakenUnder offset es es') => Union es a -> Union es' a
+weakensUnder = weakenNUnder @(PrefixLength es es') @offset
+{-# INLINE weakensUnder #-}
+
 weakenNUnder
     :: forall len offset es es' a
      . (WeakenNUnder len offset es es')
@@ -252,6 +275,12 @@ weakenNUnder u@(Union n a)
     | otherwise = Union (n + wordVal @len) a
 {-# INLINE weakenNUnder #-}
 
+strengthen :: forall e es a. (e <| es) => Union (e ': es) a -> Union es a
+strengthen (Union n a)
+    | n == 0 = Union (wordVal @(ElemIndex e es)) a
+    | otherwise = Union (n - 1) a
+{-# INLINE strengthen #-}
+
 strengthens :: forall es es' a. (Strengthen es es') => Union es a -> Union es' a
 strengthens = strengthenN @(PrefixLength es' es)
 {-# INLINE strengthens #-}
@@ -260,6 +289,13 @@ strengthenN :: forall len es es' a. (StrengthenN len es es') => Union es a -> Un
 strengthenN (Union n a) = Union (strengthenMap @_ @_ @len @es @es' n) a
 {-# INLINE strengthenN #-}
 
+strengthenUnder :: forall e2 e1 es a. (e2 <| es) => Union (e1 ': e2 ': es) a -> Union (e1 ': es) a
+strengthenUnder u@(Union n a)
+    | n == 0 = coerce u
+    | n == 1 = Union (1 + wordVal @(ElemIndex e2 es)) a
+    | otherwise = Union (n - 1) a
+{-# INLINE strengthenUnder #-}
+
 strengthensUnder :: forall offset es es' a. (StrengthenUnder offset es es') => Union es a -> Union es' a
 strengthensUnder = strengthenNUnder @(PrefixLength es' es) @offset
 {-# INLINE strengthensUnder #-}
diff --git a/heftia/src/Data/Effect/OpenUnion/Internal/HO.hs b/heftia/src/Data/Effect/OpenUnion/Internal/HO.hs
index f372e61..6af22be 100644
--- a/heftia/src/Data/Effect/OpenUnion/Internal/HO.hs
+++ b/heftia/src/Data/Effect/OpenUnion/Internal/HO.hs
@@ -61,15 +61,19 @@ module Data.Effect.OpenUnion.Internal.HO where
 
 import Control.Effect (type (~>))
 import Data.Coerce (coerce)
+import Data.Effect (IsHFunctor)
 import Data.Effect.HFunctor (HFunctor, hfmap)
+import Data.Effect.Key (type (##>))
 import Data.Effect.OpenUnion.Internal (
     BundleUnder,
     Drop,
+    ElemIndex,
     FindElem,
     IfNotFound,
     IsSuffixOf,
     KnownLength,
     Length,
+    LookupError,
     P (unP),
     PrefixLength,
     Reverse,
@@ -81,6 +85,7 @@ import Data.Effect.OpenUnion.Internal (
     Take,
     WeakenN,
     WeakenNUnder,
+    WeakenUnder,
     elemNo,
     prefixLen,
     reifyLength,
@@ -90,6 +95,7 @@ import Data.Effect.OpenUnion.Internal (
     type (++),
  )
 import Data.Kind (Type)
+import Data.Type.Bool (type (&&))
 import GHC.TypeNats (KnownNat, type (-))
 import Unsafe.Coerce (unsafeCoerce)
 
@@ -107,11 +113,19 @@ data UnionH (es :: [EffectH]) (f :: Type -> Type) (a :: Type) where
         -- ^ Continuation of interpretation. Due to this component, this open union becomes a free 'HFunctor', which contributes to performance improvement.
         -> UnionH es f a
 
-hfmapUnion :: (f ~> g) -> UnionH es f a -> UnionH es g a
+class HFunctors es
+instance HFunctors '[]
+instance (IsHFunctor e ~ 'True, HFunctors es) => HFunctors (e ': es)
+
+type family IsHFunctors es where
+    IsHFunctors '[] = 'True
+    IsHFunctors (e ': es) = IsHFunctor e && IsHFunctors es
+
+hfmapUnion :: (HFunctors es) => (f ~> g) -> UnionH es f a -> UnionH es g a
 hfmapUnion phi (UnionH n e koi) = UnionH n e (phi . koi)
 {-# INLINE hfmapUnion #-}
 
-instance HFunctor (UnionH es) where
+instance (HFunctors es) => HFunctor (UnionH es) where
     hfmap f = hfmapUnion f
     {-# INLINE hfmap #-}
 
@@ -136,8 +150,17 @@ instance (FindElem e es, IfNotFound e es es) => MemberH e es where
     prjH = unsafePrjH $ unP (elemNo :: P e es)
     {-# INLINE prjH #-}
 
-infix 3 <!!
-type (<!!) = MemberH
+infix 3 <<|
+type (<<|) = MemberH
+
+type MemberHBy key es = LookupH key es <<| es
+
+type LookupH key es = LookupH_ key es es
+
+type family LookupH_ (key :: k) r w :: EffectH where
+    LookupH_ key (key ##> e ': _) w = key ##> e
+    LookupH_ key (_ ': r) w = LookupH_ key r w
+    LookupH_ key '[] w = LookupError key w
 
 decompH :: (HFunctor e) => UnionH (e ': es) f a -> Either (UnionH es f a) (e f a)
 decompH (UnionH 0 a koi) = Right $ hfmap koi $ unsafeCoerce a
@@ -160,7 +183,7 @@ extractH :: (HFunctor e) => UnionH '[e] f a -> e f a
 extractH (UnionH _ a koi) = hfmap koi $ unsafeCoerce a
 {-# INLINE extractH #-}
 
-weakenH :: UnionH es f a -> UnionH (any ': es) f a
+weakenH :: forall any es f a. UnionH es f a -> UnionH (any ': es) f a
 weakenH (UnionH n a koi) = UnionH (n + 1) a koi
 {-# INLINE weakenH #-}
 
@@ -172,6 +195,16 @@ weakenNH :: forall len es es' f a. (WeakenN len es es') => UnionH es f a -> Unio
 weakenNH (UnionH n a koi) = UnionH (n + wordVal @len) a koi
 {-# INLINE weakenNH #-}
 
+weakenUnderH :: forall any e es f a. UnionH (e ': es) f a -> UnionH (e ': any ': es) f a
+weakenUnderH u@(UnionH n a koi)
+    | n == 0 = coerce u
+    | otherwise = UnionH (n + 1) a koi
+{-# INLINE weakenUnderH #-}
+
+weakensUnderH :: forall offset es es' f a. (WeakenUnder offset es es') => UnionH es f a -> UnionH es' f a
+weakensUnderH = weakenNUnderH @(PrefixLength es es') @offset
+{-# INLINE weakensUnderH #-}
+
 weakenNUnderH
     :: forall len offset es es' f a
      . (WeakenNUnder len offset es es')
@@ -182,6 +215,12 @@ weakenNUnderH u@(UnionH n a koi)
     | otherwise = UnionH (n + wordVal @len) a koi
 {-# INLINE weakenNUnderH #-}
 
+strengthenH :: forall e es f a. (e <<| es) => UnionH (e ': es) f a -> UnionH es f a
+strengthenH (UnionH n a koi)
+    | n == 0 = UnionH (wordVal @(ElemIndex e es)) a koi
+    | otherwise = UnionH (n - 1) a koi
+{-# INLINE strengthenH #-}
+
 strengthensH :: forall es es' f a. (Strengthen es es') => UnionH es f a -> UnionH es' f a
 strengthensH = strengthenNH @(PrefixLength es' es)
 {-# INLINE strengthensH #-}
@@ -190,6 +229,13 @@ strengthenNH :: forall len es es' f a. (StrengthenN len es es') => UnionH es f a
 strengthenNH (UnionH n a koi) = UnionH (strengthenMap @_ @_ @len @es @es' n) a koi
 {-# INLINE strengthenNH #-}
 
+strengthenUnderH :: forall e2 e1 es f a. (e2 <<| es) => UnionH (e1 ': e2 ': es) f a -> UnionH (e1 ': es) f a
+strengthenUnderH u@(UnionH n a koi)
+    | n == 0 = coerce u
+    | n == 1 = UnionH (1 + wordVal @(ElemIndex e2 es)) a koi
+    | otherwise = UnionH (n - 1) a koi
+{-# INLINE strengthenUnderH #-}
+
 strengthensUnderH
     :: forall offset es es' f a
      . (StrengthenUnder offset es es')
@@ -300,7 +346,7 @@ bundleAllUnionH :: UnionH es f a -> UnionH '[UnionH es] f a
 bundleAllUnionH u = UnionH 0 u id
 {-# INLINE bundleAllUnionH #-}
 
-unbundleAllUnionH :: UnionH '[UnionH es] f a -> UnionH es f a
+unbundleAllUnionH :: (HFunctors es) => UnionH '[UnionH es] f a -> UnionH es f a
 unbundleAllUnionH = extractH
 {-# INLINE unbundleAllUnionH #-}