[fix] Change the order of type arguments for heftia transformers.

[fix] Unify signature sum types with those of the datacomp package.
2024-11-27 07:37:56 +03:00 · 2023-09-04 11:44:27 +09:00 · 2023-09-04 11:44:27 +09:00 · 9e22c667e4
commit 9e22c667e4
parent e7988fb3a4
11 changed files with 278 additions and 368 deletions
--- 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:
--- 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)
--- a/heftia/src/Control/Effect/Heftia.hs
+++ 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
--- 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
-}
--- 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 #-}
--- 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)
--- 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 #-}
--- 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 #-}
--- 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
--- 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 #-}
--- 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