{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

-- 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.Transform (raise, raisePrefix, raisePrefix1)
import Data.Effect.OpenUnion (Each, KnownLength, type (++))
import Data.Functor.Const (Const (Const))
import Data.Functor.Identity (Identity (Identity), runIdentity)

-- | 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 #-}

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_ #-}

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 #-}

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_ #-}

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__ #-}

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__ #-}