{-# LANGUAGE TypeInType,
GADTs,
KindSignatures,
TypeOperators,
TypeFamilies,
MultiParamTypeClasses,
FlexibleInstances,
FlexibleContexts,
StandaloneDeriving,
UndecidableInstances,
FunctionalDependencies,
ConstraintKinds,
ScopedTypeVariables
#-}
module Language.Grammars.AspectAG.HList where
import Language.Grammars.AspectAG.TPrelude
import Data.Proxy
import Data.Type.Equality
import Data.Kind
import GHC.Exts
data HList (l :: [Type]) :: Type where
HNil :: HList '[]
HCons :: x -> HList xs -> HList (x ': xs)
class HMember (t :: Type) (l :: [Type]) where
type HMemberRes t l :: Bool
hMember :: Label t -> HList l -> Proxy (HMemberRes t l)
instance HMember t '[] where
type HMemberRes t '[] = 'False
hMember _ _ = Proxy
instance HMember t (t' ': ts) where
type HMemberRes t (t' ': ts) = Or (t == t') (HMemberRes t ts)
hMember _ _ = Proxy
class HMember' (t :: k) (l :: [k]) where
type HMemberRes' t l :: Bool
hMember' :: f t -> KList l -> Proxy (HMemberRes' t l)
instance HMember' t '[] where
type HMemberRes' t '[] = 'False
hMember' _ _ = Proxy
instance HMember' t (t' ': ts) where
type HMemberRes' t (t' ': ts) = Or (t == t') (HMemberRes' t ts)
hMember' _ _ = Proxy
infixr 2 .:
(.:) = HCons
ε = HNil
data KList (l :: [k]) :: Type where
KNil :: KList '[]
KCons :: Label h -> KList l -> KList (h ': l)
infixr 2 .:.
(.:.) = KCons
eL = KNil