{-# LANGUAGE UndecidableInstances #-}

-- SPDX-License-Identifier: MPL-2.0

{- |
Copyright   :  (c) 2024 Sayo Koyoneda
License     :  MPL-2.0 (see the LICENSE file)
Maintainer  :  ymdfield@outlook.jp
-}
module Control.Monad.Hefty.Provider where

import Control.Monad.Hefty (
    Eff,
    HFunctor,
    MemberHBy,
    interpretH,
    raise,
    raiseNH,
    tag,
    tagH,
    untag,
    untagH,
    type (~>),
 )
import Data.Effect.Key (KeyH (KeyH))
import Data.Effect.Provider (Provider, Provider' (Provide), ProviderKey)
import Data.Effect.Provider qualified as P
import Data.Effect.Tag (type (#), type (##))
import Data.Functor.Identity (Identity (Identity))

type ProviderFix ctx i eh rh ef rf = Provider ctx i (ProviderBase ctx i eh rh ef rf)
type ProviderFix_ i eh rh ef rf = Provider Identity i (ProviderBase Identity i eh rh ef rf)

newtype ProviderBase ctx i eh rh ef rf a
    = ProviderBase
    { forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
ProviderBase ctx i eh rh ef rf a
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
unProviderBase
        :: Eff (eh ': ProviderFix ctx i eh rh ef rf ': rh) (ef ': rf) a
    }
    deriving newtype ((forall a b.
 (a -> b)
 -> ProviderBase ctx i eh rh ef rf a
 -> ProviderBase ctx i eh rh ef rf b)
-> (forall a b.
    a
    -> ProviderBase ctx i eh rh ef rf b
    -> ProviderBase ctx i eh rh ef rf a)
-> Functor (ProviderBase ctx i eh rh ef rf)
forall a b.
a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
forall a b.
(a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
(a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
$cfmap :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
(a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
fmap :: forall a b.
(a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
$c<$ :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
<$ :: forall a b.
a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
Functor, Functor (ProviderBase ctx i eh rh ef rf)
Functor (ProviderBase ctx i eh rh ef rf) =>
(forall a. a -> ProviderBase ctx i eh rh ef rf a)
-> (forall a b.
    ProviderBase ctx i eh rh ef rf (a -> b)
    -> ProviderBase ctx i eh rh ef rf a
    -> ProviderBase ctx i eh rh ef rf b)
-> (forall a b c.
    (a -> b -> c)
    -> ProviderBase ctx i eh rh ef rf a
    -> ProviderBase ctx i eh rh ef rf b
    -> ProviderBase ctx i eh rh ef rf c)
-> (forall a b.
    ProviderBase ctx i eh rh ef rf a
    -> ProviderBase ctx i eh rh ef rf b
    -> ProviderBase ctx i eh rh ef rf b)
-> (forall a b.
    ProviderBase ctx i eh rh ef rf a
    -> ProviderBase ctx i eh rh ef rf b
    -> ProviderBase ctx i eh rh ef rf a)
-> Applicative (ProviderBase ctx i eh rh ef rf)
forall a. a -> ProviderBase ctx i eh rh ef rf a
forall a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
forall a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
forall a b.
ProviderBase ctx i eh rh ef rf (a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
forall a b c.
(a -> b -> c)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]).
Functor (ProviderBase ctx i eh rh ef rf)
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
a -> ProviderBase ctx i eh rh ef rf a
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf (a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b c.
(a -> b -> c)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf c
$cpure :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
a -> ProviderBase ctx i eh rh ef rf a
pure :: forall a. a -> ProviderBase ctx i eh rh ef rf a
$c<*> :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf (a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
<*> :: forall a b.
ProviderBase ctx i eh rh ef rf (a -> b)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
$cliftA2 :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b c.
(a -> b -> c)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf c
liftA2 :: forall a b c.
(a -> b -> c)
-> ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf c
$c*> :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
*> :: forall a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
$c<* :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
<* :: forall a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf a
Applicative, Applicative (ProviderBase ctx i eh rh ef rf)
Applicative (ProviderBase ctx i eh rh ef rf) =>
(forall a b.
 ProviderBase ctx i eh rh ef rf a
 -> (a -> ProviderBase ctx i eh rh ef rf b)
 -> ProviderBase ctx i eh rh ef rf b)
-> (forall a b.
    ProviderBase ctx i eh rh ef rf a
    -> ProviderBase ctx i eh rh ef rf b
    -> ProviderBase ctx i eh rh ef rf b)
-> (forall a. a -> ProviderBase ctx i eh rh ef rf a)
-> Monad (ProviderBase ctx i eh rh ef rf)
forall a. a -> ProviderBase ctx i eh rh ef rf a
forall a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
forall a b.
ProviderBase ctx i eh rh ef rf a
-> (a -> ProviderBase ctx i eh rh ef rf b)
-> ProviderBase ctx i eh rh ef rf b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]).
Applicative (ProviderBase ctx i eh rh ef rf)
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
a -> ProviderBase ctx i eh rh ef rf a
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> (a -> ProviderBase ctx i eh rh ef rf b)
-> ProviderBase ctx i eh rh ef rf b
$c>>= :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> (a -> ProviderBase ctx i eh rh ef rf b)
-> ProviderBase ctx i eh rh ef rf b
>>= :: forall a b.
ProviderBase ctx i eh rh ef rf a
-> (a -> ProviderBase ctx i eh rh ef rf b)
-> ProviderBase ctx i eh rh ef rf b
$c>> :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
>> :: forall a b.
ProviderBase ctx i eh rh ef rf a
-> ProviderBase ctx i eh rh ef rf b
-> ProviderBase ctx i eh rh ef rf b
$creturn :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
a -> ProviderBase ctx i eh rh ef rf a
return :: forall a. a -> ProviderBase ctx i eh rh ef rf a
Monad)

runProvider
    :: forall ctx i eh rh ef rf
     . ( forall x
          . i
         -> Eff (eh ': ProviderFix ctx i eh rh ef rf ': rh) (ef ': rf) x
         -> Eff (ProviderFix ctx i eh rh ef rf ': rh) rf (ctx x)
       )
    -> Eff (ProviderFix ctx i eh rh ef rf ': rh) rf ~> Eff rh rf
runProvider :: forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]).
(forall x.
 i
 -> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
 -> Eff (ProviderFix ctx i eh rh ef rf : rh) rf (ctx x))
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf ~> Eff rh rf
runProvider forall x.
i
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf (ctx x)
run = Eff (ProviderFix ctx i eh rh ef rf : rh) rf x -> Eff rh rf x
Eff (ProviderFix ctx i eh rh ef rf : rh) rf ~> Eff rh rf
loop
  where
    loop :: Eff (ProviderFix ctx i eh rh ef rf ': rh) rf ~> Eff rh rf
    loop :: Eff (ProviderFix ctx i eh rh ef rf : rh) rf ~> Eff rh rf
loop = (ProviderFix ctx i eh rh ef rf ~~> Eff rh rf)
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf ~> Eff rh rf
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH \(KeyH (Provide i
i (forall x. Eff rh rf x -> ProviderBase ctx i eh rh ef rf x)
-> ProviderBase ctx i eh rh ef rf a1
f)) ->
        Eff (ProviderFix ctx i eh rh ef rf : rh) rf x -> Eff rh rf x
Eff (ProviderFix ctx i eh rh ef rf : rh) rf ~> Eff rh rf
loop (Eff (ProviderFix ctx i eh rh ef rf : rh) rf x -> Eff rh rf x)
-> (ProviderBase ctx i eh rh ef rf a1
    -> Eff (ProviderFix ctx i eh rh ef rf : rh) rf x)
-> ProviderBase ctx i eh rh ef rf a1
-> Eff rh rf x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a1
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf (ctx a1)
forall x.
i
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf (ctx x)
run i
i (Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a1
 -> Eff (ProviderFix ctx i eh rh ef rf : rh) rf x)
-> (ProviderBase ctx i eh rh ef rf a1
    -> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a1)
-> ProviderBase ctx i eh rh ef rf a1
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderBase ctx i eh rh ef rf a1
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a1
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
ProviderBase ctx i eh rh ef rf a
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
unProviderBase (ProviderBase ctx i eh rh ef rf a1 -> Eff rh rf x)
-> ProviderBase ctx i eh rh ef rf a1 -> Eff rh rf x
forall a b. (a -> b) -> a -> b
$
            (forall x. Eff rh rf x -> ProviderBase ctx i eh rh ef rf x)
-> ProviderBase ctx i eh rh ef rf a1
f (Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
-> ProviderBase ctx i eh rh ef rf x
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
-> ProviderBase ctx i eh rh ef rf a
ProviderBase (Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
 -> ProviderBase ctx i eh rh ef rf x)
-> (Eff rh rf x
    -> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x)
-> Eff rh rf x
-> ProviderBase ctx i eh rh ef rf x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (len :: Natural) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]).
WeakenN len eh eh' =>
Eff eh ef ~> Eff eh' ef
raiseNH @2 (Eff rh (ef : rf) x
 -> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x)
-> (Eff rh rf x -> Eff rh (ef : rf) x)
-> Eff rh rf x
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff rh rf x -> Eff rh (ef : rf) x
forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) x.
Eff eh ef x -> Eff eh (e : ef) x
raise)

runProvider_
    :: forall i eh rh ef rf
     . ( i
         -> Eff (eh ': ProviderFix_ i eh rh ef rf ': rh) (ef ': rf)
            ~> Eff (ProviderFix_ i eh rh ef rf ': rh) rf
       )
    -> Eff (ProviderFix_ i eh rh ef rf ': rh) rf ~> Eff rh rf
runProvider_ :: forall i (eh :: EffectH) (rh :: [EffectH]) (ef :: * -> *)
       (rf :: [* -> *]).
(i
 -> Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf)
    ~> Eff (ProviderFix_ i eh rh ef rf : rh) rf)
-> Eff (ProviderFix_ i eh rh ef rf : rh) rf ~> Eff rh rf
runProvider_ i
-> Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf)
   ~> Eff (ProviderFix_ i eh rh ef rf : rh) rf
run = (forall x.
 i
 -> Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) x
 -> Eff (ProviderFix_ i eh rh ef rf : rh) rf (Identity x))
-> Eff (ProviderFix_ i eh rh ef rf : rh) rf ~> Eff rh rf
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]).
(forall x.
 i
 -> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) x
 -> Eff (ProviderFix ctx i eh rh ef rf : rh) rf (ctx x))
-> Eff (ProviderFix ctx i eh rh ef rf : rh) rf ~> Eff rh rf
runProvider \i
i Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) x
m -> i
-> Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf)
   ~> Eff (ProviderFix_ i eh rh ef rf : rh) rf
run i
i (Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) (Identity x)
 -> Eff (ProviderFix_ i eh rh ef rf : rh) rf (Identity x))
-> Eff
     (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) (Identity x)
-> Eff (ProviderFix_ i eh rh ef rf : rh) rf (Identity x)
forall a b. (a -> b) -> a -> b
$ x -> Identity x
forall a. a -> Identity a
Identity (x -> Identity x)
-> Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) x
-> Eff
     (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) (Identity x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eff (eh : ProviderFix_ i eh rh ef rf : rh) (ef : rf) x
m

provide
    :: forall tag ctx i eh ef a sh bh sf bf
     . ( MemberHBy
            (ProviderKey ctx i)
            (Provider' ctx i (ProviderBase ctx i sh bh sf bf))
            eh
       , HFunctor sh
       )
    => i
    -> ( (Eff eh ef ~> Eff (sh ## tag ': ProviderFix ctx i sh bh sf bf ': bh) (sf # tag ': bf))
         -> Eff (sh ## tag ': ProviderFix ctx i sh bh sf bf ': bh) (sf # tag ': bf) a
       )
    -> Eff eh ef (ctx a)
provide :: forall {k} (tag :: k) (ctx :: * -> *) i (eh :: [EffectH])
       (ef :: [* -> *]) a (sh :: EffectH) (bh :: [EffectH]) (sf :: * -> *)
       (bf :: [* -> *]).
(MemberHBy
   (ProviderKey ctx i)
   (Provider' ctx i (ProviderBase ctx i sh bh sf bf))
   eh,
 HFunctor sh) =>
i
-> ((Eff eh ef
     ~> Eff
          ((sh ## tag) : ProviderFix ctx i sh bh sf bf : bh)
          ((sf # tag) : bf))
    -> Eff
         ((sh ## tag) : ProviderFix ctx i sh bh sf bf : bh)
         ((sf # tag) : bf)
         a)
-> Eff eh ef (ctx a)
provide i
i (Eff eh ef
 ~> Eff
      ((sh ## tag)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf))
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
f =
    i
i i
-> ((Eff eh ef ~> ProviderBase ctx i sh bh sf bf)
    -> ProviderBase ctx i sh bh sf bf a)
-> Eff eh ef (ctx a)
forall (ctx :: * -> *) i (f :: * -> *) a (b :: * -> *).
SendHOEBy (ProviderKey ctx i) (Provider' ctx i b) f =>
i -> ((f ~> b) -> b a) -> f (ctx a)
P...! \Eff eh ef ~> ProviderBase ctx i sh bh sf bf
runInBase ->
        Eff
  (sh
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  (sf : bf)
  a
-> ProviderBase ctx i sh bh sf bf a
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
-> ProviderBase ctx i eh rh ef rf a
ProviderBase (Eff
   (sh
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
      : bh)
   (sf : bf)
   a
 -> ProviderBase ctx i sh bh sf bf a)
-> (Eff
      ((sh ## tag)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      a
    -> Eff
         (sh
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
            : bh)
         (sf : bf)
         a)
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
-> ProviderBase ctx i sh bh sf bf a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  (sh
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
  a
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     (sf : bf)
     a
forall {k} (tag :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh ((e # tag) : ef) x -> Eff eh (e : ef) x
untag (Eff
   (sh
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
      : bh)
   ((sf # tag) : bf)
   a
 -> Eff
      (sh
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      (sf : bf)
      a)
-> (Eff
      ((sh ## tag)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      a
    -> Eff
         (sh
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
            : bh)
         ((sf # tag) : bf)
         a)
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     (sf : bf)
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  ((sh ## tag)
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
  a
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
Eff
  ((sh ## tag)
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
~> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
forall {k} (tag :: k) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
Eff ((e ## tag) : eh) ef ~> Eff (e : eh) ef
untagH (Eff
   ((sh ## tag)
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
      : bh)
   ((sf # tag) : bf)
   a
 -> ProviderBase ctx i sh bh sf bf a)
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
-> ProviderBase ctx i sh bh sf bf a
forall a b. (a -> b) -> a -> b
$ (Eff eh ef
 ~> Eff
      ((sh ## tag)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf))
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
f ((Eff eh ef
  ~> Eff
       ((sh ## tag)
          : (ProviderKey ctx i
             ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
          : bh)
       ((sf # tag) : bf))
 -> Eff
      ((sh ## tag)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      a)
-> (Eff eh ef
    ~> Eff
         ((sh ## tag)
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
            : bh)
         ((sf # tag) : bf))
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
forall a b. (a -> b) -> a -> b
$ Eff
  (sh
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
  x
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
Eff
  (sh
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
~> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
forall {k} (tag :: k) (e :: EffectH) (ef :: [* -> *])
       (eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((e ## tag) : eh) ef
tagH (Eff
   (sh
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
      : bh)
   ((sf # tag) : bf)
   x
 -> Eff
      ((sh ## tag)
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      x)
-> (Eff eh ef x
    -> Eff
         (sh
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
            : bh)
         ((sf # tag) : bf)
         x)
-> Eff eh ef x
-> Eff
     ((sh ## tag)
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  (sh
     : (ProviderKey ctx i
        ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
     : bh)
  (sf : bf)
  x
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
forall {k} (tag :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((e # tag) : ef) x
tag (Eff
   (sh
      : (ProviderKey ctx i
         ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
      : bh)
   (sf : bf)
   x
 -> Eff
      (sh
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      x)
-> (Eff eh ef x
    -> Eff
         (sh
            : (ProviderKey ctx i
               ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
            : bh)
         (sf : bf)
         x)
-> Eff eh ef x
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderBase ctx i sh bh sf bf x
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     (sf : bf)
     x
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
ProviderBase ctx i eh rh ef rf a
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
unProviderBase (ProviderBase ctx i sh bh sf bf x
 -> Eff
      (sh
         : (ProviderKey ctx i
            ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
         : bh)
      (sf : bf)
      x)
-> (Eff eh ef x -> ProviderBase ctx i sh bh sf bf x)
-> Eff eh ef x
-> Eff
     (sh
        : (ProviderKey ctx i
           ##> Provider' ctx i (ProviderBase ctx i sh bh sf bf))
        : bh)
     (sf : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff eh ef x -> ProviderBase ctx i sh bh sf bf x
Eff eh ef ~> ProviderBase ctx i sh bh sf bf
runInBase

provide_
    :: forall tag i eh ef a sh bh sf bf
     . ( MemberHBy
            (ProviderKey Identity i)
            (Provider' Identity i (ProviderBase Identity i sh bh sf bf))
            eh
       , HFunctor sh
       )
    => i
    -> ( (Eff eh ef ~> Eff (sh ## tag ': ProviderFix_ i sh bh sf bf ': bh) (sf # tag ': bf))
         -> Eff (sh ## tag ': ProviderFix_ i sh bh sf bf ': bh) (sf # tag ': bf) a
       )
    -> Eff eh ef a
provide_ :: forall {k} (tag :: k) i (eh :: [EffectH]) (ef :: [* -> *]) a
       (sh :: EffectH) (bh :: [EffectH]) (sf :: * -> *) (bf :: [* -> *]).
(MemberHBy
   (ProviderKey Identity i)
   (Provider' Identity i (ProviderBase Identity i sh bh sf bf))
   eh,
 HFunctor sh) =>
i
-> ((Eff eh ef
     ~> Eff
          ((sh ## tag) : ProviderFix_ i sh bh sf bf : bh) ((sf # tag) : bf))
    -> Eff
         ((sh ## tag) : ProviderFix_ i sh bh sf bf : bh)
         ((sf # tag) : bf)
         a)
-> Eff eh ef a
provide_ i
i (Eff eh ef
 ~> Eff
      ((sh ## tag)
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf))
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
f =
    i
i i
-> ((Eff eh ef ~> ProviderBase Identity i sh bh sf bf)
    -> ProviderBase Identity i sh bh sf bf a)
-> Eff eh ef a
forall i (f :: * -> *) a (b :: * -> *).
(SendHOEBy (ProviderKey Identity i) (Provider' Identity i b) f,
 Functor f) =>
i -> ((f ~> b) -> b a) -> f a
P..! \Eff eh ef ~> ProviderBase Identity i sh bh sf bf
runInBase ->
        Eff
  (sh
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  (sf : bf)
  a
-> ProviderBase Identity i sh bh sf bf a
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
-> ProviderBase ctx i eh rh ef rf a
ProviderBase (Eff
   (sh
      : (ProviderKey Identity i
         ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
      : bh)
   (sf : bf)
   a
 -> ProviderBase Identity i sh bh sf bf a)
-> (Eff
      ((sh ## tag)
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      a
    -> Eff
         (sh
            : (ProviderKey Identity i
               ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
            : bh)
         (sf : bf)
         a)
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
-> ProviderBase Identity i sh bh sf bf a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  (sh
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
  a
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     (sf : bf)
     a
forall {k} (tag :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh ((e # tag) : ef) x -> Eff eh (e : ef) x
untag (Eff
   (sh
      : (ProviderKey Identity i
         ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
      : bh)
   ((sf # tag) : bf)
   a
 -> Eff
      (sh
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      (sf : bf)
      a)
-> (Eff
      ((sh ## tag)
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      a
    -> Eff
         (sh
            : (ProviderKey Identity i
               ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
            : bh)
         ((sf # tag) : bf)
         a)
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     (sf : bf)
     a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  ((sh ## tag)
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
  a
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
Eff
  ((sh ## tag)
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
~> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
forall {k} (tag :: k) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]).
HFunctor e =>
Eff ((e ## tag) : eh) ef ~> Eff (e : eh) ef
untagH (Eff
   ((sh ## tag)
      : (ProviderKey Identity i
         ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
      : bh)
   ((sf # tag) : bf)
   a
 -> ProviderBase Identity i sh bh sf bf a)
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
-> ProviderBase Identity i sh bh sf bf a
forall a b. (a -> b) -> a -> b
$ (Eff eh ef
 ~> Eff
      ((sh ## tag)
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf))
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
f ((Eff eh ef
  ~> Eff
       ((sh ## tag)
          : (ProviderKey Identity i
             ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
          : bh)
       ((sf # tag) : bf))
 -> Eff
      ((sh ## tag)
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      a)
-> (Eff eh ef
    ~> Eff
         ((sh ## tag)
            : (ProviderKey Identity i
               ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
            : bh)
         ((sf # tag) : bf))
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     a
forall a b. (a -> b) -> a -> b
$ Eff
  (sh
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
  x
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
Eff
  (sh
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  ((sf # tag) : bf)
~> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
forall {k} (tag :: k) (e :: EffectH) (ef :: [* -> *])
       (eh :: [EffectH]).
HFunctor e =>
Eff (e : eh) ef ~> Eff ((e ## tag) : eh) ef
tagH (Eff
   (sh
      : (ProviderKey Identity i
         ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
      : bh)
   ((sf # tag) : bf)
   x
 -> Eff
      ((sh ## tag)
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      x)
-> (Eff eh ef x
    -> Eff
         (sh
            : (ProviderKey Identity i
               ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
            : bh)
         ((sf # tag) : bf)
         x)
-> Eff eh ef x
-> Eff
     ((sh ## tag)
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff
  (sh
     : (ProviderKey Identity i
        ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
     : bh)
  (sf : bf)
  x
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
forall {k} (tag :: k) (e :: * -> *) (ef :: [* -> *])
       (eh :: [EffectH]) x.
Eff eh (e : ef) x -> Eff eh ((e # tag) : ef) x
tag (Eff
   (sh
      : (ProviderKey Identity i
         ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
      : bh)
   (sf : bf)
   x
 -> Eff
      (sh
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      ((sf # tag) : bf)
      x)
-> (Eff eh ef x
    -> Eff
         (sh
            : (ProviderKey Identity i
               ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
            : bh)
         (sf : bf)
         x)
-> Eff eh ef x
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     ((sf # tag) : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProviderBase Identity i sh bh sf bf x
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     (sf : bf)
     x
forall (ctx :: * -> *) i (eh :: EffectH) (rh :: [EffectH])
       (ef :: * -> *) (rf :: [* -> *]) a.
ProviderBase ctx i eh rh ef rf a
-> Eff (eh : ProviderFix ctx i eh rh ef rf : rh) (ef : rf) a
unProviderBase (ProviderBase Identity i sh bh sf bf x
 -> Eff
      (sh
         : (ProviderKey Identity i
            ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
         : bh)
      (sf : bf)
      x)
-> (Eff eh ef x -> ProviderBase Identity i sh bh sf bf x)
-> Eff eh ef x
-> Eff
     (sh
        : (ProviderKey Identity i
           ##> Provider' Identity i (ProviderBase Identity i sh bh sf bf))
        : bh)
     (sf : bf)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eff eh ef x -> ProviderBase Identity i sh bh sf bf x
Eff eh ef ~> ProviderBase Identity i sh bh sf bf
runInBase