{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE LambdaCase     #-}
{-# LANGUAGE RankNTypes     #-}
{-# LANGUAGE PolyKinds      #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators  #-}
module Polysemy.Extra where

import Control.Arrow
import Data.Map as Map
import Polysemy
import Polysemy.KVStore
import Polysemy.Input
import Polysemy.Output
import Polysemy.Membership

-- | Run a KVStore in terms of another KVStore by way of pure key and value
-- transformations.
runKVStoreAsKVStore :: forall k v k' v' r a.
                       (k  -> k')
                    -> (v  -> v')
                    -> (v' -> v )
                    -> Sem (KVStore k v ': r) a
                    -> Sem (KVStore k' v' ': r) a
runKVStoreAsKVStore :: (k -> k')
-> (v -> v')
-> (v' -> v)
-> Sem (KVStore k v : r) a
-> Sem (KVStore k' v' : r) a
runKVStoreAsKVStore k -> k'
f v -> v'
g v' -> v
h = (forall (rInitial :: EffectRow) x.
 KVStore k v (Sem rInitial) x -> Sem (KVStore k' v' : r) x)
-> Sem (KVStore k v : r) a -> Sem (KVStore k' v' : r) a
forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
FirstOrder e1 "reinterpret" =>
(forall (rInitial :: EffectRow) x.
 e1 (Sem rInitial) x -> Sem (e2 : r) x)
-> Sem (e1 : r) a -> Sem (e2 : r) a
reinterpret \case
  LookupKV k   -> (v' -> v) -> Maybe v' -> Maybe v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v' -> v
h (Maybe v' -> Maybe v)
-> Sem (KVStore k' v' : r) (Maybe v')
-> Sem (KVStore k' v' : r) (Maybe v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k' -> Sem (KVStore k' v' : r) (Maybe v')
forall k v (r :: EffectRow).
MemberWithError (KVStore k v) r =>
k -> Sem r (Maybe v)
lookupKV @k' @v' (k -> k'
f k
k)
  UpdateKV k x -> k' -> Maybe v' -> Sem (KVStore k' v' : r) ()
forall k v (r :: EffectRow).
MemberWithError (KVStore k v) r =>
k -> Maybe v -> Sem r ()
updateKV @k' @v' (k -> k'
f k
k) ((v -> v') -> Maybe v -> Maybe v'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> v'
g Maybe v
x)

-- | Run a KVStore in terms of another KVStore by way of transforming the
-- keys and values with Sem functions.
runKVStoreAsKVStoreSem :: forall k v k' v' r a.
                          Members '[KVStore k' v'] r
                       => (k  -> Sem r k')
                       -> (v  -> Sem r v')
                       -> (v' -> Sem r v )
                       -> Sem (KVStore k v ': r) a
                       -> Sem r a
runKVStoreAsKVStoreSem :: (k -> Sem r k')
-> (v -> Sem r v')
-> (v' -> Sem r v)
-> Sem (KVStore k v : r) a
-> Sem r a
runKVStoreAsKVStoreSem k -> Sem r k'
f v -> Sem r v'
g v' -> Sem r v
h = (forall x (rInitial :: EffectRow).
 KVStore k v (Sem rInitial) x -> Sem r x)
-> Sem (KVStore k v : r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
  LookupKV k   -> k -> Sem r k'
f k
k Sem r k' -> (k' -> Sem r (Maybe v')) -> Sem r (Maybe v')
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (r :: EffectRow).
MemberWithError (KVStore k' v') r =>
k' -> Sem r (Maybe v')
forall k v (r :: EffectRow).
MemberWithError (KVStore k v) r =>
k -> Sem r (Maybe v)
lookupKV @k' @v' Sem r (Maybe v')
-> (Maybe v' -> Sem r (Maybe v)) -> Sem r (Maybe v)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (v' -> Sem r v) -> Maybe v' -> Sem r (Maybe v)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM v' -> Sem r v
h
  UpdateKV k x -> do
    k'
z  <- k -> Sem r k'
f k
k
    Maybe v'
z' <- (v -> Sem r v') -> Maybe v -> Sem r (Maybe v')
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM v -> Sem r v'
g Maybe v
x
    k' -> Maybe v' -> Sem r ()
forall k v (r :: EffectRow).
MemberWithError (KVStore k v) r =>
k -> Maybe v -> Sem r ()
updateKV @k' @v' k'
z Maybe v'
z'

-- | Run an `Output (Map k v)` as a `KVStore` by writing the values to
-- the keys.
runOutputMapAsKVStore :: Members '[ KVStore k v ] r
                      => Sem (Output (Map k v) ': r) a
                      -> Sem r a
runOutputMapAsKVStore :: Sem (Output (Map k v) : r) a -> Sem r a
runOutputMapAsKVStore = (forall x (rInitial :: EffectRow).
 Output (Map k v) (Sem rInitial) x -> Sem r x)
-> Sem (Output (Map k v) : r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
  Output xs -> ((k, v) -> Sem r ()) -> [(k, v)] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((k -> v -> Sem r ()) -> (k, v) -> Sem r ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k -> v -> Sem r ()
forall k v (r :: EffectRow).
Member (KVStore k v) r =>
k -> v -> Sem r ()
writeKV) (Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
xs)

-- | Map an Output forwards
mapOutput :: Members '[ Output o' ] r
          => (o -> o')
          -> Sem (Output o ': r) a
          -> Sem r a
mapOutput :: (o -> o') -> Sem (Output o : r) a -> Sem r a
mapOutput o -> o'
f = (forall x (rInitial :: EffectRow).
 Output o (Sem rInitial) x -> Sem r x)
-> Sem (Output o : r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
  Output o -> o' -> Sem r ()
forall o (r :: EffectRow).
MemberWithError (Output o) r =>
o -> Sem r ()
output (o -> o'
f o
o)

-- | Map an Output forwards through a monadic function.
mapOutputSem :: Members '[ Output o' ] r
             => (o -> Sem r o')
             -> Sem (Output o ': r) a
             -> Sem r a
mapOutputSem :: (o -> Sem r o') -> Sem (Output o : r) a -> Sem r a
mapOutputSem o -> Sem r o'
f = (forall x (rInitial :: EffectRow).
 Output o (Sem rInitial) x -> Sem r x)
-> Sem (Output o : r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
  Output o -> o -> Sem r o'
f o
o Sem r o' -> (o' -> Sem r ()) -> Sem r ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= o' -> Sem r ()
forall o (r :: EffectRow).
MemberWithError (Output o) r =>
o -> Sem r ()
output

-- | Map an `Input` contravariantly.
contramapInput :: forall i i' r a.
            Members '[ Input i' ] r
         => (i' -> i)
         -> Sem (Input i ': r) a
         -> Sem r a
contramapInput :: (i' -> i) -> Sem (Input i : r) a -> Sem r a
contramapInput i' -> i
f = (forall x (rInitial :: EffectRow).
 Input i (Sem rInitial) x -> Sem r x)
-> Sem (Input i : r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
  Input i (Sem rInitial) x
Input -> i' -> i
f (i' -> i) -> Sem r i' -> Sem r i
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). MemberWithError (Input i') r => Sem r i'
forall i (r :: EffectRow). MemberWithError (Input i) r => Sem r i
input @i'

-- | Map an `Input` contravariantly through a monadic function.
contramapInputSem :: forall i i' r a.
                     Members '[ Input i' ] r
                  => (i' -> Sem r i)
                  -> Sem (Input i ': r) a
                  -> Sem r a
contramapInputSem :: (i' -> Sem r i) -> Sem (Input i : r) a -> Sem r a
contramapInputSem i' -> Sem r i
f = (forall x (rInitial :: EffectRow).
 Input i (Sem rInitial) x -> Sem r x)
-> Sem (Input i : r) a -> Sem r a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
FirstOrder e "interpret" =>
(forall x (rInitial :: EffectRow). e (Sem rInitial) x -> Sem r x)
-> Sem (e : r) a -> Sem r a
interpret \case
  Input i (Sem rInitial) x
Input -> i' -> Sem r i
f (i' -> Sem r i) -> Sem r i' -> Sem r i
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (r :: EffectRow). MemberWithError (Input i') r => Sem r i'
forall i (r :: EffectRow). MemberWithError (Input i) r => Sem r i
input @i'

-- | Reinterpret the second effect in the stack into a single effect.
reinterpretUnder :: forall e1 e2 e3 r a.
                    (forall m x. Sem (e2 ': m) x -> Sem (e3 ': m) x)
                 -> Sem (e1 ': e2 ': r) a
                 -> Sem (e1 ': e3 ': r) a
reinterpretUnder :: (forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : m) x)
-> Sem (e1 : e2 : r) a -> Sem (e1 : e3 : r) a
reinterpretUnder forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : m) x
f = forall (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e1 : r) a
forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under @e1 @e1 @e2
                 (Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e1 : r) a)
-> (Sem (e1 : e2 : e1 : r) a -> Sem (e1 : e3 : r) a)
-> Sem (e1 : e2 : r) a
-> Sem (e1 : e3 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e1 (e2 : e1 : r)
-> Sem (e1 : e2 : e1 : r) a -> Sem (e2 : e1 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e1 (ElemOf e1 (e1 : r) -> ElemOf e1 (e2 : e1 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e1 (e1 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)
                 (Sem (e1 : e2 : e1 : r) a -> Sem (e2 : e1 : r) a)
-> (Sem (e2 : e1 : r) a -> Sem (e1 : e3 : r) a)
-> Sem (e1 : e2 : e1 : r) a
-> Sem (e1 : e3 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (e2 : e1 : r) a -> Sem (e3 : e1 : r) a
forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : m) x
f
                 (Sem (e2 : e1 : r) a -> Sem (e3 : e1 : r) a)
-> (Sem (e3 : e1 : r) a -> Sem (e1 : e3 : r) a)
-> Sem (e2 : e1 : r) a
-> Sem (e1 : e3 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow) a.
Sem (e3 : e1 : r) a -> Sem (e3 : e1 : e3 : r) a
forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under @e3 @e3 @e1
                 (Sem (e3 : e1 : r) a -> Sem (e3 : e1 : e3 : r) a)
-> (Sem (e3 : e1 : e3 : r) a -> Sem (e1 : e3 : r) a)
-> Sem (e3 : e1 : r) a
-> Sem (e1 : e3 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e3 (e1 : e3 : r)
-> Sem (e3 : e1 : e3 : r) a -> Sem (e1 : e3 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e3 (ElemOf e3 (e3 : r) -> ElemOf e3 (e1 : e3 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e3 (e3 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)

-- | Reinterpret the third effect in the stack into a single effect.
reinterpretUnder2 :: forall e1 e2 e3 e4 r a.
                     (forall m x. Sem (e3 ': m) x -> Sem (e4 ': m) x)
                  -> Sem (e1 ': e2 ': e3 ': r) a
                  -> Sem (e1 ': e2 ': e4 ': r) a
reinterpretUnder2 :: (forall (m :: EffectRow) x. Sem (e3 : m) x -> Sem (e4 : m) x)
-> Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e4 : r) a
reinterpretUnder2 forall (m :: EffectRow) x. Sem (e3 : m) x -> Sem (e4 : m) x
f = forall (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e1 : r) a
forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e1 @e1 @e2 @e3
                  (Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e1 : r) a)
-> (Sem (e1 : e2 : e3 : e1 : r) a -> Sem (e1 : e2 : e4 : r) a)
-> Sem (e1 : e2 : e3 : r) a
-> Sem (e1 : e2 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e1 (e2 : e3 : e1 : r)
-> Sem (e1 : e2 : e3 : e1 : r) a -> Sem (e2 : e3 : e1 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e1 (ElemOf e1 (e3 : e1 : r) -> ElemOf e1 (e2 : e3 : e1 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There (ElemOf e1 (e3 : e1 : r) -> ElemOf e1 (e2 : e3 : e1 : r))
-> ElemOf e1 (e3 : e1 : r) -> ElemOf e1 (e2 : e3 : e1 : r)
forall a b. (a -> b) -> a -> b
$ ElemOf e1 (e1 : r) -> ElemOf e1 (e3 : e1 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e1 (e1 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)
                  (Sem (e1 : e2 : e3 : e1 : r) a -> Sem (e2 : e3 : e1 : r) a)
-> (Sem (e2 : e3 : e1 : r) a -> Sem (e1 : e2 : e4 : r) a)
-> Sem (e1 : e2 : e3 : e1 : r) a
-> Sem (e1 : e2 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow) a.
Sem (e2 : e3 : e1 : r) a -> Sem (e2 : e3 : e1 : e2 : r) a
forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e2 @e2 @e3 @e1
                  (Sem (e2 : e3 : e1 : r) a -> Sem (e2 : e3 : e1 : e2 : r) a)
-> (Sem (e2 : e3 : e1 : e2 : r) a -> Sem (e1 : e2 : e4 : r) a)
-> Sem (e2 : e3 : e1 : r) a
-> Sem (e1 : e2 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e2 (e3 : e1 : e2 : r)
-> Sem (e2 : e3 : e1 : e2 : r) a -> Sem (e3 : e1 : e2 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e2 (ElemOf e2 (e1 : e2 : r) -> ElemOf e2 (e3 : e1 : e2 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There (ElemOf e2 (e1 : e2 : r) -> ElemOf e2 (e3 : e1 : e2 : r))
-> ElemOf e2 (e1 : e2 : r) -> ElemOf e2 (e3 : e1 : e2 : r)
forall a b. (a -> b) -> a -> b
$ ElemOf e2 (e2 : r) -> ElemOf e2 (e1 : e2 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e2 (e2 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)
                  (Sem (e2 : e3 : e1 : e2 : r) a -> Sem (e3 : e1 : e2 : r) a)
-> (Sem (e3 : e1 : e2 : r) a -> Sem (e1 : e2 : e4 : r) a)
-> Sem (e2 : e3 : e1 : e2 : r) a
-> Sem (e1 : e2 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (e3 : e1 : e2 : r) a -> Sem (e4 : e1 : e2 : r) a
forall (m :: EffectRow) x. Sem (e3 : m) x -> Sem (e4 : m) x
f
                  (Sem (e3 : e1 : e2 : r) a -> Sem (e4 : e1 : e2 : r) a)
-> (Sem (e4 : e1 : e2 : r) a -> Sem (e1 : e2 : e4 : r) a)
-> Sem (e3 : e1 : e2 : r) a
-> Sem (e1 : e2 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow) a.
Sem (e4 : e1 : e2 : r) a -> Sem (e4 : e1 : e2 : e4 : r) a
forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e4 @e4 @e1 @e2
                  (Sem (e4 : e1 : e2 : r) a -> Sem (e4 : e1 : e2 : e4 : r) a)
-> (Sem (e4 : e1 : e2 : e4 : r) a -> Sem (e1 : e2 : e4 : r) a)
-> Sem (e4 : e1 : e2 : r) a
-> Sem (e1 : e2 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e4 (e1 : e2 : e4 : r)
-> Sem (e4 : e1 : e2 : e4 : r) a -> Sem (e1 : e2 : e4 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e4 (ElemOf e4 (e2 : e4 : r) -> ElemOf e4 (e1 : e2 : e4 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There (ElemOf e4 (e2 : e4 : r) -> ElemOf e4 (e1 : e2 : e4 : r))
-> ElemOf e4 (e2 : e4 : r) -> ElemOf e4 (e1 : e2 : e4 : r)
forall a b. (a -> b) -> a -> b
$ ElemOf e4 (e4 : r) -> ElemOf e4 (e2 : e4 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e4 (e4 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)

-- | Reinterpret the second effect in the stack in terms of two effects.
reinterpret2Under :: forall e1 e2 e3 e4 r a.
                     (forall m x. Sem (e2 ': m) x -> Sem (e3 ': e4 ': m) x)
                  -> Sem (e1 ': e2 ': r) a
                  -> Sem (e1 ': e3 ': e4 ': r) a
reinterpret2Under :: (forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : e4 : m) x)
-> Sem (e1 : e2 : r) a -> Sem (e1 : e3 : e4 : r) a
reinterpret2Under forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : e4 : m) x
f = forall (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e1 : r) a
forall (e3 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e3 : r) a
raise2Under @e1 @e1 @e2
                  (Sem (e1 : e2 : r) a -> Sem (e1 : e2 : e1 : r) a)
-> (Sem (e1 : e2 : e1 : r) a -> Sem (e1 : e3 : e4 : r) a)
-> Sem (e1 : e2 : r) a
-> Sem (e1 : e3 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e1 (e2 : e1 : r)
-> Sem (e1 : e2 : e1 : r) a -> Sem (e2 : e1 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e1 (ElemOf e1 (e1 : r) -> ElemOf e1 (e2 : e1 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e1 (e1 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)
                  (Sem (e1 : e2 : e1 : r) a -> Sem (e2 : e1 : r) a)
-> (Sem (e2 : e1 : r) a -> Sem (e1 : e3 : e4 : r) a)
-> Sem (e1 : e2 : e1 : r) a
-> Sem (e1 : e3 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Sem (e2 : e1 : r) a -> Sem (e3 : e4 : e1 : r) a
forall (m :: EffectRow) x. Sem (e2 : m) x -> Sem (e3 : e4 : m) x
f
                  (Sem (e2 : e1 : r) a -> Sem (e3 : e4 : e1 : r) a)
-> (Sem (e3 : e4 : e1 : r) a -> Sem (e1 : e3 : e4 : r) a)
-> Sem (e2 : e1 : r) a
-> Sem (e1 : e3 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow) a.
Sem (e3 : e4 : e1 : r) a -> Sem (e3 : e4 : e1 : e3 : r) a
forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e3 @e3 @e4 @e1
                  (Sem (e3 : e4 : e1 : r) a -> Sem (e3 : e4 : e1 : e3 : r) a)
-> (Sem (e3 : e4 : e1 : e3 : r) a -> Sem (e1 : e3 : e4 : r) a)
-> Sem (e3 : e4 : e1 : r) a
-> Sem (e1 : e3 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e3 (e4 : e1 : e3 : r)
-> Sem (e3 : e4 : e1 : e3 : r) a -> Sem (e4 : e1 : e3 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e3 (ElemOf e3 (e1 : e3 : r) -> ElemOf e3 (e4 : e1 : e3 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There (ElemOf e3 (e1 : e3 : r) -> ElemOf e3 (e4 : e1 : e3 : r))
-> ElemOf e3 (e1 : e3 : r) -> ElemOf e3 (e4 : e1 : e3 : r)
forall a b. (a -> b) -> a -> b
$ ElemOf e3 (e3 : r) -> ElemOf e3 (e1 : e3 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e3 (e3 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)
                  (Sem (e3 : e4 : e1 : e3 : r) a -> Sem (e4 : e1 : e3 : r) a)
-> (Sem (e4 : e1 : e3 : r) a -> Sem (e1 : e3 : e4 : r) a)
-> Sem (e3 : e4 : e1 : e3 : r) a
-> Sem (e1 : e3 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (r :: EffectRow) a.
Sem (e4 : e1 : e3 : r) a -> Sem (e4 : e1 : e3 : e4 : r) a
forall (e4 :: (* -> *) -> * -> *) (e1 :: (* -> *) -> * -> *)
       (e2 :: (* -> *) -> * -> *) (e3 :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Sem (e1 : e2 : e3 : r) a -> Sem (e1 : e2 : e3 : e4 : r) a
raise3Under @e4 @e4 @e1 @e3
                  (Sem (e4 : e1 : e3 : r) a -> Sem (e4 : e1 : e3 : e4 : r) a)
-> (Sem (e4 : e1 : e3 : e4 : r) a -> Sem (e1 : e3 : e4 : r) a)
-> Sem (e4 : e1 : e3 : r) a
-> Sem (e1 : e3 : e4 : r) a
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ElemOf e4 (e1 : e3 : e4 : r)
-> Sem (e4 : e1 : e3 : e4 : r) a -> Sem (e1 : e3 : e4 : r) a
forall (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
ElemOf e r -> Sem (e : r) a -> Sem r a
subsumeUsing @e4 (ElemOf e4 (e3 : e4 : r) -> ElemOf e4 (e1 : e3 : e4 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There (ElemOf e4 (e3 : e4 : r) -> ElemOf e4 (e1 : e3 : e4 : r))
-> ElemOf e4 (e3 : e4 : r) -> ElemOf e4 (e1 : e3 : e4 : r)
forall a b. (a -> b) -> a -> b
$ ElemOf e4 (e4 : r) -> ElemOf e4 (e3 : e4 : r)
forall a (e :: a) (r1 :: [a]) (e' :: a).
ElemOf e r1 -> ElemOf e (e' : r1)
There ElemOf e4 (e4 : r)
forall a (e :: a) (r1 :: [a]). ElemOf e (e : r1)
Here)