{-# LANGUAGE AllowAmbiguousTypes #-}

{-# OPTIONS_HADDOCK not-home #-}

module Polysemy.Internal.Bundle where

import Data.Proxy
import Polysemy
import Polysemy.Internal.Union

type family Append l r where
  Append (a ': l) r = a ': (Append l r)
  Append '[] r = r

extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
extendMembership :: ElemOf e r -> ElemOf e (Append r r')
extendMembership ElemOf e r
Here = ElemOf e (Append r r')
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
Here
extendMembership (There ElemOf e r
e) = ElemOf e (Append r r') -> ElemOf e (e' : Append r r')
forall a (e :: a) (r :: [a]) (e' :: a).
ElemOf e r -> ElemOf e (e' : r)
There (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 #-}

subsumeMembership :: forall r r' e. Members r r' => ElemOf e r -> ElemOf e r'
subsumeMembership :: ElemOf e r -> ElemOf e r'
subsumeMembership ElemOf e r
Here = Member e r' => ElemOf e r'
forall a (e :: a) (r :: [a]). Member e r => ElemOf e r
membership @e @r'
subsumeMembership (There (ElemOf e r
pr :: ElemOf e r'')) = ElemOf e r -> ElemOf e r'
forall a (r :: [a]) (r' :: [a]) (e :: a).
Members r r' =>
ElemOf e r -> ElemOf e r'
subsumeMembership @r'' @r' ElemOf e r
pr
{-# INLINE subsumeMembership #-}

weakenList :: forall r' r m a
            . KnownList r'
           => Union r m a
           -> Union (Append r' r) m a
weakenList :: Union r m a -> Union (Append r' r) m a
weakenList Union r m a
u = ((r' ~ '[]) => Union (Append r' r) m a)
-> (forall (x :: Effect) (r :: [Effect]).
    (r' ~ (x : r), KnownList r) =>
    Proxy x -> Proxy r -> Union (Append r' r) m a)
-> Union (Append r' r) m a
forall k (l :: [k]) a.
KnownList l =>
((l ~ '[]) => a)
-> (forall (x :: k) (r :: [k]).
    (l ~ (x : r), KnownList r) =>
    Proxy x -> Proxy r -> a)
-> a
unconsKnownList @_ @r' Union r m a
(r' ~ '[]) => Union (Append r' r) m a
u (\Proxy x
_ (Proxy r
_ :: Proxy r'') -> Union (Append r r) m a -> Union (x : Append r r) m a
forall (e :: Effect) (r :: [Effect]) (m :: * -> *) a.
Union r m a -> Union (e : r) m a
weaken (Union r m a -> Union (Append r r) m a
forall (r' :: [Effect]) (r :: [Effect]) (m :: * -> *) a.
KnownList r' =>
Union r m a -> Union (Append r' r) m a
weakenList @r'' Union r m a
u))
{-# INLINE weakenList #-}


------------------------------------------------------------------------------
-- | A class for type-level lists with a known spine.
--
-- This constraint is eventually satisfied as @r@ is instantied to a
-- concrete list.
class KnownList (l :: [k]) where
  unconsKnownList :: (l ~ '[] => a)
                  -> (  forall x r
                      . (l ~ (x ': r), KnownList r)
                     => Proxy x
                     -> Proxy r
                     -> a
                     )
                  -> a

instance KnownList '[] where
  unconsKnownList :: (('[] ~ '[]) => a)
-> (forall (x :: k) (r :: [k]).
    ('[] ~ (x : r), KnownList r) =>
    Proxy x -> Proxy r -> a)
-> a
unconsKnownList ('[] ~ '[]) => a
b forall (x :: k) (r :: [k]).
('[] ~ (x : r), KnownList r) =>
Proxy x -> Proxy r -> a
_ = a
('[] ~ '[]) => a
b
  {-# INLINE unconsKnownList #-}

instance KnownList r => KnownList (x ': r) where
  unconsKnownList :: (((x : r) ~ '[]) => a)
-> (forall (x :: k) (r :: [k]).
    ((x : r) ~ (x : r), KnownList r) =>
    Proxy x -> Proxy r -> a)
-> a
unconsKnownList ((x : r) ~ '[]) => a
_ forall (x :: k) (r :: [k]).
((x : r) ~ (x : r), KnownList r) =>
Proxy x -> Proxy r -> a
b = Proxy x -> Proxy r -> a
forall (x :: k) (r :: [k]).
((x : r) ~ (x : r), KnownList r) =>
Proxy x -> Proxy r -> a
b Proxy x
forall k (t :: k). Proxy t
Proxy Proxy r
forall k (t :: k). Proxy t
Proxy
  {-# INLINE unconsKnownList #-}