{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- SPDX-License-Identifier: MPL-2.0

{- |
Copyright   :  (c) 2024-2025 Sayo contributors
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
-}
module Data.Effect.OpenUnion where

import Control.Arrow ((&&&))
import Data.Coerce (coerce)
import Data.Data (Proxy (Proxy), (:~:) (Refl))
import Data.Effect (Effect, EffectForm (Exponential, Polynomial), EffectOrder (FirstOrder, HigherOrder), FirstOrder, FormCase, FormOf, LabelOf, OrderCase, OrderOf, PolyHFunctor)
import Data.Effect.HFunctor (HFunctor, hfmap)
import Data.Effect.Tag (type (#))
import Data.Kind (Constraint, Type)
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), KnownNat, Natural, Symbol, TypeError, natVal, type (+), type (-))
import Unsafe.Coerce (unsafeCoerce)

data Union (es :: [Effect]) (f :: Type -> Type) (a :: Type) where
    UnsafeUnion
        :: {-# UNPACK #-} !Int
        -- ^ A natural number tag to identify the element of the union.
        -> e g a
        -> {-# UNPACK #-} !EffectOrder
        -> (forall x. g x -> f x)
        -> Union es f a

instance HFunctor (Union es) where
    hfmap :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Union es f a -> Union es g a
hfmap forall x. f x -> g x
phi u :: Union es f a
u@(UnsafeUnion Int
n e g a
e EffectOrder
order forall x. g x -> f x
koi) =
        case EffectOrder
order of
            EffectOrder
FirstOrder -> Union es f a -> Union es g a
forall a b. a -> b
unsafeCoerce Union es f a
u
            EffectOrder
HigherOrder -> Int
-> e g a -> EffectOrder -> (forall x. g x -> g x) -> Union es g a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion Int
n e g a
e EffectOrder
HigherOrder (f x -> g x
forall x. f x -> g x
phi (f x -> g x) -> (g x -> f x) -> g x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> f x
forall x. g x -> f x
koi)
    {-# INLINE hfmap #-}

hfmapUnion :: (forall x. f x -> g x) -> Union es f a -> Union es g a
hfmapUnion :: forall (f :: * -> *) (g :: * -> *) (es :: [Effect]) a.
(forall x. f x -> g x) -> Union es f a -> Union es g a
hfmapUnion forall x. f x -> g x
phi u :: Union es f a
u@(UnsafeUnion Int
n e g a
e EffectOrder
order forall x. g x -> f x
koi) =
    case EffectOrder
order of
        EffectOrder
FirstOrder -> Union es f a -> Union es g a
forall a b. a -> b
unsafeCoerce Union es f a
u
        EffectOrder
HigherOrder -> Int
-> e g a -> EffectOrder -> (forall x. g x -> g x) -> Union es g a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion Int
n e g a
e EffectOrder
HigherOrder (f x -> g x
forall x. f x -> g x
phi (f x -> g x) -> (g x -> f x) -> g x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> f x
forall x. g x -> f x
koi)
{-# INLINE hfmapUnion #-}

-- | The list @es@ consists only of first-order effects.
class FOEs (es :: [Effect])

instance FOEs '[]
instance (FirstOrder e, FOEs es) => FOEs (e ': es)

-- | The list @es@ consists only of polynomial effects.
class PolyHFunctors (es :: [Effect])

instance PolyHFunctors '[]
instance (PolyHFunctor e, PolyHFunctors es) => PolyHFunctors (e ': es)

coerceFOEs :: (FOEs es) => Union es f a -> Union es g a
coerceFOEs :: forall (es :: [Effect]) (f :: * -> *) a (g :: * -> *).
FOEs es =>
Union es f a -> Union es g a
coerceFOEs = Union es f a -> Union es g a
forall a b. a -> b
unsafeCoerce
{-# INLINE coerceFOEs #-}

type instance OrderOf (Union es) = 'HigherOrder

newtype Membership (e :: Effect) (es :: [Effect]) = UnsafeMembership {forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership :: Int}
    deriving stock (Membership e es -> Membership e es -> Bool
(Membership e es -> Membership e es -> Bool)
-> (Membership e es -> Membership e es -> Bool)
-> Eq (Membership e es)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (e :: Effect) (es :: [Effect]).
Membership e es -> Membership e es -> Bool
$c== :: forall (e :: Effect) (es :: [Effect]).
Membership e es -> Membership e es -> Bool
== :: Membership e es -> Membership e es -> Bool
$c/= :: forall (e :: Effect) (es :: [Effect]).
Membership e es -> Membership e es -> Bool
/= :: Membership e es -> Membership e es -> Bool
Eq, Int -> Membership e es -> ShowS
[Membership e es] -> ShowS
Membership e es -> String
(Int -> Membership e es -> ShowS)
-> (Membership e es -> String)
-> ([Membership e es] -> ShowS)
-> Show (Membership e es)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (e :: Effect) (es :: [Effect]).
Int -> Membership e es -> ShowS
forall (e :: Effect) (es :: [Effect]). [Membership e es] -> ShowS
forall (e :: Effect) (es :: [Effect]). Membership e es -> String
$cshowsPrec :: forall (e :: Effect) (es :: [Effect]).
Int -> Membership e es -> ShowS
showsPrec :: Int -> Membership e es -> ShowS
$cshow :: forall (e :: Effect) (es :: [Effect]). Membership e es -> String
show :: Membership e es -> String
$cshowList :: forall (e :: Effect) (es :: [Effect]). [Membership e es] -> ShowS
showList :: [Membership e es] -> ShowS
Show)

pattern Here :: Membership e (e ': es)
pattern $mHere :: forall {r} {e :: Effect} {es :: [Effect]}.
Membership e (e : es) -> ((# #) -> r) -> ((# #) -> r) -> r
$bHere :: forall (e :: Effect) (es :: [Effect]). Membership e (e : es)
Here = UnsafeMembership 0
{-# INLINE Here #-}

pattern There :: Membership e es -> Membership e (e ': es)
pattern $mThere :: forall {r} {e :: Effect} {es :: [Effect]}.
Membership e (e : es)
-> (Membership e es -> r) -> ((# #) -> r) -> r
$bThere :: forall (e :: Effect) (es :: [Effect]).
Membership e es -> Membership e (e : es)
There i <- ((UnsafeMembership . (`subtract` 1) &&& (/= 0)) . unMembership -> (i, True))
    where
        There (UnsafeMembership Int
n) = Int -> Membership e (e : es)
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# INLINE There #-}

infixr 5 !:>
(!:>) :: forall e e' es r. ((e :~: e') -> r) -> (Membership e es -> r) -> Membership e (e' ': es) -> r
((e :~: e') -> r
f !:> :: forall (e :: Effect) (e' :: Effect) (es :: [Effect]) r.
((e :~: e') -> r)
-> (Membership e es -> r) -> Membership e (e' : es) -> r
!:> Membership e es -> r
g) (UnsafeMembership Int
n)
    | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = (e :~: e') -> r
f ((e :~: e') -> r) -> (e :~: e') -> r
forall a b. (a -> b) -> a -> b
$ (Any :~: Any) -> e :~: e'
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl
    | Bool
otherwise = Membership e es -> r
g (Membership e es -> r) -> Membership e es -> r
forall a b. (a -> b) -> a -> b
$ Int -> Membership e es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e es) -> Int -> Membership e es
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
{-# INLINE (!:>) #-}

weakenFor :: Membership e es -> Membership e (e' ': es)
weakenFor :: forall (e :: Effect) (es :: [Effect]) (e' :: Effect).
Membership e es -> Membership e (e' : es)
weakenFor (UnsafeMembership Int
n) = Int -> Membership e (e' : es)
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e (e' : es)) -> Int -> Membership e (e' : es)
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
{-# INLINE weakenFor #-}

mapUnion
    :: forall es es' f a
     . (forall e. Membership e es -> Membership e es')
    -> Union es f a
    -> Union es' f a
mapUnion :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion forall (e :: Effect). Membership e es -> Membership e es'
f (UnsafeUnion Int
n e g a
e EffectOrder
order forall x. g x -> f x
koi) =
    Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es' f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion (Membership Any es' -> Int
forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership (Membership Any es' -> Int) -> Membership Any es' -> Int
forall a b. (a -> b) -> a -> b
$ Membership Any es -> Membership Any es'
forall (e :: Effect). Membership e es -> Membership e es'
f (Membership Any es -> Membership Any es')
-> Membership Any es -> Membership Any es'
forall a b. (a -> b) -> a -> b
$ Int -> Membership Any es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership Int
n) e g a
e EffectOrder
order g x -> f x
forall x. g x -> f x
koi
{-# INLINE mapUnion #-}

membershipAt :: forall i es. (KnownNat i) => Membership (At i es) es
membershipAt :: forall (i :: Nat) (es :: [Effect]).
KnownNat i =>
Membership (At i es) es
membershipAt = Int -> Membership (At i es) es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership (At i es) es) -> Int -> Membership (At i es) es
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Int
intVal @i
{-# INLINE membershipAt #-}

compareMembership :: Membership e es -> Membership e' es -> Maybe (e :~: e')
compareMembership :: forall (e :: Effect) (es :: [Effect]) (e' :: Effect).
Membership e es -> Membership e' es -> Maybe (e :~: e')
compareMembership (UnsafeMembership Int
m) (UnsafeMembership Int
n)
    | Int
m Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n = (e :~: e') -> Maybe (e :~: e')
forall a. a -> Maybe a
Just ((e :~: e') -> Maybe (e :~: e')) -> (e :~: e') -> Maybe (e :~: e')
forall a b. (a -> b) -> a -> b
$ (Any :~: Any) -> e :~: e'
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl
    | Bool
otherwise = Maybe (e :~: e')
forall a. Maybe a
Nothing

type family At i es where
    At 0 (e ': es) = e
    At n (e ': es) = At (n - 1) es
    At _ '[] = TypeError ('Text "Effect index out of range")

intVal :: forall n. (KnownNat n) => Int
intVal :: forall (n :: Nat). KnownNat n => Int
intVal = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy
{-# INLINE intVal #-}

data LabelResolver
data KeyResolver
data IdentityResolver

data KeyDiscriminator key
data NoKeyDiscriminator

data IdentityDiscriminator (e :: Effect)

type family Discriminator resolver (e :: Effect)
type instance Discriminator LabelResolver e = LabelOf e
type instance Discriminator KeyResolver e = KeyOf e
type instance Discriminator IdentityResolver e = IdentityDiscriminator e

type family KeyOf e where
    KeyOf (e # key) = KeyDiscriminator key
    KeyOf e = NoKeyDiscriminator

type family ResolverName resolver :: Symbol
type instance ResolverName LabelResolver = "label"
type instance ResolverName KeyResolver = "key"
type instance ResolverName IdentityResolver = "identity"

infix 4 :>
infix 4 `In`

type e :> es = MemberBy LabelResolver (Discriminator LabelResolver e) e es
type Has key e es = MemberBy KeyResolver (KeyDiscriminator key) (e # key) es
type e `In` es = MemberBy IdentityResolver (IdentityDiscriminator e) e es
type KnownIndex i es = (KnownNat i, KnownOrder (At i es))

type FindByLabel label e es = MemberBy LabelResolver label e es

type MemberBy resolver dscr e es =
    ( FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es
    , ErrorIfNotFound resolver dscr (Discriminator resolver (HeadOf es)) e es es
    , KnownOrder e
    )

class
    (dscr ~ Discriminator resolver e, dscr' ~ Discriminator resolver (HeadOf r)) =>
    FindBy resolver dscr dscr' e r
        | resolver dscr dscr' r -> e
    where
    findBy :: Membership e r

instance
    (dscr ~ Discriminator resolver e, dscr ~ Discriminator resolver e', e ~ e')
    => FindBy resolver dscr dscr e (e' ': r)
    where
    findBy :: Membership e (e' : r)
findBy = Membership e (e : r)
Membership e (e' : r)
forall (e :: Effect) (es :: [Effect]). Membership e (e : es)
Here
    {-# INLINE findBy #-}

instance
    {-# OVERLAPPABLE #-}
    ( dscr ~ Discriminator resolver e
    , dscr' ~ Discriminator resolver e'
    , FindBy resolver dscr (Discriminator resolver (HeadOf r)) e r
    )
    => FindBy resolver dscr dscr' e (e' ': r)
    where
    findBy :: Membership e (e' : r)
findBy = Membership e r -> Membership e (e' : r)
forall (e :: Effect) (es :: [Effect]) (e' :: Effect).
Membership e es -> Membership e (e' : es)
weakenFor (Membership e r -> Membership e (e' : r))
-> Membership e r -> Membership e (e' : r)
forall a b. (a -> b) -> a -> b
$ forall resolver dscr dscr' (e :: Effect) (r :: [Effect]).
FindBy resolver dscr dscr' e r =>
Membership e r
findBy @resolver @dscr @(Discriminator resolver (HeadOf r)) @e @r
    {-# INLINE findBy #-}

membership
    :: forall resolver dscr e es
     . (FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es)
    => Membership e es
membership :: forall resolver dscr (e :: Effect) (es :: [Effect]).
FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es =>
Membership e es
membership = forall resolver dscr dscr' (e :: Effect) (r :: [Effect]).
FindBy resolver dscr dscr' e r =>
Membership e r
findBy @resolver @dscr @(Discriminator resolver (HeadOf es)) @e @es
{-# INLINE membership #-}

labelMembership
    :: forall e es
     . (FindBy LabelResolver (LabelOf e) (LabelOf (HeadOf es)) e es)
    => Membership e es
labelMembership :: forall (e :: Effect) (es :: [Effect]).
FindBy LabelResolver (LabelOf e) (LabelOf (HeadOf es)) e es =>
Membership e es
labelMembership = forall resolver dscr (e :: Effect) (es :: [Effect]).
FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es =>
Membership e es
membership @LabelResolver
{-# INLINE labelMembership #-}

keyMembership
    :: forall key e es
     . (FindBy KeyResolver (KeyDiscriminator key) (KeyOf (HeadOf es)) (e # key) es)
    => Membership (e # key) es
keyMembership :: forall {k} (key :: k) (e :: Effect) (es :: [Effect]).
FindBy
  KeyResolver
  (KeyDiscriminator key)
  (KeyOf (HeadOf es))
  (e # key)
  es =>
Membership (e # key) es
keyMembership = forall resolver dscr (e :: Effect) (es :: [Effect]).
FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es =>
Membership e es
membership @KeyResolver
{-# INLINE keyMembership #-}

identityMembership
    :: forall e es
     . (FindBy IdentityResolver (IdentityDiscriminator e) (IdentityDiscriminator (HeadOf es)) e es)
    => Membership e es
identityMembership :: forall (e :: Effect) (es :: [Effect]).
FindBy
  IdentityResolver
  (IdentityDiscriminator e)
  (IdentityDiscriminator (HeadOf es))
  e
  es =>
Membership e es
identityMembership = forall resolver dscr (e :: Effect) (es :: [Effect]).
FindBy resolver dscr (Discriminator resolver (HeadOf es)) e es =>
Membership e es
membership @IdentityResolver
{-# INLINE identityMembership #-}
class
    (dscr ~ Discriminator resolver e, dscr' ~ Discriminator resolver (HeadOf r)) =>
    ErrorIfNotFound resolver dscr dscr' (e :: Effect) (r :: [Effect]) (w :: [Effect])

instance
    ( TypeError
        ( 'Text "The effect ‘"
            ':<>: 'ShowType e
            ':<>: 'Text "’ does not exist within the effect list"
            ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"
            ':$$: 'Text "Resolver: " ':<>: 'Text (ResolverName resolver)
            ':$$: 'Text "Discriminator: " ':<>: 'ShowType dscr
        )
    , dscr ~ Discriminator resolver e
    , dscr' ~ Discriminator resolver (HeadOf '[])
    )
    => ErrorIfNotFound resolver dscr dscr' e '[] w

instance
    (dscr ~ Discriminator resolver e, dscr ~ Discriminator resolver e', e ~ e')
    => ErrorIfNotFound resolver dscr dscr e (e' ': r) w

instance
    {-# OVERLAPPABLE #-}
    ( dscr ~ Discriminator resolver e
    , dscr' ~ Discriminator resolver e'
    , ErrorIfNotFound resolver dscr (Discriminator resolver (HeadOf r)) e r w
    )
    => ErrorIfNotFound resolver dscr dscr' e (e' ': r) w

instance
    {-# INCOHERENT #-}
    ( dscr ~ Discriminator resolver e
    , dscr' ~ Discriminator resolver (HeadOf r)
    )
    => ErrorIfNotFound resolver dscr dscr' e r w

type family HeadOf es where
    HeadOf (e ': es) = e

type KnownOrder e = Elem e (OrderOf e)

class (order ~ OrderOf e) => Elem e order where
    inject :: Membership e es -> e f a -> Union es f a
    project :: Membership e es -> Union es f a -> Maybe (e f a)
    (!:) :: (e f a -> r) -> (Union es f a -> r) -> Union (e ': es) f a -> r
    extract :: Union '[e] f a -> e f a

    infixr 5 !:

decomp :: (KnownOrder e, HFunctor e) => Union (e ': es) f a -> Either (e f a) (Union es f a)
decomp :: forall (e :: Effect) (es :: [Effect]) (f :: * -> *) a.
(KnownOrder e, HFunctor e) =>
Union (e : es) f a -> Either (e f a) (Union es f a)
decomp = e f a -> Either (e f a) (Union es f a)
forall a b. a -> Either a b
Left (e f a -> Either (e f a) (Union es f a))
-> (Union es f a -> Either (e f a) (Union es f a))
-> Union (e : es) f a
-> Either (e f a) (Union es f a)
forall (f :: * -> *) a r (es :: [Effect]).
(e f a -> r) -> (Union es f a -> r) -> Union (e : es) f a -> r
forall (e :: Effect) (order :: EffectOrder) (f :: * -> *) a r
       (es :: [Effect]).
Elem e order =>
(e f a -> r) -> (Union es f a -> r) -> Union (e : es) f a -> r
!: Union es f a -> Either (e f a) (Union es f a)
forall a b. b -> Either a b
Right
{-# INLINE decomp #-}

instance (FirstOrder e) => Elem e 'FirstOrder where
    inject :: forall es f a. Membership e es -> e f a -> Union es f a
    inject :: forall (es :: [Effect]) (f :: * -> *) a.
Membership e es -> e f a -> Union es f a
inject Membership e es
i = Membership e es
-> Ordership 'FirstOrder e f f -> e f a -> Union es f a
forall (e :: Effect) (es :: [Effect]) (o :: EffectOrder)
       (f :: * -> *) (g :: * -> *) a.
Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion Membership e es
i Ordership 'FirstOrder e f f
forall (e :: Effect) (f :: * -> *) (g :: * -> *).
FirstOrder e =>
Ordership 'FirstOrder e f g
firstOrdership

    project
        :: forall es f a
         . Membership e es
        -> Union es f a
        -> Maybe (e f a)
    project :: forall (es :: [Effect]) (f :: * -> *) a.
Membership e es -> Union es f a -> Maybe (e f a)
project Membership e es
i (UnsafeUnion Int
n e g a
e EffectOrder
_ forall x. g x -> f x
_) =
        if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Membership e es -> Int
forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership Membership e es
i
            then e f a -> Maybe (e f a)
forall a. a -> Maybe a
Just (e f a -> Maybe (e f a)) -> e f a -> Maybe (e f a)
forall a b. (a -> b) -> a -> b
$ e g a -> e f a
forall a b. a -> b
unsafeCoerce e g a
e
            else Maybe (e f a)
forall a. Maybe a
Nothing

    (e f a -> r
f !: :: forall (f :: * -> *) a r (es :: [Effect]).
(e f a -> r) -> (Union es f a -> r) -> Union (e : es) f a -> r
!: Union es f a -> r
g) (UnsafeUnion Int
n e g a
e EffectOrder
koi forall x. g x -> f x
order) =
        if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
            then e f a -> r
f (e f a -> r) -> e f a -> r
forall a b. (a -> b) -> a -> b
$ e g a -> e f a
forall a b. a -> b
unsafeCoerce e g a
e
            else Union es f a -> r
g (Union es f a -> r) -> Union es f a -> r
forall a b. (a -> b) -> a -> b
$ Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) e g a
e EffectOrder
koi g x -> f x
forall x. g x -> f x
order

    extract :: forall (f :: * -> *) a. Union '[e] f a -> e f a
extract (UnsafeUnion Int
_ e g a
e EffectOrder
_ forall x. g x -> f x
_) = e g a -> e f a
forall a b. a -> b
unsafeCoerce e g a
e

    {-# INLINE inject #-}
    {-# INLINE project #-}
    {-# INLINE (!:) #-}
    {-# INLINE extract #-}

instance (OrderOf e ~ 'HigherOrder, HFunctor e) => Elem e 'HigherOrder where
    inject :: forall es f a. Membership e es -> e f a -> Union es f a
    inject :: forall (es :: [Effect]) (f :: * -> *) a.
Membership e es -> e f a -> Union es f a
inject Membership e es
i = Membership e es
-> Ordership 'HigherOrder e f f -> e f a -> Union es f a
forall (e :: Effect) (es :: [Effect]) (o :: EffectOrder)
       (f :: * -> *) (g :: * -> *) a.
Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion Membership e es
i ((forall x. f x -> f x) -> Ordership 'HigherOrder e f f
forall (e :: Effect) (g :: * -> *) (f :: * -> *).
(OrderOf e ~ 'HigherOrder) =>
(forall x. g x -> f x) -> Ordership 'HigherOrder e f g
higherOrdership f x -> f x
forall a. a -> a
forall x. f x -> f x
id)

    project :: forall es f a. Membership e es -> Union es f a -> Maybe (e f a)
    project :: forall (es :: [Effect]) (f :: * -> *) a.
Membership e es -> Union es f a -> Maybe (e f a)
project Membership e es
i (UnsafeUnion Int
n e g a
e EffectOrder
_ forall x. g x -> f x
koi) =
        if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Membership e es -> Int
forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership Membership e es
i
            then e f a -> Maybe (e f a)
forall a. a -> Maybe a
Just (e f a -> Maybe (e f a)) -> e f a -> Maybe (e f a)
forall a b. (a -> b) -> a -> b
$ (forall x. g x -> f x) -> e g a -> e f a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> e f a -> e g a
forall (ff :: Effect) (f :: * -> *) (g :: * -> *) a.
HFunctor ff =>
(forall x. f x -> g x) -> ff f a -> ff g a
hfmap g x -> f x
forall x. g x -> f x
koi (e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
e)
            else Maybe (e f a)
forall a. Maybe a
Nothing

    (e f a -> r
f !: :: forall (f :: * -> *) a r (es :: [Effect]).
(e f a -> r) -> (Union es f a -> r) -> Union (e : es) f a -> r
!: Union es f a -> r
g) (UnsafeUnion Int
n e g a
e EffectOrder
_ forall x. g x -> f x
koi) =
        if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
            then e f a -> r
f (e f a -> r) -> e f a -> r
forall a b. (a -> b) -> a -> b
$ (forall x. g x -> f x) -> e g a -> e f a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> e f a -> e g a
forall (ff :: Effect) (f :: * -> *) (g :: * -> *) a.
HFunctor ff =>
(forall x. f x -> g x) -> ff f a -> ff g a
hfmap g x -> f x
forall x. g x -> f x
koi (e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
e)
            else Union es f a -> r
g (Union es f a -> r) -> Union es f a -> r
forall a b. (a -> b) -> a -> b
$ Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) e g a
e EffectOrder
HigherOrder g x -> f x
forall x. g x -> f x
koi

    extract :: forall (f :: * -> *) a. Union '[e] f a -> e f a
extract (UnsafeUnion Int
_ e g a
e EffectOrder
_ forall x. g x -> f x
koi) = (forall x. g x -> f x) -> e g a -> e f a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> e f a -> e g a
forall (ff :: Effect) (f :: * -> *) (g :: * -> *) a.
HFunctor ff =>
(forall x. f x -> g x) -> ff f a -> ff g a
hfmap g x -> f x
forall x. g x -> f x
koi (e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
e)

    {-# INLINE inject #-}
    {-# INLINE project #-}
    {-# INLINE (!:) #-}
    {-# INLINE extract #-}

projectAnyOrder :: forall e es f a. (HFunctor e) => Membership e es -> Union es f a -> Maybe (e f a)
projectAnyOrder :: forall (e :: Effect) (es :: [Effect]) (f :: * -> *) a.
HFunctor e =>
Membership e es -> Union es f a -> Maybe (e f a)
projectAnyOrder Membership e es
i (UnsafeUnion Int
n e g a
e EffectOrder
order forall x. g x -> f x
koi) =
    if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Membership e es -> Int
forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership Membership e es
i
        then e f a -> Maybe (e f a)
forall a. a -> Maybe a
Just (e f a -> Maybe (e f a)) -> e f a -> Maybe (e f a)
forall a b. (a -> b) -> a -> b
$ EffectOrder -> (forall x. g x -> f x) -> e g a -> e f a
forall (e' :: Effect) (f :: * -> *) (g :: * -> *) (e :: Effect) a.
HFunctor e' =>
EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a
hfmapDynUnsafeCoerce EffectOrder
order g x -> f x
forall x. g x -> f x
koi e g a
e
        else Maybe (e f a)
forall a. Maybe a
Nothing

infixr 5 `caseAnyOrder`

caseAnyOrder :: (HFunctor e) => (e f a -> r) -> (Union es f a -> r) -> Union (e ': es) f a -> r
(e f a -> r
f caseAnyOrder :: forall (e :: Effect) (f :: * -> *) a r (es :: [Effect]).
HFunctor e =>
(e f a -> r) -> (Union es f a -> r) -> Union (e : es) f a -> r
`caseAnyOrder` Union es f a -> r
g) (UnsafeUnion Int
n e g a
e EffectOrder
order forall x. g x -> f x
koi) =
    if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
        then e f a -> r
f (e f a -> r) -> e f a -> r
forall a b. (a -> b) -> a -> b
$ EffectOrder -> (forall x. g x -> f x) -> e g a -> e f a
forall (e' :: Effect) (f :: * -> *) (g :: * -> *) (e :: Effect) a.
HFunctor e' =>
EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a
hfmapDynUnsafeCoerce EffectOrder
order g x -> f x
forall x. g x -> f x
koi e g a
e
        else Union es f a -> r
g (Union es f a -> r) -> Union es f a -> r
forall a b. (a -> b) -> a -> b
$ Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) e g a
e EffectOrder
order g x -> f x
forall x. g x -> f x
koi

extractAnyOrder :: (HFunctor e) => Union es f a -> e f a
extractAnyOrder :: forall (e :: Effect) (es :: [Effect]) (f :: * -> *) a.
HFunctor e =>
Union es f a -> e f a
extractAnyOrder (UnsafeUnion Int
_ e g a
e EffectOrder
order forall x. g x -> f x
koi) = EffectOrder -> (forall x. g x -> f x) -> e g a -> e f a
forall (e' :: Effect) (f :: * -> *) (g :: * -> *) (e :: Effect) a.
HFunctor e' =>
EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a
hfmapDynUnsafeCoerce EffectOrder
order g x -> f x
forall x. g x -> f x
koi e g a
e

{-# INLINE projectAnyOrder #-}
{-# INLINE caseAnyOrder #-}
{-# INLINE extractAnyOrder #-}

hfmapDynUnsafeCoerce :: (HFunctor e') => EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a
hfmapDynUnsafeCoerce :: forall (e' :: Effect) (f :: * -> *) (g :: * -> *) (e :: Effect) a.
HFunctor e' =>
EffectOrder -> (forall x. f x -> g x) -> e f a -> e' g a
hfmapDynUnsafeCoerce EffectOrder
order forall x. f x -> g x
phi e f a
e = case EffectOrder
order of
    EffectOrder
FirstOrder -> e f a -> e' g a
forall a b. a -> b
unsafeCoerce e f a
e
    EffectOrder
HigherOrder -> (forall x. f x -> g x) -> e' f a -> e' g a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> e' f a -> e' g a
forall (ff :: Effect) (f :: * -> *) (g :: * -> *) a.
HFunctor ff =>
(forall x. f x -> g x) -> ff f a -> ff g a
hfmap f x -> g x
forall x. f x -> g x
phi (e f a -> e' f a
forall a b. a -> b
unsafeCoerce e f a
e)
{-# INLINE hfmapDynUnsafeCoerce #-}

nil :: Union '[] f a -> r
nil :: forall (f :: * -> *) a r. Union '[] f a -> r
nil Union '[] f a
_ = String -> r
forall a. HasCallStack => String -> a
error String
"Effect system internal error: nil - An empty effect union, which should not be possible to create, has been created."

nilMembership :: Membership e '[] -> r
nilMembership :: forall (e :: Effect) r. Membership e '[] -> r
nilMembership Membership e '[]
_ = String -> r
forall a. HasCallStack => String -> a
error String
"Effect system internal error: nil - An empty effect union membership, which should not be possible to create, has been created."

weakensFor :: forall es es' e. (Suffix es es') => Membership e es -> Membership e es'
weakensFor :: forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect).
Suffix es es' =>
Membership e es -> Membership e es'
weakensFor (UnsafeMembership Int
n) = Int -> Membership e es'
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e es') -> Int -> Membership e es'
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (es :: [Effect]) (es' :: [Effect]). Suffix es es' => Int
prefixLen @es @es'
{-# INLINE weakensFor #-}

class Suffix (es :: [Effect]) (es' :: [Effect]) where
    prefixLen :: Int

instance Suffix es es where
    prefixLen :: Int
prefixLen = Int
0
    {-# INLINE prefixLen #-}

instance {-# INCOHERENT #-} (Suffix es es') => Suffix es (e ': es') where
    prefixLen :: Int
prefixLen = forall (es :: [Effect]) (es' :: [Effect]). Suffix es es' => Int
prefixLen @es @es' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    {-# INLINE prefixLen #-}

class SuffixUnder (es :: [Effect]) (es' :: [Effect]) where
    prefixLenUnder :: Int
    offset :: Int

instance (Suffix es es') => SuffixUnder es es' where
    prefixLenUnder :: Int
prefixLenUnder = forall (es :: [Effect]) (es' :: [Effect]). Suffix es es' => Int
prefixLen @es @es'
    offset :: Int
offset = Int
0

    {-# INLINE prefixLenUnder #-}
    {-# INLINE offset #-}

instance {-# INCOHERENT #-} (SuffixUnder es es') => SuffixUnder (e ': es) (e ': es') where
    prefixLenUnder :: Int
prefixLenUnder = forall (es :: [Effect]) (es' :: [Effect]).
SuffixUnder es es' =>
Int
prefixLenUnder @es @es'
    offset :: Int
offset = forall (es :: [Effect]) (es' :: [Effect]).
SuffixUnder es es' =>
Int
offset @es @es' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

    {-# INLINE prefixLenUnder #-}
    {-# INLINE offset #-}

weakensUnderFor :: forall es es' e. (SuffixUnder es es') => Membership e es -> Membership e es'
weakensUnderFor :: forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect).
SuffixUnder es es' =>
Membership e es -> Membership e es'
weakensUnderFor (UnsafeMembership Int
n) =
    Int -> Membership e es'
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership
        if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< forall (es :: [Effect]) (es' :: [Effect]).
SuffixUnder es es' =>
Int
offset @es @es'
            then Int
n
            else Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (es :: [Effect]) (es' :: [Effect]).
SuffixUnder es es' =>
Int
prefixLenUnder @es @es'
{-# INLINE weakensUnderFor #-}

type family RemoveHOEs (es :: [Effect]) where
    RemoveHOEs '[] = '[]
    RemoveHOEs (e ': es) =
        OrderCase (OrderOf e) (e ': RemoveHOEs es) (RemoveHOEs es)

type WeakenHOEs es = (WeakenHOEs_ es 0 (OrderOf (HeadOf es)), FOEs (RemoveHOEs es))

class (orderOfHead ~ OrderOf (HeadOf es)) => WeakenHOEs_ es (countF :: Natural) orderOfHead where
    -- | Example for '[H,F,F,H,H,F,H,F]
    --
    -- +----+-------+--------+----------------------+
    -- | ix | order | countF | shifter accumulation |
    -- +====+=======+========+======================+
    -- |  0 |     H |      0 | 01234... -> 12345... |
    -- +----+-------+--------+----------------------+
    -- |  1 |     F |      0 | 01234... -> 12345... |
    -- +----+-------+--------+----------------------+
    -- |  2 |     F |      1 | 01234... -> 12345... |
    -- +----+-------+--------+----------------------+
    -- |  3 |     H |      2 | 01234... -> 12456... |
    -- +----+-------+--------+----------------------+
    -- |  4 |     H |      2 | 01234... -> 12567... |
    -- +----+-------+--------+----------------------+
    -- |  5 |     F |      2 | 01234... -> 12567... |
    -- +----+-------+--------+----------------------+
    -- |  6 |     H |      3 | 01234... -> 12578... |
    -- +----+-------+--------+----------------------+
    -- |  7 |     F |      3 | 01234... -> 12578... |
    -- +----+-------+--------+----------------------+
    foldHoeIndexShifter :: (Int -> Int) -> (Int -> Int)

instance (OrderOf (HeadOf '[]) ~ orderOfHead) => WeakenHOEs_ '[] countF orderOfHead where
    foldHoeIndexShifter :: (Int -> Int) -> Int -> Int
foldHoeIndexShifter = (Int -> Int) -> Int -> Int
forall a. a -> a
id
    {-# INLINE foldHoeIndexShifter #-}

instance (FirstOrder e, WeakenHOEs_ es (countF + 1) _orderOfHead) => WeakenHOEs_ (e ': es) countF 'FirstOrder where
    foldHoeIndexShifter :: (Int -> Int) -> Int -> Int
foldHoeIndexShifter = forall (es :: [Effect]) (countF :: Nat)
       (orderOfHead :: EffectOrder).
WeakenHOEs_ es countF orderOfHead =>
(Int -> Int) -> Int -> Int
foldHoeIndexShifter @es @(countF + 1)
    {-# INLINE foldHoeIndexShifter #-}

instance
    (OrderOf e ~ 'HigherOrder, WeakenHOEs_ es countF _orderOfHead, KnownNat countF)
    => WeakenHOEs_ (e ': es) countF 'HigherOrder
    where
    foldHoeIndexShifter :: (Int -> Int) -> Int -> Int
foldHoeIndexShifter Int -> Int
shifterAcc =
        forall (es :: [Effect]) (countF :: Nat)
       (orderOfHead :: EffectOrder).
WeakenHOEs_ es countF orderOfHead =>
(Int -> Int) -> Int -> Int
foldHoeIndexShifter @es @countF \Int
ix ->
            let shiftedIx :: Int
shiftedIx = Int -> Int
shifterAcc Int
ix
             in if Int
ix Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). KnownNat n => Int
intVal @countF
                    then Int
shiftedIx
                    else Int
shiftedIx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    {-# INLINE foldHoeIndexShifter #-}

type family RemoveExps (es :: [Effect]) where
    RemoveExps '[] = '[]
    RemoveExps (e ': es) =
        FormCase (FormOf e) (e ': RemoveExps es) (RemoveExps es)

type WeakenExps es = (WeakenExps_ es 0 (FormOf (HeadOf es)), PolyHFunctors (RemoveExps es))

class (formOfHead ~ FormOf (HeadOf es)) => WeakenExps_ es (countP :: Natural) formOfHead where
    foldExpIndexShifter :: (Int -> Int) -> (Int -> Int)

instance (FormOf (HeadOf '[]) ~ formOfHead) => WeakenExps_ '[] countP formOfHead where
    foldExpIndexShifter :: (Int -> Int) -> Int -> Int
foldExpIndexShifter = (Int -> Int) -> Int -> Int
forall a. a -> a
id
    {-# INLINE foldExpIndexShifter #-}

instance (PolyHFunctor e, WeakenExps_ es (countP + 1) _formOfHead) => WeakenExps_ (e ': es) countP 'Polynomial where
    foldExpIndexShifter :: (Int -> Int) -> Int -> Int
foldExpIndexShifter = forall (es :: [Effect]) (countP :: Nat) (formOfHead :: EffectForm).
WeakenExps_ es countP formOfHead =>
(Int -> Int) -> Int -> Int
foldExpIndexShifter @es @(countP + 1)
    {-# INLINE foldExpIndexShifter #-}

instance
    (FormOf e ~ 'Exponential, WeakenExps_ es countP _formOfHead, KnownNat countP)
    => WeakenExps_ (e ': es) countP 'Exponential
    where
    foldExpIndexShifter :: (Int -> Int) -> Int -> Int
foldExpIndexShifter Int -> Int
shifterAcc =
        forall (es :: [Effect]) (countP :: Nat) (formOfHead :: EffectForm).
WeakenExps_ es countP formOfHead =>
(Int -> Int) -> Int -> Int
foldExpIndexShifter @es @countP \Int
ix ->
            let shiftedIx :: Int
shiftedIx = Int -> Int
shifterAcc Int
ix
             in if Int
ix Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). KnownNat n => Int
intVal @countP
                    then Int
shiftedIx
                    else Int
shiftedIx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    {-# INLINE foldExpIndexShifter #-}

weaken :: Union es f a -> Union (e ': es) f a
weaken :: forall (es :: [Effect]) (f :: * -> *) a (e :: Effect).
Union es f a -> Union (e : es) f a
weaken = (forall (e :: Effect). Membership e es -> Membership e (e : es))
-> Union es f a -> Union (e : es) f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion Membership e es -> Membership e (e : es)
forall (e :: Effect). Membership e es -> Membership e (e : es)
forall (e :: Effect) (es :: [Effect]) (e' :: Effect).
Membership e es -> Membership e (e' : es)
weakenFor
{-# INLINE weaken #-}

weakens :: (Suffix es es') => Union es f a -> Union es' f a
weakens :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
Suffix es es' =>
Union es f a -> Union es' f a
weakens = (forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion Membership e es -> Membership e es'
forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect).
Suffix es es' =>
Membership e es -> Membership e es'
forall (e :: Effect). Membership e es -> Membership e es'
weakensFor
{-# INLINE weakens #-}

weakensUnder :: (SuffixUnder es es') => Union es f a -> Union es' f a
weakensUnder :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
SuffixUnder es es' =>
Union es f a -> Union es' f a
weakensUnder = (forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion Membership e es -> Membership e es'
forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect).
SuffixUnder es es' =>
Membership e es -> Membership e es'
forall (e :: Effect). Membership e es -> Membership e es'
weakensUnderFor
{-# INLINE weakensUnder #-}

weakenHOEsFor :: forall es e. (WeakenHOEs es) => Membership e (RemoveHOEs es) -> Membership e es
weakenHOEsFor :: forall (es :: [Effect]) (e :: Effect).
WeakenHOEs es =>
Membership e (RemoveHOEs es) -> Membership e es
weakenHOEsFor = Int -> Membership e es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e es)
-> (Membership e (RemoveHOEs es) -> Int)
-> Membership e (RemoveHOEs es)
-> Membership e es
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (es :: [Effect]) (countF :: Nat)
       (orderOfHead :: EffectOrder).
WeakenHOEs_ es countF orderOfHead =>
(Int -> Int) -> Int -> Int
foldHoeIndexShifter @es @0 Int -> Int
forall a. a -> a
id (Int -> Int)
-> (Membership e (RemoveHOEs es) -> Int)
-> Membership e (RemoveHOEs es)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership e (RemoveHOEs es) -> Int
forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership
{-# INLINE weakenHOEsFor #-}

weakenHOEs :: forall es f a. (WeakenHOEs es) => Union (RemoveHOEs es) f a -> Union es f a
weakenHOEs :: forall (es :: [Effect]) (f :: * -> *) a.
WeakenHOEs es =>
Union (RemoveHOEs es) f a -> Union es f a
weakenHOEs = (forall (e :: Effect).
 Membership e (RemoveHOEs es) -> Membership e es)
-> Union (RemoveHOEs es) f a -> Union es f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion Membership e (RemoveHOEs es) -> Membership e es
forall (es :: [Effect]) (e :: Effect).
WeakenHOEs es =>
Membership e (RemoveHOEs es) -> Membership e es
forall (e :: Effect).
Membership e (RemoveHOEs es) -> Membership e es
weakenHOEsFor
{-# INLINE weakenHOEs #-}

weakenExpsFor :: forall es e. (WeakenExps es) => Membership e (RemoveExps es) -> Membership e es
weakenExpsFor :: forall (es :: [Effect]) (e :: Effect).
WeakenExps es =>
Membership e (RemoveExps es) -> Membership e es
weakenExpsFor = Int -> Membership e es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e es)
-> (Membership e (RemoveExps es) -> Int)
-> Membership e (RemoveExps es)
-> Membership e es
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (es :: [Effect]) (countP :: Nat) (formOfHead :: EffectForm).
WeakenExps_ es countP formOfHead =>
(Int -> Int) -> Int -> Int
foldExpIndexShifter @es @0 Int -> Int
forall a. a -> a
id (Int -> Int)
-> (Membership e (RemoveExps es) -> Int)
-> Membership e (RemoveExps es)
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Membership e (RemoveExps es) -> Int
forall (e :: Effect) (es :: [Effect]). Membership e es -> Int
unMembership
{-# INLINE weakenExpsFor #-}

weakenExps :: forall es f a. (WeakenExps es) => Union (RemoveExps es) f a -> Union es f a
weakenExps :: forall (es :: [Effect]) (f :: * -> *) a.
WeakenExps es =>
Union (RemoveExps es) f a -> Union es f a
weakenExps = (forall (e :: Effect).
 Membership e (RemoveExps es) -> Membership e es)
-> Union (RemoveExps es) f a -> Union es f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion Membership e (RemoveExps es) -> Membership e es
forall (es :: [Effect]) (e :: Effect).
WeakenExps es =>
Membership e (RemoveExps es) -> Membership e es
forall (e :: Effect).
Membership e (RemoveExps es) -> Membership e es
weakenExpsFor
{-# INLINE weakenExps #-}

type KnownLength :: forall {k}. [k] -> Constraint
class KnownLength xs where
    reifyLength :: Int

instance KnownLength '[] where
    reifyLength :: Int
reifyLength = Int
0
    {-# INLINE reifyLength #-}

instance (KnownLength xs) => KnownLength (x ': xs) where
    reifyLength :: Int
reifyLength = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (xs :: [k]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @xs
    {-# INLINE reifyLength #-}

infixr 5 ++

type family (es :: [Effect]) ++ (es' :: [Effect]) where
    '[] ++ es = es
    (e ': es) ++ es' = e ': (es ++ es')

infixr 5 !++

(!++) :: forall es es' f a r. (KnownLength es) => (Union es f a -> r) -> (Union es' f a -> r) -> Union (es ++ es') f a -> r
(Union es f a -> r
h !++ :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a r.
KnownLength es =>
(Union es f a -> r)
-> (Union es' f a -> r) -> Union (es ++ es') f a -> r
!++ Union es' f a -> r
h') (UnsafeUnion Int
n e g a
e EffectOrder
o forall x. g x -> f x
koi) =
    if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< forall (xs :: [Effect]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @es
        then Union es f a -> r
h (Union es f a -> r) -> Union es f a -> r
forall a b. (a -> b) -> a -> b
$ Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion Int
n e g a
e EffectOrder
o g x -> f x
forall x. g x -> f x
koi
        else Union es' f a -> r
h' (Union es' f a -> r) -> Union es' f a -> r
forall a b. (a -> b) -> a -> b
$ Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es' f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- forall (xs :: [Effect]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @es) e g a
e EffectOrder
o g x -> f x
forall x. g x -> f x
koi
{-# INLINE (!++) #-}

bundleUnion
    :: forall es es' f a
     . (KnownLength es)
    => Union (es ++ es') f a
    -> Union (Union es ': es') f a
bundleUnion :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
KnownLength es =>
Union (es ++ es') f a -> Union (Union es : es') f a
bundleUnion = (forall (e :: Effect) (o :: EffectOrder) (g :: * -> *).
 Membership e (es ++ es')
 -> Ordership o e f g -> e g a -> Union (Union es : es') f a)
-> Union (es ++ es') f a -> Union (Union es : es') f a
forall (es :: [Effect]) (f :: * -> *) a r.
(forall (e :: Effect) (o :: EffectOrder) (g :: * -> *).
 Membership e es -> Ordership o e f g -> e g a -> r)
-> Union es f a -> r
union \Membership e (es ++ es')
i Ordership o e f g
o e g a
e ->
    forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect) r.
KnownLength es =>
(Membership e es -> r)
-> (Membership e es' -> r) -> Membership e (es ++ es') -> r
splitFor @es @es'
        (\Membership e es
j -> Membership (Union es) (Union es : es')
-> Ordership 'HigherOrder (Union es) f f
-> Union es f a
-> Union (Union es : es') f a
forall (e :: Effect) (es :: [Effect]) (o :: EffectOrder)
       (f :: * -> *) (g :: * -> *) a.
Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion Membership (Union es) (Union es : es')
forall (e :: Effect) (es :: [Effect]). Membership e (e : es)
Here ((forall x. f x -> f x) -> Ordership 'HigherOrder (Union es) f f
forall (e :: Effect) (g :: * -> *) (f :: * -> *).
(OrderOf e ~ 'HigherOrder) =>
(forall x. g x -> f x) -> Ordership 'HigherOrder e f g
higherOrdership f x -> f x
forall a. a -> a
forall x. f x -> f x
id) (Membership e es -> Ordership o e f g -> e g a -> Union es f a
forall (e :: Effect) (es :: [Effect]) (o :: EffectOrder)
       (f :: * -> *) (g :: * -> *) a.
Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion Membership e es
j Ordership o e f g
o e g a
e))
        (\Membership e es'
j -> Membership e (Union es : es')
-> Ordership o e f g -> e g a -> Union (Union es : es') f a
forall (e :: Effect) (es :: [Effect]) (o :: EffectOrder)
       (f :: * -> *) (g :: * -> *) a.
Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion (Membership e es' -> Membership e (Union es : es')
forall (e :: Effect) (es :: [Effect]) (e' :: Effect).
Membership e es -> Membership e (e' : es)
weakenFor Membership e es'
j) Ordership o e f g
o e g a
e)
        Membership e (es ++ es')
i
{-# INLINE bundleUnion #-}

unbundleUnion
    :: forall es es' f a
     . (KnownLength es)
    => Union (Union es ': es') f a
    -> Union (es ++ es') f a
unbundleUnion :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
KnownLength es =>
Union (Union es : es') f a -> Union (es ++ es') f a
unbundleUnion = (forall (e :: Effect). Membership e es -> Membership e (es ++ es'))
-> Union es f a -> Union (es ++ es') f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
Membership e es -> Membership e (es ++ es')
suffixFor @es') (Union es f a -> Union (es ++ es') f a)
-> (Union es' f a -> Union (es ++ es') f a)
-> Union (Union es : es') f a
-> Union (es ++ es') f a
forall (f :: * -> *) a r (es :: [Effect]).
(Union es f a -> r)
-> (Union es f a -> r) -> Union (Union es : es) f a -> r
forall (e :: Effect) (order :: EffectOrder) (f :: * -> *) a r
       (es :: [Effect]).
Elem e order =>
(e f a -> r) -> (Union es f a -> r) -> Union (e : es) f a -> r
!: (forall (e :: Effect).
 Membership e es' -> Membership e (es ++ es'))
-> Union es' f a -> Union (es ++ es') f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
KnownLength es' =>
Membership e es -> Membership e (es' ++ es)
prefixFor @es)
{-# INLINE unbundleUnion #-}

splitUnion
    :: forall es es' es'' f a
     . (KnownLength es)
    => (forall e. Membership e es -> Membership e es'')
    -> (forall e. Membership e es' -> Membership e es'')
    -> Union (es ++ es') f a
    -> Union es'' f a
splitUnion :: forall (es :: [Effect]) (es' :: [Effect]) (es'' :: [Effect])
       (f :: * -> *) a.
KnownLength es =>
(forall (e :: Effect). Membership e es -> Membership e es'')
-> (forall (e :: Effect). Membership e es' -> Membership e es'')
-> Union (es ++ es') f a
-> Union es'' f a
splitUnion forall (e :: Effect). Membership e es -> Membership e es''
injL forall (e :: Effect). Membership e es' -> Membership e es''
injR = (forall (e :: Effect).
 Membership e (es ++ es') -> Membership e es'')
-> Union (es ++ es') f a -> Union es'' f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion ((forall (e :: Effect).
  Membership e (es ++ es') -> Membership e es'')
 -> Union (es ++ es') f a -> Union es'' f a)
-> (forall (e :: Effect).
    Membership e (es ++ es') -> Membership e es'')
-> Union (es ++ es') f a
-> Union es'' f a
forall a b. (a -> b) -> a -> b
$ forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect) r.
KnownLength es =>
(Membership e es -> r)
-> (Membership e es' -> r) -> Membership e (es ++ es') -> r
splitFor @es @es' Membership e es -> Membership e es''
forall (e :: Effect). Membership e es -> Membership e es''
injL Membership e es' -> Membership e es''
forall (e :: Effect). Membership e es' -> Membership e es''
injR
{-# INLINE splitUnion #-}

mergeUnion
    :: forall es es' f a
     . (KnownLength es)
    => Either (Union es f a) (Union es' f a)
    -> Union (es ++ es') f a
mergeUnion :: forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
KnownLength es =>
Either (Union es f a) (Union es' f a) -> Union (es ++ es') f a
mergeUnion = \case
    Left Union es f a
u -> (forall (e :: Effect). Membership e es -> Membership e (es ++ es'))
-> Union es f a -> Union (es ++ es') f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
Membership e es -> Membership e (es ++ es')
suffixFor @es') Union es f a
u
    Right Union es' f a
u -> (forall (e :: Effect).
 Membership e es' -> Membership e (es ++ es'))
-> Union es' f a -> Union (es ++ es') f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
KnownLength es' =>
Membership e es -> Membership e (es' ++ es)
prefixFor @es) Union es' f a
u
{-# INLINE mergeUnion #-}

splitUnion1
    :: forall fs x es es' f a
     . (KnownLength fs)
    => (forall e. Membership e (Each fs x) -> Membership e es')
    -> (forall e. Membership e es -> Membership e es')
    -> Union (Each fs x ++ es) f a
    -> Union es' f a
splitUnion1 :: forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (es' :: [Effect]) (f :: * -> *) a.
KnownLength fs =>
(forall (e :: Effect).
 Membership e (Each fs x) -> Membership e es')
-> (forall (e :: Effect). Membership e es -> Membership e es')
-> Union (Each fs x ++ es) f a
-> Union es' f a
splitUnion1 forall (e :: Effect). Membership e (Each fs x) -> Membership e es'
injL forall (e :: Effect). Membership e es -> Membership e es'
injR = (forall (e :: Effect).
 Membership e (Each fs x ++ es) -> Membership e es')
-> Union (Each fs x ++ es) f a -> Union es' f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion ((forall (e :: Effect).
  Membership e (Each fs x ++ es) -> Membership e es')
 -> Union (Each fs x ++ es) f a -> Union es' f a)
-> (forall (e :: Effect).
    Membership e (Each fs x ++ es) -> Membership e es')
-> Union (Each fs x ++ es) f a
-> Union es' f a
forall a b. (a -> b) -> a -> b
$ forall (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (e :: Effect) r.
KnownLength fs =>
(Membership e (Each fs x) -> r)
-> (Membership e es -> r) -> Membership e (Each fs x ++ es) -> r
forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (e :: Effect) r.
KnownLength fs =>
(Membership e (Each fs x) -> r)
-> (Membership e es -> r) -> Membership e (Each fs x ++ es) -> r
splitFor1 @fs @x @es Membership e (Each fs x) -> Membership e es'
forall (e :: Effect). Membership e (Each fs x) -> Membership e es'
injL Membership e es -> Membership e es'
forall (e :: Effect). Membership e es -> Membership e es'
injR
{-# INLINE splitUnion1 #-}

mergeUnion1
    :: forall fs x es f a
     . (KnownLength fs)
    => Either (Union (Each fs x) f a) (Union es f a)
    -> Union (Each fs x ++ es) f a
mergeUnion1 :: forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (f :: * -> *) a.
KnownLength fs =>
Either (Union (Each fs x) f a) (Union es f a)
-> Union (Each fs x ++ es) f a
mergeUnion1 = \case
    Left Union (Each fs x) f a
u -> (forall (e :: Effect).
 Membership e (Each fs x) -> Membership e (Each fs x ++ es))
-> Union (Each fs x) f a -> Union (Each fs x ++ es) f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
Membership e es -> Membership e (es ++ es')
suffixFor @es) Union (Each fs x) f a
u
    Right Union es f a
u -> (forall (e :: Effect).
 Membership e es -> Membership e (Each fs x ++ es))
-> Union es f a -> Union (Each fs x ++ es) f a
forall (es :: [Effect]) (es' :: [Effect]) (f :: * -> *) a.
(forall (e :: Effect). Membership e es -> Membership e es')
-> Union es f a -> Union es' f a
mapUnion (forall (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (e :: Effect).
KnownLength fs =>
Membership e es -> Membership e (Each fs x ++ es)
forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (e :: Effect).
KnownLength fs =>
Membership e es -> Membership e (Each fs x ++ es)
prefixFor1 @fs @x) Union es f a
u
{-# INLINE mergeUnion1 #-}

splitFor
    :: forall es es' e r
     . (KnownLength es)
    => (Membership e es -> r)
    -> (Membership e es' -> r)
    -> Membership e (es ++ es')
    -> r
splitFor :: forall (es :: [Effect]) (es' :: [Effect]) (e :: Effect) r.
KnownLength es =>
(Membership e es -> r)
-> (Membership e es' -> r) -> Membership e (es ++ es') -> r
splitFor Membership e es -> r
f Membership e es' -> r
g (UnsafeMembership Int
n)
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
l = Membership e es -> r
f (Membership e es -> r) -> Membership e es -> r
forall a b. (a -> b) -> a -> b
$ Int -> Membership e es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership Int
n
    | Bool
otherwise = Membership e es' -> r
g (Membership e es' -> r) -> Membership e es' -> r
forall a b. (a -> b) -> a -> b
$ Int -> Membership e es'
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e es') -> Int -> Membership e es'
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l
  where
    l :: Int
l = forall (xs :: [Effect]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @es
{-# INLINE splitFor #-}

splitFor1
    :: forall fs x es e r
     . (KnownLength fs)
    => (Membership e (Each fs x) -> r)
    -> (Membership e es -> r)
    -> Membership e (Each fs x ++ es)
    -> r
splitFor1 :: forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (e :: Effect) r.
KnownLength fs =>
(Membership e (Each fs x) -> r)
-> (Membership e es -> r) -> Membership e (Each fs x ++ es) -> r
splitFor1 Membership e (Each fs x) -> r
f Membership e es -> r
g (UnsafeMembership Int
n)
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
l = Membership e (Each fs x) -> r
f (Membership e (Each fs x) -> r) -> Membership e (Each fs x) -> r
forall a b. (a -> b) -> a -> b
$ Int -> Membership e (Each fs x)
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership Int
n
    | Bool
otherwise = Membership e es -> r
g (Membership e es -> r) -> Membership e es -> r
forall a b. (a -> b) -> a -> b
$ Int -> Membership e es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e es) -> Int -> Membership e es
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l
  where
    l :: Int
l = forall (xs :: [k -> Effect]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @fs
{-# INLINE splitFor1 #-}

suffixFor :: forall es' es e. Membership e es -> Membership e (es ++ es')
suffixFor :: forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
Membership e es -> Membership e (es ++ es')
suffixFor = Membership e es -> Membership e (es ++ es')
forall a b. Coercible a b => a -> b
coerce
{-# INLINE suffixFor #-}

prefixFor :: forall es' es e. (KnownLength es') => Membership e es -> Membership e (es' ++ es)
prefixFor :: forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
KnownLength es' =>
Membership e es -> Membership e (es' ++ es)
prefixFor (UnsafeMembership Int
n) = Int -> Membership e (es' ++ es)
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e (es' ++ es))
-> Int -> Membership e (es' ++ es)
forall a b. (a -> b) -> a -> b
$ forall (xs :: [Effect]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @es' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
{-# INLINE prefixFor #-}

type family Each (fs :: [k -> Effect]) x where
    Each (f ': fs) x = (f x ': Each fs x)
    Each '[] x = '[]

prefixFor1 :: forall fs x es e. (KnownLength fs) => Membership e es -> Membership e (Each fs x ++ es)
prefixFor1 :: forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect])
       (e :: Effect).
KnownLength fs =>
Membership e es -> Membership e (Each fs x ++ es)
prefixFor1 (UnsafeMembership Int
n) = Int -> Membership e (Each fs x ++ es)
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership (Int -> Membership e (Each fs x ++ es))
-> Int -> Membership e (Each fs x ++ es)
forall a b. (a -> b) -> a -> b
$ forall (xs :: [k -> Effect]). KnownLength xs => Int
forall {k} (xs :: [k]). KnownLength xs => Int
reifyLength @fs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n
{-# INLINE prefixFor1 #-}

data Ordership (o :: EffectOrder) (e :: Effect) (f :: Type -> Type) (g :: Type -> Type) where
    UnsafeFirst :: Ordership 'FirstOrder e f g
    UnsafeHigher :: (forall x. g x -> f x) -> Ordership 'HigherOrder e f g

union :: (forall e o g. Membership e es -> Ordership o e f g -> e g a -> r) -> Union es f a -> r
union :: forall (es :: [Effect]) (f :: * -> *) a r.
(forall (e :: Effect) (o :: EffectOrder) (g :: * -> *).
 Membership e es -> Ordership o e f g -> e g a -> r)
-> Union es f a -> r
union forall (e :: Effect) (o :: EffectOrder) (g :: * -> *).
Membership e es -> Ordership o e f g -> e g a -> r
f (UnsafeUnion Int
n e g a
e EffectOrder
o forall x. g x -> f x
koi) =
    let i :: Membership e es
i = Int -> Membership e es
forall (e :: Effect) (es :: [Effect]). Int -> Membership e es
UnsafeMembership Int
n
     in case EffectOrder
o of
            EffectOrder
FirstOrder -> Membership e es -> Ordership 'FirstOrder e f g -> e g a -> r
forall (e :: Effect) (o :: EffectOrder) (g :: * -> *).
Membership e es -> Ordership o e f g -> e g a -> r
f Membership e es
i Ordership 'FirstOrder e f g
forall (e :: Effect) (f :: * -> *) (g :: * -> *).
Ordership 'FirstOrder e f g
UnsafeFirst e g a
e
            EffectOrder
HigherOrder -> Membership e es -> Ordership 'HigherOrder e f g -> e g a -> r
forall (e :: Effect) (o :: EffectOrder) (g :: * -> *).
Membership e es -> Ordership o e f g -> e g a -> r
f Membership e es
i ((forall x. g x -> f x) -> Ordership 'HigherOrder e f g
forall (g :: * -> *) (f :: * -> *) (e :: Effect).
(forall x. g x -> f x) -> Ordership 'HigherOrder e f g
UnsafeHigher g x -> f x
forall x. g x -> f x
koi) e g a
e
{-# INLINE union #-}

mkUnion :: Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion :: forall (e :: Effect) (es :: [Effect]) (o :: EffectOrder)
       (f :: * -> *) (g :: * -> *) a.
Membership e es -> Ordership o e f g -> e g a -> Union es f a
mkUnion (UnsafeMembership Int
i) Ordership o e f g
o e g a
e = case Ordership o e f g
o of
    Ordership o e f g
UnsafeFirst -> Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion Int
i e g a
e EffectOrder
FirstOrder g x -> f x
forall x. g x -> f x
forall a. HasCallStack => a
undefined
    UnsafeHigher forall x. g x -> f x
koi -> Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
forall (e :: Effect) (g :: * -> *) a (f :: * -> *)
       (es :: [Effect]).
Int
-> e g a -> EffectOrder -> (forall x. g x -> f x) -> Union es f a
UnsafeUnion Int
i e g a
e EffectOrder
HigherOrder g x -> f x
forall x. g x -> f x
koi
{-# INLINE mkUnion #-}

firstOrdership :: (FirstOrder e) => Ordership 'FirstOrder e f g
firstOrdership :: forall (e :: Effect) (f :: * -> *) (g :: * -> *).
FirstOrder e =>
Ordership 'FirstOrder e f g
firstOrdership = Ordership 'FirstOrder e f g
forall (e :: Effect) (f :: * -> *) (g :: * -> *).
Ordership 'FirstOrder e f g
UnsafeFirst
{-# INLINE firstOrdership #-}

higherOrdership :: (OrderOf e ~ 'HigherOrder) => (forall x. g x -> f x) -> Ordership 'HigherOrder e f g
higherOrdership :: forall (e :: Effect) (g :: * -> *) (f :: * -> *).
(OrderOf e ~ 'HigherOrder) =>
(forall x. g x -> f x) -> Ordership 'HigherOrder e f g
higherOrdership = (forall x. g x -> f x) -> Ordership 'HigherOrder e f g
forall (g :: * -> *) (f :: * -> *) (e :: Effect).
(forall x. g x -> f x) -> Ordership 'HigherOrder e f g
UnsafeHigher
{-# INLINE higherOrdership #-}

shrinkOrdership :: Ordership o e f g -> Ordership (OrderOf e) e f g
shrinkOrdership :: forall (o :: EffectOrder) (e :: Effect) (f :: * -> *)
       (g :: * -> *).
Ordership o e f g -> Ordership (OrderOf e) e f g
shrinkOrdership = Ordership o e f g -> Ordership (OrderOf e) e f g
forall a b. a -> b
unsafeCoerce

continuationOfInterpretation :: Ordership 'HigherOrder e f g -> (forall x. g x -> f x)
continuationOfInterpretation :: forall (e :: Effect) (f :: * -> *) (g :: * -> *).
Ordership 'HigherOrder e f g -> forall x. g x -> f x
continuationOfInterpretation (UnsafeHigher forall x. g x -> f x
koi) = g x -> f x
forall x. g x -> f x
koi
{-# INLINE continuationOfInterpretation #-}