diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -9,3 +9,9 @@
 * Remove the type operator for HCont.
 * Rename the terms "instruction" and "signature" to the simpler "FOE" and "HOE".
 * Support for GHC 9.8.2.
+
+## 0.4.0.0 -- 2025-04-16
+
+* The new v4 interface.
+    * Unified first-order and higher-order effect interfaces.
+    * Added a generic `Eff` carrier type.
diff --git a/data-effects-core.cabal b/data-effects-core.cabal
--- a/data-effects-core.cabal
+++ b/data-effects-core.cabal
@@ -1,6 +1,6 @@
-cabal-version:      2.4
+cabal-version:      3.0
 name:               data-effects-core
-version:            0.2.0.0
+version:            0.4.0.0
 
 -- A short (one-line) description of the package.
 synopsis: A basic framework for effect systems based on effects represented by GADTs.
@@ -15,12 +15,12 @@
 -- The license under which the package is released.
 license:            MPL-2.0
 license-file:       LICENSE
-author:             Sayo Koyoneda <ymdfield@outlook.jp>
-maintainer:         Sayo Koyoneda <ymdfield@outlook.jp>
+author:             Sayo contributors <ymdfield@outlook.jp>
+maintainer:         ymdfield <ymdfield@outlook.jp>
 
 -- A copyright notice.
 copyright:
-    2023-2024 Sayo Koyoneda
+    2023-2025 Sayo contributors
 
 category: Control, Effect
 
@@ -29,27 +29,30 @@
     NOTICE
     README.md
 
-tested-with:
-    GHC == 9.8.2
-    GHC == 9.4.1
-    GHC == 9.2.8
+tested-with: GHC == {9.2.8, 9.4.8, 9.6.7, 9.8.4, 9.10.1, 9.12.2}
 
+common warnings
+    ghc-options: -Wall -Wredundant-constraints
+
 source-repository head
     type: git
     location: https://github.com/sayo-hs/data-effects
-    tag: v0.2.0
+    tag: v0.4.0
     subdir: data-effects-core
 
 library
+    import: warnings
+
     exposed-modules:
         Data.Effect
+        -- Data.Effect.OpenUnion
         Data.Effect.Tag
-        Data.Effect.Key
         Data.Effect.HFunctor
         Data.Effect.HFunctor.HCont
+        Data.Effect.OpenUnion
         Control.Effect
-        Control.Effect.Tag
-        Control.Effect.Key
+        Control.Effect.Interpret
+        Control.Effect.Transform
 
     -- Modules included in this executable, other than Main.
     -- other-modules:
@@ -57,9 +60,12 @@
     -- LANGUAGE extensions used by modules in this package.
     -- other-extensions:
     build-depends:
-        base                          >= 4.16.4 && < 4.21,
-        compdata                      >= 0.13.1 && < 0.14,
+        base                          >= 4.16.4 && < 4.22,
         mtl                           >= 2.2.2 && < 2.4,
+        kan-extensions,
+        free,
+        unliftio,
+        primitive,
 
     hs-source-dirs:   src
     ghc-options:      -Wall
@@ -75,16 +81,21 @@
         RecordWildCards,
         DefaultSignatures
 
-
 test-suite test
+    import: warnings
+
     main-is: Driver.hs
     hs-source-dirs: test
     build-depends:
         data-effects-core,
         base,
         tasty                         >= 1.4 && < 1.6,
-        tasty-hunit                   ^>= 0.10,
+        tasty-hspec                   ^>= 1.2,
+        hspec                         >= 2.5 && < 2.12,
 
+    other-modules:
+        OpenUnion
+
     type: exitcode-stdio-1.0
 
     build-tool-depends:
@@ -101,3 +112,4 @@
         FunctionalDependencies,
         RecordWildCards,
         DefaultSignatures
+
diff --git a/src/Control/Effect.hs b/src/Control/Effect.hs
--- a/src/Control/Effect.hs
+++ b/src/Control/Effect.hs
@@ -1,44 +1,350 @@
--- 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 AllowAmbiguousTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
 
+-- SPDX-License-Identifier: MPL-2.0
+
 {- |
-Copyright   :  (c) 2023-2024 Sayo Koyoneda
+Copyright   :  (c) 2023-2025 Sayo contributors
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
 -}
 module Control.Effect where
 
-import Data.Effect (EffectF, EffectH, LiftFOE (unliftFOE))
+import Control.Alternative.Free qualified as Tree
+import Control.Alternative.Free.Final qualified as Final
+import Control.Applicative (Alternative, empty, (<|>))
+import Control.Applicative.Free qualified as Tree
+import Control.Applicative.Free.Fast qualified as Fast
+import Control.Applicative.Free.Final qualified as Final
+import Control.Monad (MonadPlus)
+import Control.Monad.Cont qualified as Cont
+import Control.Monad.Except (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 (MonadReader (ask), local)
+import Control.Monad.State (MonadState, get, put)
+import Control.Monad.Writer (MonadWriter, listen, tell)
+import Control.Monad.Writer qualified as Writer
+import Data.Effect (
+    Ask (Ask),
+    AskLabel,
+    CC (Jump, SubFork),
+    Catch (Catch),
+    ChooseH (ChooseH),
+    Emb (Emb),
+    Empty (Empty),
+    Fail (Fail),
+    Fix (Efix),
+    Local (Local),
+    State (Get, Put),
+    StateLabel,
+    Tell (Tell),
+    TellLabel,
+    Throw (Throw),
+    ThrowLabel,
+    UnliftBase (WithRunInBase),
+    UnliftIO,
+    WriterH (Listen),
+ )
+import Data.Effect.OpenUnion (
+    At,
+    FindByLabel,
+    Has,
+    IdentityResolver,
+    In,
+    KeyDiscriminator,
+    KeyResolver,
+    KnownIndex,
+    KnownOrder,
+    LabelResolver,
+    Membership,
+    Union,
+    hfmapUnion,
+    inject,
+    membership,
+    membershipAt,
+    type (:>),
+ )
+import Data.Effect.Tag (Tagged (Tag), type (#))
+import Data.Functor.Coyoneda (Coyoneda (Coyoneda), hoistCoyoneda, liftCoyoneda, lowerCoyoneda)
 import Data.Kind (Type)
+import Data.Tuple (swap)
+import UnliftIO qualified as IO
 
--- | A type class that represents the ability to send an first-order effect @ins@ to carrier @f@.
-class SendFOE (ins :: EffectF) f where
-    -- | Send an /instruction/ @ins@ to carrier @f@.
-    sendFOE :: ins a -> f a
+newtype Eff ff es a = Eff {unEff :: ff (Union es (Eff ff es)) a}
 
--- | The operator version of `SendFOE`.
-type (<:) = SendFOE
+perform :: forall e es ff a c. (e :> es, Free c ff) => e (Eff ff es) a -> Eff ff es a
+perform = sendFor $ membership @LabelResolver
+{-# INLINE perform #-}
 
-infix 2 <:
+perform' :: forall key e es ff a c. (Has key e es, Free c ff) => e (Eff ff es) a -> Eff ff es a
+perform' = sendFor (membership @KeyResolver @(KeyDiscriminator key)) . Tag
+{-# INLINE perform' #-}
 
--- | A type class that represents the ability to send a higher-order effect @sig@ to carrier @f@.
-class SendHOE (sig :: EffectH) f where
-    -- | Send a higher-order effect @sig@ to carrier @f@.
-    sendHOE :: sig f a -> f a
+perform'' :: forall tag e es ff a c. (e # tag :> es, Free c ff) => e (Eff ff es) a -> Eff ff es a
+perform'' = perform . Tag @tag
+{-# INLINE perform'' #-}
 
--- | The operator version of `SendHOE`.
-type (<<:) = SendHOE
+send :: forall e es ff a c. (e `In` es, Free c ff) => e (Eff ff es) a -> Eff ff es a
+send = sendFor $ membership @IdentityResolver
+{-# INLINE send #-}
 
-infix 2 <<:
+sendAt :: forall i es ff a c. (KnownIndex i es, Free c ff) => At i es (Eff ff es) a -> Eff ff es a
+sendAt = sendFor $ membershipAt @i
+{-# INLINE sendAt #-}
 
-instance (SendFOE ins f) => SendHOE (LiftFOE ins) f where
-    sendHOE = sendFOE . unliftFOE
-    {-# INLINE sendHOE #-}
+sendFor
+    :: forall e es ff a c
+     . (KnownOrder e, Free c ff)
+    => Membership e es
+    -> e (Eff ff es) a
+    -> Eff ff es a
+sendFor i = Eff . liftFree . inject i
+{-# INLINE sendFor #-}
 
+emb :: forall f es ff a c. (Emb f :> es, Free c ff) => f a -> Eff ff es a
+emb = perform . Emb
+{-# INLINE emb #-}
+
 -- | A natural transformation.
 type f ~> g = forall (x :: Type). f x -> g x
 
 infixr 2 ~>
+
+type e ~~> f = e f ~> f
+
+infix 2 ~~>
+
+infixr 3 $
+infixr 4 $$
+
+-- | Type-level infix applcation for functors.
+type (f :: Type -> Type) $ a = f a
+
+-- | Type-level infix applcation for higher-order functors.
+type (h :: (Type -> Type) -> Type -> Type) $$ f = h f
+
+instance
+    (FindByLabel AskLabel (Ask r) es, Local r :> es, Monad (Eff ff es), Free c ff)
+    => MonadReader r (Eff ff es)
+    where
+    ask = perform Ask
+    local f a = perform $ Local f a
+    {-# INLINE ask #-}
+    {-# INLINE local #-}
+
+instance
+    (FindByLabel TellLabel (Tell w) es, WriterH w :> es, Monoid w, Monad (Eff ff es), Free c ff)
+    => MonadWriter w (Eff ff es)
+    where
+    tell = perform . Tell
+    listen a = fmap swap $ perform $ Listen a
+    pass = pass . fmap swap
+    {-# INLINE tell #-}
+    {-# INLINE listen #-}
+
+{- |
+For a given scope, uses the function (the first component of the pair returned
+by that scope) to modify the accumulated value of that scope, and then
+accumulates the result into the current outer scope.
+
+@
+pass m = do
+    (w, (f, a)) <- listen m
+    tell $ f w
+    pure a
+@
+-}
+pass
+    :: forall w a es ff c
+     . (Tell w :> es, WriterH w :> es, Monad (Eff ff es), Free c ff)
+    => Eff ff es (w -> w, a)
+    -> Eff ff es a
+pass m = do
+    (w, (f, a)) <- perform $ Listen m
+    perform $ Tell $ f w
+    pure a
+{-# INLINE pass #-}
+
+instance (FindByLabel StateLabel (State s) es, Monad (Eff ff es), Free c ff) => MonadState s (Eff ff es) where
+    get = perform Get
+    put = perform . Put
+    {-# INLINE get #-}
+    {-# INLINE put #-}
+
+instance
+    ( FindByLabel AskLabel (Ask r) es
+    , Local r :> es
+    , FindByLabel TellLabel (Tell w) es
+    , WriterH w :> es
+    , FindByLabel StateLabel (State s) es
+    , Monoid w
+    , Monad (Eff ff es)
+    , Free c ff
+    )
+    => MonadRWS r w s (Eff ff es)
+
+instance
+    (FindByLabel ThrowLabel (Throw e) es, Catch e :> es, Monad (Eff ff es), Free c ff)
+    => MonadError e (Eff ff es)
+    where
+    throwError = perform . Throw
+    catchError a hdl = perform $ Catch a hdl
+    {-# INLINE throwError #-}
+    {-# INLINE catchError #-}
+
+instance
+    (Empty :> es, ChooseH :> es, Applicative (Eff ff es), Free c ff)
+    => Alternative (Eff ff es)
+    where
+    empty = perform Empty
+    a <|> b = perform $ ChooseH a b
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
+
+instance (Empty :> es, ChooseH :> es, Monad (Eff ff es), Free c ff) => MonadPlus (Eff ff es)
+
+instance (CC ref :> es, Monad (Eff ff es), Free c ff) => Cont.MonadCont (Eff ff es) where
+    callCC = callCC_
+    {-# INLINE callCC #-}
+
+sub
+    :: forall ref a b es ff c
+     . (CC ref :> es, Monad (Eff ff es), Free c ff)
+    => (ref a -> Eff ff es b)
+    -> (a -> Eff ff es b)
+    -> Eff ff es b
+sub p q = perform SubFork >>= either p q
+{-# INLINE sub #-}
+
+callCC_
+    :: forall ref a b es ff c
+     . (CC ref :> es, Monad (Eff ff es), Free c ff)
+    => ((a -> Eff ff es b) -> Eff ff es a)
+    -> Eff ff es a
+callCC_ f = sub (f . jump) pure
+  where
+    jump ref x = perform $ Jump ref x
+{-# INLINE callCC_ #-}
+
+instance (Emb IO :> es, Monad (Eff ff es), Free c ff) => MonadIO (Eff ff es) where
+    liftIO = emb
+    {-# INLINE liftIO #-}
+
+instance (Fail :> es, Monad (Eff ff es), Free c ff) => MonadFail (Eff ff es) where
+    fail = perform . Fail
+    {-# INLINE fail #-}
+
+instance (Fix :> es, Monad (Eff ff es), Free c ff) => MonadFix (Eff ff es) where
+    mfix = perform . Efix
+    {-# INLINE mfix #-}
+
+instance
+    (UnliftIO :> es, Emb IO :> es, Monad (Eff ff es), Free c ff)
+    => IO.MonadUnliftIO (Eff ff es)
+    where
+    withRunInIO f = perform $ WithRunInBase f
+    {-# INLINE withRunInIO #-}
+
+-- Free
+
+class (forall f. c (ff f)) => Free c (ff :: (Type -> Type) -> Type -> Type) | ff -> c where
+    {-# MINIMAL liftFree, (runFree | (retract, hoist)) #-}
+
+    liftFree :: f a -> ff f a
+    runFree :: (c g) => (forall x. f x -> g x) -> ff f a -> g a
+    retract :: (c f) => ff f a -> f a
+    hoist :: (forall x. f x -> g x) -> ff f a -> ff g a
+
+    runFree f = retract . hoist f
+    retract = runFree id
+
+    default hoist :: (c (ff g)) => (forall x. f x -> g x) -> ff f a -> ff g a
+    hoist phi = runFree $ liftFree . phi
+
+    {-# INLINE runFree #-}
+    {-# INLINE retract #-}
+    {-# INLINE hoist #-}
+
+convertEff
+    :: forall ff gg es a c c'
+     . (Free c ff, Free c' gg, forall r. c (gg r))
+    => Eff ff es a
+    -> Eff gg es a
+convertEff = go
+  where
+    go :: Eff ff es ~> Eff gg es
+    go = Eff . hoist (hfmapUnion go) . convertFree . unEff
+{-# INLINE convertEff #-}
+
+convertFree :: (Free c ff, Free c' gg, c (gg r)) => ff r a -> gg r a
+convertFree = runFree liftFree
+{-# INLINE convertFree #-}
+
+deriving instance (forall f. Functor (ff f)) => Functor (Eff ff es)
+deriving instance (forall r. Applicative (ff r)) => Applicative (Eff ff es)
+deriving instance (forall r. Monad (ff r)) => Monad (Eff ff es)
+
+instance Free Functor Coyoneda where
+    liftFree = liftCoyoneda
+    runFree f (Coyoneda g x) = g <$> f x
+    retract = lowerCoyoneda
+    hoist = hoistCoyoneda
+
+    {-# INLINE liftFree #-}
+    {-# INLINE runFree #-}
+    {-# INLINE retract #-}
+    {-# INLINE hoist #-}
+
+instance Free Applicative Tree.Ap where
+    liftFree = Tree.liftAp
+    runFree = Tree.runAp
+    retract = Tree.retractAp
+    hoist = Tree.hoistAp
+
+    {-# INLINE liftFree #-}
+    {-# INLINE runFree #-}
+    {-# INLINE retract #-}
+    {-# INLINE hoist #-}
+
+instance Free Applicative Fast.Ap where
+    liftFree = Fast.liftAp
+    runFree = Fast.runAp
+    retract = Fast.retractAp
+    hoist = Fast.hoistAp
+
+    {-# INLINE liftFree #-}
+    {-# INLINE runFree #-}
+    {-# INLINE retract #-}
+    {-# INLINE hoist #-}
+
+instance Free Applicative Final.Ap where
+    liftFree = Final.liftAp
+    runFree = Final.runAp
+    retract = Final.retractAp
+    hoist = Final.hoistAp
+
+    {-# INLINE liftFree #-}
+    {-# INLINE runFree #-}
+    {-# INLINE retract #-}
+    {-# INLINE hoist #-}
+
+instance Free Alternative Tree.Alt where
+    liftFree = Tree.liftAlt
+    runFree = Tree.runAlt
+    hoist = Tree.hoistAlt
+
+    {-# INLINE liftFree #-}
+    {-# INLINE runFree #-}
+    {-# INLINE hoist #-}
+
+instance Free Alternative Final.Alt where
+    liftFree = Final.liftAlt
+    runFree = Final.runAlt
+    hoist = Final.hoistAlt
+
+    {-# INLINE liftFree #-}
+    {-# INLINE runFree #-}
+    {-# INLINE hoist #-}
diff --git a/src/Control/Effect/Interpret.hs b/src/Control/Effect/Interpret.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Interpret.hs
@@ -0,0 +1,197 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Avoid lambda" #-}
+
+-- SPDX-License-Identifier: MPL-2.0
+
+{- |
+Copyright   :  (c) 2025 Sayo contributors
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+-}
+module Control.Effect.Interpret where
+
+import Control.Effect (
+    Eff (..),
+    Free (liftFree),
+    hoist,
+    runFree,
+    type (~>),
+    type (~~>),
+ )
+import Data.Effect (Emb, getEmb)
+import Data.Effect.OpenUnion (
+    Has,
+    In,
+    KnownLength,
+    KnownOrder,
+    Membership,
+    Suffix,
+    Union,
+    hfmapUnion,
+    identityMembership,
+    keyMembership,
+    labelMembership,
+    nil,
+    project,
+    weakens,
+    (!++),
+    (!:),
+    (:>),
+    type (++),
+ )
+import Data.Effect.Tag (unTag)
+import Data.Functor.Identity (Identity, runIdentity)
+
+runEff :: (Free c ff, c f) => Eff ff '[Emb f] a -> f a
+runEff = runFree (getEmb !: nil) . unEff
+{-# INLINE runEff #-}
+
+runPure :: (Free c ff, c Identity) => Eff ff '[] a -> a
+runPure = runIdentity . runFree nil . unEff
+{-# INLINE runPure #-}
+
+interpret
+    :: forall e es ff a c
+     . (KnownOrder e, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff (e ': es) a
+    -> Eff ff es a
+interpret i = interpretAll $ i !: Eff . liftFree
+{-# INLINE interpret #-}
+
+reinterpret
+    :: forall e es es' ff a c
+     . (Suffix es es', KnownOrder e, Free c ff)
+    => e ~~> Eff ff es'
+    -> Eff ff (e ': es) a
+    -> Eff ff es' a
+reinterpret i = interpretAll $ i !: Eff . liftFree . weakens
+{-# INLINE reinterpret #-}
+
+interprets
+    :: forall es r ff a c
+     . (KnownLength es, Free c ff)
+    => Union es ~~> Eff ff r
+    -> Eff ff (es ++ r) a
+    -> Eff ff r a
+interprets i = interpretAll $ i !++ Eff . liftFree
+{-# INLINE interprets #-}
+
+reinterprets
+    :: forall es r r' ff a c
+     . (Suffix r r', KnownLength es, Free c ff)
+    => (Union es (Eff ff r') ~> Eff ff r')
+    -> Eff ff (es ++ r) a
+    -> Eff ff r' a
+reinterprets i = interpretAll $ i !++ Eff . liftFree . weakens @r
+{-# INLINE reinterprets #-}
+
+interpose
+    :: forall e es ff a c
+     . (e :> es, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+interpose = interposeFor labelMembership
+{-# INLINE interpose #-}
+
+interposeOn
+    :: forall key e es ff a c
+     . (Has key e es, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+interposeOn f = interposeFor (keyMembership @key) (f . unTag)
+{-# INLINE interposeOn #-}
+
+interposeIn
+    :: forall e es ff a c
+     . (e `In` es, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+interposeIn = interposeFor identityMembership
+{-# INLINE interposeIn #-}
+
+interposeFor
+    :: forall e es ff a c
+     . (KnownOrder e, Free c ff)
+    => Membership e es
+    -> e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+interposeFor i f =
+    interpretAll \u ->
+        case project i u of
+            Just e -> f e
+            Nothing -> Eff $ liftFree u
+{-# INLINE interposeFor #-}
+
+preinterpose
+    :: forall e es ff a c
+     . (e :> es, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+preinterpose = preinterposeFor labelMembership
+{-# INLINE preinterpose #-}
+
+preinterposeOn
+    :: forall key e es ff a c
+     . (Has key e es, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+preinterposeOn f = preinterposeFor (keyMembership @key) (f . unTag)
+{-# INLINE preinterposeOn #-}
+
+preinterposeIn
+    :: forall e es ff a c
+     . (e `In` es, Free c ff)
+    => e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+preinterposeIn = preinterposeFor identityMembership
+{-# INLINE preinterposeIn #-}
+
+preinterposeFor
+    :: forall e es ff a c
+     . (KnownOrder e, Free c ff)
+    => Membership e es
+    -> e ~~> Eff ff es
+    -> Eff ff es a
+    -> Eff ff es a
+preinterposeFor i f = go
+  where
+    go :: Eff ff es ~> Eff ff es
+    go (Eff a) = Eff $ (`runFree` a) \u ->
+        hoist (hfmapUnion go) $ case project i u of
+            Just e -> unEff $ f e
+            Nothing -> liftFree u
+{-# INLINE preinterposeFor #-}
+
+interpretAll
+    :: forall es es' ff a c
+     . (Free c ff)
+    => (Union es ~~> Eff ff es')
+    -> Eff ff es a
+    -> Eff ff es' a
+interpretAll i = go
+  where
+    go :: Eff ff es ~> Eff ff es'
+    go = Eff . runFree (unEff . i . hfmapUnion go) . unEff
+{-# INLINE interpretAll #-}
+
+iterAllEff
+    :: forall es f ff a c
+     . (Free c ff, c f)
+    => Union es ~~> f
+    -> Eff ff es a
+    -> f a
+iterAllEff i = go
+  where
+    go :: Eff ff es ~> f
+    go = runFree (i . hfmapUnion go) . unEff
+{-# INLINE iterAllEff #-}
diff --git a/src/Control/Effect/Key.hs b/src/Control/Effect/Key.hs
deleted file mode 100644
--- a/src/Control/Effect/Key.hs
+++ /dev/null
@@ -1,66 +0,0 @@
-{-# 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/.
-
-{- |
-Copyright   :  (c) 2023-2024 Sayo Koyoneda
-License     :  MPL-2.0 (see the file LICENSE)
-Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
--}
-module Control.Effect.Key where
-
-import Control.Applicative (Alternative)
-import Control.Effect (SendFOE (sendFOE), SendHOE (sendHOE))
-import Control.Monad (MonadPlus)
-import Control.Monad.Except (MonadError)
-import Control.Monad.Fix (MonadFix)
-import Control.Monad.IO.Class (MonadIO)
-import Control.Monad.RWS (MonadRWS)
-import Control.Monad.Reader (MonadReader)
-import Control.Monad.State (MonadState)
-import Control.Monad.Writer (MonadWriter)
-import Data.Coerce (coerce)
-import Data.Effect (EffectF, EffectH)
-import Data.Effect.HFunctor (HFunctor, hfmap)
-import Data.Kind (Type)
-
-class SendFOEBy key (ins :: EffectF) f | key f -> ins where
-    sendFOEBy :: ins a -> f a
-
-class SendHOEBy key (sig :: EffectH) f | key f -> sig where
-    sendHOEBy :: sig f a -> f a
-
--- | A wrapper data type to represent sending an effect to the carrier @f@ with the specified key.
-newtype ByKey key (f :: Type -> Type) a = ByKey {runByKey :: f a}
-    deriving newtype
-        ( Functor
-        , Applicative
-        , Alternative
-        , Monad
-        , MonadPlus
-        , MonadFix
-        , MonadIO
-        , MonadFail
-        , MonadReader r
-        , MonadWriter w
-        , MonadState s
-        , MonadRWS r w s
-        , MonadError e
-        )
-
--- | Send all effects within the scope, keyed, to carrier @f@.
-key :: forall key f a. ByKey key f a -> f a
-key = runByKey
-{-# INLINE key #-}
-
-instance (SendFOEBy key ins f) => SendFOE ins (ByKey key f) where
-    sendFOE = ByKey . sendFOEBy @key
-    {-# INLINE sendFOE #-}
-
-instance (SendHOEBy key sig f, HFunctor sig) => SendHOE sig (ByKey key f) where
-    sendHOE = ByKey . sendHOEBy @key . hfmap coerce
-    {-# INLINE sendHOE #-}
diff --git a/src/Control/Effect/Tag.hs b/src/Control/Effect/Tag.hs
deleted file mode 100644
--- a/src/Control/Effect/Tag.hs
+++ /dev/null
@@ -1,70 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE UndecidableInstances #-}
-
--- 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 Sayo Koyoneda
-License     :  MPL-2.0 (see the file LICENSE)
-Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
--}
-module Control.Effect.Tag where
-
-import Control.Applicative (Alternative)
-import Control.Effect (SendFOE (sendFOE), SendHOE (sendHOE))
-import Control.Effect.Key (SendFOEBy, SendHOEBy, sendFOEBy, sendHOEBy)
-import Control.Monad (MonadPlus)
-import Control.Monad.Except (MonadError)
-import Control.Monad.Fix (MonadFix)
-import Control.Monad.IO.Class (MonadIO)
-import Control.Monad.RWS (MonadRWS)
-import Control.Monad.Reader (MonadReader)
-import Control.Monad.State (MonadState)
-import Control.Monad.Writer (MonadWriter)
-import Data.Coerce (coerce)
-import Data.Effect.HFunctor (HFunctor, hfmap)
-import Data.Effect.Tag (pattern T, pattern TH, type (#), type (##))
-import Data.Kind (Type)
-
--- | A wrapper data type to represent sending an effect to the carrier @f@ with the specified tag.
-newtype ViaTag tag (f :: Type -> Type) a = ViaTag {runViaTag :: f a}
-    deriving newtype
-        ( Functor
-        , Applicative
-        , Alternative
-        , Monad
-        , MonadPlus
-        , MonadFix
-        , MonadIO
-        , MonadFail
-        , MonadReader r
-        , MonadWriter w
-        , MonadState s
-        , MonadRWS r w s
-        , MonadError e
-        )
-
--- | Send all effects within the scope, tagged, to carrier @f@.
-tag :: forall tag f a. ViaTag tag f a -> f a
-tag = runViaTag
-{-# INLINE tag #-}
-
-instance (SendFOE (ins # tag) f) => SendFOE ins (ViaTag tag f) where
-    sendFOE = ViaTag . sendFOE . T @tag
-    {-# INLINE sendFOE #-}
-
-instance (SendHOE (sig ## tag) f, HFunctor sig) => SendHOE sig (ViaTag tag f) where
-    sendHOE = ViaTag . sendHOE . TH @tag . hfmap coerce
-    {-# INLINE sendHOE #-}
-
-instance (SendFOEBy key (ins # tag) f) => SendFOEBy key ins (ViaTag tag f) where
-    sendFOEBy = ViaTag . sendFOEBy @key . T @tag
-    {-# INLINE sendFOEBy #-}
-
-instance (SendHOEBy key (sig ## tag) f, HFunctor sig) => SendHOEBy key sig (ViaTag tag f) where
-    sendHOEBy = ViaTag . sendHOEBy @key . TH @tag . hfmap coerce
-    {-# INLINE sendHOEBy #-}
diff --git a/src/Control/Effect/Transform.hs b/src/Control/Effect/Transform.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Transform.hs
@@ -0,0 +1,215 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+-- SPDX-License-Identifier: MPL-2.0
+
+{- |
+Copyright   :  (c) 2025 Sayo contributors
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+-}
+module Control.Effect.Transform where
+
+import Control.Effect (Eff (..), Free, hoist, sendFor, type (~>))
+import Control.Effect.Interpret (interposeFor, interpret, reinterpret)
+import Data.Effect.OpenUnion (
+    Each,
+    Has,
+    In,
+    KnownLength,
+    KnownOrder,
+    Membership,
+    RemoveHOEs,
+    Suffix,
+    SuffixUnder,
+    Union,
+    WeakenHOEs,
+    hfmapUnion,
+    identityMembership,
+    inject,
+    keyMembership,
+    labelMembership,
+    mapUnion,
+    prefixFor,
+    prefixFor1,
+    suffixFor,
+    weaken,
+    weakenFor,
+    weakenHOEs,
+    weakens,
+    weakensUnder,
+    (!:),
+    pattern Here,
+    type (++),
+    type (:>),
+ )
+import Data.Effect.Tag (Tagged (Tag), unTag, type (#))
+
+raise :: forall e es a ff c. (Free c ff) => Eff ff es a -> Eff ff (e ': es) a
+raise = raises
+{-# INLINE raise #-}
+
+raises :: forall es es' a ff c. (Suffix es es', Free c ff) => Eff ff es a -> Eff ff es' a
+raises = transAll weakens
+{-# INLINE raises #-}
+
+raiseUnder :: forall e0 e1 es a ff c. (Free c ff) => Eff ff (e0 ': es) a -> Eff ff (e0 ': e1 ': es) a
+raiseUnder = raisesUnder
+{-# INLINE raiseUnder #-}
+
+raisesUnder :: forall e es es' a ff c. (Suffix es es', Free c ff) => Eff ff (e ': es) a -> Eff ff (e ': es') a
+raisesUnder = transAll weakensUnder
+{-# INLINE raisesUnder #-}
+
+raisesUnders :: forall es es' a ff c. (SuffixUnder es es', Free c ff) => Eff ff es a -> Eff ff es' a
+raisesUnders = transAll weakensUnder
+{-# INLINE raisesUnders #-}
+
+onlyFOEs :: forall es a ff c. (Free c ff, WeakenHOEs es) => Eff ff (RemoveHOEs es) a -> Eff ff es a
+onlyFOEs = transAll weakenHOEs
+{-# INLINE onlyFOEs #-}
+
+raisePrefix
+    :: forall es' es a ff c
+     . (KnownLength es', Free c ff)
+    => Eff ff es a
+    -> Eff ff (es' ++ es) a
+raisePrefix = transAll $ mapUnion $ prefixFor @es'
+{-# INLINE raisePrefix #-}
+
+raiseSuffix
+    :: forall es' es a ff c
+     . (Free c ff)
+    => Eff ff es a
+    -> Eff ff (es ++ es') a
+raiseSuffix = transAll $ mapUnion $ suffixFor @es'
+{-# INLINE raiseSuffix #-}
+
+raisePrefix1
+    :: forall fs x es a ff c
+     . (KnownLength fs, Free c ff)
+    => Eff ff es a
+    -> Eff ff (Each fs x ++ es) a
+raisePrefix1 = transAll $ mapUnion $ prefixFor1 @fs @x
+{-# INLINE raisePrefix1 #-}
+
+subsume :: forall e es a ff c. (e `In` es, Free c ff) => Eff ff (e ': es) a -> Eff ff es a
+subsume = transAll $ inject identityMembership !: id
+{-# INLINE subsume #-}
+
+subsumeUnder :: forall e1 e0 es a ff c. (e1 `In` es, KnownOrder e0, Free c ff) => Eff ff (e0 ': e1 ': es) a -> Eff ff (e0 ': es) a
+subsumeUnder = transAll $ inject Here !: inject (weakenFor identityMembership) !: weaken
+{-# INLINE subsumeUnder #-}
+
+-- todo: generalize subsume by type-class
+
+transform
+    :: forall e e' es a ff c
+     . (KnownOrder e, KnownOrder e', Free c ff)
+    => (e (Eff ff (e' ': es)) ~> e' (Eff ff (e' ': es)))
+    -> Eff ff (e ': es) a
+    -> Eff ff (e' ': es) a
+transform f = reinterpret $ sendFor Here . f
+{-# INLINE transform #-}
+
+translate
+    :: forall e e' es a ff c
+     . (KnownOrder e, e' :> es, Free c ff)
+    => (e (Eff ff es) ~> e' (Eff ff es))
+    -> Eff ff (e ': es) a
+    -> Eff ff es a
+translate = translateFor labelMembership
+{-# INLINE translate #-}
+
+translateOn
+    :: forall key e e' es a ff c
+     . (KnownOrder e, Has key e' es, Free c ff)
+    => (e (Eff ff es) ~> e' (Eff ff es))
+    -> Eff ff (e ': es) a
+    -> Eff ff es a
+translateOn f = translateFor (keyMembership @key) (Tag . f)
+{-# INLINE translateOn #-}
+
+translateIn
+    :: forall e e' es a ff c
+     . (KnownOrder e, e' `In` es, Free c ff)
+    => (e (Eff ff es) ~> e' (Eff ff es))
+    -> Eff ff (e ': es) a
+    -> Eff ff es a
+translateIn = translateFor identityMembership
+{-# INLINE translateIn #-}
+
+translateFor
+    :: forall e e' es a ff c
+     . (KnownOrder e, KnownOrder e', Free c ff)
+    => Membership e' es
+    -> (e (Eff ff es) ~> e' (Eff ff es))
+    -> Eff ff (e ': es) a
+    -> Eff ff es a
+translateFor i f = interpret $ sendFor i . f
+{-# INLINE translateFor #-}
+
+rewrite
+    :: forall e es a ff c
+     . (e :> es, Free c ff)
+    => (e (Eff ff es) ~> e (Eff ff es))
+    -> Eff ff es a
+    -> Eff ff es a
+rewrite = rewriteFor labelMembership
+{-# INLINE rewrite #-}
+
+rewriteOn
+    :: forall key e es a ff c
+     . (Has key e es, Free c ff)
+    => (e (Eff ff es) ~> e (Eff ff es))
+    -> Eff ff es a
+    -> Eff ff es a
+rewriteOn f = rewriteFor (keyMembership @key) (Tag . f . unTag)
+{-# INLINE rewriteOn #-}
+
+rewriteIn
+    :: forall e es a ff c
+     . (e `In` es, Free c ff)
+    => (e (Eff ff es) ~> e (Eff ff es))
+    -> Eff ff es a
+    -> Eff ff es a
+rewriteIn = rewriteFor identityMembership
+{-# INLINE rewriteIn #-}
+
+rewriteFor
+    :: forall e es a ff c
+     . (KnownOrder e, Free c ff)
+    => Membership e es
+    -> (e (Eff ff es) ~> e (Eff ff es))
+    -> Eff ff es a
+    -> Eff ff es a
+rewriteFor i f = interposeFor i (sendFor i . f)
+{-# INLINE rewriteFor #-}
+
+transAll
+    :: forall es es' ff a c
+     . (Free c ff)
+    => (Union es (Eff ff es') ~> Union es' (Eff ff es'))
+    -> Eff ff es a
+    -> Eff ff es' a
+transAll f = go
+  where
+    go :: Eff ff es ~> Eff ff es'
+    go (Eff a) = Eff $ hoist (f . hfmapUnion go) a
+{-# INLINE transAll #-}
+
+tag
+    :: forall tag e es a ff c
+     . (KnownOrder e, KnownOrder (e # tag), Free c ff)
+    => Eff ff (e ': es) a
+    -> Eff ff (e # tag ': es) a
+tag = transform Tag
+{-# INLINE tag #-}
+
+untag
+    :: forall tag e es a ff c
+     . (KnownOrder e, KnownOrder (e # tag), Free c ff)
+    => Eff ff (e # tag ': es) a
+    -> Eff ff (e ': es) a
+untag = transform unTag
+{-# INLINE untag #-}
diff --git a/src/Data/Effect.hs b/src/Data/Effect.hs
--- a/src/Data/Effect.hs
+++ b/src/Data/Effect.hs
@@ -1,40 +1,298 @@
--- 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 DeriveAnyClass #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 
+-- SPDX-License-Identifier: MPL-2.0
+
 {- |
-Copyright   :  (c) 2023-2024 Sayo Koyoneda
-               (c) 2023 Casper Bach Poulsen and Cas van der Rest
+Copyright   :  (c) 2023-2024 Sayo contributors
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
 -}
 module Data.Effect where
 
+import Data.Coerce (Coercible, coerce)
 import Data.Effect.HFunctor (HFunctor, hfmap)
 import Data.Kind (Type)
 
--- | The kind of first-order effects.
-type EffectF = Type -> Type
+-- | The kind for effects.
+type Effect = (Type -> Type) -> Type -> Type
 
--- | The kind of higher-order effects.
-type EffectH = (Type -> Type) -> Type -> Type
+-- | An order of effect.
+data EffectOrder = FirstOrder | HigherOrder
+    deriving (Show, Eq, Ord)
 
-{- | Lift first-order effects to higher-order effects.
+type family OrderOf (e :: Effect) :: EffectOrder
 
-     Come from [heft-lang\/POPL2023\/haskell\/src\/Elab.hs]
-    (https://github.com/heft-lang/POPL2023/blob/74afe1d5ce0b491cffe40cc5c73a2a5ee6a94d9c/haskell/src/Elab.hs#L9-L10).
+type family OrderCase (e :: EffectOrder) a b where
+    OrderCase 'FirstOrder a b = a
+    OrderCase 'HigherOrder a b = b
+
+type family LabelOf (e :: Effect)
+
+class
+    ( OrderOf e ~ 'FirstOrder
+    , forall f g a. Coercible (e f a) (e g a)
+    ) =>
+    FirstOrder (e :: Effect)
+
+-- * Nop Effect
+
+-- | A effect with no operations.
+data Nop :: Effect
+    deriving anyclass (FirstOrder)
+
+data NopLabel
+type instance LabelOf Nop = NopLabel
+type instance OrderOf Nop = 'FirstOrder
+instance HFunctor Nop where
+    hfmap _ = \case {}
+    {-# INLINE hfmap #-}
+
+-- * Embedding Effect
+
+newtype Emb e (f :: Type -> Type) (a :: Type) = Emb {getEmb :: e a}
+    deriving anyclass (FirstOrder)
+    deriving newtype (Functor, Applicative, Monad, Foldable)
+    deriving stock (Traversable)
+
+data EmbLabel (e :: Type -> Type)
+type instance LabelOf (Emb e) = EmbLabel e
+type instance OrderOf (Emb e) = 'FirstOrder
+instance HFunctor (Emb e) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+newtype Unemb e a = Unemb {getUnemb :: forall f. e f a}
+
+-- * Reader Effects
+
+-- | An effect that holds a value of type @r@ in the context (environment).
+data Ask r :: Effect where
+    -- | Obtain a value from the environment.
+    Ask :: Ask r f r
+
+data AskLabel
+type instance LabelOf (Ask r) = AskLabel
+type instance OrderOf (Ask r) = 'FirstOrder
+instance FirstOrder (Ask r)
+instance HFunctor (Ask r) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- | An effect that locally modifies the value held in the environment.
+data Local r :: Effect where
+    -- | Locally modifies the value held in the environment.
+    Local
+        :: (r -> r)
+        -- ^ A function that transforms the original value to the modified value.
+        -> f a
+        -- ^ The local scope where the modification is applied.
+        -> Local r f a
+
+data LocalLabel
+type instance LabelOf (Local r) = LocalLabel
+type instance OrderOf (Local r) = 'HigherOrder
+instance HFunctor (Local r) where
+    hfmap phi (Local f a) = Local f (phi a)
+    {-# INLINE hfmap #-}
+
+-- * State Effect
+
+-- | An effect for holding mutable state values in the context.
+data State s :: Effect where
+    -- | Retrieves the current state value from the context.
+    Get :: State s f s
+    -- | Overwrites the state value in the context.
+    Put :: s -> State s f ()
+
+data StateLabel
+type instance LabelOf (State s) = StateLabel
+type instance OrderOf (State s) = 'FirstOrder
+instance FirstOrder (State s)
+instance HFunctor (State s) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- * Writer Effects
+
+-- | An effect that can accumulate values monoidally in a context.
+data Tell w :: Effect where
+    -- | Accumulates new values to the cumulative value held in the context.
+    Tell :: w -> Tell w f ()
+
+data TellLabel
+type instance LabelOf (Tell w) = TellLabel
+type instance OrderOf (Tell w) = 'FirstOrder
+instance FirstOrder (Tell w)
+instance HFunctor (Tell w) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- | An effect that performs local operations on accumulations in the context on a per-scope basis.
+data WriterH w :: Effect where
+    -- | Obtains the accumulated value in the scope and returns it together as a pair.
+    Listen
+        :: f a
+        -- ^ The scope from which to obtain the accumulation.
+        -> WriterH w f (w, a)
+    -- | Modifies the accumulation in the scope based on the given function.
+    Censor
+        :: (w -> w)
+        -- ^ A function for modifying the accumulated value.
+        -> f a
+        -- ^ The scope where the modification is applied.
+        -> WriterH w f a
+
+data WriterHLabel
+type instance LabelOf (WriterH w) = WriterHLabel
+type instance OrderOf (WriterH w) = 'HigherOrder
+instance HFunctor (WriterH w) where
+    hfmap phi = \case
+        Listen a -> Listen $ phi a
+        Censor f a -> Censor f (phi a)
+    {-# INLINE hfmap #-}
+
+-- * Exception Effects
+
+-- | An effect to escape from the normal control structure with an exception value of type @e@ in the middle of a context.
+data Throw e :: Effect where
+    -- | Throws an exception; that is, escapes from the normal control structure with an exception value in the middle of a context.
+    Throw :: e -> Throw e f a
+
+data ThrowLabel
+type instance LabelOf (Throw e) = ThrowLabel
+type instance OrderOf (Throw e) = 'FirstOrder
+instance FirstOrder (Throw e)
+instance HFunctor (Throw e) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- | An effect to catch exceptions.
+data Catch e :: Effect where
+    -- | Catches exceptions within a scope and processes them according to the given exception handler.
+    Catch
+        :: f a
+        -- ^ The scope in which to catch exceptions.
+        -> (e -> f a)
+        -- ^ Exception handler. Defines the processing to perform when an exception is thrown within the scope.
+        -> Catch e f a
+
+data CatchLabel
+type instance LabelOf (Catch w) = CatchLabel
+type instance OrderOf (Catch w) = 'HigherOrder
+instance HFunctor (Catch w) where
+    hfmap phi (Catch a hdl) = Catch (phi a) (phi . hdl)
+    {-# INLINE hfmap #-}
+
+-- * Non-Determinism Effects
+
+-- | An effect that eliminates a branch by causing the current branch context of a non-deterministic computation to fail.
+data Empty :: Effect where
+    -- | Eliminates a branch by causing the current branch context of a non-deterministic computation to fail.
+    Empty :: Empty f a
+
+data EmptyLabel
+type instance LabelOf Empty = EmptyLabel
+type instance OrderOf Empty = 'FirstOrder
+instance FirstOrder Empty
+instance HFunctor Empty where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- | An effect that splits the computation into two branches.
+data Choose :: Effect where
+    -- | Splits the computation into two branches.
+    -- As a result of executing @choose@, the world branches into one where `False` is returned and one where `True` is returned.
+    Choose :: Choose f Bool
+
+data ChooseLabel
+type instance LabelOf Choose = ChooseLabel
+type instance OrderOf Choose = 'FirstOrder
+instance FirstOrder Choose
+instance HFunctor Choose where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+{- |
+An effect that executes two branches as scopes.
+A higher-order version of the t`Choose` effect.
 -}
-newtype LiftFOE (ins :: EffectF) (f :: Type -> Type) a = LiftFOE {unliftFOE :: ins a}
-    deriving stock (Functor, Foldable, Traversable)
+data ChooseH :: Effect where
+    -- | Executes the given two scopes as branches.
+    -- Even if one fails due to the `empty` operation, the whole does not fail as long as the other does not fail.
+    ChooseH :: f a -> f a -> ChooseH f a
 
-instance HFunctor (LiftFOE ins) where
-    hfmap _ (LiftFOE e) = LiftFOE e
+data ChooseHLabel
+type instance LabelOf ChooseH = ChooseHLabel
+type instance OrderOf ChooseH = 'HigherOrder
+instance HFunctor ChooseH where
+    hfmap phi (ChooseH a b) = ChooseH (phi a) (phi b)
     {-# INLINE hfmap #-}
 
--- | A first-order effect with no operations.
-data Nop :: EffectF
+-- * Fail Effect
 
--- | A higher-order effect with no operations.
-type LNop = LiftFOE Nop
+data Fail :: Effect where
+    Fail :: String -> Fail f a
+
+data FailLabel
+type instance LabelOf Fail = FailLabel
+type instance OrderOf Fail = 'FirstOrder
+instance FirstOrder Fail
+instance HFunctor Fail where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- * Fix Effect
+
+data Fix :: Effect where
+    Efix :: (a -> f a) -> Fix f a
+
+data FixLabel
+type instance LabelOf Fix = FixLabel
+type instance OrderOf Fix = 'HigherOrder
+instance HFunctor Fix where
+    hfmap phi (Efix f) = Efix $ phi . f
+    {-# INLINE hfmap #-}
+
+-- * Unlift Effect
+
+data UnliftBase b f (a :: Type) where
+    WithRunInBase :: ((forall x. f x -> b x) -> b a) -> UnliftBase b f a
+
+type UnliftIO = UnliftBase IO
+
+data UnliftBaseLabel (b :: Type -> Type)
+type instance LabelOf (UnliftBase b) = UnliftBaseLabel b
+type instance OrderOf (UnliftBase b) = 'HigherOrder
+instance HFunctor (UnliftBase b) where
+    hfmap phi (WithRunInBase f) = WithRunInBase \run -> f $ run . phi
+    {-# INLINE hfmap #-}
+
+-- * CallCC Effect (Sub/Jump-based)
+
+data CC ref :: Effect where
+    SubFork :: CC ref f (Either (ref a) a)
+    Jump :: ref a -> a -> CC ref f b
+
+data CCLabel
+type instance LabelOf (CC ref) = CCLabel
+type instance OrderOf (CC ref) = 'FirstOrder
+instance FirstOrder (CC ref)
+instance HFunctor (CC ref) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
+
+-- * Shift Effect
+
+data Shift ans ref :: Effect where
+    SubShiftFork :: Shift ans ref f (Either (ref a) a)
+    Call :: ref a -> a -> Shift ans ref f ans
+    Abort :: ans -> Shift ans ref f a
+
+data ShiftLabel
+type instance LabelOf (Shift ans ref) = ShiftLabel
+type instance OrderOf (Shift ans ref) = 'FirstOrder
+instance FirstOrder (Shift ans ref)
+instance HFunctor (Shift ans ref) where
+    hfmap _ = coerce
+    {-# INLINE hfmap #-}
diff --git a/src/Data/Effect/HFunctor.hs b/src/Data/Effect/HFunctor.hs
--- a/src/Data/Effect/HFunctor.hs
+++ b/src/Data/Effect/HFunctor.hs
@@ -1,46 +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
 
 {- |
-Copyright   :  (c) 2023 Sayo Koyoneda
-License     :  MPL-2.0 (see the file LICENSE)
+Copyright   :  (c) 2025 Sayo contributors
+License     :  MPL-2.0 (see the LICENSE file)
 Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
-
-This module re-exports the `HFunctor` type class and related definitions from the `compdata`
-package. For more details, please refer to the
-    [`compdata` documentation](https://hackage.haskell.org/package/compdata-0.13.0/docs/Data-Comp-Multi-HFunctor.html).
 -}
-module Data.Effect.HFunctor (
-    HFunctor (..),
-    RemA (..),
-    DistAnn (..),
-    (:&:) (..),
-    (:=:),
-    (:<:),
-    Subsume (..),
-    Elem,
-    (:+:) (..),
-    caseH,
-    inj,
-    proj,
-    spl,
-) where
+module Data.Effect.HFunctor where
 
-import Data.Comp.Multi.HFunctor (HFunctor (hfmap))
-import Data.Comp.Multi.Ops (
-    DistAnn (injectA, projectA),
-    Elem,
-    RemA (remA),
-    Subsume (..),
-    caseH,
-    inj,
-    proj,
-    spl,
-    type (:&:) ((:&:)),
-    type (:+:) (Inl, Inr),
-    type (:<:),
-    type (:=:),
- )
+import Data.Kind (Type)
+
+class HFunctor (ff :: (Type -> Type) -> Type -> Type) where
+    hfmap :: (forall x. f x -> g x) -> ff f a -> ff g a
diff --git a/src/Data/Effect/HFunctor/HCont.hs b/src/Data/Effect/HFunctor/HCont.hs
--- a/src/Data/Effect/HFunctor/HCont.hs
+++ b/src/Data/Effect/HFunctor/HCont.hs
@@ -1,25 +1,24 @@
 {-# LANGUAGE QuantifiedConstraints #-}
 
--- 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) 2024 Sayo Koyoneda
+Copyright   :  (c) 2024 Sayo contributors
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
 -}
 module Data.Effect.HFunctor.HCont where
 
 import Control.Effect (type (~>))
+import Data.Effect (EffectOrder (HigherOrder), OrderOf)
 import Data.Effect.HFunctor (HFunctor, hfmap)
 import Data.Kind (Type)
 
 -- | This represents that the effect @ff@ is finally interpreted as the base carrier @b@.
 newtype HCont ff b f (a :: Type) = HCont {unHCont :: (f ~> b) -> ff b a}
     deriving stock (Functor)
+
+type instance OrderOf (HCont ff b) = 'HigherOrder
 
 instance HFunctor (HCont ff g) where
     hfmap phi (HCont f) = HCont \k -> f $ k . phi
diff --git a/src/Data/Effect/Key.hs b/src/Data/Effect/Key.hs
deleted file mode 100644
--- a/src/Data/Effect/Key.hs
+++ /dev/null
@@ -1,48 +0,0 @@
-{-# LANGUAGE PatternSynonyms #-}
-
--- 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 Sayo Koyoneda
-License     :  MPL-2.0 (see the file LICENSE)
-Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
--}
-module Data.Effect.Key where
-
-import Data.Comp.Multi.HFunctor (HFunctor)
-import Data.Effect (EffectF, EffectH)
-
--- | Keyed first-order effect.
-newtype Key key (ins :: EffectF) a = Key {unKey :: ins a}
-    deriving stock (Functor, Foldable, Traversable)
-
--- | Keyed first-order effect.
-type (#>) = Key
-
-infixr 7 #>
-
--- | Keyed first-order effect.
-pattern K :: forall key ins a. ins a -> Key key ins a
-pattern K e = Key e
-
-{-# COMPLETE K #-}
-
--- | Keyed higher-order effect.
-newtype KeyH key (sig :: EffectH) f a = KeyH {unKeyH :: sig f a}
-    deriving stock (Functor, Foldable, Traversable)
-    deriving newtype (HFunctor)
-
--- | Keyed higher-order effect.
-type (##>) = KeyH
-
-infixr 7 ##>
-
--- | Keyed higher-order effect.
-pattern KH :: forall key sig f a. sig f a -> KeyH key sig f a
-pattern KH e = KeyH e
-
-{-# COMPLETE KH #-}
diff --git a/src/Data/Effect/OpenUnion.hs b/src/Data/Effect/OpenUnion.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Effect/OpenUnion.hs
@@ -0,0 +1,564 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
+-- SPDX-License-Identifier: MPL-2.0
+
+{- |
+Copyright   :  (c) 2024-2025 Sayo contributors
+License     :  MPL-2.0 (see the file LICENSE)
+Maintainer  :  ymdfield@outlook.jp
+-}
+module Data.Effect.OpenUnion where
+
+import Control.Arrow ((&&&))
+import Data.Coerce (coerce)
+import Data.Data (Proxy (Proxy), (:~:) (Refl))
+import Data.Effect (Effect, EffectOrder (FirstOrder, HigherOrder), FirstOrder, LabelOf, OrderCase, OrderOf)
+import Data.Effect.HFunctor (HFunctor, hfmap)
+import Data.Effect.Tag (type (#))
+import Data.Kind (Constraint, Type)
+import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), KnownNat, Symbol, TypeError, natVal, type (+), type (-))
+import Unsafe.Coerce (unsafeCoerce)
+
+data Union (es :: [Effect]) (f :: Type -> Type) (a :: Type) where
+    UnsafeUnion
+        :: {-# UNPACK #-} !Int
+        -- ^ A natural number tag to identify the element of the union.
+        -> e g a
+        -> {-# UNPACK #-} !EffectOrder
+        -> (forall x. g x -> f x)
+        -> Union es f a
+
+instance HFunctor (Union es) where
+    hfmap phi u@(UnsafeUnion n e order koi) =
+        case order of
+            FirstOrder -> unsafeCoerce u
+            HigherOrder -> UnsafeUnion n e HigherOrder (phi . koi)
+    {-# INLINE hfmap #-}
+
+hfmapUnion :: (forall x. f x -> g x) -> Union es f a -> Union es g a
+hfmapUnion phi u@(UnsafeUnion n e order koi) =
+    case order of
+        FirstOrder -> unsafeCoerce u
+        HigherOrder -> UnsafeUnion n e HigherOrder (phi . koi)
+{-# INLINE hfmapUnion #-}
+
+class FOEs es
+instance FOEs '[]
+instance (FirstOrder e, FOEs es) => FOEs (e ': es)
+
+coerceFOEs :: (FOEs es) => Union es f a -> Union es g a
+coerceFOEs = unsafeCoerce
+{-# INLINE coerceFOEs #-}
+
+type instance OrderOf (Union es) = 'HigherOrder
+
+newtype Membership (e :: Effect) (es :: [Effect]) = UnsafeMembership {unMembership :: Int}
+    deriving stock (Eq, Show)
+
+pattern Here :: Membership e (e ': es)
+pattern Here = UnsafeMembership 0
+{-# INLINE Here #-}
+
+pattern There :: Membership e es -> Membership e (e ': es)
+pattern There i <- ((UnsafeMembership . (`subtract` 1) &&& (/= 0)) . unMembership -> (i, True))
+    where
+        There (UnsafeMembership n) = UnsafeMembership (n + 1)
+{-# INLINE There #-}
+
+{-# COMPLETE Here, There #-}
+
+weakenFor :: Membership e es -> Membership e (e' ': es)
+weakenFor (UnsafeMembership n) = UnsafeMembership $ n + 1
+{-# INLINE weakenFor #-}
+
+mapUnion
+    :: forall es es' f a
+     . (forall e. Membership e es -> Membership e es')
+    -> Union es f a
+    -> Union es' f a
+mapUnion f (UnsafeUnion n e order koi) =
+    UnsafeUnion (unMembership $ f $ UnsafeMembership n) e order koi
+{-# INLINE mapUnion #-}
+
+membershipAt :: forall i es. (KnownNat i) => Membership (At i es) es
+membershipAt = UnsafeMembership $ intVal @i
+{-# INLINE membershipAt #-}
+
+compareMembership :: Membership e es -> Membership e' es -> Maybe (e :~: e')
+compareMembership (UnsafeMembership m) (UnsafeMembership n)
+    | m == n = Just $ unsafeCoerce Refl
+    | otherwise = Nothing
+
+type family At i es where
+    At 0 (e ': es) = e
+    At n (e ': es) = At (n - 1) es
+    At _ '[] = TypeError ('Text "Effect index out of range")
+
+intVal :: forall n. (KnownNat n) => Int
+intVal = fromIntegral $ natVal @n Proxy
+{-# INLINE intVal #-}
+
+data LabelResolver
+data KeyResolver
+data IdentityResolver
+
+data KeyDiscriminator key
+data NoKeyDiscriminator
+
+data IdentityDiscriminator (e :: Effect)
+
+type family Discriminator resolver (e :: Effect)
+type instance Discriminator LabelResolver e = LabelOf e
+type instance Discriminator KeyResolver e = KeyOf e
+type instance Discriminator IdentityResolver e = IdentityDiscriminator e
+
+type family KeyOf e where
+    KeyOf (e # key) = KeyDiscriminator key
+    KeyOf e = NoKeyDiscriminator
+
+type family ResolverName resolver :: Symbol
+type instance ResolverName LabelResolver = "label"
+type instance ResolverName KeyResolver = "key"
+type instance ResolverName IdentityResolver = "identity"
+
+infix 4 :>
+infix 4 `In`
+
+type e :> es = MemberBy LabelResolver (Discriminator LabelResolver e) e es
+type Has key e es = MemberBy KeyResolver (KeyDiscriminator key) (e # key) es
+type e `In` es = MemberBy IdentityResolver (IdentityDiscriminator e) e es
+type KnownIndex i es = (KnownNat i, KnownOrder (At i es))
+
+type FindByLabel label e es = MemberBy LabelResolver label e es
+
+type MemberBy resolver dscr e es =
+    ( FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es
+    , ErrorIfNotFound resolver dscr (Discriminator resolver (HeadOf es)) e es es
+    , KnownOrder e
+    )
+
+class
+    (dscr ~ Discriminator resolver e, dscr' ~ Discriminator resolver (HeadOf r)) =>
+    FindBy resolver dscr dscr' e r
+        | resolver dscr dscr' r -> e
+    where
+    findBy :: Membership e r
+
+instance
+    (dscr ~ Discriminator resolver e, dscr ~ Discriminator resolver e', e ~ e')
+    => FindBy resolver dscr dscr e (e' ': r)
+    where
+    findBy = Here
+    {-# INLINE findBy #-}
+
+instance
+    {-# OVERLAPPABLE #-}
+    ( dscr ~ Discriminator resolver e
+    , dscr' ~ Discriminator resolver e'
+    , FindBy resolver dscr (Discriminator resolver (HeadOf r)) e r
+    )
+    => FindBy resolver dscr dscr' e (e' ': r)
+    where
+    findBy = weakenFor $ findBy @resolver @dscr @(Discriminator resolver (HeadOf r)) @e @r
+    {-# INLINE findBy #-}
+
+membership
+    :: forall resolver dscr e es
+     . (FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es)
+    => Membership e es
+membership = findBy @resolver @dscr @(Discriminator resolver (HeadOf es)) @e @es
+{-# INLINE membership #-}
+
+labelMembership
+    :: forall e es
+     . (FindBy LabelResolver (LabelOf e) (LabelOf (HeadOf es)) e es)
+    => Membership e es
+labelMembership = membership @LabelResolver
+{-# INLINE labelMembership #-}
+
+keyMembership
+    :: forall key e es
+     . (FindBy KeyResolver (KeyDiscriminator key) (KeyOf (HeadOf es)) (e # key) es)
+    => Membership (e # key) es
+keyMembership = membership @KeyResolver
+{-# INLINE keyMembership #-}
+
+identityMembership
+    :: forall e es
+     . (FindBy IdentityResolver (IdentityDiscriminator e) (IdentityDiscriminator (HeadOf es)) e es)
+    => Membership e es
+identityMembership = membership @IdentityResolver
+{-# INLINE identityMembership #-}
+class
+    (dscr ~ Discriminator resolver e, dscr' ~ Discriminator resolver (HeadOf r)) =>
+    ErrorIfNotFound resolver dscr dscr' (e :: Effect) (r :: [Effect]) (w :: [Effect])
+
+instance
+    ( TypeError
+        ( 'Text "The effect ‘"
+            ':<>: 'ShowType e
+            ':<>: 'Text "’ does not exist within the effect list"
+            ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"
+            ':$$: 'Text "Resolver: " ':<>: 'Text (ResolverName resolver)
+            ':$$: 'Text "Discriminator: " ':<>: 'ShowType dscr
+        )
+    , dscr ~ Discriminator resolver e
+    , dscr' ~ Discriminator resolver (HeadOf '[])
+    )
+    => ErrorIfNotFound resolver dscr dscr' e '[] w
+
+instance
+    (dscr ~ Discriminator resolver e, dscr ~ Discriminator resolver e', e ~ e')
+    => ErrorIfNotFound resolver dscr dscr e (e' ': r) w
+
+instance
+    {-# OVERLAPPABLE #-}
+    ( dscr ~ Discriminator resolver e
+    , dscr' ~ Discriminator resolver e'
+    , ErrorIfNotFound resolver dscr (Discriminator resolver (HeadOf r)) e r w
+    )
+    => ErrorIfNotFound resolver dscr dscr' e (e' ': r) w
+
+instance
+    {-# INCOHERENT #-}
+    ( dscr ~ Discriminator resolver e
+    , dscr' ~ Discriminator resolver (HeadOf r)
+    )
+    => ErrorIfNotFound resolver dscr dscr' e r w
+
+type family HeadOf es where
+    HeadOf (e ': es) = e
+
+type KnownOrder e = Elem e (OrderOf e)
+
+class (order ~ OrderOf e) => Elem e order where
+    inject :: Membership e es -> e f a -> Union es f a
+    project :: Membership e es -> Union es f a -> Maybe (e f a)
+    (!:) :: (e f a -> r) -> (Union es f a -> r) -> Union (e ': es) f a -> r
+    extract :: Union '[e] f a -> e f a
+
+    infixr 5 !:
+
+decomp :: (KnownOrder e, HFunctor e) => Union (e ': es) f a -> Either (e f a) (Union es f a)
+decomp = Left !: Right
+{-# INLINE decomp #-}
+
+instance (FirstOrder e) => Elem e 'FirstOrder where
+    inject :: forall es f a. Membership e es -> e f a -> Union es f a
+    inject i = mkUnion i firstOrdership
+
+    project
+        :: forall es f a
+         . Membership e es
+        -> Union es f a
+        -> Maybe (e f a)
+    project i (UnsafeUnion n e _ _) =
+        if n == unMembership i
+            then Just $ unsafeCoerce e
+            else Nothing
+
+    (f !: g) (UnsafeUnion n e koi order) =
+        if n == 0
+            then f $ unsafeCoerce e
+            else g $ UnsafeUnion (n - 1) e koi order
+
+    extract (UnsafeUnion _ e _ _) = unsafeCoerce e
+
+    {-# INLINE inject #-}
+    {-# INLINE project #-}
+    {-# INLINE (!:) #-}
+    {-# INLINE extract #-}
+
+instance (OrderOf e ~ 'HigherOrder, HFunctor e) => Elem e 'HigherOrder where
+    inject :: forall es f a. Membership e es -> e f a -> Union es f a
+    inject i = mkUnion i (higherOrdership id)
+
+    project :: forall es f a. Membership e es -> Union es f a -> Maybe (e f a)
+    project i (UnsafeUnion n e _ koi) =
+        if n == unMembership i
+            then Just $ hfmap koi (unsafeCoerce e)
+            else Nothing
+
+    (f !: g) (UnsafeUnion n e _ koi) =
+        if n == 0
+            then f $ hfmap koi (unsafeCoerce e)
+            else g $ UnsafeUnion (n - 1) e HigherOrder koi
+
+    extract (UnsafeUnion _ e _ koi) = hfmap koi (unsafeCoerce e)
+
+    {-# INLINE inject #-}
+    {-# INLINE project #-}
+    {-# INLINE (!:) #-}
+    {-# INLINE extract #-}
+
+projectAnyOrder :: forall e es f a. (HFunctor e) => Membership e es -> Union es f a -> Maybe (e f a)
+projectAnyOrder i (UnsafeUnion n e order koi) =
+    if n == unMembership i
+        then Just $ hfmapDynUnsafeCoerce order koi e
+        else Nothing
+
+infixr 5 `caseAnyOrder`
+
+caseAnyOrder :: (HFunctor e) => (e f a -> r) -> (Union es f a -> r) -> Union (e ': es) f a -> r
+(f `caseAnyOrder` g) (UnsafeUnion n e order koi) =
+    if n == 0
+        then f $ hfmapDynUnsafeCoerce order koi e
+        else g $ UnsafeUnion (n - 1) e order koi
+
+extractAnyOrder :: (HFunctor e) => Union es f a -> e f a
+extractAnyOrder (UnsafeUnion _ e order koi) = hfmapDynUnsafeCoerce order koi e
+
+{-# INLINE projectAnyOrder #-}
+{-# INLINE caseAnyOrder #-}
+{-# INLINE extractAnyOrder #-}
+
+hfmapDynUnsafeCoerce :: (HFunctor e') => EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a
+hfmapDynUnsafeCoerce order phi e = case order of
+    FirstOrder -> unsafeCoerce e
+    HigherOrder -> hfmap phi (unsafeCoerce e)
+{-# INLINE hfmapDynUnsafeCoerce #-}
+
+nil :: Union '[] f a -> r
+nil _ = error "Effect system internal error: nil - An empty effect union, which should not be possible to create, has been created."
+
+nilMembership :: Membership e '[] -> r
+nilMembership _ = error "Effect system internal error: nil - An empty effect union membership, which should not be possible to create, has been created."
+
+weakensFor :: forall es es' e. (Suffix es es') => Membership e es -> Membership e es'
+weakensFor (UnsafeMembership n) = UnsafeMembership $ n + prefixLen @es @es'
+{-# INLINE weakensFor #-}
+
+class Suffix (es :: [Effect]) (es' :: [Effect]) where
+    prefixLen :: Int
+
+instance Suffix es es where
+    prefixLen = 0
+    {-# INLINE prefixLen #-}
+
+instance {-# INCOHERENT #-} (Suffix es es') => Suffix es (e ': es') where
+    prefixLen = prefixLen @es @es' + 1
+    {-# INLINE prefixLen #-}
+
+class SuffixUnder (es :: [Effect]) (es' :: [Effect]) where
+    prefixLenUnder :: Int
+    offset :: Int
+
+instance (Suffix es es') => SuffixUnder es es' where
+    prefixLenUnder = prefixLen @es @es'
+    offset = 0
+
+    {-# INLINE prefixLenUnder #-}
+    {-# INLINE offset #-}
+
+instance {-# INCOHERENT #-} (SuffixUnder es es') => SuffixUnder (e ': es) (e ': es') where
+    prefixLenUnder = prefixLenUnder @es @es'
+    offset = offset @es @es' + 1
+
+    {-# INLINE prefixLenUnder #-}
+    {-# INLINE offset #-}
+
+weakensUnderFor :: forall es es' e. (SuffixUnder es es') => Membership e es -> Membership e es'
+weakensUnderFor (UnsafeMembership n) =
+    UnsafeMembership
+        if n < offset @es @es'
+            then n
+            else n + prefixLenUnder @es @es'
+{-# INLINE weakensUnderFor #-}
+
+type family RemoveHOEs (es :: [Effect]) where
+    RemoveHOEs '[] = '[]
+    RemoveHOEs (e ': es) =
+        OrderCase (OrderOf e) (e ': RemoveHOEs es) (RemoveHOEs es)
+
+type WeakenHOEs es = (WeakenHOEs_ es 0 (OrderOf (HeadOf es)), FOEs (RemoveHOEs es))
+
+class (orderOfHead ~ OrderOf (HeadOf es)) => WeakenHOEs_ es countF orderOfHead where
+    -- | Example for '[H,F,F,H,H,F,H,F]
+    --
+    -- +----+-------+--------+----------------------+
+    -- | ix | order | countF | shifter accumulation |
+    -- +====+=======+========+======================+
+    -- |  0 |     H |      0 | 01234... -> 12345... |
+    -- |  1 |     F |      0 | 01234... -> 12345... |
+    -- |  2 |     F |      1 | 01234... -> 12345... |
+    -- |  3 |     H |      2 | 01234... -> 12456... |
+    -- |  4 |     H |      2 | 01234... -> 12567... |
+    -- |  5 |     F |      2 | 01234... -> 12567... |
+    -- |  6 |     H |      3 | 01234... -> 12578... |
+    -- |  7 |     F |      3 | 01234... -> 12578... |
+    -- +----+-------+--------+----------------------+
+    foldHoeIndexShifter :: (Int -> Int) -> (Int -> Int)
+
+instance (OrderOf (HeadOf '[]) ~ orderOfHead) => WeakenHOEs_ '[] countF orderOfHead where
+    foldHoeIndexShifter = id
+    {-# INLINE foldHoeIndexShifter #-}
+
+instance (FirstOrder e, WeakenHOEs_ es (countF + 1) _orderOfHead) => WeakenHOEs_ (e ': es) countF 'FirstOrder where
+    foldHoeIndexShifter = foldHoeIndexShifter @es @(countF + 1)
+    {-# INLINE foldHoeIndexShifter #-}
+
+instance
+    (OrderOf e ~ 'HigherOrder, WeakenHOEs_ es countF _orderOfHead, KnownNat countF)
+    => WeakenHOEs_ (e ': es) countF 'HigherOrder
+    where
+    foldHoeIndexShifter shifterAcc =
+        foldHoeIndexShifter @es @countF \ix ->
+            let shiftedIx = shifterAcc ix
+             in if ix < intVal @countF
+                    then shiftedIx
+                    else shiftedIx + 1
+    {-# INLINE foldHoeIndexShifter #-}
+
+weaken :: Union es f a -> Union (e ': es) f a
+weaken = mapUnion weakenFor
+{-# INLINE weaken #-}
+
+weakens :: (Suffix es es') => Union es f a -> Union es' f a
+weakens = mapUnion weakensFor
+{-# INLINE weakens #-}
+
+weakensUnder :: (SuffixUnder es es') => Union es f a -> Union es' f a
+weakensUnder = mapUnion weakensUnderFor
+{-# INLINE weakensUnder #-}
+
+weakenHOEsFor :: forall es e. (WeakenHOEs es) => Membership e (RemoveHOEs es) -> Membership e es
+weakenHOEsFor = UnsafeMembership . foldHoeIndexShifter @es @0 id . unMembership
+{-# INLINE weakenHOEsFor #-}
+
+weakenHOEs :: forall es f a. (WeakenHOEs es) => Union (RemoveHOEs es) f a -> Union es f a
+weakenHOEs = mapUnion weakenHOEsFor
+{-# INLINE weakenHOEs #-}
+
+type KnownLength :: forall {k}. [k] -> Constraint
+class KnownLength xs where
+    reifyLength :: Int
+
+instance KnownLength '[] where
+    reifyLength = 0
+    {-# INLINE reifyLength #-}
+
+instance (KnownLength xs) => KnownLength (x ': xs) where
+    reifyLength = 1 + reifyLength @xs
+    {-# INLINE reifyLength #-}
+
+infixr 5 ++
+
+type family (es :: [Effect]) ++ (es' :: [Effect]) where
+    '[] ++ es = es
+    (e ': es) ++ es' = e ': (es ++ es')
+
+infixr 5 !++
+
+(!++) :: forall es es' f a r. (KnownLength es) => (Union es f a -> r) -> (Union es' f a -> r) -> Union (es ++ es') f a -> r
+(h !++ h') (UnsafeUnion n e o koi) =
+    if n < reifyLength @es
+        then h $ UnsafeUnion n e o koi
+        else h' $ UnsafeUnion (n - reifyLength @es) e o koi
+{-# INLINE (!++) #-}
+
+bundleUnion
+    :: forall es es' f a
+     . (KnownLength es)
+    => Union (es ++ es') f a
+    -> Union (Union es ': es') f a
+bundleUnion = union \i o e ->
+    splitFor @es @es'
+        (\j -> mkUnion Here (higherOrdership id) (mkUnion j o e))
+        (\j -> mkUnion (weakenFor j) o e)
+        i
+{-# INLINE bundleUnion #-}
+
+unbundleUnion
+    :: forall es es' f a
+     . (KnownLength es)
+    => Union (Union es ': es') f a
+    -> Union (es ++ es') f a
+unbundleUnion = mapUnion (suffixFor @es') !: mapUnion (prefixFor @es)
+{-# INLINE unbundleUnion #-}
+
+splitUnion
+    :: forall es es' es'' f a
+     . (KnownLength es)
+    => (forall e. Membership e es -> Membership e es'')
+    -> (forall e. Membership e es' -> Membership e es'')
+    -> Union (es ++ es') f a
+    -> Union es'' f a
+splitUnion injL injR = mapUnion $ splitFor @es @es' injL injR
+{-# INLINE splitUnion #-}
+
+mergeUnion
+    :: forall es es' f a
+     . (KnownLength es)
+    => Either (Union es f a) (Union es' f a)
+    -> Union (es ++ es') f a
+mergeUnion = \case
+    Left u -> mapUnion (suffixFor @es') u
+    Right u -> mapUnion (prefixFor @es) u
+{-# INLINE mergeUnion #-}
+
+splitFor
+    :: forall es es' e r
+     . (KnownLength es)
+    => (Membership e es -> r)
+    -> (Membership e es' -> r)
+    -> Membership e (es ++ es')
+    -> r
+splitFor f g (UnsafeMembership n)
+    | n < l = f $ UnsafeMembership n
+    | otherwise = g $ UnsafeMembership $ n - l
+  where
+    l = reifyLength @es
+{-# INLINE splitFor #-}
+
+suffixFor :: forall es' es e. Membership e es -> Membership e (es ++ es')
+suffixFor = coerce
+{-# INLINE suffixFor #-}
+
+prefixFor :: forall es' es e. (KnownLength es') => Membership e es -> Membership e (es' ++ es)
+prefixFor (UnsafeMembership n) = UnsafeMembership $ reifyLength @es' + n
+{-# INLINE prefixFor #-}
+
+type family Each (fs :: [k -> Effect]) x where
+    Each (f ': fs) x = (f x ': Each fs x)
+    Each '[] x = '[]
+
+prefixFor1 :: forall fs x es e. (KnownLength fs) => Membership e es -> Membership e (Each fs x ++ es)
+prefixFor1 (UnsafeMembership n) = UnsafeMembership $ reifyLength @fs + n
+{-# INLINE prefixFor1 #-}
+
+data Ordership (o :: EffectOrder) (e :: Effect) (f :: Type -> Type) (g :: Type -> Type) where
+    UnsafeFirst :: Ordership 'FirstOrder e f g
+    UnsafeHigher :: (forall x. g x -> f x) -> Ordership 'HigherOrder e f g
+
+union :: (forall e o g. Membership e es -> Ordership o e f g -> e g a -> r) -> Union es f a -> r
+union f (UnsafeUnion n e o koi) =
+    let i = UnsafeMembership n
+     in case o of
+            FirstOrder -> f i UnsafeFirst e
+            HigherOrder -> f i (UnsafeHigher koi) e
+{-# INLINE union #-}
+
+mkUnion :: Membership e es -> Ordership o e f g -> e g a -> Union es f a
+mkUnion (UnsafeMembership i) o e = case o of
+    UnsafeFirst -> UnsafeUnion i e FirstOrder undefined
+    UnsafeHigher koi -> UnsafeUnion i e HigherOrder koi
+{-# INLINE mkUnion #-}
+
+firstOrdership :: (FirstOrder e) => Ordership 'FirstOrder e f g
+firstOrdership = UnsafeFirst
+{-# INLINE firstOrdership #-}
+
+higherOrdership :: (OrderOf e ~ 'HigherOrder) => (forall x. g x -> f x) -> Ordership 'HigherOrder e f g
+higherOrdership = UnsafeHigher
+{-# INLINE higherOrdership #-}
+
+shrinkOrdership :: Ordership o e f g -> Ordership (OrderOf e) e f g
+shrinkOrdership = unsafeCoerce
+
+continuationOfInterpretation :: Ordership 'HigherOrder e f g -> (forall x. g x -> f x)
+continuationOfInterpretation (UnsafeHigher koi) = koi
+{-# INLINE continuationOfInterpretation #-}
diff --git a/src/Data/Effect/Tag.hs b/src/Data/Effect/Tag.hs
--- a/src/Data/Effect/Tag.hs
+++ b/src/Data/Effect/Tag.hs
@@ -1,48 +1,28 @@
-{-# LANGUAGE PatternSynonyms #-}
-
--- 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-2024 Sayo Koyoneda
+Copyright   :  (c) 2023-2024 Sayo contributors
 License     :  MPL-2.0 (see the file LICENSE)
 Maintainer  :  ymdfield@outlook.jp
-Stability   :  experimental
-Portability :  portable
 -}
 module Data.Effect.Tag where
 
-import Data.Comp.Multi.HFunctor (HFunctor)
-import Data.Effect (EffectF, EffectH)
-
--- | Tagged first-order effect.
-newtype Tag (ins :: EffectF) tag a = Tag {unTag :: ins a}
-    deriving stock (Functor, Foldable, Traversable)
-
--- | Tagged first-order effect.
-type (#) = Tag
-
-infixl 8 #
-
--- | Tagged first-order effect.
-pattern T :: forall tag ins a. ins a -> Tag ins tag a
-pattern T e = Tag e
-
-{-# COMPLETE T #-}
+import Data.Effect (Effect, FirstOrder, LabelOf, OrderOf)
+import Data.Effect.HFunctor (HFunctor)
+import Data.Kind (Type)
 
--- | Tagged higher-order effect.
-newtype TagH (sig :: EffectH) tag f a = TagH {unTagH :: sig f a}
+-- | Tagged effect.
+newtype Tagged tag (e :: Effect) f a = Tag {unTag :: e f a}
     deriving stock (Functor, Foldable, Traversable)
     deriving newtype (HFunctor)
 
--- | Tagged higher-order effect.
-type (##) = TagH
+type instance OrderOf (Tagged tag e) = OrderOf e
+instance (FirstOrder e) => FirstOrder (Tagged tag e)
 
-infixl 8 ##
+type instance LabelOf (Tagged tag e) = TaggedLabel tag (LabelOf e)
+data TaggedLabel tag (label :: Type)
 
--- | Tagged higher-order effect.
-pattern TH :: forall tag sig f a. sig f a -> TagH sig tag f a
-pattern TH e = TagH e
+-- | Tagged effect.
+type e # tag = Tagged tag e
 
-{-# COMPLETE TH #-}
+infixl 7 #
diff --git a/test/OpenUnion.hs b/test/OpenUnion.hs
new file mode 100644
--- /dev/null
+++ b/test/OpenUnion.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+{-# OPTIONS_GHC -fconstraint-solver-iterations=16 #-}
+
+-- SPDX-License-Identifier: MPL-2.0
+
+module OpenUnion where
+
+import Control.Effect (Eff, Free, perform)
+import Data.Effect (Catch, Effect, LabelOf, Throw (Throw))
+import Data.Effect.OpenUnion (Membership (UnsafeMembership), labelMembership, membershipAt, weakenHOEsFor, (:>))
+import Data.Proxy (Proxy (Proxy))
+import GHC.TypeNats (KnownNat, Natural, natVal)
+import Test.Hspec (Spec, describe, it, shouldBe)
+
+data A x :: Effect
+data ALabel
+type instance LabelOf (A x) = ALabel
+
+data B x y :: Effect
+data BLabel x
+type instance LabelOf (B x y) = BLabel x
+
+spec_membership :: Spec
+spec_membership = describe "Open-Union Membership" do
+    it "Membership (A 0) '[B 1 2, A 0] -> 1" $
+        label1 `shouldBe` UnsafeMembership 1
+
+    it "Membership (B 5 6) '[B 1 2, B 3 4, A 1, B 5 6, A 0] -> 3" $
+        label2 `shouldBe` UnsafeMembership 3
+
+    it "Membership (B 5 ?) '[B 1 2, B 3 4, A 1, B 5 6, A 0] --infer--> ?=6" $
+        infer1 labelMembership `shouldBe` 6
+  where
+    label1 :: Membership (A 0) '[B 1 2, A 0]
+    label1 = labelMembership
+
+    label2 :: Membership (B 5 6) '[B 1 2, B 3 4, A 1, B 5 6, A 0]
+    label2 = labelMembership
+
+    infer1 :: forall x. (KnownNat x) => Membership (B 5 x) '[B 1 2, B 3 4, A 1, B 5 6, A 0] -> Natural
+    infer1 _ = natVal @x Proxy
+
+type F = Throw ()
+type H = Catch ()
+
+spec_onlyFOEs :: Spec
+spec_onlyFOEs = describe "onlyFOEs index shift" do
+    it "'[<F>, F , F , F ] -> '[ H ,<F>, F , H , H , F , H , F ]" $
+        shiftIx ix0 `shouldBe` UnsafeMembership 1
+    it "'[ F ,<F>, F , F ] -> '[ H , F ,<F>, H , H , F , H , F ]" $
+        shiftIx ix1 `shouldBe` UnsafeMembership 2
+    it "'[ F , F ,<F>, F ] -> '[ H , F , F , H , H ,<F>, H , F ]" $
+        shiftIx ix2 `shouldBe` UnsafeMembership 5
+    it "'[ F , F , F ,<F>] -> '[ H , F , F , H , H , F , H ,<F>]" $
+        shiftIx ix3 `shouldBe` UnsafeMembership 7
+  where
+    shiftIx :: Membership e '[F, F, F, F] -> Membership e '[H, F, F, H, H, F, H, F]
+    shiftIx = weakenHOEsFor
+
+    ix0, ix1, ix2, ix3 :: Membership F '[F, F, F, F]
+    ix0 = membershipAt @0
+    ix1 = membershipAt @1
+    ix2 = membershipAt @2
+    ix3 = membershipAt @3
+
+inferCompileTest :: (Throw () :> es, Catch () :> es, Free Monad ff) => Eff ff es a
+inferCompileTest = perform $ Throw mempty