{-# LANGUAGE AllowAmbiguousTypes #-}

{-# OPTIONS_HADDOCK not-home #-}

-- | Description: Stack manipulation handlers for the 'Polysemy.Bundle.Bundle' effect
module Polysemy.Internal.Bundle where

import Polysemy (Members)
import Polysemy.Internal.Union (ElemOf(..), membership)
import Polysemy.Internal.Kind (Append)

------------------------------------------------------------------------------
-- | Extend a membership proof's stack by arbitrary effects.
extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
extendMembership :: forall {a} (r :: [a]) (r' :: [a]) (e :: a).
ElemOf e r -> ElemOf e (Append r r')
extendMembership ElemOf e r
Here = ElemOf e (e : Append r' r')
ElemOf e (Append r r')
forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here
extendMembership (There ElemOf e r
e) = ElemOf e (Append r r') -> ElemOf e (e' : Append r r')
forall {k} (r' :: [k]) (e :: k) (e' :: k) (r :: [k]).
(r' ~ (e' : r)) =>
ElemOf e r -> ElemOf e r'
There (forall (r :: [a]) (r' :: [a]) (e :: a).
ElemOf e r -> ElemOf e (Append r r')
forall {a} (r :: [a]) (r' :: [a]) (e :: a).
ElemOf e r -> ElemOf e (Append r r')
extendMembership @_ @r' ElemOf e r
e)
{-# INLINE extendMembership #-}

------------------------------------------------------------------------------
-- | Transform a membership proof's stack by arbitrary effects using evidence
-- from the context.
subsumeMembership :: forall r r' e. Members r r' => ElemOf e r -> ElemOf e r'
subsumeMembership :: forall (r :: [Effect]) (r' :: [Effect]) (e :: Effect).
Members r r' =>
ElemOf e r -> ElemOf e r'
subsumeMembership ElemOf e r
Here = forall (e :: Effect) (r :: [Effect]). Member e r => ElemOf e r
membership @e @r'
subsumeMembership (There (ElemOf e r
pr :: ElemOf e r'')) = forall (r :: [Effect]) (r' :: [Effect]) (e :: Effect).
Members r r' =>
ElemOf e r -> ElemOf e r'
subsumeMembership @r'' @r' ElemOf e r
pr
{-# INLINE subsumeMembership #-}