-- SPDX-License-Identifier: MPL-2.0

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

Interpreters for the [Provider]("Data.Effect.Provider") effects.
-}
module Control.Monad.Hefty.Provider (
    module Control.Monad.Hefty.Provider,
    module Data.Effect.Provider,
)
where

import Control.Monad.Hefty (
    Eff,
    HFunctor,
    KeyH (KeyH),
    MemberHBy,
    Type,
    interpretH,
    key,
    keyH,
    transEffHF,
    unkey,
    unkeyH,
    weaken,
    weakenNH,
    type (##>),
    type (#>),
    type (~>),
 )
import Data.Effect.Provider
import Data.Functor.Const (Const (Const))
import Data.Functor.Identity (Identity (Identity))

type Provide ctx i sh sf eh ef = Provider ctx i (ProviderEff ctx i sh sf eh ef)

newtype ProviderEff ctx i sh sf eh ef p a
    = ProviderEff {forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
ProviderEff ctx i sh sf eh ef p a
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
unProviderEff :: Eff (sh p ': Provide ctx i sh sf eh ef ': eh) (sf p ': ef) a}

type Provide_ i sh sf eh ef =
    Provider (Const1 Identity) (Const i :: () -> Type) (Const1 (ProviderEff_ i sh sf eh ef))

newtype ProviderEff_ i sh sf eh ef a
    = ProviderEff_ {forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]) a.
ProviderEff_ i sh sf eh ef a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
unProviderEff_ :: Eff (sh ': Provide_ i sh sf eh ef ': eh) (sf ': ef) a}

-- | Interpret the t'Provider' effect using the given effect interpreter.
runProvider
    :: forall ctx i sh sf eh ef
     . ( forall p x
          . i p
         -> Eff (sh p ': Provide ctx i sh sf eh ef ': eh) (sf p ': ef) x
         -> Eff (Provide ctx i sh sf eh ef ': eh) ef (ctx p x)
       )
    -> Eff (Provide ctx i sh sf eh ef ': eh) ef ~> Eff eh ef
runProvider :: forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]).
(forall (p :: k) x.
 i p
 -> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
 -> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x))
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
run =
    (Provide ctx i sh sf eh ef ~~> Eff eh ef)
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH \(KeyH (Provide i p
i (forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1
f)) ->
        (forall (p :: k) x.
 i p
 -> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
 -> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x))
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]).
(forall (p :: k) x.
 i p
 -> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
 -> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x))
-> Eff (Provide ctx i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
run (Eff (Provide ctx i sh sf eh ef : eh) ef x -> Eff eh ef x)
-> Eff (Provide ctx i sh sf eh ef : eh) ef x -> Eff eh ef x
forall a b. (a -> b) -> a -> b
$
            i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p a1)
forall (p :: k) x.
i p
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> Eff (Provide ctx i sh sf eh ef : eh) ef (ctx p x)
run i p
i (ProviderEff ctx i sh sf eh ef p a1
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
ProviderEff ctx i sh sf eh ef p a
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
unProviderEff (ProviderEff ctx i sh sf eh ef p a1
 -> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1)
-> ProviderEff ctx i sh sf eh ef p a1
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a1
forall a b. (a -> b) -> a -> b
$ (forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1
f ((forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
 -> ProviderEff ctx i sh sf eh ef p a1)
-> (forall x. Eff eh ef x -> ProviderEff ctx i sh sf eh ef p x)
-> ProviderEff ctx i sh sf eh ef p a1
forall a b. (a -> b) -> a -> b
$ Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
-> ProviderEff ctx i sh sf eh ef p x
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
-> ProviderEff ctx i sh sf eh ef p a
ProviderEff (Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x
 -> ProviderEff ctx i sh sf eh ef p x)
-> (Eff eh ef x
    -> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) x)
-> Eff eh ef x
-> ProviderEff ctx i sh sf eh ef p x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnionH
   eh (Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef))
 ~> UnionH
      (sh p : Provide ctx i sh sf eh ef : eh)
      (Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef)))
-> (Union ef ~> Union (sf p : ef))
-> Eff eh ef
   ~> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef)
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *])
       (ef' :: [* -> *]).
(UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
-> (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh' ef'
transEffHF (forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
       (f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH @2) Union ef x -> Union (sf p : ef) x
Union ef ~> Union (sf p : ef)
forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken)

{- |
Interpret the t'Provider' effect using the given effect interpreter.
A version of 'runProvider' where the type of t'Provider' is simpler.
-}
runProvider_
    :: forall i sh sf eh ef
     . (HFunctor sh)
    => ( forall x
          . i
         -> Eff (sh ': Provide_ i sh sf eh ef ': eh) (sf ': ef) x
         -> Eff (Provide_ i sh sf eh ef ': eh) ef x
       )
    -> Eff (Provide_ i sh sf eh ef ': eh) ef ~> Eff eh ef
runProvider_ :: forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor sh =>
(forall x.
 i
 -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
 -> Eff (Provide_ i sh sf eh ef : eh) ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider_ forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
run =
    (Provide_ i sh sf eh ef ~~> Eff eh ef)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH \(KeyH (Provide (Const i
i) (forall x. Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
f)) ->
        (forall x.
 i
 -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
 -> Eff (Provide_ i sh sf eh ef : eh) ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor sh =>
(forall x.
 i
 -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
 -> Eff (Provide_ i sh sf eh ef : eh) ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef ~> Eff eh ef
runProvider_ i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
run (Eff (Provide_ i sh sf eh ef : eh) ef x -> Eff eh ef x)
-> Eff (Provide_ i sh sf eh ef : eh) ef x -> Eff eh ef x
forall a b. (a -> b) -> a -> b
$
            i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
forall x.
i
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> Eff (Provide_ i sh sf eh ef : eh) ef x
run
                i
i
                ( (a1 -> x)
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
forall a b.
(a -> b)
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Identity a1 -> x
Identity a1 -> Const1 Identity p a1
forall {k} {k1} (f :: k -> *) (x :: k1) (a :: k).
f a -> Const1 f x a
Const1 (Identity a1 -> x) -> (a1 -> Identity a1) -> a1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a1 -> Identity a1
forall a. a -> Identity a
Identity)
                    (Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
 -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x)
-> (Const1 (ProviderEff_ i sh sf eh ef) p a1
    -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderEff_ i sh sf eh ef a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]) a.
ProviderEff_ i sh sf eh ef a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
unProviderEff_
                    (ProviderEff_ i sh sf eh ef a1
 -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1)
-> (Const1 (ProviderEff_ i sh sf eh ef) p a1
    -> ProviderEff_ i sh sf eh ef a1)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const1 (ProviderEff_ i sh sf eh ef) p a1
-> ProviderEff_ i sh sf eh ef a1
forall {k1} {k2} (f :: k1 -> *) (x :: k2) (a :: k1).
Const1 f x a -> f a
getConst1
                    (Const1 (ProviderEff_ i sh sf eh ef) p a1
 -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
forall a b. (a -> b) -> a -> b
$ (forall x. Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
f
                    ((forall x. Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
 -> Const1 (ProviderEff_ i sh sf eh ef) p a1)
-> (forall x.
    Eff eh ef x -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> Const1 (ProviderEff_ i sh sf eh ef) p a1
forall a b. (a -> b) -> a -> b
$ ProviderEff_ i sh sf eh ef x
-> Const1 (ProviderEff_ i sh sf eh ef) p x
forall {k} {k1} (f :: k -> *) (x :: k1) (a :: k).
f a -> Const1 f x a
Const1
                        (ProviderEff_ i sh sf eh ef x
 -> Const1 (ProviderEff_ i sh sf eh ef) p x)
-> (Eff eh ef x -> ProviderEff_ i sh sf eh ef x)
-> Eff eh ef x
-> Const1 (ProviderEff_ i sh sf eh ef) p x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
-> ProviderEff_ i sh sf eh ef x
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]) a.
Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
-> ProviderEff_ i sh sf eh ef a
ProviderEff_
                        (Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x
 -> ProviderEff_ i sh sf eh ef x)
-> (Eff eh ef x
    -> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) x)
-> Eff eh ef x
-> ProviderEff_ i sh sf eh ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UnionH eh (Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef))
 ~> UnionH
      (sh : Provide_ i sh sf eh ef : eh)
      (Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef)))
-> (Union ef ~> Union (sf : ef))
-> Eff eh ef ~> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef)
forall (eh :: [EffectH]) (eh' :: [EffectH]) (ef :: [* -> *])
       (ef' :: [* -> *]).
(UnionH eh (Eff eh' ef') ~> UnionH eh' (Eff eh' ef'))
-> (Union ef ~> Union ef') -> Eff eh ef ~> Eff eh' ef'
transEffHF (forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
       (f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH @2) Union ef x -> Union (sf : ef) x
Union ef ~> Union (sf : ef)
forall (any :: * -> *) (es :: [* -> *]) a.
Union es a -> Union (any : es) a
weaken
                )

-- | Introduces a new local scope that provides effects @sh p@ and @sf p@ parameterized by @i p@ value and with results wrapped in @ctx p@.
scope
    :: forall key ctx i p eh ef a sh sf bh bf
     . ( MemberHBy
            (ProviderKey ctx i)
            (Provider' ctx i (ProviderEff ctx i sh sf bh bf))
            eh
       , HFunctor (sh p)
       )
    => i p
    -> ( Eff eh ef ~> Eff (key ##> sh p ': Provide ctx i sh sf bh bf ': bh) (key #> sf p ': bf)
         -> Eff (key ##> sh p ': Provide ctx i sh sf bh bf ': bh) (key #> sf p ': bf) a
       )
    -> Eff eh ef (ctx p a)
scope :: forall {k} {k} (key :: k) (ctx :: k -> * -> *) (i :: k -> *)
       (p :: k) (eh :: [EffectH]) (ef :: [* -> *]) a (sh :: k -> EffectH)
       (sf :: k -> * -> *) (bh :: [EffectH]) (bf :: [* -> *]).
(MemberHBy
   (ProviderKey ctx i)
   (Provider' ctx i (ProviderEff ctx i sh sf bh bf))
   eh,
 HFunctor (sh p)) =>
i p
-> ((Eff eh ef
     ~> Eff
          ((key ##> sh p) : Provide ctx i sh sf bh bf : bh)
          ((key #> sf p) : bf))
    -> Eff
         ((key ##> sh p) : Provide ctx i sh sf bh bf : bh)
         ((key #> sf p) : bf)
         a)
-> Eff eh ef (ctx p a)
scope i p
i (Eff eh ef
 ~> Eff
      ((key ##> sh p)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      ((key #> sf p) : bf))
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     a
f =
    i p
i i p
-> ((Eff eh ef ~> ProviderEff ctx i sh sf bh bf p)
    -> ProviderEff ctx i sh sf bh bf p a)
-> Eff eh ef (ctx p a)
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (p :: k)
       (f :: * -> *) a (b :: k -> * -> *).
SendHOEBy (ProviderKey ctx i) (Provider' ctx i b) f =>
i p -> ((f ~> b p) -> b p a) -> f (ctx p a)
..! \Eff eh ef ~> ProviderEff ctx i sh sf bh bf p
runInScope ->
        Eff
  (sh p
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  (sf p : bf)
  a
-> ProviderEff ctx i sh sf bh bf p a
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
-> ProviderEff ctx i sh sf eh ef p a
ProviderEff (Eff
   (sh p
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
      : bh)
   (sf p : bf)
   a
 -> ProviderEff ctx i sh sf bh bf p a)
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     a
-> ProviderEff ctx i sh sf bh bf p a
forall a b. (a -> b) -> a -> b
$ Eff
  ((key ##> sh p)
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  (sf p : bf)
  a
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     a
Eff
  ((key ##> sh p)
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  (sf p : bf)
~> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
forall {k} (key :: k) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
Eff ((key ##> e) : eh) ef ~> Eff (e : eh) ef
unkeyH (Eff
   ((key ##> sh p)
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
      : bh)
   (sf p : bf)
   a
 -> Eff
      (sh p
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      (sf p : bf)
      a)
-> (Eff
      ((key ##> sh p)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      ((key #> sf p) : bf)
      a
    -> Eff
         ((key ##> sh p)
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
            : bh)
         (sf p : bf)
         a)
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     a
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  ((key ##> sh p)
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  ((key #> sf p) : bf)
  a
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     a
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh ((key #> e) : ef) x -> Eff eh (e : ef) x
unkey (Eff
   ((key ##> sh p)
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
      : bh)
   ((key #> sf p) : bf)
   a
 -> Eff
      (sh p
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      (sf p : bf)
      a)
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     a
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     a
forall a b. (a -> b) -> a -> b
$ (Eff eh ef
 ~> Eff
      ((key ##> sh p)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      ((key #> sf p) : bf))
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     a
f (Eff
  (sh p
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  ((key #> sf p) : bf)
  x
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     x
Eff
  (sh p
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  ((key #> sf p) : bf)
~> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
forall {k} (key :: k) (e :: EffectH) (ef :: [* -> *])
       (eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((key ##> e) : eh) ef
keyH (Eff
   (sh p
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
      : bh)
   ((key #> sf p) : bf)
   x
 -> Eff
      ((key ##> sh p)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      ((key #> sf p) : bf)
      x)
-> (Eff eh ef x
    -> Eff
         (sh p
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
            : bh)
         ((key #> sf p) : bf)
         x)
-> Eff eh ef x
-> Eff
     ((key ##> sh p)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  (sh p
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
     : bh)
  (sf p : bf)
  x
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     x
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((key #> e) : ef) x
key (Eff
   (sh p
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
      : bh)
   (sf p : bf)
   x
 -> Eff
      (sh p
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      ((key #> sf p) : bf)
      x)
-> (Eff eh ef x
    -> Eff
         (sh p
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
            : bh)
         (sf p : bf)
         x)
-> Eff eh ef x
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     ((key #> sf p) : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderEff ctx i sh sf bh bf p x
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     x
forall {k} (ctx :: k -> * -> *) (i :: k -> *) (sh :: k -> EffectH)
       (sf :: k -> * -> *) (eh :: [EffectH]) (ef :: [* -> *]) (p :: k) a.
ProviderEff ctx i sh sf eh ef p a
-> Eff (sh p : Provide ctx i sh sf eh ef : eh) (sf p : ef) a
unProviderEff (ProviderEff ctx i sh sf bh bf p x
 -> Eff
      (sh p
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
         : bh)
      (sf p : bf)
      x)
-> (Eff eh ef x -> ProviderEff ctx i sh sf bh bf p x)
-> Eff eh ef x
-> Eff
     (sh p
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderEff ctx i sh sf bh bf))
        : bh)
     (sf p : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff eh ef x -> ProviderEff ctx i sh sf bh bf p x
Eff eh ef ~> ProviderEff ctx i sh sf bh bf p
runInScope)

-- | Introduces a new local scope that provides effects @sh@ and @sf@ parameterized by @i@ value.
scope_
    :: forall key i eh ef a sh sf bh bf
     . ( MemberHBy
            (ProviderKey (Const1 Identity :: () -> Type -> Type) (Const i :: () -> Type))
            ( Provider'
                (Const1 Identity)
                (Const i)
                (Const1 (ProviderEff_ i sh sf bh bf))
            )
            eh
       , HFunctor sh
       )
    => i
    -> ( Eff eh ef ~> Eff (key ##> sh ': Provide_ i sh sf bh bf ': bh) (key #> sf ': bf)
         -> Eff (key ##> sh ': Provide_ i sh sf bh bf ': bh) (key #> sf ': bf) a
       )
    -> Eff eh ef a
scope_ :: forall {k} {k} (key :: k) i (eh :: [EffectH]) (ef :: [* -> *]) a
       (sh :: EffectH) (sf :: * -> *) (bh :: [EffectH]) (bf :: [* -> *]).
(MemberHBy
   (ProviderKey (Const1 Identity) (Const i))
   (Provider'
      (Const1 Identity) (Const i) (Const1 (ProviderEff_ i sh sf bh bf)))
   eh,
 HFunctor sh) =>
i
-> ((Eff eh ef
     ~> Eff
          ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf))
    -> Eff
         ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a)
-> Eff eh ef a
scope_ i
i (Eff eh ef
 ~> Eff
      ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf))
-> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
f =
    i
i i
-> ((Eff eh ef ~> ProviderEff_ i sh sf bh bf)
    -> ProviderEff_ i sh sf bh bf a)
-> Eff eh ef a
forall {k} i (f :: * -> *) a (b :: * -> *).
(SendHOEBy
   (ProviderKey (Const1 Identity) (Const i))
   (Provider' (Const1 Identity) (Const i) (Const1 b))
   f,
 Functor f) =>
i -> ((f ~> b) -> b a) -> f a
.! \Eff eh ef ~> ProviderEff_ i sh sf bh bf
runInScope ->
        Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> ProviderEff_ i sh sf bh bf a
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]) a.
Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
-> ProviderEff_ i sh sf eh ef a
ProviderEff_ (Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
 -> ProviderEff_ i sh sf bh bf a)
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> ProviderEff_ i sh sf bh bf a
forall a b. (a -> b) -> a -> b
$ Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf)
~> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf)
forall {k} (key :: k) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
Eff ((key ##> e) : eh) ef ~> Eff (e : eh) ef
unkeyH (Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a
 -> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a)
-> (Eff
      ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
    -> Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a)
-> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff ((key ##> sh) : Provide_ i sh sf bh bf : bh) (sf : bf) a
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh ((key #> e) : ef) x -> Eff eh (e : ef) x
unkey (Eff
   ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
 -> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a)
-> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) a
forall a b. (a -> b) -> a -> b
$ (Eff eh ef
 ~> Eff
      ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf))
-> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) a
f (Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
-> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf)
~> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf)
forall {k} (key :: k) (e :: EffectH) (ef :: [* -> *])
       (eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((key ##> e) : eh) ef
keyH (Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
 -> Eff
      ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x)
-> (Eff eh ef x
    -> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x)
-> Eff eh ef x
-> Eff
     ((key ##> sh) : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
-> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
forall {k} (key :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((key #> e) : ef) x
key (Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
 -> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x)
-> (Eff eh ef x
    -> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x)
-> Eff eh ef x
-> Eff (sh : Provide_ i sh sf bh bf : bh) ((key #> sf) : bf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderEff_ i sh sf bh bf x
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
forall i (sh :: EffectH) (sf :: * -> *) (eh :: [EffectH])
       (ef :: [* -> *]) a.
ProviderEff_ i sh sf eh ef a
-> Eff (sh : Provide_ i sh sf eh ef : eh) (sf : ef) a
unProviderEff_ (ProviderEff_ i sh sf bh bf x
 -> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x)
-> (Eff eh ef x -> ProviderEff_ i sh sf bh bf x)
-> Eff eh ef x
-> Eff (sh : Provide_ i sh sf bh bf : bh) (sf : bf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff eh ef x -> ProviderEff_ i sh sf bh bf x
Eff eh ef ~> ProviderEff_ i sh sf bh bf
runInScope)