{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- SPDX-License-Identifier: MPL-2.0

{- |
Copyright   :  (c) 2023-2025 Sayo contributors
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp

This module provides the `Provider` effect, like [@Effectful.Provider@](https://hackage.haskell.org/package/effectful-core-2.3.0.0/docs/Effectful-Provider.html)
in the @effectful@ package.
-}
module Data.Effect.Provider where

import Control.Effect (emb)
import Control.Effect.Transform (raise, raisePrefix, raisePrefix1, transAll)
import Data.Effect (Emb, UnliftBase)
import Data.Effect.OpenUnion (
    Each,
    KnownLength,
    RemoveExps,
    WeakenExps,
    prefixFor,
    prefixFor1,
    splitUnion,
    splitUnion1,
    suffixFor,
    weakenExpsFor,
    (!:>),
    pattern Here,
    type (++),
 )
import Data.Effect.Unlift (withRunInBase)
import Data.Functor.Const (Const (Const))
import Data.Functor.Identity (Identity (Identity), runIdentity)
import Data.Type.Equality (type (:~:) (Refl))

-- | An effect to introduce a new local scope that provides effect context @b s@.
data Scope t i b :: Effect where
    -- | Introduces a new local scope that provides an effect context @b s@ parameterized by type @i s@ and with results wrapped in @t s@.
    Scope
        :: forall s t i a f b
         . i s
        -> ((forall x. f x -> b s x) -> b s a)
        -> Scope t i b f (t s a)

makeEffectH' (def & noGenerateLabel) ''Scope

-- | A type-level label to uniquely resolve the effect context carrier @b@ from @t@ and @i@.
data ScopeLabel (t :: k -> Type -> Type) (i :: k -> Type)

type instance LabelOf (Scope t i b) = ScopeLabel t i

newtype Const1 f x (a :: Type) = Const1 {forall {k} (f :: * -> *) (x :: k) a. Const1 f x a -> f a
getConst1 :: f a}

-- | An effect to introduce a new local scope that provides the scope-parametrized effect @es@.
type Scoped ff t i es r = Scope t i (ScopeC ff t i es r)

newtype ScopeC ff t i fs r s a
    = ScopeC {forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
ScopeC ff t i fs r s a
-> Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
unScopeC :: Eff ff (Each fs s ++ Scoped ff t i fs r ': r) a}

-- | An effect to introduce a new local scope that provides the effect @es@.
type Scoped_ ff t i es r = Scope t i (Const1 (ScopeC_ ff t i es r))

newtype ScopeC_ ff t i es r a
    = ScopeC_ {forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
ScopeC_ ff t i es r a -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
unScopeC_ :: Eff ff (es ++ Scoped_ ff t i es r ': r) a}

type Provider ff t i e es = Scoped_ ff (Const1 t) (Const i :: () -> Type) e es

runScoped
    :: forall t i a es r ff c
     . (KnownLength es, Free c ff)
    => ( forall s x
          . i s
         -> Eff ff (Each es s ++ Scoped ff t i es r ': r) x
         -> Eff ff (Scoped ff t i es r ': r) (t s x)
       )
    -> Eff ff (Scoped ff t i es r ': r) a
    -> Eff ff r a
runScoped :: forall {k} (t :: k -> * -> *) (i :: k -> *) a (es :: [k -> Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength es, Free c ff) =>
(forall (s :: k) x.
 i s
 -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
 -> Eff ff (Scoped ff t i es r : r) (t s x))
-> Eff ff (Scoped ff t i es r : r) a -> Eff ff r a
runScoped forall (s :: k) x.
i s
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
-> Eff ff (Scoped ff t i es r : r) (t s x)
run = Eff ff (Scoped ff t i es r : r) a -> Eff ff r a
Eff ff (Scoped ff t i es r : r) ~> Eff ff r
loop
  where
    loop :: Eff ff (Scoped ff t i es r ': r) ~> Eff ff r
    loop :: Eff ff (Scoped ff t i es r : r) ~> Eff ff r
loop = (Scoped ff t i es r ~~> Eff ff r)
-> Eff ff (Scoped ff t i es r : r) x -> Eff ff r x
forall (e :: Effect) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(KnownOrder e, Free c ff) =>
(e ~~> Eff ff es) -> Eff ff (e : es) a -> Eff ff es a
interpret \(Scope (i s
i :: i s) (forall x. Eff ff r x -> ScopeC ff t i es r s x)
-> ScopeC ff t i es r s a
f) ->
        Eff ff (Scoped ff t i es r : r) x -> Eff ff r x
Eff ff (Scoped ff t i es r : r) ~> Eff ff r
loop (Eff ff (Scoped ff t i es r : r) x -> Eff ff r x)
-> Eff ff (Scoped ff t i es r : r) x -> Eff ff r x
forall a b. (a -> b) -> a -> b
$ i s
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
-> Eff ff (Scoped ff t i es r : r) (t s a)
forall (s :: k) x.
i s
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
-> Eff ff (Scoped ff t i es r : r) (t s x)
run i s
i (ScopeC ff t i es r s a
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
ScopeC ff t i fs r s a
-> Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
unScopeC (ScopeC ff t i es r s a
 -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a)
-> ScopeC ff t i es r s a
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
forall a b. (a -> b) -> a -> b
$ (forall x. Eff ff r x -> ScopeC ff t i es r s x)
-> ScopeC ff t i es r s a
f ((forall x. Eff ff r x -> ScopeC ff t i es r s x)
 -> ScopeC ff t i es r s a)
-> (forall x. Eff ff r x -> ScopeC ff t i es r s x)
-> ScopeC ff t i es r s a
forall a b. (a -> b) -> a -> b
$ Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
-> ScopeC ff t i es r s x
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
-> ScopeC ff t i fs r s a
ScopeC (Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
 -> ScopeC ff t i es r s x)
-> (Eff ff r x -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x)
-> Eff ff r x
-> ScopeC ff t i es r s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fs :: [k -> Effect]) (x :: k) (es :: [Effect]) a
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength fs, Free c ff) =>
Eff ff es a -> Eff ff (Each fs x ++ es) a
forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect]) a
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength fs, Free c ff) =>
Eff ff es a -> Eff ff (Each fs x ++ es) a
raisePrefix1 @es @s (Eff ff (Scoped ff t i es r : r) x
 -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x)
-> (Eff ff r x -> Eff ff (Scoped ff t i es r : r) x)
-> Eff ff r x
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: Effect) (es :: [Effect]) a (ff :: Effect)
       (c :: (* -> *) -> Constraint).
Free c ff =>
Eff ff es a -> Eff ff (e : es) a
raise @(Scoped ff t i es r))
{-# INLINE runScoped #-}

runRegionScoped
    :: forall b t i a es r ff c
     . (WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r, KnownLength es, Free c ff)
    => ( forall s x
          . i s
         -> Eff ff (Each es s ++ Scoped ff t i es (RemoveExps r) ': r) x
         -> Eff ff (Scoped ff t i es (RemoveExps r) ': r) (t s x)
       )
    -> Eff ff (Scoped ff t i es (RemoveExps r) ': r) a
    -> Eff ff r a
runRegionScoped :: forall {k} (b :: * -> *) (t :: k -> * -> *) (i :: k -> *) a
       (es :: [k -> Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 KnownLength es, Free c ff) =>
(forall (s :: k) x.
 i s
 -> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) x
 -> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s x))
-> Eff ff (Scoped ff t i es (RemoveExps r) : r) a -> Eff ff r a
runRegionScoped forall (s :: k) x.
i s
-> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) x
-> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s x)
runScope = Eff ff (Scoped ff t i es (RemoveExps r) : r) a -> Eff ff r a
Eff ff (Scoped ff t i es (RemoveExps r) : r) ~> Eff ff r
loop
  where
    loop :: Eff ff (Scoped ff t i es (RemoveExps r) ': r) ~> Eff ff r
    loop :: Eff ff (Scoped ff t i es (RemoveExps r) : r) ~> Eff ff r
loop Eff ff (Scoped ff t i es (RemoveExps r) : r) x
a = forall (b :: * -> *) a (f :: * -> *) (es :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(Free c ff, f ~ Eff ff es, UnliftBase b :> es) =>
((forall x. f x -> b x) -> b a) -> f a
withRunInBase @b \forall x. Eff ff r x -> b x
runInBase ->
        Eff ff r x -> b x
forall x. Eff ff r x -> b x
runInBase (Eff ff r x -> b x) -> Eff ff r x -> b x
forall a b. (a -> b) -> a -> b
$
            Eff ff (Scoped ff t i es (RemoveExps r) : r) x
a Eff ff (Scoped ff t i es (RemoveExps r) : r) x
-> (Eff ff (Scoped ff t i es (RemoveExps r) : r) x -> Eff ff r x)
-> Eff ff r x
forall a b. a -> (a -> b) -> b
& (Scoped ff t i es (RemoveExps r) ~~> Eff ff r)
-> Eff ff (Scoped ff t i es (RemoveExps r) : r) x -> Eff ff r x
forall (e :: Effect) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(KnownOrder e, Free c ff) =>
(e ~~> Eff ff es) -> Eff ff (e : es) a -> Eff ff es a
interpret \(Scope (i s
i :: i s) (forall x. Eff ff r x -> ScopeC ff t i es (RemoveExps r) s x)
-> ScopeC ff t i es (RemoveExps r) s a
f) ->
                Eff ff (Scoped ff t i es (RemoveExps r) : r) x -> Eff ff r x
Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s a) -> Eff ff r x
Eff ff (Scoped ff t i es (RemoveExps r) : r) ~> Eff ff r
loop
                    (Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s a)
 -> Eff ff r x)
-> (ScopeC ff t i es (RemoveExps r) s a
    -> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s a))
-> ScopeC ff t i es (RemoveExps r) s a
-> Eff ff r x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i s
-> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) a
-> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s a)
forall (s :: k) x.
i s
-> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) x
-> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s x)
runScope i s
i
                    (Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) a
 -> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s a))
-> (ScopeC ff t i es (RemoveExps r) s a
    -> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) a)
-> ScopeC ff t i es (RemoveExps r) s a
-> Eff ff (Scoped ff t i es (RemoveExps r) : r) (t s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Union
   (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
   (Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)))
 ~> Union
      (Each es s ++ (Scoped ff t i es (RemoveExps r) : r))
      (Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r))))
-> Eff
     ff
     (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
     a
-> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) a
forall (es :: [Effect]) (es' :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
Free c ff =>
(Union es (Eff ff es') ~> Union es' (Eff ff es'))
-> Eff ff es a -> Eff ff es' a
transAll
                        ( forall (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
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 @es @s @(Scoped ff t i es (RemoveExps r) ': RemoveExps r)
                            (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
Membership e es -> Membership e (es ++ es')
suffixFor @(Scoped ff t i es (RemoveExps r) ': r))
                            ( 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 @es @s @(Scoped ff t i es (RemoveExps r) ': r)
                                (Membership e (Scoped ff t i es (RemoveExps r) : r)
 -> Membership
      e (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)))
-> (Membership e (Scoped ff t i es (RemoveExps r) : RemoveExps r)
    -> Membership e (Scoped ff t i es (RemoveExps r) : r))
-> Membership e (Scoped ff t i es (RemoveExps r) : RemoveExps r)
-> Membership
     e (Each es s ++ (Scoped ff t i es (RemoveExps r) : r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((\e :~: Scoped ff t i es (RemoveExps r)
Refl -> Membership e (e : r)
Membership e (Scoped ff t i es (RemoveExps r) : r)
forall (e :: Effect) (es :: [Effect]). Membership e (e : es)
Here) ((e :~: Scoped ff t i es (RemoveExps r))
 -> Membership e (Scoped ff t i es (RemoveExps r) : r))
-> (Membership e (RemoveExps r)
    -> Membership e (Scoped ff t i es (RemoveExps r) : r))
-> Membership e (Scoped ff t i es (RemoveExps r) : RemoveExps r)
-> Membership e (Scoped ff t i es (RemoveExps r) : r)
forall (e :: Effect) (e' :: Effect) (es :: [Effect]) r.
((e :~: e') -> r)
-> (Membership e es -> r) -> Membership e (e' : es) -> r
!:> Membership e (RemoveExps r)
-> Membership e (Scoped ff t i es (RemoveExps r) : r)
Membership e (RemoveExps (Scoped ff t i es (RemoveExps r) : r))
-> Membership e (Scoped ff t i es (RemoveExps r) : r)
forall (es :: [Effect]) (e :: Effect).
WeakenExps es =>
Membership e (RemoveExps es) -> Membership e es
weakenExpsFor)
                            )
                        )
                    (Eff
   ff
   (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
   a
 -> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) a)
-> (ScopeC ff t i es (RemoveExps r) s a
    -> Eff
         ff
         (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
         a)
-> ScopeC ff t i es (RemoveExps r) s a
-> Eff ff (Each es s ++ (Scoped ff t i es (RemoveExps r) : r)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeC ff t i es (RemoveExps r) s a
-> Eff
     ff
     (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
     a
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
ScopeC ff t i fs r s a
-> Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
unScopeC
                    (ScopeC ff t i es (RemoveExps r) s a -> Eff ff r x)
-> ScopeC ff t i es (RemoveExps r) s a -> Eff ff r x
forall a b. (a -> b) -> a -> b
$ (forall x. Eff ff r x -> ScopeC ff t i es (RemoveExps r) s x)
-> ScopeC ff t i es (RemoveExps r) s a
f
                    ((forall x. Eff ff r x -> ScopeC ff t i es (RemoveExps r) s x)
 -> ScopeC ff t i es (RemoveExps r) s a)
-> (forall x. Eff ff r x -> ScopeC ff t i es (RemoveExps r) s x)
-> ScopeC ff t i es (RemoveExps r) s a
forall a b. (a -> b) -> a -> b
$ Eff
  ff
  (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
  x
-> ScopeC ff t i es (RemoveExps r) s x
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
-> ScopeC ff t i fs r s a
ScopeC (Eff
   ff
   (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
   x
 -> ScopeC ff t i es (RemoveExps r) s x)
-> (Eff ff r x
    -> Eff
         ff
         (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
         x)
-> Eff ff r x
-> ScopeC ff t i es (RemoveExps r) s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fs :: [k -> Effect]) (x :: k) (es :: [Effect]) a
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength fs, Free c ff) =>
Eff ff es a -> Eff ff (Each fs x ++ es) a
forall {k} (fs :: [k -> Effect]) (x :: k) (es :: [Effect]) a
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength fs, Free c ff) =>
Eff ff es a -> Eff ff (Each fs x ++ es) a
raisePrefix1 @es @s @(Scoped ff t i es (RemoveExps r) ': RemoveExps r) (Eff ff (Scoped ff t i es (RemoveExps r) : RemoveExps r) x
 -> Eff
      ff
      (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
      x)
-> (Eff ff r x
    -> Eff ff (Scoped ff t i es (RemoveExps r) : RemoveExps r) x)
-> Eff ff r x
-> Eff
     ff
     (Each es s ++ (Scoped ff t i es (RemoveExps r) : RemoveExps r))
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> Eff ff (Scoped ff t i es (RemoveExps r) : RemoveExps r) x
forall (f :: * -> *) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(Emb f :> es, Free c ff) =>
f a -> Eff ff es a
emb (b x -> Eff ff (Scoped ff t i es (RemoveExps r) : RemoveExps r) x)
-> (Eff ff r x -> b x)
-> Eff ff r x
-> Eff ff (Scoped ff t i es (RemoveExps r) : RemoveExps r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff ff r x -> b x
forall x. Eff ff r x -> b x
runInBase
{-# INLINE runRegionScoped #-}

scoped
    :: forall t i s a es' es r ff c
     . (Scoped ff t i es r :> es', Free c ff)
    => i s
    -> ( Eff ff es' ~> Eff ff (Each es s ++ Scoped ff t i es r ': r)
         -> Eff ff (Each es s ++ Scoped ff t i es r ': r) a
       )
    -> Eff ff es' (t s a)
scoped :: forall {k} (t :: k -> * -> *) (i :: k -> *) (s :: k) a
       (es' :: [Effect]) (es :: [k -> Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(Scoped ff t i es r :> es', Free c ff) =>
i s
-> ((Eff ff es' ~> Eff ff (Each es s ++ (Scoped ff t i es r : r)))
    -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a)
-> Eff ff es' (t s a)
scoped i s
i (Eff ff es' ~> Eff ff (Each es s ++ (Scoped ff t i es r : r)))
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
f = i s
-> ((forall x. Eff ff es' x -> ScopeC ff t i es r s x)
    -> ScopeC ff t i es r s a)
-> Eff ff es' (t s a)
forall {k} (s :: k) (t :: k -> * -> *) (i :: k -> *) a
       (b :: k -> * -> *) (f :: * -> *) (es :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(Free c ff, f ~ Eff ff es, Scope t i b :> es) =>
i s -> ((forall x. f x -> b s x) -> b s a) -> f (t s a)
scope i s
i \forall x. Eff ff es' x -> ScopeC ff t i es r s x
detach -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
-> ScopeC ff t i es r s a
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
-> ScopeC ff t i fs r s a
ScopeC (Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
 -> ScopeC ff t i es r s a)
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
-> ScopeC ff t i es r s a
forall a b. (a -> b) -> a -> b
$ (Eff ff es' ~> Eff ff (Each es s ++ (Scoped ff t i es r : r)))
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
f ((Eff ff es' ~> Eff ff (Each es s ++ (Scoped ff t i es r : r)))
 -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a)
-> (Eff ff es' ~> Eff ff (Each es s ++ (Scoped ff t i es r : r)))
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) a
forall a b. (a -> b) -> a -> b
$ ScopeC ff t i es r s x
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (fs :: [k -> Effect]) (r :: [Effect]) (s :: k) a.
ScopeC ff t i fs r s a
-> Eff ff (Each fs s ++ (Scoped ff t i fs r : r)) a
unScopeC (ScopeC ff t i es r s x
 -> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x)
-> (Eff ff es' x -> ScopeC ff t i es r s x)
-> Eff ff es' x
-> Eff ff (Each es s ++ (Scoped ff t i es r : r)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff ff es' x -> ScopeC ff t i es r s x
forall x. Eff ff es' x -> ScopeC ff t i es r s x
detach
{-# INLINE scoped #-}

runScoped_
    :: forall t i a es r ff c
     . (KnownLength es, Free c ff)
    => ( forall p x
          . i p
         -> Eff ff (es ++ Scoped_ ff t i es r ': r) x
         -> Eff ff (Scoped_ ff t i es r ': r) (t p x)
       )
    -> Eff ff (Scoped_ ff t i es r ': r) a
    -> Eff ff r a
runScoped_ :: forall {k} (t :: k -> * -> *) (i :: k -> *) a (es :: [Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength es, Free c ff) =>
(forall (p :: k) x.
 i p
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
 -> Eff ff (Scoped_ ff t i es r : r) (t p x))
-> Eff ff (Scoped_ ff t i es r : r) a -> Eff ff r a
runScoped_ forall (p :: k) x.
i p
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
-> Eff ff (Scoped_ ff t i es r : r) (t p x)
run = Eff ff (Scoped_ ff t i es r : r) a -> Eff ff r a
Eff ff (Scoped_ ff t i es r : r) ~> Eff ff r
loop
  where
    loop :: Eff ff (Scoped_ ff t i es r ': r) ~> Eff ff r
    loop :: Eff ff (Scoped_ ff t i es r : r) ~> Eff ff r
loop = (Scoped_ ff t i es r ~~> Eff ff r)
-> Eff ff (Scoped_ ff t i es r : r) x -> Eff ff r x
forall (e :: Effect) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(KnownOrder e, Free c ff) =>
(e ~~> Eff ff es) -> Eff ff (e : es) a -> Eff ff es a
interpret \(Scope i s
i (forall x. Eff ff r x -> Const1 (ScopeC_ ff t i es r) s x)
-> Const1 (ScopeC_ ff t i es r) s a
f) ->
        Eff ff (Scoped_ ff t i es r : r) x -> Eff ff r x
Eff ff (Scoped_ ff t i es r : r) ~> Eff ff r
loop (Eff ff (Scoped_ ff t i es r : r) x -> Eff ff r x)
-> Eff ff (Scoped_ ff t i es r : r) x -> Eff ff r x
forall a b. (a -> b) -> a -> b
$ i s
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
-> Eff ff (Scoped_ ff t i es r : r) (t s a)
forall (p :: k) x.
i p
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
-> Eff ff (Scoped_ ff t i es r : r) (t p x)
run i s
i (ScopeC_ ff t i es r a -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
ScopeC_ ff t i es r a -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
unScopeC_ (ScopeC_ ff t i es r a
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a)
-> (Const1 (ScopeC_ ff t i es r) s a -> ScopeC_ ff t i es r a)
-> Const1 (ScopeC_ ff t i es r) s a
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const1 (ScopeC_ ff t i es r) s a -> ScopeC_ ff t i es r a
forall {k} (f :: * -> *) (x :: k) a. Const1 f x a -> f a
getConst1 (Const1 (ScopeC_ ff t i es r) s a
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a)
-> Const1 (ScopeC_ ff t i es r) s a
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
forall a b. (a -> b) -> a -> b
$ (forall x. Eff ff r x -> Const1 (ScopeC_ ff t i es r) s x)
-> Const1 (ScopeC_ ff t i es r) s a
f ((forall x. Eff ff r x -> Const1 (ScopeC_ ff t i es r) s x)
 -> Const1 (ScopeC_ ff t i es r) s a)
-> (forall x. Eff ff r x -> Const1 (ScopeC_ ff t i es r) s x)
-> Const1 (ScopeC_ ff t i es r) s a
forall a b. (a -> b) -> a -> b
$ ScopeC_ ff t i es r x -> Const1 (ScopeC_ ff t i es r) s x
forall {k} (f :: * -> *) (x :: k) a. f a -> Const1 f x a
Const1 (ScopeC_ ff t i es r x -> Const1 (ScopeC_ ff t i es r) s x)
-> (Eff ff r x -> ScopeC_ ff t i es r x)
-> Eff ff r x
-> Const1 (ScopeC_ ff t i es r) s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff ff (es ++ (Scoped_ ff t i es r : r)) x -> ScopeC_ ff t i es r x
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
Eff ff (es ++ (Scoped_ ff t i es r : r)) a -> ScopeC_ ff t i es r a
ScopeC_ (Eff ff (es ++ (Scoped_ ff t i es r : r)) x
 -> ScopeC_ ff t i es r x)
-> (Eff ff r x -> Eff ff (es ++ (Scoped_ ff t i es r : r)) x)
-> Eff ff r x
-> ScopeC_ ff t i es r x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (es' :: [Effect]) (es :: [Effect]) a (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(KnownLength es', Free c ff) =>
Eff ff es a -> Eff ff (es' ++ es) a
raisePrefix @es (Eff ff (Scoped_ ff t i es r : r) x
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) x)
-> (Eff ff r x -> Eff ff (Scoped_ ff t i es r : r) x)
-> Eff ff r x
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: Effect) (es :: [Effect]) a (ff :: Effect)
       (c :: (* -> *) -> Constraint).
Free c ff =>
Eff ff es a -> Eff ff (e : es) a
raise @(Scoped_ ff t i es r))
{-# INLINE runScoped_ #-}

runRegionScoped_
    :: forall b t i a es r ff c
     . (WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r, KnownLength es, Free c ff)
    => ( forall p x
          . i p
         -> Eff ff (es ++ Scoped_ ff t i es (RemoveExps r) ': r) x
         -> Eff ff (Scoped_ ff t i es (RemoveExps r) ': r) (t p x)
       )
    -> Eff ff (Scoped_ ff t i es (RemoveExps r) ': r) a
    -> Eff ff r a
runRegionScoped_ :: forall {k} (b :: * -> *) (t :: k -> * -> *) (i :: k -> *) a
       (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 KnownLength es, Free c ff) =>
(forall (p :: k) x.
 i p
 -> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) x
 -> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t p x))
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) a -> Eff ff r a
runRegionScoped_ forall (p :: k) x.
i p
-> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) x
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t p x)
runScope = Eff ff (Scoped_ ff t i es (RemoveExps r) : r) a -> Eff ff r a
Eff ff (Scoped_ ff t i es (RemoveExps r) : r) ~> Eff ff r
loop
  where
    loop :: Eff ff (Scoped_ ff t i es (RemoveExps r) ': r) ~> Eff ff r
    loop :: Eff ff (Scoped_ ff t i es (RemoveExps r) : r) ~> Eff ff r
loop Eff ff (Scoped_ ff t i es (RemoveExps r) : r) x
a = forall (b :: * -> *) a (f :: * -> *) (es :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(Free c ff, f ~ Eff ff es, UnliftBase b :> es) =>
((forall x. f x -> b x) -> b a) -> f a
withRunInBase @b \forall x. Eff ff r x -> b x
runInBase ->
        Eff ff r x -> b x
forall x. Eff ff r x -> b x
runInBase (Eff ff r x -> b x) -> Eff ff r x -> b x
forall a b. (a -> b) -> a -> b
$
            Eff ff (Scoped_ ff t i es (RemoveExps r) : r) x
a Eff ff (Scoped_ ff t i es (RemoveExps r) : r) x
-> (Eff ff (Scoped_ ff t i es (RemoveExps r) : r) x -> Eff ff r x)
-> Eff ff r x
forall a b. a -> (a -> b) -> b
& (Scoped_ ff t i es (RemoveExps r) ~~> Eff ff r)
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) x -> Eff ff r x
forall (e :: Effect) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(KnownOrder e, Free c ff) =>
(e ~~> Eff ff es) -> Eff ff (e : es) a -> Eff ff es a
interpret \(Scope i s
i (forall x.
 Eff ff r x -> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
f) ->
                Eff ff (Scoped_ ff t i es (RemoveExps r) : r) x -> Eff ff r x
Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t s a) -> Eff ff r x
Eff ff (Scoped_ ff t i es (RemoveExps r) : r) ~> Eff ff r
loop
                    (Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t s a)
 -> Eff ff r x)
-> (Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
    -> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t s a))
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
-> Eff ff r x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i s
-> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) a
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t s a)
forall (p :: k) x.
i p
-> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) x
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t p x)
runScope i s
i
                    (Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) a
 -> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t s a))
-> (Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
    -> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) a)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Union
   (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r))
   (Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)))
 ~> Union
      (es ++ (Scoped_ ff t i es (RemoveExps r) : r))
      (Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r))))
-> Eff
     ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) a
-> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) a
forall (es :: [Effect]) (es' :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
Free c ff =>
(Union es (Eff ff es') ~> Union es' (Eff ff es'))
-> Eff ff es a -> Eff ff es' a
transAll
                        ( 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 @es @(Scoped_ ff t i es (RemoveExps r) ': RemoveExps r)
                            (forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
Membership e es -> Membership e (es ++ es')
suffixFor @(Scoped_ ff t i es (RemoveExps r) ': r))
                            ( forall (es' :: [Effect]) (es :: [Effect]) (e :: Effect).
KnownLength es' =>
Membership e es -> Membership e (es' ++ es)
prefixFor @es @(Scoped_ ff t i es (RemoveExps r) ': r)
                                (Membership e (Scoped_ ff t i es (RemoveExps r) : r)
 -> Membership e (es ++ (Scoped_ ff t i es (RemoveExps r) : r)))
-> (Membership e (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)
    -> Membership e (Scoped_ ff t i es (RemoveExps r) : r))
-> Membership e (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)
-> Membership e (es ++ (Scoped_ ff t i es (RemoveExps r) : r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((\e :~: Scoped_ ff t i es (RemoveExps r)
Refl -> Membership e (e : r)
Membership e (Scoped_ ff t i es (RemoveExps r) : r)
forall (e :: Effect) (es :: [Effect]). Membership e (e : es)
Here) ((e :~: Scoped_ ff t i es (RemoveExps r))
 -> Membership e (Scoped_ ff t i es (RemoveExps r) : r))
-> (Membership e (RemoveExps r)
    -> Membership e (Scoped_ ff t i es (RemoveExps r) : r))
-> Membership e (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)
-> Membership e (Scoped_ ff t i es (RemoveExps r) : r)
forall (e :: Effect) (e' :: Effect) (es :: [Effect]) r.
((e :~: e') -> r)
-> (Membership e es -> r) -> Membership e (e' : es) -> r
!:> Membership e (RemoveExps r)
-> Membership e (Scoped_ ff t i es (RemoveExps r) : r)
Membership e (RemoveExps (Scoped_ ff t i es (RemoveExps r) : r))
-> Membership e (Scoped_ ff t i es (RemoveExps r) : r)
forall (es :: [Effect]) (e :: Effect).
WeakenExps es =>
Membership e (RemoveExps es) -> Membership e es
weakenExpsFor)
                            )
                        )
                    (Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) a
 -> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) a)
-> (Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
    -> Eff
         ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) a)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
-> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeC_ ff t i es (RemoveExps r) a
-> Eff
     ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) a
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
ScopeC_ ff t i es r a -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
unScopeC_
                    (ScopeC_ ff t i es (RemoveExps r) a
 -> Eff
      ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) a)
-> (Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
    -> ScopeC_ ff t i es (RemoveExps r) a)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
-> Eff
     ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
-> ScopeC_ ff t i es (RemoveExps r) a
forall {k} (f :: * -> *) (x :: k) a. Const1 f x a -> f a
getConst1
                    (Const1 (ScopeC_ ff t i es (RemoveExps r)) s a -> Eff ff r x)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a -> Eff ff r x
forall a b. (a -> b) -> a -> b
$ (forall x.
 Eff ff r x -> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
f
                    ((forall x.
  Eff ff r x -> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x)
 -> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a)
-> (forall x.
    Eff ff r x -> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x)
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s a
forall a b. (a -> b) -> a -> b
$ ScopeC_ ff t i es (RemoveExps r) x
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x
forall {k} (f :: * -> *) (x :: k) a. f a -> Const1 f x a
Const1 (ScopeC_ ff t i es (RemoveExps r) x
 -> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x)
-> (Eff ff r x -> ScopeC_ ff t i es (RemoveExps r) x)
-> Eff ff r x
-> Const1 (ScopeC_ ff t i es (RemoveExps r)) s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) x
-> ScopeC_ ff t i es (RemoveExps r) x
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
Eff ff (es ++ (Scoped_ ff t i es r : r)) a -> ScopeC_ ff t i es r a
ScopeC_ (Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) x
 -> ScopeC_ ff t i es (RemoveExps r) x)
-> (Eff ff r x
    -> Eff
         ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) x)
-> Eff ff r x
-> ScopeC_ ff t i es (RemoveExps r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (es' :: [Effect]) (es :: [Effect]) a (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(KnownLength es', Free c ff) =>
Eff ff es a -> Eff ff (es' ++ es) a
raisePrefix @es @(Scoped_ ff t i es (RemoveExps r) ': RemoveExps r) (Eff ff (Scoped_ ff t i es (RemoveExps r) : RemoveExps r) x
 -> Eff
      ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) x)
-> (Eff ff r x
    -> Eff ff (Scoped_ ff t i es (RemoveExps r) : RemoveExps r) x)
-> Eff ff r x
-> Eff
     ff (es ++ (Scoped_ ff t i es (RemoveExps r) : RemoveExps r)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b x -> Eff ff (Scoped_ ff t i es (RemoveExps r) : RemoveExps r) x
forall (f :: * -> *) (es :: [Effect]) (ff :: Effect) a
       (c :: (* -> *) -> Constraint).
(Emb f :> es, Free c ff) =>
f a -> Eff ff es a
emb (b x -> Eff ff (Scoped_ ff t i es (RemoveExps r) : RemoveExps r) x)
-> (Eff ff r x -> b x)
-> Eff ff r x
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : RemoveExps r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff ff r x -> b x
forall x. Eff ff r x -> b x
runInBase
{-# INLINE runRegionScoped_ #-}

scoped_
    :: forall t i s a es' es r ff c
     . (Scoped_ ff t i es r :> es', Free c ff)
    => i s
    -> ( Eff ff es' ~> Eff ff (es ++ Scoped_ ff t i es r ': r)
         -> Eff ff (es ++ Scoped_ ff t i es r ': r) a
       )
    -> Eff ff es' (t s a)
scoped_ :: forall {k} (t :: k -> * -> *) (i :: k -> *) (s :: k) a
       (es' :: [Effect]) (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(Scoped_ ff t i es r :> es', Free c ff) =>
i s
-> ((Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
    -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a)
-> Eff ff es' (t s a)
scoped_ i s
i (Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
f = i s
-> ((forall x. Eff ff es' x -> Const1 (ScopeC_ ff t i es r) s x)
    -> Const1 (ScopeC_ ff t i es r) s a)
-> Eff ff es' (t s a)
forall {k} (s :: k) (t :: k -> * -> *) (i :: k -> *) a
       (b :: k -> * -> *) (f :: * -> *) (es :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(Free c ff, f ~ Eff ff es, Scope t i b :> es) =>
i s -> ((forall x. f x -> b s x) -> b s a) -> f (t s a)
scope i s
i \forall x. Eff ff es' x -> Const1 (ScopeC_ ff t i es r) s x
pop -> ScopeC_ ff t i es r a -> Const1 (ScopeC_ ff t i es r) s a
forall {k} (f :: * -> *) (x :: k) a. f a -> Const1 f x a
Const1 (ScopeC_ ff t i es r a -> Const1 (ScopeC_ ff t i es r) s a)
-> ScopeC_ ff t i es r a -> Const1 (ScopeC_ ff t i es r) s a
forall a b. (a -> b) -> a -> b
$ Eff ff (es ++ (Scoped_ ff t i es r : r)) a -> ScopeC_ ff t i es r a
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
Eff ff (es ++ (Scoped_ ff t i es r : r)) a -> ScopeC_ ff t i es r a
ScopeC_ (Eff ff (es ++ (Scoped_ ff t i es r : r)) a
 -> ScopeC_ ff t i es r a)
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
-> ScopeC_ ff t i es r a
forall a b. (a -> b) -> a -> b
$ (Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
f ((Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a)
-> (Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
forall a b. (a -> b) -> a -> b
$ ScopeC_ ff t i es r x -> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
forall {k} (ff :: Effect) (t :: k -> * -> *) (i :: k -> *)
       (es :: [Effect]) (r :: [Effect]) a.
ScopeC_ ff t i es r a -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a
unScopeC_ (ScopeC_ ff t i es r x
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) x)
-> (Eff ff es' x -> ScopeC_ ff t i es r x)
-> Eff ff es' x
-> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const1 (ScopeC_ ff t i es r) s x -> ScopeC_ ff t i es r x
forall {k} (f :: * -> *) (x :: k) a. Const1 f x a -> f a
getConst1 (Const1 (ScopeC_ ff t i es r) s x -> ScopeC_ ff t i es r x)
-> (Eff ff es' x -> Const1 (ScopeC_ ff t i es r) s x)
-> Eff ff es' x
-> ScopeC_ ff t i es r x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff ff es' x -> Const1 (ScopeC_ ff t i es r) s x
forall x. Eff ff es' x -> Const1 (ScopeC_ ff t i es r) s x
pop
{-# INLINE scoped_ #-}

runProvider
    :: forall t i a es r ff c
     . (forall es'. Functor (Eff ff es'), KnownLength es, Free c ff)
    => ( forall x
          . i
         -> Eff ff (es ++ Provider ff t i es r ': r) x
         -> Eff ff (Provider ff t i es r ': r) (t x)
       )
    -> Eff ff (Provider ff t i es r ': r) a
    -> Eff ff r a
runProvider :: forall (t :: * -> *) i a (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff t i es r : r)) x
 -> Eff ff (Provider ff t i es r : r) (t x))
-> Eff ff (Provider ff t i es r : r) a -> Eff ff r a
runProvider forall x.
i
-> Eff ff (es ++ (Provider ff t i es r : r)) x
-> Eff ff (Provider ff t i es r : r) (t x)
run = (forall (p :: ()) x.
 Const i p
 -> Eff ff (es ++ (Provider ff t i es r : r)) x
 -> Eff ff (Provider ff t i es r : r) (Const1 t p x))
-> Eff ff (Provider ff t i es r : r) a -> Eff ff r a
forall {k} (t :: k -> * -> *) (i :: k -> *) a (es :: [Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(KnownLength es, Free c ff) =>
(forall (p :: k) x.
 i p
 -> Eff ff (es ++ (Scoped_ ff t i es r : r)) x
 -> Eff ff (Scoped_ ff t i es r : r) (t p x))
-> Eff ff (Scoped_ ff t i es r : r) a -> Eff ff r a
runScoped_ \(Const i
i) Eff ff (es ++ (Provider ff t i es r : r)) x
a -> t x -> Const1 t p x
forall {k} (f :: * -> *) (x :: k) a. f a -> Const1 f x a
Const1 (t x -> Const1 t p x)
-> Eff ff (Provider ff t i es r : r) (t x)
-> Eff ff (Provider ff t i es r : r) (Const1 t p x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i
-> Eff ff (es ++ (Provider ff t i es r : r)) x
-> Eff ff (Provider ff t i es r : r) (t x)
forall x.
i
-> Eff ff (es ++ (Provider ff t i es r : r)) x
-> Eff ff (Provider ff t i es r : r) (t x)
run i
i Eff ff (es ++ (Provider ff t i es r : r)) x
a
{-# INLINE runProvider #-}

runRegionProvider
    :: forall b t i a es r ff c
     . ( WeakenExps r
       , UnliftBase b :> r
       , Emb b :> RemoveExps r
       , forall es'. Functor (Eff ff es')
       , KnownLength es
       , Free c ff
       )
    => ( forall x
          . i
         -> Eff ff (es ++ Provider ff t i es (RemoveExps r) ': r) x
         -> Eff ff (Provider ff t i es (RemoveExps r) ': r) (t x)
       )
    -> Eff ff (Provider ff t i es (RemoveExps r) ': r) a
    -> Eff ff r a
runRegionProvider :: forall (b :: * -> *) (t :: * -> *) i a (es :: [Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
 -> Eff ff (Provider ff t i es (RemoveExps r) : r) (t x))
-> Eff ff (Provider ff t i es (RemoveExps r) : r) a -> Eff ff r a
runRegionProvider forall x.
i
-> Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
-> Eff ff (Provider ff t i es (RemoveExps r) : r) (t x)
run = forall {k} (b :: * -> *) (t :: k -> * -> *) (i :: k -> *) a
       (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 KnownLength es, Free c ff) =>
(forall (p :: k) x.
 i p
 -> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) x
 -> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t p x))
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) a -> Eff ff r a
forall (b :: * -> *) (t :: () -> * -> *) (i :: () -> *) a
       (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 KnownLength es, Free c ff) =>
(forall (p :: ()) x.
 i p
 -> Eff ff (es ++ (Scoped_ ff t i es (RemoveExps r) : r)) x
 -> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) (t p x))
-> Eff ff (Scoped_ ff t i es (RemoveExps r) : r) a -> Eff ff r a
runRegionScoped_ @b \(Const i
i) Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
a -> t x -> Const1 t p x
forall {k} (f :: * -> *) (x :: k) a. f a -> Const1 f x a
Const1 (t x -> Const1 t p x)
-> Eff ff (Provider ff t i es (RemoveExps r) : r) (t x)
-> Eff ff (Provider ff t i es (RemoveExps r) : r) (Const1 t p x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i
-> Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
-> Eff ff (Provider ff t i es (RemoveExps r) : r) (t x)
forall x.
i
-> Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
-> Eff ff (Provider ff t i es (RemoveExps r) : r) (t x)
run i
i Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
a
{-# INLINE runRegionProvider #-}

provide
    :: forall t i a es' es r ff c
     . (Provider ff t i es r :> es', forall es''. Functor (Eff ff es''), Free c ff)
    => i
    -> ( Eff ff es' ~> Eff ff (es ++ Provider ff t i es r ': r)
         -> Eff ff (es ++ Provider ff t i es r ': r) a
       )
    -> Eff ff es' (t a)
provide :: forall (t :: * -> *) i a (es' :: [Effect]) (es :: [Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(Provider ff t i es r :> es',
 forall (es'' :: [Effect]). Functor (Eff ff es''), Free c ff) =>
i
-> ((Eff ff es' ~> Eff ff (es ++ (Provider ff t i es r : r)))
    -> Eff ff (es ++ (Provider ff t i es r : r)) a)
-> Eff ff es' (t a)
provide i
i (Eff ff es' ~> Eff ff (es ++ (Provider ff t i es r : r)))
-> Eff ff (es ++ (Provider ff t i es r : r)) a
f = Const1 t '() a -> t a
forall {k} (f :: * -> *) (x :: k) a. Const1 f x a -> f a
getConst1 (Const1 t '() a -> t a)
-> Eff ff es' (Const1 t '() a) -> Eff ff es' (t a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (t :: k -> * -> *) (i :: k -> *) (s :: k) a
       (es' :: [Effect]) (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(Scoped_ ff t i es r :> es', Free c ff) =>
i s
-> ((Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
    -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a)
-> Eff ff es' (t s a)
forall (t :: () -> * -> *) (i :: () -> *) (s :: ()) a
       (es' :: [Effect]) (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(Scoped_ ff t i es r :> es', Free c ff) =>
i s
-> ((Eff ff es' ~> Eff ff (es ++ (Scoped_ ff t i es r : r)))
    -> Eff ff (es ++ (Scoped_ ff t i es r : r)) a)
-> Eff ff es' (t s a)
scoped_ @_ @_ @'() (i -> Const i '()
forall {k} a (b :: k). a -> Const a b
Const i
i) (Eff ff es' ~> Eff ff (es ++ (Provider ff t i es r : r)))
-> Eff ff (es ++ (Provider ff t i es r : r)) a
f
{-# INLINE provide #-}

runProvider_
    :: forall i a es r ff c
     . (forall es'. Functor (Eff ff es'), KnownLength es, Free c ff)
    => ( forall x
          . i
         -> Eff ff (es ++ Provider ff Identity i es r ': r) x
         -> Eff ff (Provider ff Identity i es r ': r) x
       )
    -> Eff ff (Provider ff Identity i es r ': r) a
    -> Eff ff r a
runProvider_ :: forall i a (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff Identity i es r : r)) x
 -> Eff ff (Provider ff Identity i es r : r) x)
-> Eff ff (Provider ff Identity i es r : r) a -> Eff ff r a
runProvider_ forall x.
i
-> Eff ff (es ++ (Provider ff Identity i es r : r)) x
-> Eff ff (Provider ff Identity i es r : r) x
run = (forall x.
 i
 -> Eff ff (es ++ (Provider ff Identity i es r : r)) x
 -> Eff ff (Provider ff Identity i es r : r) (Identity x))
-> Eff ff (Provider ff Identity i es r : r) a -> Eff ff r a
forall (t :: * -> *) i a (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff t i es r : r)) x
 -> Eff ff (Provider ff t i es r : r) (t x))
-> Eff ff (Provider ff t i es r : r) a -> Eff ff r a
runProvider \i
i Eff ff (es ++ (Provider ff Identity i es r : r)) x
a -> x -> Identity x
forall a. a -> Identity a
Identity (x -> Identity x)
-> Eff ff (Provider ff Identity i es r : r) x
-> Eff ff (Provider ff Identity i es r : r) (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i
-> Eff ff (es ++ (Provider ff Identity i es r : r)) x
-> Eff ff (Provider ff Identity i es r : r) x
forall x.
i
-> Eff ff (es ++ (Provider ff Identity i es r : r)) x
-> Eff ff (Provider ff Identity i es r : r) x
run i
i Eff ff (es ++ (Provider ff Identity i es r : r)) x
a
{-# INLINE runProvider_ #-}

runRegionProvider_
    :: forall b i a es r ff c
     . ( WeakenExps r
       , UnliftBase b :> r
       , Emb b :> RemoveExps r
       , forall es'. Functor (Eff ff es')
       , KnownLength es
       , Free c ff
       )
    => ( forall x
          . i
         -> Eff ff (es ++ Provider ff Identity i es (RemoveExps r) ': r) x
         -> Eff ff (Provider ff Identity i es (RemoveExps r) ': r) x
       )
    -> Eff ff (Provider ff Identity i es (RemoveExps r) ': r) a
    -> Eff ff r a
runRegionProvider_ :: forall (b :: * -> *) i a (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
 -> Eff ff (Provider ff Identity i es (RemoveExps r) : r) x)
-> Eff ff (Provider ff Identity i es (RemoveExps r) : r) a
-> Eff ff r a
runRegionProvider_ forall x.
i
-> Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
-> Eff ff (Provider ff Identity i es (RemoveExps r) : r) x
run = forall (b :: * -> *) (t :: * -> *) i a (es :: [Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff t i es (RemoveExps r) : r)) x
 -> Eff ff (Provider ff t i es (RemoveExps r) : r) (t x))
-> Eff ff (Provider ff t i es (RemoveExps r) : r) a -> Eff ff r a
runRegionProvider @b \i
i Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
a -> x -> Identity x
forall a. a -> Identity a
Identity (x -> Identity x)
-> Eff ff (Provider ff Identity i es (RemoveExps r) : r) x
-> Eff
     ff (Provider ff Identity i es (RemoveExps r) : r) (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i
-> Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
-> Eff ff (Provider ff Identity i es (RemoveExps r) : r) x
forall x.
i
-> Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
-> Eff ff (Provider ff Identity i es (RemoveExps r) : r) x
run i
i Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
a
{-# INLINE runRegionProvider_ #-}

provide_
    :: forall i a es' es r ff c
     . (Provider ff Identity i es r :> es', forall es''. Functor (Eff ff es''), Free c ff)
    => i
    -> ( Eff ff es' ~> Eff ff (es ++ Provider ff Identity i es r ': r)
         -> Eff ff (es ++ Provider ff Identity i es r ': r) a
       )
    -> Eff ff es' a
provide_ :: forall i a (es' :: [Effect]) (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(Provider ff Identity i es r :> es',
 forall (es'' :: [Effect]). Functor (Eff ff es''), Free c ff) =>
i
-> ((Eff ff es'
     ~> Eff ff (es ++ (Provider ff Identity i es r : r)))
    -> Eff ff (es ++ (Provider ff Identity i es r : r)) a)
-> Eff ff es' a
provide_ i
i (Eff ff es' ~> Eff ff (es ++ (Provider ff Identity i es r : r)))
-> Eff ff (es ++ (Provider ff Identity i es r : r)) a
f = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Eff ff es' (Identity a) -> Eff ff es' a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> i
-> ((Eff ff es'
     ~> Eff ff (es ++ (Provider ff Identity i es r : r)))
    -> Eff ff (es ++ (Provider ff Identity i es r : r)) a)
-> Eff ff es' (Identity a)
forall (t :: * -> *) i a (es' :: [Effect]) (es :: [Effect])
       (r :: [Effect]) (ff :: Effect) (c :: (* -> *) -> Constraint).
(Provider ff t i es r :> es',
 forall (es'' :: [Effect]). Functor (Eff ff es''), Free c ff) =>
i
-> ((Eff ff es' ~> Eff ff (es ++ (Provider ff t i es r : r)))
    -> Eff ff (es ++ (Provider ff t i es r : r)) a)
-> Eff ff es' (t a)
provide i
i (Eff ff es' ~> Eff ff (es ++ (Provider ff Identity i es r : r)))
-> Eff ff (es ++ (Provider ff Identity i es r : r)) a
f
{-# INLINE provide_ #-}

runProvider__
    :: forall a es r ff c
     . (forall es'. Functor (Eff ff es'), KnownLength es, Free c ff)
    => ( forall x
          . Eff ff (es ++ Provider ff Identity () es r ': r) x
         -> Eff ff (Provider ff Identity () es r ': r) x
       )
    -> Eff ff (Provider ff Identity () es r ': r) a
    -> Eff ff r a
runProvider__ :: forall a (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 Eff ff (es ++ (Provider ff Identity () es r : r)) x
 -> Eff ff (Provider ff Identity () es r : r) x)
-> Eff ff (Provider ff Identity () es r : r) a -> Eff ff r a
runProvider__ forall x.
Eff ff (es ++ (Provider ff Identity () es r : r)) x
-> Eff ff (Provider ff Identity () es r : r) x
run = (forall x.
 ()
 -> Eff ff (es ++ (Provider ff Identity () es r : r)) x
 -> Eff ff (Provider ff Identity () es r : r) x)
-> Eff ff (Provider ff Identity () es r : r) a -> Eff ff r a
forall i a (es :: [Effect]) (r :: [Effect]) (ff :: Effect)
       (c :: (* -> *) -> Constraint).
(forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff Identity i es r : r)) x
 -> Eff ff (Provider ff Identity i es r : r) x)
-> Eff ff (Provider ff Identity i es r : r) a -> Eff ff r a
runProvider_ \() -> Eff ff (es ++ (Provider ff Identity () es r : r)) x
-> Eff ff (Provider ff Identity () es r : r) x
forall x.
Eff ff (es ++ (Provider ff Identity () es r : r)) x
-> Eff ff (Provider ff Identity () es r : r) x
run
{-# INLINE runProvider__ #-}

runRegionProvider__
    :: forall b a es r ff c
     . ( WeakenExps r
       , UnliftBase b :> r
       , Emb b :> RemoveExps r
       , forall es'. Functor (Eff ff es')
       , KnownLength es
       , Free c ff
       )
    => ( forall x
          . Eff ff (es ++ Provider ff Identity () es (RemoveExps r) ': r) x
         -> Eff ff (Provider ff Identity () es (RemoveExps r) ': r) x
       )
    -> Eff ff (Provider ff Identity () es (RemoveExps r) ': r) a
    -> Eff ff r a
runRegionProvider__ :: forall (b :: * -> *) a (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 Eff ff (es ++ (Provider ff Identity () es (RemoveExps r) : r)) x
 -> Eff ff (Provider ff Identity () es (RemoveExps r) : r) x)
-> Eff ff (Provider ff Identity () es (RemoveExps r) : r) a
-> Eff ff r a
runRegionProvider__ forall x.
Eff ff (es ++ (Provider ff Identity () es (RemoveExps r) : r)) x
-> Eff ff (Provider ff Identity () es (RemoveExps r) : r) x
run = forall (b :: * -> *) i a (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(WeakenExps r, UnliftBase b :> r, Emb b :> RemoveExps r,
 forall (es' :: [Effect]). Functor (Eff ff es'), KnownLength es,
 Free c ff) =>
(forall x.
 i
 -> Eff ff (es ++ (Provider ff Identity i es (RemoveExps r) : r)) x
 -> Eff ff (Provider ff Identity i es (RemoveExps r) : r) x)
-> Eff ff (Provider ff Identity i es (RemoveExps r) : r) a
-> Eff ff r a
runRegionProvider_ @b \() -> Eff ff (es ++ (Provider ff Identity () es (RemoveExps r) : r)) x
-> Eff ff (Provider ff Identity () es (RemoveExps r) : r) x
forall x.
Eff ff (es ++ (Provider ff Identity () es (RemoveExps r) : r)) x
-> Eff ff (Provider ff Identity () es (RemoveExps r) : r) x
run
{-# INLINE runRegionProvider__ #-}

provide__
    :: forall a es' es r ff c
     . (Provider ff Identity () es r :> es', forall es''. Functor (Eff ff es''), Free c ff)
    => ( Eff ff es' ~> Eff ff (es ++ Provider ff Identity () es r ': r)
         -> Eff ff (es ++ Provider ff Identity () es r ': r) a
       )
    -> Eff ff es' a
provide__ :: forall a (es' :: [Effect]) (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(Provider ff Identity () es r :> es',
 forall (es'' :: [Effect]). Functor (Eff ff es''), Free c ff) =>
((Eff ff es' ~> Eff ff (es ++ (Provider ff Identity () es r : r)))
 -> Eff ff (es ++ (Provider ff Identity () es r : r)) a)
-> Eff ff es' a
provide__ = ()
-> ((forall {x}.
     Eff ff es' x
     -> Eff ff (es ++ (Provider ff Identity () es r : r)) x)
    -> Eff ff (es ++ (Provider ff Identity () es r : r)) a)
-> Eff ff es' a
forall i a (es' :: [Effect]) (es :: [Effect]) (r :: [Effect])
       (ff :: Effect) (c :: (* -> *) -> Constraint).
(Provider ff Identity i es r :> es',
 forall (es'' :: [Effect]). Functor (Eff ff es''), Free c ff) =>
i
-> ((Eff ff es'
     ~> Eff ff (es ++ (Provider ff Identity i es r : r)))
    -> Eff ff (es ++ (Provider ff Identity i es r : r)) a)
-> Eff ff es' a
provide_ ()
{-# INLINE provide__ #-}