{-# LANGUAGE EmptyCase #-}
{-# OPTIONS_HADDOCK not-home #-}
module Control.Effect.Internal.Membership where
import GHC.TypeLits
import Data.Type.Equality
data ElemOf (e :: a) (r :: [a]) where
Here :: ElemOf e (e ': r)
There :: ElemOf e r -> ElemOf e (_e ': r)
absurdMember :: ElemOf e '[] -> b
absurdMember :: ElemOf e '[] -> b
absurdMember = ElemOf e '[] -> b
\case
{-# INLINE absurdMember #-}
deriving instance Show (ElemOf e r)
sameMember :: forall e e' r
. ElemOf e r
-> ElemOf e' r
-> Maybe (e :~: e')
sameMember :: ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
sameMember ElemOf e r
Here ElemOf e' r
Here = (e :~: e) -> Maybe (e :~: e)
forall a. a -> Maybe a
Just e :~: e
forall k (a :: k). a :~: a
Refl
sameMember (There ElemOf e r
pr) (There ElemOf e' r
pr') = ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
forall k (e :: k) (e' :: k) (r :: [k]).
ElemOf e r -> ElemOf e' r -> Maybe (e :~: e')
sameMember ElemOf e r
pr ElemOf e' r
ElemOf e' r
pr'
sameMember ElemOf e r
_ ElemOf e' r
_ = Maybe (e :~: e')
forall a. Maybe a
Nothing
class Member e r where
membership :: ElemOf e r
instance {-# OVERLAPPING #-} Member e (e ': r) where
membership :: ElemOf e (e : r)
membership = ElemOf e (e : r)
forall a (e :: a) (r :: [a]). ElemOf e (e : r)
Here
{-# INLINE membership #-}
instance Member e r => Member e (_e ': r) where
membership :: ElemOf e (_e : r)
membership = ElemOf e r -> ElemOf e (_e : r)
forall a (e :: a) (r :: [a]) (_e :: a).
ElemOf e r -> ElemOf e (_e : r)
There ElemOf e r
forall k (e :: k) (r :: [k]). Member e r => ElemOf e r
membership
{-# INLINEABLE membership #-}
instance TypeError ( 'Text "Unhandled effect: " ':<>: 'ShowType e
':$$: 'Text "You need to either add or replace an \
\interpreter in your interpretation stack \
\so that the effect gets handled."
':$$: 'Text "To check what effects are currently \
\handled by your interpretation stack, use \
\`debugEffects' from `Control.Effect.Debug'."
)
=> Member e '[] where
membership :: ElemOf e '[]
membership = String -> ElemOf e '[]
forall a. HasCallStack => String -> a
error String
"impossible"