From 9e22c667e48443fe795a531d8d328b6d6853bf8f Mon Sep 17 00:00:00 2001
From: Yamada Ryo <ymdfield@outlook.jp>
Date: Mon, 4 Sep 2023 11:44:27 +0900
Subject: [PATCH] [fix] Change the order of type arguments for heftia
 transformers.

[fix] Unify signature sum types with those of the datacomp package.
---
 heftia-effects/heftia-effects.cabal           |   1 +
 .../Control/Effect/Handler/Heftia/State.hs    |  20 --
 heftia/src/Control/Effect/Heftia.hs           | 144 +++++++++++
 heftia/src/Control/Heftia.hs                  | 225 +-----------------
 heftia/src/Control/Heftia/Final.hs            |  24 +-
 heftia/src/Control/Heftia/Final/Naked.hs      |  17 +-
 heftia/src/Control/Heftia/Trans.hs            |  22 +-
 heftia/src/Control/Heftia/Trans/Final.hs      |  97 ++++----
 .../src/Control/Heftia/Trans/Final/Naked.hs   |  14 +-
 heftia/src/Control/Monad/Trans/Heftia.hs      |  43 ++--
 heftia/src/Data/Hefty/Sum.hs                  |  39 ++-
 11 files changed, 278 insertions(+), 368 deletions(-)
 create mode 100644 heftia/src/Control/Effect/Heftia.hs

diff --git a/heftia-effects/heftia-effects.cabal b/heftia-effects/heftia-effects.cabal
index ccd4524..46c9336 100644
--- a/heftia-effects/heftia-effects.cabal
+++ b/heftia-effects/heftia-effects.cabal
@@ -36,6 +36,7 @@ library
     exposed-modules:
         Control.Effect.Handler.Heftia
         Control.Effect.Handler.Heftia.Reader
+        Control.Effect.Handler.Heftia.State
 
     -- Modules included in this executable, other than Main.
     -- other-modules:
diff --git a/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs b/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs
index bb4ceff..5e04cef 100644
--- a/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs
+++ b/heftia-effects/src/Control/Effect/Handler/Heftia/State.hs
@@ -3,23 +3,3 @@
 -- file, You can obtain one at https://mozilla.org/MPL/2.0/.
 
 module Control.Effect.Handler.Heftia.State where
-
-import Control.Effect.Class.Machinery.HFunctor (HFunctor)
-import Control.Effect.Class.State (StateS, pattern GetS, pattern PutS)
-import Control.Heftia.Final (Hef)
-import Control.Heftia.Trans.Final (HeftiaFinalT, liftLowerFinal)
-import Control.Monad.State (get, put, runStateT)
-import Control.Monad.Trans.Heftia (interpretTT)
-import Data.Hefty.Sum (Sum)
-import Data.Tuple (swap)
-
-interpretState :: forall s es a. HFunctor (Sum es) => s -> Hef (StateS s ': es) a -> Hef es (s, a)
-interpretState s a =
-    fmap swap $
-        (`runStateT` s) $
-            interpretTT @(HeftiaFinalT Monad) @_ @_ @(StateS s)
-                ( \case
-                    GetS -> get
-                    PutS s' -> put s'
-                )
-                (liftLowerFinal undefined)
diff --git a/heftia/src/Control/Effect/Heftia.hs b/heftia/src/Control/Effect/Heftia.hs
new file mode 100644
index 0000000..155fa9f
--- /dev/null
+++ b/heftia/src/Control/Effect/Heftia.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# 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/.
+
+module Control.Effect.Heftia where
+
+import Control.Applicative (Alternative)
+import Control.Effect.Class (
+    LiftIns (LiftIns),
+    SendIns,
+    SendSig,
+    SendVia (SendVia),
+    Signature,
+    runSendVia,
+    sendIns,
+    sendSig,
+    type (~>),
+ )
+import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
+import Control.Freer (Freer, liftIns)
+import Control.Heftia (Heftia (..))
+import Control.Heftia.Final (HeftiaFinal)
+import Control.Monad (MonadPlus)
+import Data.Hefty.Sum (SumUnion)
+import Data.Hefty.Union (
+    Member,
+    Union,
+    decomp,
+    inject,
+    project,
+    weakenL,
+    weakenR,
+ )
+import Data.Kind (Type)
+import GHC.Generics qualified as F
+
+newtype HeftiaUnion (h :: Signature -> Type -> Type) u (es :: [Signature]) a = HeftiaUnion
+    {runHeftiaUnion :: h (u es) a}
+    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)
+    deriving stock (Foldable, Traversable)
+
+type HeftiaEffects h u es = SendVia (HeftiaUnion h u es)
+
+runHeftiaEffects :: HeftiaEffects h u es ~> h (u es)
+runHeftiaEffects = runHeftiaUnion . runSendVia
+
+heftiaEffects :: h (u es) ~> HeftiaEffects h u es
+heftiaEffects = SendVia . HeftiaUnion
+
+instance
+    (Heftia c h, Union u, Member u (LiftIns e) es, HFunctor (u es)) =>
+    SendIns e (HeftiaUnion h u es)
+    where
+    sendIns = HeftiaUnion . liftSig . inject . LiftIns
+
+instance
+    (Heftia c h, Union u, Member u e es, HFunctor (u es)) =>
+    SendSig e (HeftiaUnion h u es)
+    where
+    sendSig = HeftiaUnion . liftSig . hfmap runHeftiaUnion . inject
+
+interpret ::
+    (Heftia c h, Union u, HFunctor (u es), HFunctor (u (e : es)), HFunctor e) =>
+    (e (HeftiaEffects h u es) ~> HeftiaEffects h u es) ->
+    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u es
+interpret i a =
+    heftiaEffects $ ($ runHeftiaEffects a) $ interpretH \u ->
+        case decomp u of
+            Left e -> runHeftiaEffects $ i $ hfmap heftiaEffects e
+            Right e -> liftSig e
+
+reinterpret ::
+    (Heftia c h, Union u, HFunctor (u (e : es)), HFunctor e) =>
+    (e (HeftiaEffects h u (e ': es)) ~> HeftiaEffects h u (e ': es)) ->
+    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u (e ': es)
+reinterpret i a =
+    heftiaEffects $ ($ runHeftiaEffects a) $ reinterpretH \u ->
+        case decomp u of
+            Left e -> runHeftiaEffects $ i $ hfmap heftiaEffects e
+            Right e -> liftSig $ weakenR e
+
+translate ::
+    ( Heftia c h
+    , Union u
+    , HFunctor (u (e : es))
+    , HFunctor (u (e' : es))
+    , HFunctor e
+    , HFunctor e'
+    ) =>
+    (e (HeftiaEffects h u (e' ': es)) ~> e' (HeftiaEffects h u (e' ': es))) ->
+    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u (e' ': es)
+translate f a =
+    heftiaEffects $ ($ runHeftiaEffects a) $ translateH \u ->
+        case decomp u of
+            Left e -> weakenL $ hfmap runHeftiaEffects $ f $ hfmap heftiaEffects e
+            Right e -> weakenR e
+
+interpose ::
+    forall e h u es c.
+    (Heftia c h, Union u, Member u e es, HFunctor (u es)) =>
+    (e (HeftiaEffects h u es) ~> HeftiaEffects h u es) ->
+    HeftiaEffects h u es ~> HeftiaEffects h u es
+interpose f a =
+    heftiaEffects $ ($ runHeftiaEffects a) $ reinterpretH \u ->
+        let u' = hfmap (interpose f . heftiaEffects) u
+         in case project @_ @e u' of
+                Just e -> runHeftiaEffects $ f e
+                Nothing -> liftSig $ hfmap runHeftiaEffects u'
+
+intercept ::
+    forall e h u es c.
+    (Heftia c h, Union u, Member u e es, HFunctor (u es), HFunctor e) =>
+    (e (HeftiaEffects h u es) ~> e (HeftiaEffects h u es)) ->
+    HeftiaEffects h u es ~> HeftiaEffects h u es
+intercept f a =
+    heftiaEffects $ ($ runHeftiaEffects a) $ translateH \u ->
+        let u' = hfmap (intercept f . heftiaEffects) u
+         in case project @_ @e u' of
+                Just e -> inject $ hfmap runHeftiaEffects $ f e
+                Nothing -> hfmap runHeftiaEffects u'
+
+raiseUnder ::
+    forall e' e es h u c.
+    (Heftia c h, HFunctor (u (e : es)), HFunctor (u (e : e' : es)), Union u) =>
+    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u (e ': e' ': es)
+raiseUnder a =
+    heftiaEffects
+        . ($ runHeftiaEffects a)
+        $ translateH \u -> case decomp u of
+            Left e -> weakenL e
+            Right e -> weakenR $ weakenR e
+
+heftiaToFreer ::
+    (Heftia c h, Freer c' f, c (f (i F.:+: h e))) =>
+    h (LiftIns (i F.:+: h e)) ~> f (i F.:+: h e)
+heftiaToFreer a = ($ a) $ interpretH \case
+    LiftIns (F.L1 i) -> liftIns $ F.L1 i
+    LiftIns (F.R1 h) -> liftIns $ F.R1 h
+
+type Hef es = HeftiaEffects (HeftiaFinal Monad) SumUnion es
+type HefA es = HeftiaEffects (HeftiaFinal Applicative) SumUnion es
diff --git a/heftia/src/Control/Heftia.hs b/heftia/src/Control/Heftia.hs
index 2a3ee3b..f32197e 100644
--- a/heftia/src/Control/Heftia.hs
+++ b/heftia/src/Control/Heftia.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE QuantifiedConstraints #-}
-{-# 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
@@ -7,35 +6,9 @@
 
 module Control.Heftia where
 
-import Control.Applicative (Alternative)
-import Control.Effect.Class (
-    LiftIns (LiftIns),
-    SendIns,
-    SendSig,
-    SendVia (SendVia),
-    Signature,
-    runSendVia,
-    sendIns,
-    sendSig,
-    unliftIns,
-    type (~>),
- )
+import Control.Effect.Class (LiftIns, unliftIns, type (~>))
 import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
-import Control.Freer (Freer, liftIns)
-import Control.Monad (MonadPlus)
-import Data.Hefty.Union (
-    Member,
-    Union,
-    decomp,
-    inject,
-    project,
-    weakenL,
-    weakenR,
-    weakenSig,
-    type (<:),
- )
-import Data.Kind (Type)
-import GHC.Generics qualified as F
+import Data.Hefty.Union (weakenSig, type (<:))
 
 class (forall sig. HFunctor sig => c (h sig)) => Heftia c h | h -> c where
     {-# MINIMAL liftSig, interpretH #-}
@@ -63,197 +36,3 @@ retract = interpretH unliftIns
 
 sendH :: (s <: t, Heftia c h, HFunctor s, HFunctor t) => s (h s) a -> h t a
 sendH = liftSig . weakenSig . hfmap (translateH weakenSig)
-
-newtype HeftiaUnion (h :: Signature -> Type -> Type) u (es :: [Signature]) a = HeftiaUnion
-    {runHeftiaUnion :: h (u es) a}
-    deriving newtype (Functor, Applicative, Alternative, Monad, MonadPlus)
-    deriving stock (Foldable, Traversable)
-
-type HeftiaEffects h u es = SendVia (HeftiaUnion h u es)
-
-runHeftiaEffects :: HeftiaEffects h u es ~> h (u es)
-runHeftiaEffects = runHeftiaUnion . runSendVia
-
-heftiaEffects :: h (u es) ~> HeftiaEffects h u es
-heftiaEffects = SendVia . HeftiaUnion
-
-instance
-    (Heftia c h, Union u, Member u (LiftIns e) es, HFunctor (u es)) =>
-    SendIns e (HeftiaUnion h u es)
-    where
-    sendIns = HeftiaUnion . liftSig . inject . LiftIns
-
-instance
-    (Heftia c h, Union u, Member u e es, HFunctor (u es)) =>
-    SendSig e (HeftiaUnion h u es)
-    where
-    sendSig = HeftiaUnion . liftSig . hfmap runHeftiaUnion . inject
-
-interpret ::
-    (Heftia c h, Union u, HFunctor (u es), HFunctor (u (e : es)), HFunctor e) =>
-    (e (HeftiaEffects h u es) ~> HeftiaEffects h u es) ->
-    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u es
-interpret i a =
-    heftiaEffects $ ($ runHeftiaEffects a) $ interpretH \u ->
-        case decomp u of
-            Left e -> runHeftiaEffects $ i $ hfmap heftiaEffects e
-            Right e -> liftSig e
-
-reinterpret ::
-    (Heftia c h, Union u, HFunctor (u (e : es)), HFunctor e) =>
-    (e (HeftiaEffects h u (e ': es)) ~> HeftiaEffects h u (e ': es)) ->
-    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u (e ': es)
-reinterpret i a =
-    heftiaEffects $ ($ runHeftiaEffects a) $ reinterpretH \u ->
-        case decomp u of
-            Left e -> runHeftiaEffects $ i $ hfmap heftiaEffects e
-            Right e -> liftSig $ weakenR e
-
-translate ::
-    ( Heftia c h
-    , Union u
-    , HFunctor (u (e : es))
-    , HFunctor (u (e' : es))
-    , HFunctor e
-    , HFunctor e'
-    ) =>
-    (e (HeftiaEffects h u (e' ': es)) ~> e' (HeftiaEffects h u (e' ': es))) ->
-    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u (e' ': es)
-translate f a =
-    heftiaEffects $ ($ runHeftiaEffects a) $ translateH \u ->
-        case decomp u of
-            Left e -> weakenL $ hfmap runHeftiaEffects $ f $ hfmap heftiaEffects e
-            Right e -> weakenR e
-
-interpose ::
-    forall e h u es c.
-    (Heftia c h, Union u, Member u e es, HFunctor (u es)) =>
-    (e (HeftiaEffects h u es) ~> HeftiaEffects h u es) ->
-    HeftiaEffects h u es ~> HeftiaEffects h u es
-interpose f a =
-    heftiaEffects $ ($ runHeftiaEffects a) $ reinterpretH \u ->
-        let u' = hfmap (interpose f . heftiaEffects) u
-         in case project @_ @e u' of
-                Just e -> runHeftiaEffects $ f e
-                Nothing -> liftSig $ hfmap runHeftiaEffects u'
-
-intercept ::
-    forall e h u es c.
-    (Heftia c h, Union u, Member u e es, HFunctor (u es), HFunctor e) =>
-    (e (HeftiaEffects h u es) ~> e (HeftiaEffects h u es)) ->
-    HeftiaEffects h u es ~> HeftiaEffects h u es
-intercept f a =
-    heftiaEffects $ ($ runHeftiaEffects a) $ translateH \u ->
-        let u' = hfmap (intercept f . heftiaEffects) u
-         in case project @_ @e u' of
-                Just e -> inject $ hfmap runHeftiaEffects $ f e
-                Nothing -> hfmap runHeftiaEffects u'
-
-raiseUnder ::
-    forall e' e es h u c.
-    (Heftia c h, HFunctor (u (e : es)), HFunctor (u (e : e' : es)), Union u) =>
-    HeftiaEffects h u (e ': es) ~> HeftiaEffects h u (e ': e' ': es)
-raiseUnder a =
-    heftiaEffects
-        . ($ runHeftiaEffects a)
-        $ translateH \u -> case decomp u of
-            Left e -> weakenL e
-            Right e -> weakenR $ weakenR e
-
-heftiaToFreer ::
-    (Heftia c h, Freer c' f, c (f (i F.:+: h e))) =>
-    h (LiftIns (i F.:+: h e)) ~> f (i F.:+: h e)
-heftiaToFreer a = ($ a) $ interpretH \case
-    LiftIns (F.L1 i) -> liftIns $ F.L1 i
-    LiftIns (F.R1 h) -> liftIns $ F.R1 h
-
-{-
-interpretT ::
-    (Heftia c h, c (t (HeftiaEffects h u es)), HFunctor (u (LiftIns i : es)), Union u) =>
-    (i ~> t (HeftiaEffects h u es)) ->
-    HeftiaEffects h u (LiftIns i ': es) a ->
-    t (HeftiaEffects h u es) a
-interpretT i a =
-    ($ runHeftiaEffects a) $ interpretH \u ->
-        case decomp u of
-            Left (LiftIns e) -> i e
-            Right a -> undefined
-
-splitIns ::
-    ( Heftia c h
-    , HFunctor (u (LiftIns i : es))
-    , c (h (LiftIns (i F.:+: h (u es))))
-    , Union u
-    , HFunctor (u es)
-    ) =>
-    h (u (LiftIns i ': es)) ~> h (LiftIns (i F.:+: h (u es)))
-splitIns = interpretH \u -> case decomp u of
-    Left (LiftIns i) -> liftSig $ LiftIns $ F.L1 i
-    Right u -> liftSig $ LiftIns $ F.R1 $ liftSig u'
-      where
-        u' = hfmap undefined u
-
-heftiaToFreer ::
-    (Heftia c h, Freer c' f, c (f (i F.:+: h e))) =>
-    h (LiftIns (i F.:+: h e)) ~> f (i F.:+: h e)
-heftiaToFreer a = ($ a) $ interpretH \case
-    LiftIns (F.L1 i) -> liftIns $ F.L1 i
-    LiftIns (F.R1 h) -> liftIns $ F.R1 h
-
-interpretT ::
-    forall e t h u es a c.
-    ( Heftia c h
-    , HFunctor (u (e : es))
-    , HFunctor (u (e : LiftIns (t (HeftiaEffects h u es)) : es))
-    , Union u
-    , HFunctor e
-    , HFunctor (u (LiftIns (t (HeftiaEffects h u es)) : es))
-    , c (t (HeftiaEffects h u es))
-    , MonadTransControl t
-    , Monad (h (u es))
-    , Monad (t (HeftiaEffects h u es))
-    ) =>
-    (e (t (HeftiaEffects h u es)) ~> t (HeftiaEffects h u es)) ->
-    HeftiaEffects h u (e ': es) a ->
-    t (HeftiaEffects h u es) a
-interpretT i a = runBase a''
-  where
-    a'' = ($ a') $ interpret $ heftiaEffects . liftSig . weakenL . LiftIns . i . hfmap runBase
-    a' = raiseUnder @(LiftIns (t (HeftiaEffects h u es))) a
-
-runBase ::
-    ( Heftia c h
-    , HFunctor (u (LiftIns (t (HeftiaEffects h u es)) : es))
-    , c (t (HeftiaEffects h u es))
-    , Union u
-    , MonadTransControl t
-    , Monad (h (u es))
-    , Monad (t (HeftiaEffects h u es))
-    ) =>
-    HeftiaEffects h u (LiftIns (t (HeftiaEffects h u es)) : es)
-        ~> t (HeftiaEffects h u es)
-runBase =
-    runHeftiaEffects >>> interpretH \u -> case decomp u of
-        Left (LiftIns a) -> a
-        Right e -> controlT \run ->
-            let a' = undefined e
-             in heftiaEffects undefined
-
-runBaseK ::
-    ( Heftia c h
-    , HFunctor (u (LiftIns (ContT r (HeftiaEffects h u es)) : es))
-    , c (ContT r (HeftiaEffects h u es))
-    , Union u
-    , Monad (HeftiaEffects h u es)
-    , HFunctor (u es)
-    ) =>
-    HeftiaEffects h u (LiftIns (ContT r (HeftiaEffects h u es)) : es)
-        ~> ContT r (HeftiaEffects h u es)
-runBaseK =
-    runHeftiaEffects >>> interpretH \u -> case decomp u of
-        Left (LiftIns a) -> a
-        Right e -> ContT \k -> do
-            let e' = hfmap (\m -> runContT undefined undefined) e
-            x <- undefined
-            k x
--}
diff --git a/heftia/src/Control/Heftia/Final.hs b/heftia/src/Control/Heftia/Final.hs
index 4944311..be54a91 100644
--- a/heftia/src/Control/Heftia/Final.hs
+++ b/heftia/src/Control/Heftia/Final.hs
@@ -10,27 +10,30 @@ module Control.Heftia.Final where
 import Control.Applicative (Alternative, empty, (<|>))
 import Control.Effect.Class (Signature, type (~>))
 import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
-import Control.Heftia (Heftia, HeftiaEffects, interpretH, liftSig)
+import Control.Heftia (Heftia, interpretH, liftSig)
 import Control.Monad (MonadPlus (mplus, mzero))
-import Data.Hefty.Sum (SumUnion)
 
 newtype HeftiaFinal c (h :: Signature) a = HeftiaFinal
     {unHeftiaFinal :: forall f. c f => (h f ~> f) -> f a}
 
 runHeftiaFinal :: c f => (h f ~> f) -> HeftiaFinal c h a -> f a
 runHeftiaFinal i (HeftiaFinal f) = f i
+{-# INLINE runHeftiaFinal #-}
 
 liftSigFinal :: HFunctor h => h (HeftiaFinal c h) a -> HeftiaFinal c h a
 liftSigFinal e = HeftiaFinal \i -> i $ hfmap (runHeftiaFinal i) e
+{-# INLINE liftSigFinal #-}
 
 weakenHeftiaFinal :: (forall f. c' f => c f) => HeftiaFinal c h a -> HeftiaFinal c' h a
 weakenHeftiaFinal (HeftiaFinal f) = HeftiaFinal f
+{-# INLINE weakenHeftiaFinal #-}
 
 transformHeftiaFinal ::
     (forall f. h f ~> i f) ->
     HeftiaFinal c h a ->
     HeftiaFinal c i a
 transformHeftiaFinal phi (HeftiaFinal f) = HeftiaFinal \i -> f $ i . phi
+{-# INLINE transformHeftiaFinal #-}
 
 translateHeftiaFinal ::
     (c (HeftiaFinal c i), HFunctor i) =>
@@ -38,6 +41,7 @@ translateHeftiaFinal ::
     HeftiaFinal c h a ->
     HeftiaFinal c i a
 translateHeftiaFinal f = runHeftiaFinal $ liftSigFinal . f
+{-# INLINE translateHeftiaFinal #-}
 
 class Noop f
 instance Noop f
@@ -45,6 +49,7 @@ instance Noop f
 instance (forall f. c f => Functor f, c (HeftiaFinal c h)) => Functor (HeftiaFinal c h) where
     fmap f (HeftiaFinal g) =
         HeftiaFinal \(i :: h f ~> f) -> f <$> g i
+    {-# INLINE fmap #-}
 
 instance
     (forall f. c f => Applicative f, c (HeftiaFinal c h)) =>
@@ -55,6 +60,9 @@ instance
     HeftiaFinal f <*> HeftiaFinal g =
         HeftiaFinal \(i :: h f ~> f) -> f i <*> g i
 
+    {-# INLINE pure #-}
+    {-# INLINE (<*>) #-}
+
 instance
     (forall f. c f => Alternative f, c (HeftiaFinal c h)) =>
     Alternative (HeftiaFinal c h)
@@ -64,10 +72,14 @@ instance
     HeftiaFinal f <|> HeftiaFinal g =
         HeftiaFinal \(i :: h f ~> f) -> f i <|> g i
 
+    {-# INLINE empty #-}
+    {-# INLINE (<|>) #-}
+
 instance (forall m. c m => Monad m, c (HeftiaFinal c h)) => Monad (HeftiaFinal c h) where
     HeftiaFinal f >>= k =
         HeftiaFinal \(i :: h m ~> m) ->
             f i >>= runHeftiaFinal i . k
+    {-# INLINE (>>=) #-}
 
 instance
     (forall m. c m => MonadPlus m, Alternative (HeftiaFinal c h), Monad (HeftiaFinal c h)) =>
@@ -78,9 +90,11 @@ instance
     HeftiaFinal f `mplus` HeftiaFinal g =
         HeftiaFinal \(i :: h m ~> m) -> f i `mplus` g i
 
+    {-# INLINE mzero #-}
+    {-# INLINE mplus #-}
+
 instance (forall sig. c (HeftiaFinal c sig)) => Heftia c (HeftiaFinal c) where
     liftSig = liftSigFinal
     interpretH = runHeftiaFinal
-
-type Hef es = HeftiaEffects (HeftiaFinal Monad) SumUnion es
-type HefA es = HeftiaEffects (HeftiaFinal Applicative) SumUnion es
+    {-# INLINE liftSig #-}
+    {-# INLINE interpretH #-}
diff --git a/heftia/src/Control/Heftia/Final/Naked.hs b/heftia/src/Control/Heftia/Final/Naked.hs
index 267a10a..9e7246d 100644
--- a/heftia/src/Control/Heftia/Final/Naked.hs
+++ b/heftia/src/Control/Heftia/Final/Naked.hs
@@ -5,31 +5,34 @@
 module Control.Heftia.Final.Naked where
 
 import Control.Effect.Class (Signature, type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
+import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr))
 import Control.Freer (Freer, liftIns, retractF)
 import Control.Heftia.Final (HeftiaFinal (HeftiaFinal), Noop)
-import Data.Hefty.Sum (type (+) (L, R))
 
 newtype HeftiaFinalN (h :: Signature) a = HeftiaFinalN {unHeftiaFinalN :: forall f. (h f ~> f) -> f a}
 
 runHeftiaFinalN :: (h f ~> f) -> HeftiaFinalN h a -> f a
 runHeftiaFinalN i (HeftiaFinalN f) = f i
+{-# INLINE runHeftiaFinalN #-}
 
 liftSigFinalN :: HFunctor h => h (HeftiaFinalN h) a -> HeftiaFinalN h a
 liftSigFinalN e = HeftiaFinalN \i -> i $ hfmap (runHeftiaFinalN i) e
+{-# INLINE liftSigFinalN #-}
 
 wearHeftiaFinal :: HeftiaFinalN h a -> HeftiaFinal Noop h a
 wearHeftiaFinal (HeftiaFinalN f) = HeftiaFinal f
+{-# INLINE wearHeftiaFinal #-}
 
 nakeHeftiaFinal :: HeftiaFinal Noop h a -> HeftiaFinalN h a
 nakeHeftiaFinal (HeftiaFinal f) = HeftiaFinalN f
+{-# INLINE nakeHeftiaFinal #-}
 
-wearHeftiaFinalF :: Freer c f => HeftiaFinalN (f + h) a -> HeftiaFinal c h a
+wearHeftiaFinalF :: Freer c f => HeftiaFinalN (f :+: h) a -> HeftiaFinal c h a
 wearHeftiaFinalF (HeftiaFinalN f) =
     HeftiaFinal \i -> f \case
-        L m -> retractF m
-        R e -> i e
+        Inl m -> retractF m
+        Inr e -> i e
 
-nakeHeftiaFinalF :: (Freer c f, HFunctor h) => HeftiaFinal c h a -> HeftiaFinalN (f + h) a
+nakeHeftiaFinalF :: (Freer c f, HFunctor h) => HeftiaFinal c h a -> HeftiaFinalN (f :+: h) a
 nakeHeftiaFinalF (HeftiaFinal f) =
-    HeftiaFinalN \i -> i . L $ f $ liftIns . i . R . hfmap (i . L)
+    HeftiaFinalN \i -> i . Inl $ f $ liftIns . i . Inr . hfmap (i . Inl)
diff --git a/heftia/src/Control/Heftia/Trans.hs b/heftia/src/Control/Heftia/Trans.hs
index 46e6c26..e6e9166 100644
--- a/heftia/src/Control/Heftia/Trans.hs
+++ b/heftia/src/Control/Heftia/Trans.hs
@@ -10,31 +10,31 @@ import Control.Effect.Class (type (~>))
 import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
 import Control.Monad.Identity (IdentityT (IdentityT), runIdentityT)
 
-class (forall sig n. c n => c (h n sig)) => TransHeftia c h | h -> c where
+class (forall sig f. c f => c (h sig f)) => TransHeftia c h | h -> c where
     {-# MINIMAL liftSigT, translateT, liftLower, (hoistHeftia, interpretR | interpretHT) #-}
 
     -- | Lift a /signature/ into a Heftia monad transformer.
-    liftSigT :: HFunctor sig => sig (h m sig) a -> h m sig a
+    liftSigT :: HFunctor sig => sig (h sig f) a -> h sig f a
 
     -- | Translate /signature/s embedded in a Heftia monad transformer.
     translateT ::
-        (c m, HFunctor sig, HFunctor sig') =>
-        (sig (h m sig') ~> sig' (h m sig')) ->
-        h m sig a ->
-        h m sig' a
+        (c f, HFunctor sig, HFunctor sig') =>
+        (sig (h sig' f) ~> sig' (h sig' f)) ->
+        h sig f a ->
+        h sig' f a
 
-    liftLower :: forall sig m a. (c m, HFunctor sig) => m a -> h m sig a
+    liftLower :: forall sig f a. (c f, HFunctor sig) => f a -> h sig f a
 
     -- | Translate an underlying monad.
-    hoistHeftia :: (c m, c n, HFunctor sig) => (m ~> n) -> h m sig a -> h n sig a
+    hoistHeftia :: (c f, c g, HFunctor sig) => (f ~> g) -> h sig f a -> h sig g a
     hoistHeftia phi = interpretHT (liftLower . phi) liftSigT
     {-# INLINE hoistHeftia #-}
 
-    interpretR :: (c m, HFunctor sig) => (sig m ~> m) -> h m sig a -> m a
-    default interpretR :: (c m, c (IdentityT m), HFunctor sig) => (sig m ~> m) -> h m sig a -> m a
+    interpretR :: (c f, HFunctor sig) => (sig f ~> f) -> h sig f a -> f a
+    default interpretR :: (c f, c (IdentityT f), HFunctor sig) => (sig f ~> f) -> h sig f a -> f a
     interpretR f = runIdentityT . interpretHT IdentityT (IdentityT . f . hfmap runIdentityT)
     {-# INLINE interpretR #-}
 
-    interpretHT :: (c m, c n, HFunctor sig) => (m ~> n) -> (sig n ~> n) -> h m sig a -> n a
+    interpretHT :: (c f, c g, HFunctor sig) => (f ~> g) -> (sig g ~> g) -> h sig f a -> g a
     interpretHT phi i = interpretR i . hoistHeftia phi
     {-# INLINE interpretHT #-}
diff --git a/heftia/src/Control/Heftia/Trans/Final.hs b/heftia/src/Control/Heftia/Trans/Final.hs
index 3e1e08e..b76831b 100644
--- a/heftia/src/Control/Heftia/Trans/Final.hs
+++ b/heftia/src/Control/Heftia/Trans/Final.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -10,12 +11,19 @@ module Control.Heftia.Trans.Final where
 import Control.Applicative (Alternative)
 import Control.Effect.Class (LiftIns (LiftIns), type (~>))
 import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap, (:+:) (Inl, Inr))
-import Control.Heftia.Final (HeftiaFinal (HeftiaFinal), liftSigFinal, runHeftiaFinal, transformHeftiaFinal, weakenHeftiaFinal)
+import Control.Heftia.Final (
+    HeftiaFinal (HeftiaFinal),
+    liftSigFinal,
+    runHeftiaFinal,
+    transformHeftiaFinal,
+    weakenHeftiaFinal,
+ )
 import Control.Heftia.Trans (TransHeftia (..))
 import Control.Monad (MonadPlus)
-import Control.Monad.Trans.Heftia (MonadTransHeftia)
+import Control.Monad.Trans (MonadTrans)
+import Control.Monad.Trans.Heftia (MonadTransHeftia, ViaLiftLower (ViaLiftLower))
 
-newtype HeftiaFinalT c f h a = HeftiaFinalT
+newtype HeftiaFinalT c h f a = HeftiaFinalT
     {unHeftiaFinalT :: HeftiaFinal c (h :+: LiftIns f) a}
 
 data InterpreterT h f g = InterpreterT
@@ -23,27 +31,30 @@ data InterpreterT h f g = InterpreterT
     , interpreter :: h g ~> g
     }
 
-runHeftiaFinalT :: c g => InterpreterT h f g -> HeftiaFinalT c f h a -> g a
-runHeftiaFinalT InterpreterT{..} (HeftiaFinalT (HeftiaFinal f)) = f \case
+runHeftiaFinalT :: c g => InterpreterT h f g -> HeftiaFinalT c h f a -> g a
+runHeftiaFinalT InterpreterT{..} (HeftiaFinalT (HeftiaFinal h)) = h \case
     Inl e -> interpreter e
     Inr (LiftIns a) -> interpretLower a
 
-heftiaFinalT :: (forall g. c g => InterpreterT f h g -> g a) -> HeftiaFinalT c h f a
+heftiaFinalT :: (forall g. c g => InterpreterT h f g -> g a) -> HeftiaFinalT c h f a
 heftiaFinalT f = HeftiaFinalT $ HeftiaFinal \i -> f $ InterpreterT (i . Inr . LiftIns) (i . Inl)
 
-liftSigFinalT :: HFunctor h => h (HeftiaFinalT c f h) a -> HeftiaFinalT c f h a
+liftSigFinalT :: HFunctor h => h (HeftiaFinalT c h f) a -> HeftiaFinalT c h f a
 liftSigFinalT = HeftiaFinalT . liftSigFinal . Inl . hfmap unHeftiaFinalT
+{-# INLINE liftSigFinalT #-}
 
-liftLowerFinal :: HFunctor h => f a -> HeftiaFinalT c f h a
+liftLowerFinal :: HFunctor h => f a -> HeftiaFinalT c h f a
 liftLowerFinal = HeftiaFinalT . liftSigFinal . Inr . LiftIns
+{-# INLINE liftLowerFinal #-}
 
-weakenHeftiaFinalT :: (forall g. c' g => c g) => HeftiaFinalT c f h a -> HeftiaFinalT c' f h a
+weakenHeftiaFinalT :: (forall g. c' g => c g) => HeftiaFinalT c h f a -> HeftiaFinalT c' h f a
 weakenHeftiaFinalT = HeftiaFinalT . weakenHeftiaFinal . unHeftiaFinalT
+{-# INLINE weakenHeftiaFinalT #-}
 
 hoistHeftiaFinal ::
     (f ~> g) ->
-    HeftiaFinalT c f h a ->
-    HeftiaFinalT c g h a
+    HeftiaFinalT c h f a ->
+    HeftiaFinalT c h g a
 hoistHeftiaFinal phi (HeftiaFinalT a) =
     HeftiaFinalT $ ($ a) $ transformHeftiaFinal \case
         Inl e -> Inl e
@@ -51,38 +62,39 @@ hoistHeftiaFinal phi (HeftiaFinalT a) =
 
 deriving newtype instance
     (forall g. c g => Functor g, c (HeftiaFinal c (h :+: LiftIns f))) =>
-    Functor (HeftiaFinalT c f h)
+    Functor (HeftiaFinalT c h f)
 
 deriving newtype instance
     ( forall g. c g => Applicative g
     , c (HeftiaFinal c (h :+: LiftIns f))
-    , c (HeftiaFinalT c f h)
+    , c (HeftiaFinalT c h f)
     ) =>
-    Applicative (HeftiaFinalT c f h)
+    Applicative (HeftiaFinalT c h f)
 
 deriving newtype instance
     ( forall g. c g => Alternative g
     , c (HeftiaFinal c (h :+: LiftIns f))
-    , c (HeftiaFinalT c f h)
+    , c (HeftiaFinalT c h f)
     ) =>
-    Alternative (HeftiaFinalT c f h)
+    Alternative (HeftiaFinalT c h f)
 
 deriving newtype instance
     ( forall n. c n => Monad n
     , c (HeftiaFinal c (h :+: LiftIns m))
-    , c (HeftiaFinalT c m h)
+    , c (HeftiaFinalT c h m)
     ) =>
-    Monad (HeftiaFinalT c m h)
+    Monad (HeftiaFinalT c h m)
 
 deriving newtype instance
     ( forall n. c n => MonadPlus n
     , c (HeftiaFinal c (h :+: LiftIns m))
-    , c (HeftiaFinalT c m h)
+    , c (HeftiaFinalT c h m)
     ) =>
-    MonadPlus (HeftiaFinalT c m h)
+    MonadPlus (HeftiaFinalT c h m)
 
-instance (forall n sig. c n => c (HeftiaFinalT c n sig)) => TransHeftia c (HeftiaFinalT c) where
+instance (forall h f. c f => c (HeftiaFinalT c h f)) => TransHeftia c (HeftiaFinalT c) where
     liftSigT = liftSigFinalT
+    {-# INLINE liftSigT #-}
 
     translateT f (HeftiaFinalT a) =
         ($ a) $ runHeftiaFinal \case
@@ -90,47 +102,30 @@ instance (forall n sig. c n => c (HeftiaFinalT c n sig)) => TransHeftia c (Hefti
             Inr (LiftIns a') -> liftLower a'
 
     liftLower = liftLowerFinal
+    {-# INLINE liftLower #-}
 
     interpretR i = runHeftiaFinalT $ InterpreterT id i
+    {-# INLINE interpretR #-}
 
     hoistHeftia = hoistHeftiaFinal
+    {-# INLINE hoistHeftia #-}
+
+deriving via
+    ViaLiftLower (HeftiaFinalT Monad) h
+    instance
+        HFunctor h => MonadTrans (HeftiaFinalT Monad h)
 
 instance MonadTransHeftia (HeftiaFinalT Monad)
 
 joinHeftiaFinalT ::
-    (c (HeftiaFinalT c f h), HFunctor h) =>
-    HeftiaFinalT c (HeftiaFinalT c f h) h a ->
-    HeftiaFinalT c f h a
+    (c (HeftiaFinalT c h f), HFunctor h) =>
+    HeftiaFinalT c h (HeftiaFinalT c h f) a ->
+    HeftiaFinalT c h f a
 joinHeftiaFinalT (HeftiaFinalT (HeftiaFinal f)) =
     f \case
         Inl e -> liftSigFinalT e
         Inr (LiftIns e) -> e
 
-dupHeftiaFinalT :: HFunctor h => HeftiaFinalT c f h a -> HeftiaFinalT c (HeftiaFinalT c f h) h a
+dupHeftiaFinalT :: HFunctor h => HeftiaFinalT c h f a -> HeftiaFinalT c h (HeftiaFinalT c h f) a
 dupHeftiaFinalT = hoistHeftiaFinal liftLowerFinal
-
-{-
-interpretT ::
-    forall c h u e es t a.
-    ( Heftia c h
-    , Union u
-    , HFunctor (u es)
-    , HFunctor (u (e : es))
-    , HFunctor e
-    , c (HeftiaEffects h u (e : es))
-    , c (t (HeftiaEffects h u (e : es)))
-    , forall n sig. c n => c (HeftiaFinalT c n sig)
-    , MonadTrans t
-    , Monad (h (u (e ': es)))
-    ) =>
-    (e (t (HeftiaEffects h u es)) ~> t (HeftiaEffects h u es)) ->
-    HeftiaEffects h u (e ': es) a ->
-    t (HeftiaEffects h u es) a
-interpretT i a = undefined
-  where
-    a'' :: t (HeftiaEffects h u (e ': es)) a
-    a'' = undefined
-
-    a' :: HeftiaFinalT c (t (HeftiaEffects h u es)) (u (e ': es)) a
-    a' = liftLowerFinal undefined
--}
+{-# INLINE dupHeftiaFinalT #-}
diff --git a/heftia/src/Control/Heftia/Trans/Final/Naked.hs b/heftia/src/Control/Heftia/Trans/Final/Naked.hs
index 05f2c9d..e40cba6 100644
--- a/heftia/src/Control/Heftia/Trans/Final/Naked.hs
+++ b/heftia/src/Control/Heftia/Trans/Final/Naked.hs
@@ -19,13 +19,13 @@ import Control.Heftia.Trans.Final (
     unHeftiaFinalT,
  )
 
-newtype HeftiaFinalTN f (h :: Signature) a = HeftiaFinalTN
+newtype HeftiaFinalTN (h :: Signature) f a = HeftiaFinalTN
     {unHeftiaFinalTN :: forall g. InterpreterT h f g -> g a}
 
-runHeftiaFinalTN :: InterpreterT h f g -> HeftiaFinalTN f h a -> g a
+runHeftiaFinalTN :: InterpreterT h f g -> HeftiaFinalTN h f a -> g a
 runHeftiaFinalTN i (HeftiaFinalTN f) = f i
 
-liftSigFinalTN :: HFunctor h => h (HeftiaFinalTN f h) a -> HeftiaFinalTN f h a
+liftSigFinalTN :: HFunctor h => h (HeftiaFinalTN h f) a -> HeftiaFinalTN h f a
 liftSigFinalTN e = HeftiaFinalTN \i -> interpreter i $ hfmap (runHeftiaFinalTN i) e
 
 wearHeftiaFinalT :: HeftiaFinalTN h f a -> HeftiaFinalT Noop h f a
@@ -34,13 +34,13 @@ wearHeftiaFinalT (HeftiaFinalTN f) = heftiaFinalT f
 nakeHeftiaFinalT :: HeftiaFinalT Noop h f a -> HeftiaFinalTN h f a
 nakeHeftiaFinalT m = HeftiaFinalTN (`runHeftiaFinalT` m)
 
-wearHeftiaFinalTF :: Freer c g => HeftiaFinalTN f (g :+: h) a -> HeftiaFinalT c f h a
+wearHeftiaFinalTF :: Freer c fr => HeftiaFinalTN (fr :+: h) f a -> HeftiaFinalT c h f a
 wearHeftiaFinalTF (HeftiaFinalTN f) =
     heftiaFinalT \i -> f $ InterpreterT (interpretLower i) \case
         Inl m -> retractF m
         Inr e -> interpreter i e
 
-nakeHeftiaFinalTF :: (Freer c g, HFunctor h) => HeftiaFinalT c f h a -> HeftiaFinalTN f (g :+: h) a
+nakeHeftiaFinalTF :: (Freer c fr, HFunctor h) => HeftiaFinalT c h f a -> HeftiaFinalTN (fr :+: h) f a
 nakeHeftiaFinalTF m =
     HeftiaFinalTN \i ->
         interpreter i . Inl . (`runHeftiaFinalT` m) $
@@ -48,8 +48,8 @@ nakeHeftiaFinalTF m =
                 (liftIns . interpretLower i)
                 (liftIns . interpreter i . Inr . hfmap (interpreter i . Inl))
 
-cisHeftiaFinalN :: HeftiaFinalTN f h a -> HeftiaFinalN (h :+: LiftIns f) a
+cisHeftiaFinalN :: HeftiaFinalTN h f a -> HeftiaFinalN (h :+: LiftIns f) a
 cisHeftiaFinalN = nakeHeftiaFinal . unHeftiaFinalT . wearHeftiaFinalT
 
-transHeftiaFinalN :: HeftiaFinalN (h :+: LiftIns f) a -> HeftiaFinalTN f h a
+transHeftiaFinalN :: HeftiaFinalN (h :+: LiftIns f) a -> HeftiaFinalTN h f a
 transHeftiaFinalN = nakeHeftiaFinalT . HeftiaFinalT . wearHeftiaFinal
diff --git a/heftia/src/Control/Monad/Trans/Heftia.hs b/heftia/src/Control/Monad/Trans/Heftia.hs
index 552ffaf..128a3f2 100644
--- a/heftia/src/Control/Monad/Trans/Heftia.hs
+++ b/heftia/src/Control/Monad/Trans/Heftia.hs
@@ -1,3 +1,5 @@
+{-# 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/.
@@ -5,44 +7,46 @@
 module Control.Monad.Trans.Heftia where
 
 import Control.Effect.Class (Signature, type (~>))
-import Control.Effect.Class.Machinery.HFunctor (HFunctor)
+import Control.Effect.Class.Machinery.HFunctor (HFunctor, (:+:) (Inl, Inr))
 import Control.Heftia.Trans (TransHeftia, hoistHeftia, interpretHT, liftLower, liftSigT, translateT)
 import Control.Monad.Cont (ContT)
 import Control.Monad.Trans (MonadTrans, lift)
 import Data.Coerce (Coercible, coerce)
-import Data.Hefty.Sum (type (+) (L, R))
 import Data.Kind (Type)
 
-class TransHeftia Monad h => MonadTransHeftia h where
+class
+    (TransHeftia Monad h, forall sig. HFunctor sig => MonadTrans (h sig)) =>
+    MonadTransHeftia h
+    where
     interpretK ::
         (Monad m, HFunctor sig) =>
         (sig (ContT b m) ~> ContT b m) ->
-        h m sig a ->
+        h sig m a ->
         ContT b m a
     interpretK = interpretTT
     {-# INLINE interpretK #-}
 
     reinterpretK ::
         (Monad m, HFunctor sig) =>
-        (sig (ContT b (h m sig)) ~> ContT b (h m sig)) ->
-        h m sig a ->
-        ContT b (h m sig) a
+        (sig (ContT b (h sig m)) ~> ContT b (h sig m)) ->
+        h sig m a ->
+        ContT b (h sig m) a
     reinterpretK = reinterpretTT
     {-# INLINE reinterpretK #-}
 
     interpretTT ::
         (Monad m, MonadTrans t, Monad (t m), HFunctor sig) =>
         (sig (t m) ~> t m) ->
-        h m sig a ->
+        h sig m a ->
         t m a
     interpretTT = interpretHT lift
     {-# INLINE interpretTT #-}
 
     reinterpretTT ::
         forall m t n sig a.
-        (Monad m, MonadTrans t, Coercible n (h m sig), Monad (t n), Monad n, HFunctor sig) =>
+        (Monad m, MonadTrans t, Coercible n (h sig m), Monad (t n), Monad n, HFunctor sig) =>
         (sig (t n) ~> t n) ->
-        h m sig a ->
+        h sig m a ->
         t n a
     reinterpretTT f = interpretTT f . hoistHeftia (coerce . liftLower @Monad @h @sig)
     {-# INLINE reinterpretTT #-}
@@ -50,30 +54,31 @@ class TransHeftia Monad h => MonadTransHeftia h where
 mergeHeftia ::
     forall h m sig sig' a c.
     (HFunctor sig, HFunctor sig', TransHeftia c h, c m) =>
-    h (h m sig') sig a ->
-    h m (sig + sig') a
-mergeHeftia = interpretHT (translateT @c R) (liftSigT @c . L)
+    h sig (h sig' m) a ->
+    h (sig :+: sig') m a
+mergeHeftia = interpretHT (translateT @c Inr) (liftSigT @c . Inl)
 
 reinterpretTTViaFinal ::
     forall h m t n sig a.
     ( MonadTransHeftia h
     , Monad m
     , MonadTrans t
-    , Coercible n (h m sig)
+    , Coercible n (h sig m)
     , Monad (t n)
     , Monad n
     , HFunctor sig
     ) =>
     (sig (t n) ~> t n) ->
-    h m sig a ->
+    h sig m a ->
     t n a
 reinterpretTTViaFinal = interpretHT $ lift . coerce . liftLower @Monad @h @sig
 {-# INLINE reinterpretTTViaFinal #-}
 
-newtype HeftiaT (h :: (Type -> Type) -> Signature -> Type -> Type) sig m a = HeftiaT
-    {runHeftiaT :: h m sig a}
+newtype ViaLiftLower (h :: Signature -> (Type -> Type) -> Type -> Type) sig m a = ViaLiftLower
+    {runViaLiftLower :: h sig m a}
     deriving newtype (Functor, Applicative, Monad)
     deriving stock (Foldable, Traversable)
 
-instance (MonadTransHeftia h, HFunctor sig) => MonadTrans (HeftiaT h sig) where
-    lift = HeftiaT . liftLower
+instance (TransHeftia Monad h, HFunctor sig) => MonadTrans (ViaLiftLower h sig) where
+    lift = ViaLiftLower . liftLower
+    {-# INLINE lift #-}
diff --git a/heftia/src/Data/Hefty/Sum.hs b/heftia/src/Data/Hefty/Sum.hs
index 0c24253..0296dee 100644
--- a/heftia/src/Data/Hefty/Sum.hs
+++ b/heftia/src/Data/Hefty/Sum.hs
@@ -7,35 +7,23 @@
 module Data.Hefty.Sum where
 
 import Control.Effect.Class (LiftIns, Signature)
-import Control.Effect.Class.Machinery.HFunctor (HFunctor, hfmap)
+import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))
 import Data.Free.Sum (NopF)
 import Data.Hefty.Union (HFunctorUnion, Union, type (<:))
 import Data.Hefty.Union qualified as U
-import Data.Kind (Type)
-
-infixr 6 +
-
-data (h1 + h2) (f :: Type -> Type) a = L (h1 f a) | R (h2 f a)
-    deriving (Functor, Foldable, Traversable)
-
-instance (HFunctor h1, HFunctor h2) => HFunctor (h1 + h2) where
-    hfmap f = \case
-        L l -> L $ hfmap f l
-        R r -> R $ hfmap f r
 
 type Nop = LiftIns NopF
 
-swapSum :: (h1 + h2) f a -> (h2 + h1) f a
-swapSum = \case
-    L x -> R x
-    R x -> L x
+swapSum :: (h1 :+: h2) f a -> (h2 :+: h1) f a
+swapSum = caseH Inr Inl
 
 type family Sum hs where
     Sum '[] = Nop
-    Sum (h ': hs) = h + Sum hs
+    Sum (h ': hs) = h :+: Sum hs
 
 newtype SumUnion hs f a = SumUnion {unSumUnion :: Sum hs f a}
 
+{-
 deriving newtype instance Functor (SumUnion '[] f)
 deriving newtype instance (Functor (h f), Functor (Sum hs f)) => Functor (SumUnion (h ': hs) f)
 
@@ -44,6 +32,7 @@ deriving newtype instance (Foldable (h f), Foldable (Sum hs f)) => Foldable (Sum
 
 deriving stock instance Traversable (SumUnion '[] f)
 deriving stock instance (Traversable (h f), Traversable (Sum hs f)) => Traversable (SumUnion (h ': hs) f)
+-}
 
 deriving newtype instance HFunctor (Sum hs) => HFunctor (SumUnion hs)
 
@@ -55,12 +44,12 @@ instance Union SumUnion where
 
     comp =
         SumUnion . \case
-            Left x -> L x
-            Right (SumUnion x) -> R x
+            Left x -> Inl x
+            Right (SumUnion x) -> Inr x
 
     decomp (SumUnion sig) = case sig of
-        L x -> Left x
-        R x -> Right (SumUnion x)
+        Inl x -> Left x
+        Inr x -> Right (SumUnion x)
 
 instance HFunctor (SumUnion hs) => HFunctorUnion SumUnion hs
 
@@ -78,9 +67,9 @@ instance h < h where
     injH = id
     projH = Just
 
-instance h1 < h2 => h1 < (h2 + h3) where
-    injH = L . injH
+instance h1 < h2 => h1 < (h2 :+: h3) where
+    injH = Inl . injH
 
     projH = \case
-        L x -> projH x
-        R _ -> Nothing
+        Inl x -> projH x
+        Inr _ -> Nothing