diff --git a/heftia-effects/Example/Writer/Main.hs b/heftia-effects/Example/Writer/Main.hs
index 12a3053..67270bb 100644
--- a/heftia-effects/Example/Writer/Main.hs
+++ b/heftia-effects/Example/Writer/Main.hs
@@ -4,46 +4,34 @@
 
 module Main where
 
-import Control.Effect.Class (sendIns, type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor)
-import Control.Effect.Class.Writer (Writer, censor, tell)
-import Control.Effect.Freer (runFreerEffects)
-import Control.Effect.Handler.Heftia.Writer (
-    elaborateWriterT,
-    elaborateWriterTransactionalT,
-    interpretTell,
- )
-import Control.Effect.Heftia (Elaborator, Hef, runElaborate)
-import Data.Hefty.Union (absurdUnionH, (|+:))
+import Control.Effect (sendIns, type (<:), type (<<:))
+import Control.Effect.ExtensibleFinal (runEff)
+import Control.Effect.Handler.Heftia.Writer (elaborateWriter, elaborateWriterTransactional, interpretTell)
+import Control.Effect.Hefty (interpretH)
+import Data.Effect.Writer (Tell, WriterH, censor, tell)
 
-hello :: (Writer String m, Monad m) => m ()
+hello :: (Tell String <: m, Monad m) => m ()
 hello = do
     tell "Hello"
     tell " world!"
 
-censorHello :: (Writer String m, Monad m) => m ()
+censorHello :: (Tell String <: m, WriterH String <<: m, Monad m) => m ()
 censorHello =
     censor
         (\s -> if s == "Hello" then "Goodbye" else s)
         hello
 
 main :: IO ()
-main = runFreerEffects do
+main = runEff do
     (s :: String, _) <-
         interpretTell
-            . runElaborate' (elaborateWriterT @String)
+            . interpretH (elaborateWriter @String)
             $ censorHello
 
     (sTransactional :: String, _) <-
         interpretTell
-            . runElaborate' (elaborateWriterTransactionalT @String)
+            . interpretH (elaborateWriterTransactional @String)
             $ censorHello
 
     sendIns $ putStrLn $ "Normal: " <> s
     sendIns $ putStrLn $ "Transactional: " <> sTransactional
-
-runElaborate' ::
-    (HFunctor e, Monad f) =>
-    Elaborator e f ->
-    Hef '[e] f ~> f
-runElaborate' f = runElaborate $ f |+: absurdUnionH
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/Except.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/Except.hs
index 3da0709..b0050bd 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/Except.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/Except.hs
@@ -16,7 +16,8 @@ module Control.Effect.Handler.Heftia.Except where
 
 import Control.Effect (type (~>))
 import Control.Effect.Hefty (
-    Effectful,
+    Eff,
+    Elab,
     MemberF,
     interposeK,
     interposeT,
@@ -25,39 +26,50 @@ import Control.Effect.Hefty (
  )
 import Control.Monad.Freer (MonadFreer)
 import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
-import Data.Effect (LNop)
-import Data.Effect.Except (Catch (Catch), Throw (Throw))
-import Data.Free.Sum (type (+))
+import Data.Effect.Except (Catch (Catch), LThrow, Throw (Throw))
 import Data.Function ((&))
 import Data.Hefty.Union (Union)
 
--- | Elaborate the 'Catch' effect using a delimited continuation.
+-- | Elaborate the t'Catch' effect using the 'ExceptT' monad transformer.
 elaborateCatch ::
-    (MemberF u (Throw e) ef, MonadFreer f, Union u) =>
-    Catch e (Effectful u f LNop ef) ~> Effectful u f LNop ef
-elaborateCatch (Catch action hdl) =
-    action & interposeK pure \_ (Throw e) -> hdl e
-
--- | Elaborate the 'Catch' effect using the 'ExceptT' monad transformer.
-elaborateCatchT ::
-    (MemberF u (Throw e) ef, MonadFreer f, Union u) =>
-    Catch e (Effectful u f LNop ef) ~> Effectful u f LNop ef
-elaborateCatchT (Catch action hdl) = do
+    forall e ef fr u.
+    (MemberF u (Throw e) ef, MonadFreer fr, Union u) =>
+    Elab (Catch e) (Eff u fr '[] ef)
+elaborateCatch (Catch action hdl) = do
     r <- runExceptT $ action & interposeT \(Throw e) -> throwE e
     case r of
         Left e -> hdl e
         Right a -> pure a
 
--- | Interpret the 'Throw' effect using a delimited continuation.
+-- | Elaborate the 'Catch' effect using a delimited continuation.
+elaborateCatchK ::
+    forall e ef fr u.
+    (MemberF u (Throw e) ef, MonadFreer fr, Union u) =>
+    Elab (Catch e) (Eff u fr '[] ef)
+elaborateCatchK (Catch action hdl) =
+    action & interposeK pure \_ (Throw e) -> hdl e
+
+-- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
 interpretThrow ::
-    (MonadFreer f, Union u) =>
-    Effectful u f LNop (Throw e + es) a ->
-    Effectful u f LNop es (Either e a)
-interpretThrow = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e
+    forall e r a fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LThrow e ': r) a ->
+    Eff u fr '[] r (Either e a)
+interpretThrow = runExceptT . interpretThrowT
+{-# INLINE interpretThrow #-}
 
 -- | Interpret the 'Throw' effect using the 'ExceptT' monad transformer.
 interpretThrowT ::
-    (MonadFreer f, Union u) =>
-    Effectful u f LNop (Throw e + es) ~> ExceptT e (Effectful u f LNop es)
+    forall e r fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LThrow e ': r) ~> ExceptT e (Eff u fr '[] r)
 interpretThrowT = interpretT \(Throw e) -> throwE e
 {-# INLINE interpretThrowT #-}
+
+-- | Interpret the 'Throw' effect using a delimited continuation.
+interpretThrowK ::
+    forall e r a fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LThrow e ': r) a ->
+    Eff u fr '[] r (Either e a)
+interpretThrowK = interpretK (pure . Right) \_ (Throw e) -> pure $ Left e
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/Provider.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/Provider.hs
index 782da13..e4dc28b 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/Provider.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/Provider.hs
@@ -14,16 +14,16 @@ Elaborator for the t'Control.Effect.Class.Provider.Provider' effect class.
 module Control.Effect.Handler.Heftia.Provider where
 
 import Control.Effect (type (~>))
-import Control.Effect.Class.Provider (ProviderS (Provide))
-import Control.Effect.Heftia (Elaborator)
+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.
 elaborateProvider ::
     (c g, e g) =>
     (f ~> g) ->
     (i -> forall x. g x -> f (ctx x)) ->
-    Elaborator (ProviderS c i ctx e) f
+    Elab (Provider' c i ctx e) f
 elaborateProvider iLower run (Provide i f) = run i $ f iLower
 {-# INLINE elaborateProvider #-}
 
@@ -34,6 +34,6 @@ monad transformer.
 elaborateProviderT ::
     (Monad m, MonadTrans t, c (t m), e (t m)) =>
     (i -> forall x. t m x -> m (ctx x)) ->
-    Elaborator (ProviderS c i ctx e) m
+    Elab (Provider' c i ctx e) m
 elaborateProviderT = elaborateProvider lift
 {-# INLINE elaborateProviderT #-}
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs
index 5732ce6..3c0f1c3 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/Provider/Implicit.hs
@@ -14,26 +14,30 @@ Elaborator for the t'Control.Effect.Class.Provider.Implicit.ImplicitProvider' ef
 module Control.Effect.Handler.Heftia.Provider.Implicit where
 
 import Control.Effect (type (~>))
-import Control.Effect.Class.Provider.Implicit (ImplicitProviderS (WithImplicit))
-import Control.Effect.Class.Reader (AskI)
-import Control.Effect.Freer (Fre, raise)
 import Control.Effect.Handler.Heftia.Reader (interpretAsk)
-import Control.Effect.Heftia (Elaborator)
+import Control.Effect.Hefty (Eff, Elab, raise)
+import Control.Monad.Freer (MonadFreer)
+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'Control.Effect.Class.Provider.Implicit.ImplicitProvider' effect using the given
-interpreter.
--}
+-- | Elaborate the t'ImplicitProvider'' effect using the given interpreter.
 elaborateImplicitProvider ::
     (c g, e g) =>
     (f ~> g) ->
     (i -> forall x. g x -> f x) ->
-    Elaborator (ImplicitProviderS c i e) f
+    Elab (ImplicitProvider' c i e) f
 elaborateImplicitProvider iLower run (WithImplicit i f) = run i $ f iLower
 {-# INLINE elaborateImplicitProvider #-}
 
--- todo: make the 'classy-effects-static' handler system and use the static Reader carrier here.
 runImplicitProvider ::
-    (c (Fre (AskI i ': r) m), e (Fre (AskI i ': r) m), Monad m) =>
-    Elaborator (ImplicitProviderS c i e) (Fre r m)
+    ( e (Eff u fr eh (LAsk i ': ef))
+    , c (Eff u fr eh (LAsk i ': ef))
+    , MonadFreer fr
+    , Union u
+    , HFunctor (u eh)
+    ) =>
+    Elab (ImplicitProvider' c i e) (Eff u fr eh ef)
 runImplicitProvider (WithImplicit i f) = interpretAsk i $ f raise
+{-# INLINE runImplicitProvider #-}
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/Reader.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/Reader.hs
index 842c625..3a2a7b6 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/Reader.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/Reader.hs
@@ -1,8 +1,6 @@
 -- 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/.
-{-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE UndecidableInstances #-}
 
 {- |
 Copyright   :  (c) 2023 Yamada Ryo
@@ -19,53 +17,45 @@ module Control.Effect.Handler.Heftia.Reader where
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
 import Control.Effect.Hefty (
-    Effectful,
-    HFunctors,
+    Eff,
+    Elab,
     MemberF,
-    TailHFunctor,
     interposeRec,
     interpretRec,
     interpretRecH,
  )
 import Control.Freer (Freer)
-import Data.Effect.HFunctor (type (:+:))
-import Data.Effect.Reader (Ask (..), Local (..), ask)
-import Data.Free.Sum (type (+))
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Reader (Ask (..), LAsk, Local (..), ask)
 import Data.Function ((&))
-import Data.Hefty.Union (HFunctorUnion, Union)
+import Data.Hefty.Union (ForallHFunctor, HFunctorUnion, Union)
 
 interpretReader ::
-    ( Freer c f
-    , forall f'. c f' => Applicative f'
+    forall r rh rf fr u c.
+    ( Freer c fr
     , HFunctorUnion u
-    , TailHFunctor u eh
-    , Applicative (Effectful u f eh ef)
-    , MemberF u (Ask r) (Ask r + ef)
-    , c (Effectful u f eh ef)
-    , c (Effectful u f eh (Ask r + ef))
+    , ForallHFunctor u rh
+    , MemberF u (Ask r) (LAsk r ': rf)
+    , Functor (Eff u fr rh (LAsk r ': rf))
+    , Applicative (Eff u fr rh rf)
     ) =>
     r ->
-    Effectful u f (Local r :+: eh) (Ask r + ef) ~> Effectful u f eh ef
+    Eff u fr (Local r ': rh) (LAsk r ': rf) ~> Eff u fr rh rf
 interpretReader r = interpretRecH elaborateLocal >>> interpretAsk r
 {-# INLINE interpretReader #-}
 
 -- | Elaborate the t'Local' effect.
 elaborateLocal ::
-    forall r eh ef f u c.
-    ( MemberF u (Ask r) ef
-    , Freer c f
-    , Union u
-    , HFunctors u eh
-    , Functor (Effectful u f eh ef)
-    ) =>
-    Local r (Effectful u f eh ef) ~> Effectful u f eh ef
+    forall r eh ef fr u c.
+    (MemberF u (Ask r) ef, Freer c fr, Union u, HFunctor (u eh), Functor (Eff u fr eh ef)) =>
+    Elab (Local r) (Eff u fr eh ef)
 elaborateLocal (Local f a) = a & interposeRec @(Ask r) \Ask -> f <$> ask
 
 -- | Interpret the t'Ask' effect.
 interpretAsk ::
-    forall r eh ef f u c.
-    (Freer c f, Union u, Applicative (Effectful u f eh ef), HFunctors u eh) =>
+    forall r rs eh fr u c.
+    (Freer c fr, Union u, Applicative (Eff u fr eh rs), HFunctor (u eh)) =>
     r ->
-    Effectful u f eh (Ask r + ef) ~> Effectful u f eh ef
+    Eff u fr eh (LAsk r ': rs) ~> Eff u fr eh rs
 interpretAsk r = interpretRec \Ask -> pure r
 {-# INLINE interpretAsk #-}
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/Resource.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/Resource.hs
index b54cc53..ac15851 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/Resource.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/Resource.hs
@@ -15,12 +15,12 @@ An elaborator for the t'Control.Effect.Class.Resource.Resource' effect class.
 -}
 module Control.Effect.Handler.Heftia.Resource where
 
-import Control.Effect.Class.Resource (ResourceS (Bracket, BracketOnExcept))
-import Control.Effect.Heftia (Elaborator)
+import Control.Effect.Hefty (Elab)
+import Data.Effect.Resource (Resource (Bracket, BracketOnExcept))
 import UnliftIO (MonadUnliftIO, bracket, bracketOnError)
 
 -- | Elaborates the `Resource` effect under the `MonadUnliftIO` context.
-resourceToIO :: MonadUnliftIO m => Elaborator ResourceS m
+resourceToIO :: MonadUnliftIO m => Elab Resource m
 resourceToIO = \case
     Bracket acquire release thing -> bracket acquire release thing
     BracketOnExcept acquire onError thing -> bracketOnError acquire onError thing
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs
index 2f026b8..a13dbcf 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs
@@ -15,49 +15,72 @@ module Control.Effect.Handler.Heftia.State where
 
 import Control.Arrow ((>>>))
 import Control.Effect (type (~>))
-import Control.Effect.Class.Reader (AskI (Ask), ask)
-import Control.Effect.Class.State (StateI (Get, Put))
-import Control.Effect.Freer (Fre, interpose, interpretK, interpretT, raiseUnder)
 import Control.Effect.Handler.Heftia.Reader (interpretAsk)
+import Control.Effect.Hefty (Eff, MemberF, interpose, interpretK, interpretT, raiseUnder)
+import Control.Monad.Freer (MonadFreer)
 import Control.Monad.State (StateT)
 import Control.Monad.Trans.State (runStateT)
 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))
 import Data.Function ((&))
 import Data.Functor ((<&>))
+import Data.Hefty.Union (Union)
 import Data.Tuple (swap)
 
 -- | Interpret the 'Get'/'Put' effects using the 'StateT' monad transformer.
-interpretState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m (s, a)
+interpretState ::
+    forall s r a fr u.
+    (MonadFreer fr, Union u) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
 interpretState s a = swap <$> runStateT (interpretStateT a) s
 {-# INLINE interpretState #-}
 
-evalState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m a
+evalState ::
+    forall s r fr u.
+    (MonadFreer fr, Union u) =>
+    s ->
+    Eff u fr '[] (LState s ': r) ~> Eff u fr '[] r
 evalState s a = snd <$> interpretState s a
 {-# INLINE evalState #-}
 
-execState :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m s
+execState ::
+    forall s r a fr u.
+    (MonadFreer fr, Union u) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r s
 execState s a = fst <$> interpretState s a
 {-# INLINE execState #-}
 
 -- | Interpret the 'Get'/'Put' effects using the 'StateT' monad transformer.
-interpretStateT :: forall s es m. Monad m => Fre (StateI s ': es) m ~> StateT s (Fre es m)
-interpretStateT = interpretT \case
-    Get -> T.get
-    Put s -> T.put s
+interpretStateT ::
+    forall s r fr u.
+    (MonadFreer fr, Union u) =>
+    Eff u fr '[] (LState s ': r) ~> StateT s (Eff u fr '[] r)
+interpretStateT =
+    interpretT \case
+        Get -> T.get
+        Put s -> T.put s
 {-# INLINE interpretStateT #-}
 
-{- |
-Interpret the 'Get'/'Put' effects using the t'Control.Monad.Trans.Cont.ContT' continuation monad
-transformer.
--}
-interpretStateK :: forall s es m a. Monad m => s -> Fre (StateI s ': es) m a -> Fre es m (s, a)
+-- | Interpret the 'Get'/'Put' effects using delimited continuations.
+interpretStateK ::
+    forall s r a fr u.
+    (MonadFreer fr, Union u, HFunctor (u '[]), MemberF u (Ask s) (LAsk s ': r)) =>
+    s ->
+    Eff u fr '[] (LState s ': r) a ->
+    Eff u fr '[] r (s, a)
 interpretStateK initialState =
     raiseUnder
         >>> interpretK
             (\a -> ask <&> (,a))
             ( \k -> \case
                 Get -> k =<< ask
-                Put s -> k () & interpose @(AskI s) \Ask -> pure s
+                Put s -> k () & interpose @(Ask s) \Ask -> pure s
             )
         >>> interpretAsk initialState
 {-# INLINE interpretStateK #-}
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs
index aca1cbd..dba2f35 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/Writer.hs
@@ -17,26 +17,29 @@ See [README.md](https://github.com/sayo-hs/heftia/blob/master/README.md).
 module Control.Effect.Handler.Heftia.Writer where
 
 import Control.Effect (type (~>))
-import Control.Effect.Class.Writer (Tell (tell), TellI (Tell), WriterS (Censor, Listen))
-import Control.Effect.Freer (Fre, intercept, interposeT, interpretK, interpretT, type (<|))
+import Control.Effect.Hefty (Eff, Elab, MemberF, interposeT, interpretK, interpretT, rewrite)
+import Control.Monad.Freer (MonadFreer)
 import Control.Monad.Trans.Writer.CPS (WriterT, runWriterT)
 import Control.Monad.Trans.Writer.CPS qualified as T
+import Data.Effect.HFunctor (HFunctor)
+import Data.Effect.Writer (LTell, Tell (Tell), WriterH (Censor, Listen), tell)
 import Data.Function ((&))
+import Data.Hefty.Union (Union)
 import Data.Tuple (swap)
 
-elaborateWriterT ::
-    forall w m es.
-    (Monad m, Monoid w, TellI w <| es) =>
-    WriterS w (Fre es m) ~> Fre es m
-elaborateWriterT = \case
+elaborateWriter ::
+    forall w ef fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) ef, HFunctor (u '[])) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elaborateWriter = \case
     Listen m -> listenT m
-    Censor f m -> m & intercept @(TellI w) \(Tell w) -> Tell $ f w
+    Censor f m -> m & rewrite @(Tell w) \(Tell w) -> Tell $ f w
 
-elaborateWriterTransactionalT ::
-    forall w m es.
-    (Monad m, Monoid w, TellI w <| es) =>
-    WriterS w (Fre es m) ~> Fre es m
-elaborateWriterTransactionalT = \case
+elaborateWriterTransactional ::
+    forall w ef fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) ef) =>
+    Elab (WriterH w) (Eff u fr '[] ef)
+elaborateWriterTransactional = \case
     Listen m -> listenT m
     Censor f m -> do
         (a, w) <- confiscateT m
@@ -44,9 +47,10 @@ elaborateWriterTransactionalT = \case
         pure a
 
 listenT ::
-    (Monoid w, Monad m, TellI w <| es) =>
-    Fre es m a ->
-    Fre es m (a, w)
+    forall w es a fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) es) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es (a, w)
 listenT m = do
     (a, w) <- confiscateT m
     tell w
@@ -54,22 +58,22 @@ listenT m = do
 {-# INLINE listenT #-}
 
 confiscateT ::
-    forall w m es a.
-    (Monoid w, Monad m, TellI w <| es) =>
-    Fre es m a ->
-    Fre es m (a, w)
-confiscateT = runWriterT . interposeT @(TellI w) \(Tell w) -> T.tell w
+    forall w es a fr u.
+    (Monoid w, MonadFreer fr, Union u, MemberF u (Tell w) es) =>
+    Eff u fr '[] es a ->
+    Eff u fr '[] es (a, w)
+confiscateT = runWriterT . interposeT @(Tell w) \(Tell w) -> T.tell w
 {-# INLINE confiscateT #-}
 
-interpretTell :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> Fre es m (w, a)
+interpretTell :: (Monoid w, MonadFreer fr, Union u) => Eff u fr '[] (LTell w ': r) a -> Eff u fr '[] r (w, a)
 interpretTell = fmap swap . runWriterT . interpretTellT
 {-# INLINE interpretTell #-}
 
-interpretTellT :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> WriterT w (Fre es m) a
+interpretTellT :: (Monoid w, MonadFreer fr, Union u) => Eff u fr '[] (LTell w ': r) ~> WriterT w (Eff u fr '[] r)
 interpretTellT = interpretT \(Tell w) -> T.tell w
 {-# INLINE interpretTellT #-}
 
-interpretTellK :: (Monad m, Monoid w) => Fre (TellI w ': es) m a -> Fre es m (w, a)
+interpretTellK :: (Monoid w, MonadFreer fr, Union u) => Eff u fr '[] (LTell w ': r) a -> Eff u fr '[] r (w, a)
 interpretTellK =
     interpretK (pure . (mempty,)) \k (Tell w) -> do
         (w', r) <- k ()
diff --git a/heftia/heftia.cabal b/heftia/heftia.cabal
index 51d6340..8b94b62 100644
--- a/heftia/heftia.cabal
+++ b/heftia/heftia.cabal
@@ -56,12 +56,15 @@ library
     exposed-modules:
         Control.Effect.Hefty
         Control.Effect.Free
+        Control.Effect.ExtensibleFinal
         Control.Effect.ExtensibleChurch
         Control.Effect.ExtensibleTree
+        Control.Effect.ExtensibleFinalA
         Control.Effect.ExtensibleTreeA
         Control.Effect.ExtensibleFastA
         Control.Hefty
         Control.Freer
+        Control.Freer.Final
         Control.Monad.Freer
         Control.Monad.Freer.Church
         Control.Monad.Freer.Tree
diff --git a/heftia/src/Control/Effect/ExtensibleChurch.hs b/heftia/src/Control/Effect/ExtensibleChurch.hs
index 93d83c4..562568c 100644
--- a/heftia/src/Control/Effect/ExtensibleChurch.hs
+++ b/heftia/src/Control/Effect/ExtensibleChurch.hs
@@ -13,9 +13,13 @@ Type operators for extensible effectful programs based on the Church-encoded Fre
 -}
 module Control.Effect.ExtensibleChurch where
 
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
 import Control.Monad.Freer.Church (FreerChurch)
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion FreerChurch eh ef
@@ -29,3 +33,11 @@ type (:!) efs = EffF ExtensibleUnion FreerChurch efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Monad f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Monad f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/ExtensibleFastA.hs b/heftia/src/Control/Effect/ExtensibleFastA.hs
index fed9829..3defefc 100644
--- a/heftia/src/Control/Effect/ExtensibleFastA.hs
+++ b/heftia/src/Control/Effect/ExtensibleFastA.hs
@@ -16,8 +16,12 @@ See "Control.Applicative.Free.Fast".
 module Control.Effect.ExtensibleFastA where
 
 import Control.Applicative.Free.Fast (Ap)
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion Ap eh ef
@@ -31,3 +35,11 @@ type (:!) efs = EffF ExtensibleUnion Ap efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Applicative f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/ExtensibleFinal.hs b/heftia/src/Control/Effect/ExtensibleFinal.hs
new file mode 100644
index 0000000..9946ba4
--- /dev/null
+++ b/heftia/src/Control/Effect/ExtensibleFinal.hs
@@ -0,0 +1,43 @@
+-- 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-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the final-encoded Freer monad.
+-}
+module Control.Effect.ExtensibleFinal where
+
+import Control.Effect (type (~>))
+import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
+import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Control.Freer.Final (FreerFinal)
+import Data.Effect (LiftIns)
+import Data.Hefty.Extensible (ExtensibleUnion)
+
+type eh !! ef = Effectful ExtensibleUnion (FreerFinal Monad) eh ef
+type (!) ef = EffectfulF ExtensibleUnion (FreerFinal Monad) ef
+
+infixr 5 !!
+infixr 4 !
+
+type ehs :!! efs = Eff ExtensibleUnion (FreerFinal Monad) ehs efs
+type (:!) efs = EffF ExtensibleUnion (FreerFinal Monad) efs
+
+infixr 5 :!!
+infixr 4 :!
+
+runEff :: Monad f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Monad f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/ExtensibleFinalA.hs b/heftia/src/Control/Effect/ExtensibleFinalA.hs
new file mode 100644
index 0000000..c06188b
--- /dev/null
+++ b/heftia/src/Control/Effect/ExtensibleFinalA.hs
@@ -0,0 +1,43 @@
+-- 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-2024 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+Type operators for extensible effectful programs based on the final-encoded Freer applicative.
+-}
+module Control.Effect.ExtensibleFinalA where
+
+import Control.Effect (type (~>))
+import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
+import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Control.Freer.Final (FreerFinal)
+import Data.Effect (LiftIns)
+import Data.Hefty.Extensible (ExtensibleUnion)
+
+type eh !! ef = Effectful ExtensibleUnion (FreerFinal Applicative) eh ef
+type (!) ef = EffectfulF ExtensibleUnion (FreerFinal Applicative) ef
+
+infixr 5 !!
+infixr 4 !
+
+type ehs :!! efs = Eff ExtensibleUnion (FreerFinal Applicative) ehs efs
+type (:!) efs = EffF ExtensibleUnion (FreerFinal Applicative) efs
+
+infixr 5 :!!
+infixr 4 :!
+
+runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Applicative f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/ExtensibleTree.hs b/heftia/src/Control/Effect/ExtensibleTree.hs
index ac2ae9b..e3c7fe6 100644
--- a/heftia/src/Control/Effect/ExtensibleTree.hs
+++ b/heftia/src/Control/Effect/ExtensibleTree.hs
@@ -13,9 +13,13 @@ Type operators for extensible effectful programs based on the tree-structured en
 -}
 module Control.Effect.ExtensibleTree where
 
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
 import Control.Monad.Freer.Tree (FreerTree)
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion FreerTree eh ef
@@ -29,3 +33,11 @@ type (:!) efs = EffF ExtensibleUnion FreerTree efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Monad f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Monad f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/ExtensibleTreeA.hs b/heftia/src/Control/Effect/ExtensibleTreeA.hs
index add1db9..cfe6a15 100644
--- a/heftia/src/Control/Effect/ExtensibleTreeA.hs
+++ b/heftia/src/Control/Effect/ExtensibleTreeA.hs
@@ -17,8 +17,12 @@ See "Control.Applicative.Free".
 module Control.Effect.ExtensibleTreeA where
 
 import Control.Applicative.Free (Ap)
+import Control.Effect (type (~>))
 import Control.Effect.Free (EffF, EffectfulF)
+import Control.Effect.Free qualified as F
 import Control.Effect.Hefty (Eff, Effectful)
+import Control.Effect.Hefty qualified as H
+import Data.Effect (LiftIns)
 import Data.Hefty.Extensible (ExtensibleUnion)
 
 type eh !! ef = Effectful ExtensibleUnion Ap eh ef
@@ -32,3 +36,11 @@ type (:!) efs = EffF ExtensibleUnion Ap efs
 
 infixr 5 :!!
 infixr 4 :!
+
+runEff :: Applicative f => '[] :!! '[LiftIns f] ~> f
+runEff = H.runEff
+{-# INLINE runEff #-}
+
+runEffF :: Applicative f => (:!) '[LiftIns f] ~> f
+runEffF = F.runEffF
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/Free.hs b/heftia/src/Control/Effect/Free.hs
index 30a939d..61182e1 100644
--- a/heftia/src/Control/Effect/Free.hs
+++ b/heftia/src/Control/Effect/Free.hs
@@ -18,18 +18,18 @@ module Control.Effect.Free where
 
 import Control.Effect (type (~>))
 
-import Control.Effect.Hefty (Eff, EffUnion (EffUnion), MemberF, SumToUnionListNF, caseHF)
+import Control.Effect.Hefty (Eff, EffUnion (EffUnion), MemberF, caseHF)
 import Control.Freer (Freer, InjectIns, ViaFreer (ViaFreer), injectIns, transformFreer, viaFreer)
 import Control.Hefty (Hefty (Hefty), unHefty)
 import Data.Effect (LiftIns (LiftIns), Nop, SigClass)
 import Data.Free.Sum (pattern R1)
-import Data.Hefty.Union (Union, exhaust, injectRec)
+import Data.Hefty.Union (U, Union, exhaust, injectRec)
 
 {- |
 A common type for representing first-order extensible effectful programs that can issue effects
 belonging to the specified sum of effect classes.
 -}
-type EffectfulF u fr e = EffF u fr (SumToUnionListNF u e)
+type EffectfulF u fr e = EffF u fr (U u e)
 
 {- |
 A common type for representing first-order extensible effectful programs that can issue effects
@@ -51,12 +51,12 @@ toEffF =
         . unHefty
 {-# INLINE toEffF #-}
 
-fromEffectfulF :: forall es fr u c. Freer c fr => EffF u fr es ~> Eff u fr '[] es
-fromEffectfulF =
+fromEffF :: forall es fr u c. Freer c fr => EffF u fr es ~> Eff u fr '[] es
+fromEffF =
     Hefty
         . transformFreer (EffUnion . R1 . unEffUnionF)
         . viaFreer
-{-# INLINE fromEffectfulF #-}
+{-# INLINE fromEffF #-}
 
 {-  all types of interpret-family functions:
         - interpret   :                 e  ~> E r           ->    E (e + r)  ~> E r
@@ -76,3 +76,7 @@ fromEffectfulF =
 
     todo patterns: all ( 4x3 + 3 = 16 functions )
 -}
+
+runEffF :: forall f fr u c. (Freer c fr, Union u, c f) => EffF u fr '[LiftIns f] ~> f
+runEffF = undefined
+{-# INLINE runEffF #-}
diff --git a/heftia/src/Control/Effect/Hefty.hs b/heftia/src/Control/Effect/Hefty.hs
index 33ee09b..99ecd75 100644
--- a/heftia/src/Control/Effect/Hefty.hs
+++ b/heftia/src/Control/Effect/Hefty.hs
@@ -24,37 +24,37 @@ import Control.Monad.Freer (MonadFreer, interpretFreerK)
 import Control.Monad.Identity (Identity (Identity))
 import Control.Monad.Trans (MonadTrans)
 import Data.Coerce (coerce)
-import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns)
+import Data.Effect (LiftIns (LiftIns), Nop, SigClass, unliftIns)
 import Data.Effect.HFunctor (HFunctor, caseH, hfmap, (:+:))
 import Data.Free.Sum (caseF, pattern L1, pattern R1, type (+))
 import Data.Hefty.Union (
-    ForallHFunctor,
     HFunctorUnion,
-    HasMembership,
+    HFunctorUnion_ (ForallHFunctor),
+    HeadIns,
+    LiftInsIfSingle (liftInsIfSingle, unliftInsIfSingle),
     MemberRec,
-    Union,
-    exhaust,
-    inject0,
+    U,
+    UH,
+    Union (HasMembership, exhaust, inject0, weaken, weakenUnder, (|+:)),
+    UnliftIfSingle,
     injectRec,
     projectRec,
-    weaken,
-    weakenUnder,
-    (|+:),
+    (|+),
  )
 import Data.Kind (Type)
 
-{- |
-A common type for representing first-order and higher-order extensible effectful programs that can
-issue effects belonging to the specified sum of effect classes.
--}
-type Effectful u fr eh ef = Eff u fr (SumToUnionListNH u eh) (SumToUnionListNF u ef)
-
 {- |
 A common type for representing first-order and higher-order extensible effectful programs that can
 issue effects belonging to the specified list of effect classes.
 -}
 type Eff u fr ehs efs = Hefty fr (EffUnion u ehs efs)
 
+{- |
+A common type for representing first-order and higher-order extensible effectful programs that can
+issue effects belonging to the specified sum of effect classes.
+-}
+type Effectful u fr eh ef = Eff u fr (UH u eh) (U u ef)
+
 {- |
 A common wrapper data type for representing first-order and higher-order extensible effect union.
 -}
@@ -90,75 +90,7 @@ type (f :: Type -> Type) $ a = f a
 -- | Type-level infix applcation for higher-order functors.
 type (h :: (Type -> Type) -> Type -> Type) $$ f = h f
 
-{- |
-Recursively decompose the sum of higher-order effects into a list, following the direction of right
-association, with normalization.
--}
-type SumToUnionListNH u eh = SumToUnionList u (NormalizeSig eh)
-
-{- |
-Recursively decompose the sum of first-order effects into a list, following the direction of right
-association, with normalization.
--}
-type SumToUnionListNF u ef = SumToUnionListNH u (LiftIns ef)
-
-{- |
-Recursively decompose the sum of higher-order effects into a list, following the direction of right
-association.
--}
-type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where
-    SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2
-    SumToUnionList u LNop = '[]
-    SumToUnionList u (SingleSig e) = '[e]
-
-{- |
-Convert a given list of higher-order effect classes into a suitable representation type for each
-case of being empty, single, or multiple.
--}
-type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
-    MultiListToUnion u '[] = LNop
-    MultiListToUnion u '[e] = e
-    MultiListToUnion u es = u es
-
-{- |
-Normalization in preparation for decomposing the sum of effect classes into a list.
-
-In particular, mark an indivisible, single effect class by applying the t'SingleSig' wrapper to it.
--}
-type family NormalizeSig e where
-    NormalizeSig (LiftIns Nop) = LiftIns Nop
-    NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2)
-    NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2
-    NormalizeSig e = SingleSig e
-
-{- |
-A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as
-a sum.
--}
-newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a}
-    deriving newtype (HFunctor)
-
-type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le
-
-type family UnliftIfSingle e where
-    UnliftIfSingle (LiftIns e) = e
-    UnliftIfSingle e = e Nop
-
-class LiftInsIfSingle e le where
-    liftInsIfSingle :: e ~> le Nop
-    unliftInsIfSingle :: le Nop ~> e
-
-instance LiftInsIfSingle (e Nop) e where
-    liftInsIfSingle = id
-    unliftInsIfSingle = id
-    {-# INLINE liftInsIfSingle #-}
-    {-# INLINE unliftInsIfSingle #-}
-
-instance LiftInsIfSingle e (LiftIns e) where
-    liftInsIfSingle = LiftIns
-    unliftInsIfSingle = unliftIns
-    {-# INLINE liftInsIfSingle #-}
-    {-# INLINE unliftInsIfSingle #-}
+type Elab e f = e f ~> f
 
 injectH :: (Freer c f, HFunctor (u ehs)) => u ehs (Eff u f ehs efs) ~> Eff u f ehs efs
 injectH = Hefty . liftIns . EffUnion . L1
@@ -199,7 +131,7 @@ injectF = Hefty . liftIns . EffUnion . R1
             - FH
 
     todo patterns:
-        - translate*, rewrite* in tramsform-family ( 2x3 = 6 functions )
+        - translate* in tramsform-family ( 3 functions )
         - *{FH,FH_} in interpret-family ( (4x2+1) + 2 = 11 functions )
 -}
 
@@ -228,7 +160,7 @@ interpretH_ ::
 interpretH_ i = interpretAllH_ $ i |+: exhaust
 {-# INLINE interpretH_ #-}
 
--- | Interpret the leading first-order effect class using a delimited continuation.
+-- | Interpret the leading first-order effect class using delimited continuations.
 interpretK ::
     forall e rs r a ehs fr u.
     (MonadFreer fr, Union u, HeadIns e) =>
@@ -755,6 +687,48 @@ transformFH fh ff =
         (inject0 . (liftInsIfSingle . ff . unliftInsIfSingle) |+: weaken)
 {-# INLINE transformFH #-}
 
+rewrite ::
+    forall e efs ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), MemberF u e efs) =>
+    (e ~> e) ->
+    Eff u fr ehs efs ~> Eff u fr ehs efs
+rewrite f =
+    transformAll
+        \u -> case projectRec u of
+            Just (LiftIns e) -> injectRec $ LiftIns $ f e
+            Nothing -> u
+{-# INLINE rewrite #-}
+
+rewriteH ::
+    forall e efs ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), MemberH u e ehs) =>
+    (e (Eff u fr ehs efs) ~> e (Eff u fr ehs efs)) ->
+    Eff u fr ehs efs ~> Eff u fr ehs efs
+rewriteH f =
+    transformAllH
+        \u -> case projectRec u of
+            Just e -> injectRec $ f e
+            Nothing -> u
+{-# INLINE rewriteH #-}
+
+rewriteFH ::
+    forall eh ef efs ehs fr u c.
+    (Freer c fr, Union u, HFunctor (u ehs), MemberH u eh ehs, MemberF u ef efs) =>
+    (eh (Eff u fr ehs efs) ~> eh (Eff u fr ehs efs)) ->
+    (ef ~> ef) ->
+    Eff u fr ehs efs ~> Eff u fr ehs efs
+rewriteFH fh ff =
+    transformAllFH
+        ( \u -> case projectRec u of
+            Just e -> injectRec $ fh e
+            Nothing -> u
+        )
+        ( \u -> case projectRec u of
+            Just (LiftIns e) -> injectRec $ LiftIns $ ff e
+            Nothing -> u
+        )
+{-# INLINE rewriteFH #-}
+
 transformAll ::
     forall efs' efs ehs fr u c.
     (Freer c fr, Union u, HFunctor (u ehs)) =>
@@ -852,3 +826,7 @@ send0 = Hefty . liftIns . EffUnion . R1 . inject0 . liftInsIfSingle
 send0H :: (Freer c fr, Union u) => e (Eff u fr (e ': r) ef) ~> Eff u fr (e ': r) ef
 send0H = Hefty . liftIns . EffUnion . L1 . inject0
 {-# INLINE send0H #-}
+
+runEff :: forall f fr u c. (Freer c fr, Union u, c f) => Eff u fr '[] '[LiftIns f] ~> f
+runEff = interpretAll $ id |+ exhaust
+{-# INLINE runEff #-}
diff --git a/heftia/src/Control/Freer.hs b/heftia/src/Control/Freer.hs
index 2513919..37ae9e1 100644
--- a/heftia/src/Control/Freer.hs
+++ b/heftia/src/Control/Freer.hs
@@ -18,6 +18,7 @@ module Control.Freer where
 
 import Control.Applicative (Alternative)
 import Control.Applicative.Free (Ap, liftAp, runAp)
+import Control.Applicative.Free.Fast qualified as Fast
 import Control.Effect (SendIns, sendIns, type (~>))
 import Control.Monad (MonadPlus)
 import Control.Monad.Base (MonadBase)
@@ -65,6 +66,12 @@ instance Freer Applicative Ap where
     {-# INLINE liftIns #-}
     {-# INLINE interpretFreer #-}
 
+instance Freer Applicative Fast.Ap where
+    liftIns = Fast.liftAp
+    interpretFreer = Fast.runAp
+    {-# INLINE liftIns #-}
+    {-# INLINE interpretFreer #-}
+
 newtype
     ViaFreer
         (fr :: InsClass -> Type -> Type)
diff --git a/heftia/src/Control/Freer/Final.hs b/heftia/src/Control/Freer/Final.hs
new file mode 100644
index 0000000..2b74af4
--- /dev/null
+++ b/heftia/src/Control/Freer/Final.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Use fmap" #-}
+{-# HLINT ignore "Use const" #-}
+{-# HLINT ignore "Avoid lambda" #-}
+
+-- 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 Yamada Ryo
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+Stability   :  experimental
+Portability :  portable
+
+A final-encoded generic Freer carrier.
+-}
+module Control.Freer.Final where
+
+import Control.Applicative (Alternative, empty, liftA2, many, some, (<|>))
+import Control.Effect (type (~>))
+import Control.Freer (Freer, interpretFreer, liftIns)
+import Control.Monad (MonadPlus, mplus, mzero)
+import Control.Monad.Freer (MonadFreer)
+
+-- | A final-encoded generic Freer carrier.
+newtype FreerFinal c f a = FreerFinal {unFreerFinal :: forall m. c m => (f ~> m) -> m a}
+
+deriving stock instance (forall f. c f => Functor f) => Functor (FreerFinal c e)
+
+instance
+    (forall f. c f => Applicative f, Functor (FreerFinal c e)) =>
+    Applicative (FreerFinal c e)
+    where
+    pure x = FreerFinal \_ -> pure x
+
+    FreerFinal f <*> FreerFinal g =
+        FreerFinal \i -> f i <*> g i
+
+    liftA2 f (FreerFinal fa) (FreerFinal fb) =
+        FreerFinal \i -> liftA2 f (fa i) (fb i)
+
+    FreerFinal f *> FreerFinal g =
+        FreerFinal \i -> f i *> g i
+
+    FreerFinal f <* FreerFinal g =
+        FreerFinal \i -> f i <* g i
+
+    {-# INLINE pure #-}
+    {-# INLINE (<*>) #-}
+    {-# INLINE liftA2 #-}
+    {-# INLINE (*>) #-}
+    {-# INLINE (<*) #-}
+
+instance
+    (forall f. c f => Alternative f, Applicative (FreerFinal c e)) =>
+    Alternative (FreerFinal c e)
+    where
+    empty = FreerFinal \_ -> empty
+
+    FreerFinal f <|> FreerFinal g =
+        FreerFinal \i -> f i <|> g i
+
+    some (FreerFinal f) = FreerFinal \i -> some (f i)
+    many (FreerFinal f) = FreerFinal \i -> many (f i)
+
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
+    {-# INLINE some #-}
+    {-# INLINE many #-}
+
+instance (forall m. c m => Monad m, Applicative (FreerFinal c f)) => Monad (FreerFinal c f) where
+    FreerFinal f >>= k =
+        FreerFinal \i ->
+            f i >>= interpretFreerFinal i . k
+
+    (>>) = (*>)
+    return = pure
+
+    {-# INLINE (>>=) #-}
+    {-# INLINE (>>) #-}
+    {-# INLINE return #-}
+
+instance
+    (forall m. c m => MonadPlus m, Alternative (FreerFinal c f), Monad (FreerFinal c f)) =>
+    MonadPlus (FreerFinal c f)
+    where
+    mzero = FreerFinal \_ -> mzero
+
+    FreerFinal f `mplus` FreerFinal g =
+        FreerFinal \i -> f i `mplus` g i
+
+    {-# INLINE mzero #-}
+    {-# INLINE mplus #-}
+
+interpretFreerFinal :: c f => (e ~> f) -> FreerFinal c e a -> f a
+interpretFreerFinal i (FreerFinal f) = f i
+{-# INLINE interpretFreerFinal #-}
+
+liftInsFinal :: ins a -> FreerFinal c ins a
+liftInsFinal e = FreerFinal \i -> i e
+{-# INLINE liftInsFinal #-}
+
+instance (forall e. c (FreerFinal c e)) => Freer c (FreerFinal c) where
+    liftIns = liftInsFinal
+    interpretFreer = interpretFreerFinal
+    {-# INLINE liftIns #-}
+    {-# INLINE interpretFreer #-}
+
+instance MonadFreer (FreerFinal Monad)
diff --git a/heftia/src/Control/Hefty.hs b/heftia/src/Control/Hefty.hs
index 4714372..2224af6 100644
--- a/heftia/src/Control/Hefty.hs
+++ b/heftia/src/Control/Hefty.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE QuantifiedConstraints #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- This Source Code Form is subject to the terms of the Mozilla Public
diff --git a/heftia/src/Control/Monad/Freer.hs b/heftia/src/Control/Monad/Freer.hs
index 28fe4b7..af49845 100644
--- a/heftia/src/Control/Monad/Freer.hs
+++ b/heftia/src/Control/Monad/Freer.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 
 {-# HLINT ignore "Eta reduce" #-}
@@ -12,7 +14,15 @@ import Control.Effect (type (~>))
 import Control.Freer (Freer, interpretFreer)
 import Control.Monad.Cont (Cont)
 
-class Freer Monad f => MonadFreer f where
-    interpretFreerK :: (e ~> Cont r) -> f e ~> Cont r
+class Freer Monad fr => MonadFreer fr where
+    interpretFreerK :: (e ~> Cont r) -> fr e ~> Cont r
     interpretFreerK i = interpretFreer i
     {-# INLINE interpretFreerK #-}
+
+{-
+class (Freer c fr, forall f. c f => Monad f) => MonadFreer c fr where
+    interpretFreerK :: (e ~> Cont r) -> fr e ~> Cont r
+    default interpretFreerK :: c (Cont r) => (e ~> Cont r) -> fr e ~> Cont r
+    interpretFreerK i = interpretFreer i
+    {-# INLINE interpretFreerK #-}
+-}
diff --git a/heftia/src/Data/Hefty/Union.hs b/heftia/src/Data/Hefty/Union.hs
index 0c86941..8a9cb70 100644
--- a/heftia/src/Data/Hefty/Union.hs
+++ b/heftia/src/Data/Hefty/Union.hs
@@ -22,9 +22,9 @@ module Data.Hefty.Union where
 import Control.Effect (type (~>))
 import Control.Monad ((<=<))
 import Data.Bool.Singletons (SBool (SFalse, STrue))
-import Data.Coerce (Coercible)
-import Data.Effect (LiftIns, SigClass, unliftIns)
+import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns)
 import Data.Effect.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))
+import Data.Free.Sum (type (+))
 import Data.Kind (Constraint)
 import Data.Singletons (SingI, sing)
 import Data.Type.Bool (If, type (||))
@@ -305,3 +305,91 @@ infixr 5 |+
 (|+) :: Union u => (e a -> r) -> (u es f a -> r) -> u (LiftIns e ': es) f a -> r
 f |+ g = f . unliftIns |+: g
 {-# INLINE (|+) #-}
+
+{- |
+Recursively decompose the sum of first-order effects into a list, following the direction of right
+association, with normalization.
+-}
+type U u ef = UH u (LiftIns ef)
+
+{- |
+Recursively decompose the sum of higher-order effects into a list, following the direction of right
+association, with normalization.
+-}
+type UH u eh = SumToUnionList u (NormalizeSig eh)
+
+{- |
+Recursively decompose the sum of higher-order effects into a list, following the direction of right
+association.
+-}
+type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where
+    SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2
+    SumToUnionList u LNop = '[]
+    SumToUnionList u (SingleSig e) = '[e]
+
+{- |
+Convert a given list of higher-order effect classes into a suitable representation type for each
+case of being empty, single, or multiple.
+-}
+type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
+    MultiListToUnion u '[] = LNop
+    MultiListToUnion u '[e] = e
+    MultiListToUnion u es = u es
+
+{- |
+Normalization in preparation for decomposing the sum of effect classes into a list.
+
+In particular, mark an indivisible, single effect class by applying the t'SingleSig' wrapper to it.
+-}
+type family NormalizeSig e where
+    NormalizeSig LNop = LNop
+    NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2)
+    NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2
+    NormalizeSig e = SingleSig e
+
+{- |
+A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as
+a sum.
+-}
+newtype SingleSig (e :: SigClass) f a = SingleSig {unSingleSig :: e f a}
+    deriving newtype (HFunctor)
+
+type family UnionListToSum (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
+    UnionListToSum u '[e] = UnionToSum u e
+    UnionListToSum u '[] = LNop
+    UnionListToSum u (e ': r) = UnionToSum u e :+: UnionListToSum u r
+
+type family UnionToSum (u :: [SigClass] -> SigClass) (e :: SigClass) :: SigClass where
+    UnionToSum u (u es) = UnionListToSum u es
+    UnionToSum u e = e
+
+type S u es = UnionListToSum u es Nop
+type SH u es = UnionListToSum u es
+
+type NormalFormUnionList u es = U u (S u es) ~ es
+type NormalFormUnionListH u es = UH u (SH u es) ~ es
+
+type NFU u es = NormalFormUnionList u es
+type NFUH u es = NormalFormUnionListH u es
+
+type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le
+
+type family UnliftIfSingle e where
+    UnliftIfSingle (LiftIns e) = e
+    UnliftIfSingle e = e Nop
+
+class LiftInsIfSingle e le where
+    liftInsIfSingle :: e ~> le Nop
+    unliftInsIfSingle :: le Nop ~> e
+
+instance LiftInsIfSingle (e Nop) e where
+    liftInsIfSingle = id
+    unliftInsIfSingle = id
+    {-# INLINE liftInsIfSingle #-}
+    {-# INLINE unliftInsIfSingle #-}
+
+instance LiftInsIfSingle e (LiftIns e) where
+    liftInsIfSingle = LiftIns
+    unliftInsIfSingle = unliftIns
+    {-# INLINE liftInsIfSingle #-}
+    {-# INLINE unliftInsIfSingle #-}