{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Data.Effect.OpenUnion.Internal.HO where
import Control.Effect (type (~>))
import Data.Coerce (coerce)
import Data.Effect (EffectH)
import Data.Effect.HFunctor (HFunctor, hfmap)
import Data.Effect.Key (type (##>))
import Data.Effect.OpenUnion.Internal (
BundleUnder,
Drop,
ElemAt,
ElemIndex,
FindElem,
IfKeyNotFound,
IfNotFound,
IsSuffixOf,
KnownLength,
Length,
P (unP),
PrefixLength,
Reverse,
Split,
Strengthen,
StrengthenN,
StrengthenNUnder,
StrengthenUnder,
Take,
WeakenN,
WeakenNUnder,
WeakenUnder,
elemNo,
prefixLen,
reifyLength,
strengthenMap,
strengthenMapUnder,
wordVal,
type (++),
)
import Data.Kind (Type)
import GHC.TypeNats (KnownNat, type (-))
import Unsafe.Coerce (unsafeCoerce)
data UnionH (es :: [EffectH]) (f :: Type -> Type) (a :: Type) where
UnionH
:: {-# UNPACK #-} !Word
-> e g a
-> (g ~> f)
-> UnionH es f a
hfmapUnion :: (f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion :: forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion f ~> g
phi (UnionH Word
n e g a
e g ~> f
koi) = Word -> e g a -> (g ~> g) -> UnionH es g a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
n e g a
e (f x -> g x
f ~> g
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
g ~> f
koi)
{-# INLINE hfmapUnion #-}
instance HFunctor (UnionH es) where
hfmap :: forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> UnionH es f :-> UnionH es g
hfmap f :-> g
f = (f :-> g) -> UnionH es f i -> UnionH es g i
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion f x -> g x
f :-> g
f
{-# INLINE hfmap #-}
unsafeInjH :: Word -> e f a -> UnionH es f a
unsafeInjH :: forall (e :: EffectH) (f :: * -> *) a (es :: [EffectH]).
Word -> e f a -> UnionH es f a
unsafeInjH Word
n e f a
e = Word -> e f a -> (f ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
n e f a
e f x -> f x
forall a. a -> a
f ~> f
id
{-# INLINE unsafeInjH #-}
unsafePrjH :: (HFunctor e) => Word -> UnionH es f a -> Maybe (e f a)
unsafePrjH :: forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
HFunctor e =>
Word -> UnionH es f a -> Maybe (e f a)
unsafePrjH Word
n (UnionH Word
n' e g a
e g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
n' = e f a -> Maybe (e f a)
forall a. a -> Maybe a
Just ((g ~> f) -> e g :-> e f
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap g i -> f i
g ~> f
koi (e g a -> e f a) -> e g a -> e f a
forall a b. (a -> b) -> a -> b
$ e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
e)
| Bool
otherwise = Maybe (e f a)
forall a. Maybe a
Nothing
{-# INLINE unsafePrjH #-}
class (FindElem e es) => MemberH (e :: EffectH) es where
injH :: e f a -> UnionH es f a
prjH :: (HFunctor e) => UnionH es f a -> Maybe (e f a)
instance (FindElem e es, IfNotFound e es es) => MemberH e es where
injH :: forall (f :: * -> *) a. e f a -> UnionH es f a
injH = Word -> e f a -> UnionH es f a
forall (e :: EffectH) (f :: * -> *) a (es :: [EffectH]).
Word -> e f a -> UnionH es f a
unsafeInjH (Word -> e f a -> UnionH es f a) -> Word -> e f a -> UnionH es f a
forall a b. (a -> b) -> a -> b
$ P e es -> Word
forall k (e :: k) (es :: [k]). P e es -> Word
unP (P e es
forall {k} (e :: k) (es :: [k]). FindElem e es => P e es
elemNo :: P e es)
{-# INLINE injH #-}
prjH :: forall (f :: * -> *) a.
HFunctor e =>
UnionH es f a -> Maybe (e f a)
prjH = Word -> UnionH es f a -> Maybe (e f a)
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
HFunctor e =>
Word -> UnionH es f a -> Maybe (e f a)
unsafePrjH (Word -> UnionH es f a -> Maybe (e f a))
-> Word -> UnionH es f a -> Maybe (e f a)
forall a b. (a -> b) -> a -> b
$ P e es -> Word
forall k (e :: k) (es :: [k]). P e es -> Word
unP (P e es
forall {k} (e :: k) (es :: [k]). FindElem e es => P e es
elemNo :: P e es)
{-# INLINE prjH #-}
infix 3 <<|
type (<<|) = MemberH
type MemberHBy key e es = (key ##> e <<| es, LookupH key es ~ key ##> e, IfKeyNotFound key es es)
type family LookupH (key :: k) r :: EffectH where
LookupH key (key ##> e ': _) = key ##> e
LookupH key (_ ': r) = LookupH key r
decompH :: (HFunctor e) => UnionH (e ': es) f a -> Either (UnionH es f a) (e f a)
decompH :: forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
HFunctor e =>
UnionH (e : es) f a -> Either (UnionH es f a) (e f a)
decompH (UnionH Word
0 e g a
a g ~> f
koi) = e f a -> Either (UnionH es f a) (e f a)
forall a b. b -> Either a b
Right (e f a -> Either (UnionH es f a) (e f a))
-> e f a -> Either (UnionH es f a) (e f a)
forall a b. (a -> b) -> a -> b
$ (g ~> f) -> e g :-> e f
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap g i -> f i
g ~> f
koi (e g a -> e f a) -> e g a -> e f a
forall a b. (a -> b) -> a -> b
$ e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
a
decompH (UnionH Word
n e g a
a g ~> f
koi) = UnionH es f a -> Either (UnionH es f a) (e f a)
forall a b. a -> Either a b
Left (UnionH es f a -> Either (UnionH es f a) (e f a))
-> UnionH es f a -> Either (UnionH es f a) (e f a)
forall a b. (a -> b) -> a -> b
$ Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) e g a
a g x -> f x
g ~> f
koi
{-# INLINE [2] decompH #-}
decomp0H :: (HFunctor e) => UnionH '[e] f a -> Either (UnionH '[] f a) (e f a)
decomp0H :: forall (e :: EffectH) (f :: * -> *) a.
HFunctor e =>
UnionH '[e] f a -> Either (UnionH '[] f a) (e f a)
decomp0H (UnionH Word
_ e g a
a g ~> f
koi) = e f a -> Either (UnionH '[] f a) (e f a)
forall a b. b -> Either a b
Right (e f a -> Either (UnionH '[] f a) (e f a))
-> e f a -> Either (UnionH '[] f a) (e f a)
forall a b. (a -> b) -> a -> b
$ (g ~> f) -> e g :-> e f
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap g i -> f i
g ~> f
koi (e g a -> e f a) -> e g a -> e f a
forall a b. (a -> b) -> a -> b
$ e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
a
{-# INLINE decomp0H #-}
{-# RULES "decomp/singleton" decompH = decomp0H #-}
infixr 5 !!+
(!!+) :: (HFunctor e) => (e f a -> r) -> (UnionH es f a -> r) -> UnionH (e : es) f a -> r
(e f a -> r
f !!+ :: forall (e :: EffectH) (f :: * -> *) a r (es :: [EffectH]).
HFunctor e =>
(e f a -> r) -> (UnionH es f a -> r) -> UnionH (e : es) f a -> r
!!+ UnionH es f a -> r
g) UnionH (e : es) f a
u = case UnionH (e : es) f a -> Either (UnionH es f a) (e f a)
forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
HFunctor e =>
UnionH (e : es) f a -> Either (UnionH es f a) (e f a)
decompH UnionH (e : es) f a
u of
Left UnionH es f a
x -> UnionH es f a -> r
g UnionH es f a
x
Right e f a
x -> e f a -> r
f e f a
x
{-# INLINE (!!+) #-}
extractH :: (HFunctor e) => UnionH '[e] f a -> e f a
(UnionH Word
_ e g a
a g ~> f
koi) = (g ~> f) -> e g :-> e f
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap g i -> f i
g ~> f
koi (e g a -> e f a) -> e g a -> e f a
forall a b. (a -> b) -> a -> b
$ e g a -> e g a
forall a b. a -> b
unsafeCoerce e g a
a
{-# INLINE extractH #-}
inj0H :: forall e es f a. e f a -> UnionH (e ': es) f a
inj0H :: forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
e f a -> UnionH (e : es) f a
inj0H e f a
a = Word -> e f a -> (f ~> f) -> UnionH (e : es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
0 e f a
a f x -> f x
forall a. a -> a
f ~> f
id
{-# INLINE inj0H #-}
injNH :: forall i es f a. (KnownNat i) => ElemAt i es f a -> UnionH es f a
injNH :: forall (i :: Nat) (es :: [EffectH]) (f :: * -> *) a.
KnownNat i =>
ElemAt i es f a -> UnionH es f a
injNH ElemAt i es f a
a = Word -> ElemAt i es f a -> (f ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (forall (n :: Nat). KnownNat n => Word
wordVal @i) ElemAt i es f a
a f x -> f x
forall a. a -> a
f ~> f
id
{-# INLINE injNH #-}
prjNH
:: forall i es f a
. (KnownNat i, HFunctor (ElemAt i es))
=> UnionH es f a
-> Maybe (ElemAt i es f a)
prjNH :: forall (i :: Nat) (es :: [EffectH]) (f :: * -> *) a.
(KnownNat i, HFunctor (ElemAt i es)) =>
UnionH es f a -> Maybe (ElemAt i es f a)
prjNH (UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== forall (n :: Nat). KnownNat n => Word
wordVal @i = ElemAt i es f a -> Maybe (ElemAt i es f a)
forall a. a -> Maybe a
Just (ElemAt i es f a -> Maybe (ElemAt i es f a))
-> ElemAt i es f a -> Maybe (ElemAt i es f a)
forall a b. (a -> b) -> a -> b
$ (g ~> f) -> ElemAt i es g :-> ElemAt i es f
forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> ElemAt i es f :-> ElemAt i es g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap g i -> f i
g ~> f
koi (ElemAt i es g a -> ElemAt i es f a)
-> ElemAt i es g a -> ElemAt i es f a
forall a b. (a -> b) -> a -> b
$ e g a -> ElemAt i es g a
forall a b. a -> b
unsafeCoerce e g a
a
| Bool
otherwise = Maybe (ElemAt i es f a)
forall a. Maybe a
Nothing
{-# INLINE prjNH #-}
weakenH :: forall any es f a. UnionH es f a -> UnionH (any ': es) f a
weakenH :: forall (any :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
UnionH es f a -> UnionH (any : es) f a
weakenH (UnionH Word
n e g a
a g ~> f
koi) = Word -> e g a -> (g ~> f) -> UnionH (any : es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e g a
a g x -> f x
g ~> f
koi
{-# INLINE weakenH #-}
weakensH :: forall es es' f a. (es `IsSuffixOf` es') => UnionH es f a -> UnionH es' f a
weakensH :: forall (es :: [EffectH]) (es' :: [EffectH]) (f :: * -> *) a.
IsSuffixOf es es' =>
UnionH es f a -> UnionH es' f a
weakensH (UnionH Word
n e g a
a g ~> f
koi) = Word -> e g a -> (g ~> f) -> UnionH es' f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [EffectH]) (es' :: [EffectH]).
IsSuffixOf es es' =>
Word
forall {k} {k1} (es :: k) (es' :: k1). IsSuffixOf es es' => Word
prefixLen @es @es') e g a
a g x -> f x
g ~> f
koi
{-# INLINE weakensH #-}
weakenNH :: forall len es es' f a. (WeakenN len es es') => UnionH es f a -> UnionH es' f a
weakenNH :: forall (len :: Nat) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH (UnionH Word
n e g a
a g ~> f
koi) = Word -> e g a -> (g ~> f) -> UnionH es' f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @len) e g a
a g x -> f x
g ~> f
koi
{-# INLINE weakenNH #-}
weakenUnderH :: forall any e es f a. UnionH (e ': es) f a -> UnionH (e ': any ': es) f a
weakenUnderH :: forall (any :: EffectH) (e :: EffectH) (es :: [EffectH])
(f :: * -> *) a.
UnionH (e : es) f a -> UnionH (e : any : es) f a
weakenUnderH u :: UnionH (e : es) f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = UnionH (e : es) f a -> UnionH (e : any : es) f a
forall a b. Coercible a b => a -> b
coerce UnionH (e : es) f a
u
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH (e : any : es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e g a
a g x -> f x
g ~> f
koi
{-# INLINE weakenUnderH #-}
weakensUnderH :: forall offset es es' f a. (WeakenUnder offset es es') => UnionH es f a -> UnionH es' f a
weakensUnderH :: forall (offset :: Nat) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
WeakenUnder offset es es' =>
UnionH es f a -> UnionH es' f a
weakensUnderH = forall (len :: Nat) (offset :: Nat) (es :: [EffectH])
(es' :: [EffectH]) (f :: * -> *) a.
WeakenNUnder len offset es es' =>
UnionH es f a -> UnionH es' f a
weakenNUnderH @(PrefixLength es es') @offset
{-# INLINE weakensUnderH #-}
weakenNUnderH
:: forall len offset es es' f a
. (WeakenNUnder len offset es es')
=> UnionH es f a
-> UnionH es' f a
weakenNUnderH :: forall (len :: Nat) (offset :: Nat) (es :: [EffectH])
(es' :: [EffectH]) (f :: * -> *) a.
WeakenNUnder len offset es es' =>
UnionH es f a -> UnionH es' f a
weakenNUnderH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). KnownNat n => Word
wordVal @offset = UnionH es f a -> UnionH es' f a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH es' f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @len) e g a
a g x -> f x
g ~> f
koi
{-# INLINE weakenNUnderH #-}
strengthenH :: forall e es f a. (e <<| es) => UnionH (e ': es) f a -> UnionH es f a
strengthenH :: forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
(e <<| es) =>
UnionH (e : es) f a -> UnionH es f a
strengthenH (UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (forall (n :: Nat). KnownNat n => Word
wordVal @(ElemIndex e es)) e g a
a g x -> f x
g ~> f
koi
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) e g a
a g x -> f x
g ~> f
koi
{-# INLINE strengthenH #-}
strengthensH :: forall es es' f a. (Strengthen es es') => UnionH es f a -> UnionH es' f a
strengthensH :: forall (es :: [EffectH]) (es' :: [EffectH]) (f :: * -> *) a.
Strengthen es es' =>
UnionH es f a -> UnionH es' f a
strengthensH = forall (len :: Nat) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
StrengthenN len es es' =>
UnionH es f a -> UnionH es' f a
strengthenNH @(PrefixLength es' es)
{-# INLINE strengthensH #-}
strengthenNH :: forall len es es' f a. (StrengthenN len es es') => UnionH es f a -> UnionH es' f a
strengthenNH :: forall (len :: Nat) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
StrengthenN len es es' =>
UnionH es f a -> UnionH es' f a
strengthenNH (UnionH Word
n e g a
a g ~> f
koi) = Word -> e g a -> (g ~> f) -> UnionH es' f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (forall k (isLenZero :: Bool) (len :: Nat) (es :: [k]) (es' :: [k]).
StrengthenMap_ isLenZero len es es' =>
Word -> Word
strengthenMap @_ @_ @len @es @es' Word
n) e g a
a g x -> f x
g ~> f
koi
{-# INLINE strengthenNH #-}
strengthenUnderH :: forall e2 e1 es f a. (e2 <<| es) => UnionH (e1 ': e2 ': es) f a -> UnionH (e1 ': es) f a
strengthenUnderH :: forall (e2 :: EffectH) (e1 :: EffectH) (es :: [EffectH])
(f :: * -> *) a.
(e2 <<| es) =>
UnionH (e1 : e2 : es) f a -> UnionH (e1 : es) f a
strengthenUnderH u :: UnionH (e1 : e2 : es) f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = UnionH (e1 : e2 : es) f a -> UnionH (e1 : es) f a
forall a b. Coercible a b => a -> b
coerce UnionH (e1 : e2 : es) f a
u
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
1 = Word -> e g a -> (g ~> f) -> UnionH (e1 : es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @(ElemIndex e2 es)) e g a
a g x -> f x
g ~> f
koi
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH (e1 : es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) e g a
a g x -> f x
g ~> f
koi
{-# INLINE strengthenUnderH #-}
strengthensUnderH
:: forall offset es es' f a
. (StrengthenUnder offset es es')
=> UnionH es f a
-> UnionH es' f a
strengthensUnderH :: forall (offset :: Nat) (es :: [EffectH]) (es' :: [EffectH])
(f :: * -> *) a.
StrengthenUnder offset es es' =>
UnionH es f a -> UnionH es' f a
strengthensUnderH = forall (len :: Nat) (offset :: Nat) (es :: [EffectH])
(es' :: [EffectH]) (f :: * -> *) a.
StrengthenNUnder len offset es es' =>
UnionH es f a -> UnionH es' f a
strengthenNUnderH @(PrefixLength es' es) @offset
{-# INLINE strengthensUnderH #-}
strengthenNUnderH
:: forall len offset es es' f a
. (StrengthenNUnder len offset es es')
=> UnionH es f a
-> UnionH es' f a
strengthenNUnderH :: forall (len :: Nat) (offset :: Nat) (es :: [EffectH])
(es' :: [EffectH]) (f :: * -> *) a.
StrengthenNUnder len offset es es' =>
UnionH es f a -> UnionH es' f a
strengthenNUnderH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
off = UnionH es f a -> UnionH es' f a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH es' f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
off Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (len :: Nat) (offset :: Nat) (es :: [EffectH])
(es' :: [EffectH]).
StrengthenNUnder len offset es es' =>
Word -> Word
forall {k} (len :: Nat) (offset :: Nat) (es :: [k]) (es' :: [k]).
StrengthenNUnder len offset es es' =>
Word -> Word
strengthenMapUnder @len @offset @es @es' (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
off)) e g a
a g x -> f x
g ~> f
koi
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
{-# INLINE strengthenNUnderH #-}
bundleUnionH
:: forall bundle es rest f a
. (Split es bundle rest)
=> UnionH es f a
-> UnionH (UnionH bundle ': rest) f a
bundleUnionH :: forall (bundle :: [EffectH]) (es :: [EffectH]) (rest :: [EffectH])
(f :: * -> *) a.
Split es bundle rest =>
UnionH es f a -> UnionH (UnionH bundle : rest) f a
bundleUnionH = forall (len :: Nat) (es :: [EffectH]) (f :: * -> *) a.
KnownNat len =>
UnionH es f a -> UnionH (UnionH (Take len es) : Drop len es) f a
bundleUnionNH @(Length bundle)
{-# INLINE bundleUnionH #-}
bundleUnionNH
:: forall len es f a
. (KnownNat len)
=> UnionH es f a
-> UnionH (UnionH (Take len es) ': Drop len es) f a
bundleUnionNH :: forall (len :: Nat) (es :: [EffectH]) (f :: * -> *) a.
KnownNat len =>
UnionH es f a -> UnionH (UnionH (Take len es) : Drop len es) f a
bundleUnionNH (UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word
-> UnionH Any f a
-> (f ~> f)
-> UnionH (UnionH (Take len es) : Drop len es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
0 (Word -> e g a -> (g ~> f) -> UnionH Any f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
n e g a
a g x -> f x
g ~> f
koi) f x -> f x
forall a. a -> a
f ~> f
id
| Bool
otherwise = Word
-> e g a
-> (g ~> f)
-> UnionH (UnionH (Take len es) : Drop len es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e g a
a g x -> f x
g ~> f
koi
where
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
{-# INLINE bundleUnionNH #-}
unbundleUnionH
:: forall bundle es rest f a
. (Split es bundle rest)
=> UnionH (UnionH bundle ': rest) f a
-> UnionH es f a
unbundleUnionH :: forall (bundle :: [EffectH]) (es :: [EffectH]) (rest :: [EffectH])
(f :: * -> *) a.
Split es bundle rest =>
UnionH (UnionH bundle : rest) f a -> UnionH es f a
unbundleUnionH = forall (len :: Nat) (es :: [EffectH]) (f :: * -> *) a.
KnownNat len =>
UnionH (UnionH (Take len es) : Drop len es) f a -> UnionH es f a
unbundleUnionNH @(Length bundle)
{-# INLINE unbundleUnionH #-}
unbundleUnionNH
:: forall len es f a
. (KnownNat len)
=> UnionH (UnionH (Take len es) ': Drop len es) f a
-> UnionH es f a
unbundleUnionNH :: forall (len :: Nat) (es :: [EffectH]) (f :: * -> *) a.
KnownNat len =>
UnionH (UnionH (Take len es) : Drop len es) f a -> UnionH es f a
unbundleUnionNH (UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
0 = case e g a -> UnionH Any g a
forall a b. a -> b
unsafeCoerce e g a
a of
UnionH Word
n' e g a
a' g ~> g
koi' -> Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
n' e g a
a' (g x -> f x
g ~> f
koi (g x -> f x) -> (g x -> g x) -> g x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> g x
g ~> g
koi')
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (n :: Nat). KnownNat n => Word
wordVal @len) e g a
a g x -> f x
g ~> f
koi
{-# INLINE unbundleUnionNH #-}
bundleUnionUnderH
:: forall offset bundle es es' f a
. (BundleUnder UnionH offset es es' bundle)
=> UnionH es f a
-> UnionH es' f a
bundleUnionUnderH :: forall (offset :: Nat) (bundle :: [EffectH]) (es :: [EffectH])
(es' :: [EffectH]) (f :: * -> *) a.
BundleUnder UnionH offset es es' bundle =>
UnionH es f a -> UnionH es' f a
bundleUnionUnderH = forall (len :: Nat) (offset :: Nat) (es :: [EffectH]) (f :: * -> *)
a.
(KnownNat len, KnownNat offset) =>
UnionH es f a
-> UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
bundleUnionNUnderH @(Length bundle) @offset
{-# INLINE bundleUnionUnderH #-}
bundleUnionNUnderH
:: forall len offset es f a
. (KnownNat len, KnownNat offset)
=> UnionH es f a
-> UnionH (Take offset es ++ (UnionH (Take len (Drop offset es)) ': Drop len (Drop offset es))) f a
bundleUnionNUnderH :: forall (len :: Nat) (offset :: Nat) (es :: [EffectH]) (f :: * -> *)
a.
(KnownNat len, KnownNat offset) =>
UnionH es f a
-> UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
bundleUnionNUnderH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
off = UnionH es f a
-> UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
| Word
n' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word
-> UnionH Any f a
-> (f ~> f)
-> UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
0 (Word -> e g a -> (g ~> f) -> UnionH Any f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
n' e g a
a g x -> f x
g ~> f
koi) f x -> f x
forall a. a -> a
f ~> f
id
| Bool
otherwise = Word
-> e g a
-> (g ~> f)
-> UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) e g a
a g x -> f x
g ~> f
koi
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
n' :: Word
n' = Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
off
{-# INLINE bundleUnionNUnderH #-}
unbundleUnionUnderH
:: forall offset bundle es es' f a
. (BundleUnder UnionH offset es es' bundle)
=> UnionH es' f a
-> UnionH es f a
unbundleUnionUnderH :: forall (offset :: Nat) (bundle :: [EffectH]) (es :: [EffectH])
(es' :: [EffectH]) (f :: * -> *) a.
BundleUnder UnionH offset es es' bundle =>
UnionH es' f a -> UnionH es f a
unbundleUnionUnderH = forall (len :: Nat) (offset :: Nat) (es :: [EffectH]) (f :: * -> *)
a.
(KnownNat len, KnownNat offset) =>
UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
-> UnionH es f a
unbundleUnionNUnderH @(Length bundle) @offset
{-# INLINE unbundleUnionUnderH #-}
unbundleUnionNUnderH
:: forall len offset es f a
. (KnownNat len, KnownNat offset)
=> UnionH (Take offset es ++ (UnionH (Take len (Drop offset es)) ': Drop len (Drop offset es))) f a
-> UnionH es f a
unbundleUnionNUnderH :: forall (len :: Nat) (offset :: Nat) (es :: [EffectH]) (f :: * -> *)
a.
(KnownNat len, KnownNat offset) =>
UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
-> UnionH es f a
unbundleUnionNUnderH u :: UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
off = UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
-> UnionH es f a
forall a b. Coercible a b => a -> b
coerce UnionH
(Take offset es
++ (UnionH (Take len (Drop offset es))
: Drop len (Drop offset es)))
f
a
u
| Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
off =
case e g a -> UnionH Any g a
forall a b. a -> b
unsafeCoerce e g a
a of
UnionH Word
n' e g a
a' g ~> g
koi' -> Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
off Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
n') e g a
a' (g x -> f x
g ~> f
koi (g x -> f x) -> (g x -> g x) -> g x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> g x
g ~> g
koi')
| Bool
otherwise = Word -> e g a -> (g ~> f) -> UnionH es f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
len) e g a
a g x -> f x
g ~> f
koi
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
{-# INLINE unbundleUnionNUnderH #-}
bundleAllUnionH :: UnionH es f a -> UnionH '[UnionH es] f a
bundleAllUnionH :: forall (es :: [EffectH]) (f :: * -> *) a.
UnionH es f a -> UnionH '[UnionH es] f a
bundleAllUnionH UnionH es f a
u = Word -> UnionH es f a -> (f ~> f) -> UnionH '[UnionH es] f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH Word
0 UnionH es f a
u f x -> f x
forall a. a -> a
f ~> f
id
{-# INLINE bundleAllUnionH #-}
unbundleAllUnionH :: UnionH '[UnionH es] f a -> UnionH es f a
unbundleAllUnionH :: forall (es :: [EffectH]) (f :: * -> *) a.
UnionH '[UnionH es] f a -> UnionH es f a
unbundleAllUnionH = UnionH '[UnionH es] f a -> UnionH es f a
forall (e :: EffectH) (f :: * -> *) a.
HFunctor e =>
UnionH '[e] f a -> e f a
extractH
{-# INLINE unbundleAllUnionH #-}
prefixUnionH :: forall any es f a. (KnownLength any) => UnionH es f a -> UnionH (any ++ es) f a
prefixUnionH :: forall (any :: [EffectH]) (es :: [EffectH]) (f :: * -> *) a.
KnownLength any =>
UnionH es f a -> UnionH (any ++ es) f a
prefixUnionH (UnionH Word
n e g a
a g ~> f
koi) = Word -> e g a -> (g ~> f) -> UnionH (any ++ es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [EffectH]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @any) e g a
a g x -> f x
g ~> f
koi
{-# INLINE prefixUnionH #-}
prefixUnionUnderH
:: forall any offset es f a
. (KnownLength any, KnownNat offset)
=> UnionH es f a
-> UnionH (Take offset es ++ any ++ Drop offset es) f a
prefixUnionUnderH :: forall (any :: [EffectH]) (offset :: Nat) (es :: [EffectH])
(f :: * -> *) a.
(KnownLength any, KnownNat offset) =>
UnionH es f a
-> UnionH (Take offset es ++ (any ++ Drop offset es)) f a
prefixUnionUnderH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). KnownNat n => Word
wordVal @offset = UnionH es f a
-> UnionH (Take offset es ++ (any ++ Drop offset es)) f a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
| Bool
otherwise = Word
-> e g a
-> (g ~> f)
-> UnionH (Take offset es ++ (any ++ Drop offset es)) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [EffectH]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @any) e g a
a g x -> f x
g ~> f
koi
{-# INLINE prefixUnionUnderH #-}
suffixUnionH :: forall any es f a. UnionH es f a -> UnionH (es ++ any) f a
suffixUnionH :: forall (any :: [EffectH]) (es :: [EffectH]) (f :: * -> *) a.
UnionH es f a -> UnionH (es ++ any) f a
suffixUnionH = UnionH es f a -> UnionH (es ++ any) f a
forall a b. Coercible a b => a -> b
coerce
{-# INLINE suffixUnionH #-}
suffixUnionOverNH
:: forall any offset es f a
. (KnownLength any, KnownNat offset, KnownLength es)
=> UnionH es f a
-> UnionH (Take (Length es - offset) es ++ any ++ Drop (Length es - offset) es) f a
suffixUnionOverNH :: forall (any :: [EffectH]) (offset :: Nat) (es :: [EffectH])
(f :: * -> *) a.
(KnownLength any, KnownNat offset, KnownLength es) =>
UnionH es f a
-> UnionH
(Take (Length es - offset) es
++ (any ++ Drop (Length es - offset) es))
f
a
suffixUnionOverNH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< forall (es :: [EffectH]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @es Word -> Word -> Word
forall a. Num a => a -> a -> a
- forall (n :: Nat). KnownNat n => Word
wordVal @offset = UnionH es f a
-> UnionH
(Take (Length es - offset) es
++ (any ++ Drop (Length es - offset) es))
f
a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
| Bool
otherwise = Word
-> e g a
-> (g ~> f)
-> UnionH
(Take (Length es - offset) es
++ (any ++ Drop (Length es - offset) es))
f
a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ forall (es :: [EffectH]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @any) e g a
a g x -> f x
g ~> f
koi
{-# INLINE suffixUnionOverNH #-}
flipAllUnionH :: forall es f a. (KnownLength es) => UnionH es f a -> UnionH (Reverse es) f a
flipAllUnionH :: forall (es :: [EffectH]) (f :: * -> *) a.
KnownLength es =>
UnionH es f a -> UnionH (Reverse es) f a
flipAllUnionH (UnionH Word
n e g a
a g ~> f
koi) = Word -> e g a -> (g ~> f) -> UnionH (Reverse_ '[] es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (forall (es :: [EffectH]). KnownLength es => Word
forall {a} (es :: [a]). KnownLength es => Word
reifyLength @es Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
n) e g a
a g x -> f x
g ~> f
koi
{-# INLINE flipAllUnionH #-}
flipUnionH
:: forall len es f a
. (KnownNat len)
=> UnionH es f a
-> UnionH (Reverse (Take len es) ++ Drop len es) f a
flipUnionH :: forall (len :: Nat) (es :: [EffectH]) (f :: * -> *) a.
KnownNat len =>
UnionH es f a -> UnionH (Reverse (Take len es) ++ Drop len es) f a
flipUnionH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word
-> e g a
-> (g ~> f)
-> UnionH (Reverse_ '[] (Take len es) ++ Drop len es) f a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
n) e g a
a g x -> f x
g ~> f
koi
| Bool
otherwise = UnionH es f a
-> UnionH (Reverse_ '[] (Take len es) ++ Drop len es) f a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
where
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
{-# INLINE flipUnionH #-}
flipUnionUnderH
:: forall len offset es f a
. (KnownNat len, KnownNat offset)
=> UnionH es f a
-> UnionH (Take offset es ++ Reverse (Take len (Drop offset es)) ++ Drop len (Drop offset es)) f a
flipUnionUnderH :: forall (len :: Nat) (offset :: Nat) (es :: [EffectH]) (f :: * -> *)
a.
(KnownNat len, KnownNat offset) =>
UnionH es f a
-> UnionH
(Take offset es
++ (Reverse (Take len (Drop offset es))
++ Drop len (Drop offset es)))
f
a
flipUnionUnderH u :: UnionH es f a
u@(UnionH Word
n e g a
a g ~> f
koi)
| Word
n Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
>= Word
off Bool -> Bool -> Bool
&& Word
n' Word -> Word -> Bool
forall a. Ord a => a -> a -> Bool
< Word
len = Word
-> e g a
-> (g ~> f)
-> UnionH
(Take offset es
++ (Reverse_ '[] (Take len (Drop offset es))
++ Drop len (Drop offset es)))
f
a
forall (e :: EffectH) (g :: * -> *) a (f :: * -> *)
(es :: [EffectH]).
Word -> e g a -> (g ~> f) -> UnionH es f a
UnionH (Word
off Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
len Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
n') e g a
a g x -> f x
g ~> f
koi
| Bool
otherwise = UnionH es f a
-> UnionH
(Take offset es
++ (Reverse_ '[] (Take len (Drop offset es))
++ Drop len (Drop offset es)))
f
a
forall a b. Coercible a b => a -> b
coerce UnionH es f a
u
where
off :: Word
off = forall (n :: Nat). KnownNat n => Word
wordVal @offset
len :: Word
len = forall (n :: Nat). KnownNat n => Word
wordVal @len
n' :: Word
n' = Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
off
{-# INLINE flipUnionUnderH #-}
nilH :: UnionH '[] f a -> r
nilH :: forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH UnionH '[] f a
_ = [Char] -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"Effect system internal error: nilH - An empty effect union, which should not be possible to create, has been created."