{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} module Language.Parser.Ptera.Syntax.SafeGrammar ( T, Grammar (..), TokensTag, RulesTag, RuleExprType, GrammarToken (..), fixGrammar, StartPoint, Terminal, NonTerminal, HasRuleExprField (..), MemberInitials (..), Rules (..), genStartPoint, RuleExpr (..), Alt (..), Expr (..), ruleExpr, (<^>), (<:>), eps, var, varA, tok, TokensMember (..), tokA, ) where import Language.Parser.Ptera.Prelude import qualified Data.HashMap.Strict as HashMap import qualified Language.Parser.Ptera.Data.HEnum as HEnum import qualified Language.Parser.Ptera.Data.HFList as HFList import qualified Language.Parser.Ptera.Syntax.Grammar as SyntaxGrammar import Prelude (String) import qualified Type.Membership as Membership type T = Grammar type Grammar :: ([Type] -> Type -> Type) -> Type -> Type -> Type -> [Symbol] -> Type newtype Grammar action rules tokens elem initials = UnsafeGrammar { Grammar action rules tokens elem initials -> FixedGrammar StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action unsafeGrammar :: SyntaxGrammar.FixedGrammar StartPoint NonTerminal Terminal elem StringLit (Maybe ()) action } type family TokensTag (tokens :: Type) :: [Symbol] type family RulesTag (rules :: Type) :: [Symbol] type family RuleExprType (rules :: Type) :: Type -> Type class GrammarToken tokens elem where tokenToTerminal :: Proxy tokens -> elem -> HEnum.T (TokensTag tokens) class KnownSymbol v => HasRuleExprField rules v where type RuleExprReturnType rules v :: Type getExprField :: rules -> proxy v -> RuleExprType rules (RuleExprReturnType rules v) nonTerminalName :: rules -> proxy v -> String nonTerminalName rules _ proxy v p = proxy v -> StringLit forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> StringLit symbolVal proxy v p type GrammarMForFixGrammar elem action = SyntaxGrammar.GrammarT StartPoint NonTerminal Terminal elem StringLit (Maybe ()) action Identity fixGrammar :: forall initials action rules tokens elem . MemberInitials rules initials => Rules rules => RuleExprType rules ~ RuleExpr action rules tokens elem => rules -> Grammar action rules tokens elem initials fixGrammar :: rules -> Grammar action rules tokens elem initials fixGrammar rules ruleDefs = FixedGrammar StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action -> Grammar action rules tokens elem initials forall (action :: [*] -> * -> *) rules tokens elem (initials :: [Symbol]). FixedGrammar StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action -> Grammar action rules tokens elem initials UnsafeGrammar do Identity (FixedGrammar StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action) -> FixedGrammar StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action forall a. Identity a -> a runIdentity do GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () -> Identity (FixedGrammar StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action) forall k1 k2 (m :: * -> *) start nonTerminal terminal (elem :: k1) varDoc altDoc (action :: [k1] -> k2 -> *). Monad m => GrammarT start nonTerminal terminal elem varDoc altDoc action m () -> m (FixedGrammar start nonTerminal terminal elem varDoc altDoc action) SyntaxGrammar.fixGrammarT do HFList (DictF (HasRuleExprField rules)) initials -> (forall (x :: Symbol). Membership initials x -> DictF (HasRuleExprField rules) x -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity ()) -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () forall k (m :: * -> *) (f :: k -> *) (xs :: [k]). Applicative m => HFList f xs -> (forall (x :: k). Membership xs x -> f x -> m ()) -> m () HFList.hforMWithIndex HFList (DictF (HasRuleExprField rules)) initials forall rules (initials :: [Symbol]). MemberInitials rules initials => T (DictF (HasRuleExprField rules)) initials memberInitials forall (x :: Symbol). Membership initials x -> DictF (HasRuleExprField rules) x -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () fixInitial HFList (DictF (HasRuleExprField rules)) (RulesTag rules) -> (forall (x :: Symbol). Membership (RulesTag rules) x -> DictF (HasRuleExprField rules) x -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity ()) -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () forall k (m :: * -> *) (f :: k -> *) (xs :: [k]). Applicative m => HFList f xs -> (forall (x :: k). Membership xs x -> f x -> m ()) -> m () HFList.hforMWithIndex HFList (DictF (HasRuleExprField rules)) (RulesTag rules) forall rules. Rules rules => T (DictF (HasRuleExprField rules)) (RulesTag rules) generateRules forall (x :: Symbol). Membership (RulesTag rules) x -> DictF (HasRuleExprField rules) x -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () fixRule where fixInitial :: Membership.Membership initials v -> HFList.DictF (HasRuleExprField rules) v -> GrammarMForFixGrammar elem action () fixInitial :: Membership initials v -> DictF (HasRuleExprField rules) v -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () fixInitial Membership initials v m DictF (HasRuleExprField rules) v HFList.DictF = do let sn :: StartPoint sn = Membership initials v -> StartPoint forall k (initials :: [k]) (v :: k). Membership initials v -> StartPoint genStartPoint Membership initials v m let vn :: StartPoint vn = StringLit -> StartPoint getNewV do Membership initials v -> StringLit forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> StringLit symbolVal Membership initials v m StartPoint -> StartPoint -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () forall k1 k2 start (m :: * -> *) nonTerminal terminal (elem :: k1) varDoc altDoc (action :: [k1] -> k2 -> *). (Enum start, Monad m) => start -> nonTerminal -> GrammarT start nonTerminal terminal elem varDoc altDoc action m () SyntaxGrammar.initialT StartPoint sn StartPoint vn fixRule :: forall v . Membership.Membership (RulesTag rules) v -> HFList.DictF (HasRuleExprField rules) v -> GrammarMForFixGrammar elem action () fixRule :: Membership (RulesTag rules) v -> DictF (HasRuleExprField rules) v -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () fixRule Membership (RulesTag rules) v m DictF (HasRuleExprField rules) v HFList.DictF = do let vn :: StartPoint vn = StringLit -> StartPoint getNewV do Membership (RulesTag rules) v -> StringLit forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> StringLit symbolVal Membership (RulesTag rules) v m let d :: StringLit d = rules -> Membership (RulesTag rules) v -> StringLit forall rules (v :: Symbol) (proxy :: Symbol -> *). HasRuleExprField rules v => rules -> proxy v -> StringLit nonTerminalName rules ruleDefs Membership (RulesTag rules) v m StartPoint -> StringLit -> RuleExpr StartPoint StartPoint elem (Maybe ()) action -> GrammarT StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action Identity () forall k1 k2 nonTerminal (m :: * -> *) varDoc terminal (elem :: k1) altDoc (action :: [k1] -> k2 -> *) start. (Enum nonTerminal, Monad m) => nonTerminal -> varDoc -> RuleExpr nonTerminal terminal elem altDoc action -> GrammarT start nonTerminal terminal elem varDoc altDoc action m () SyntaxGrammar.ruleT StartPoint vn StringLit d do RuleExpr action rules tokens elem (RuleExprReturnType rules v) -> RuleExpr StartPoint StartPoint elem (Maybe ()) action forall a. RuleExpr action rules tokens elem a -> RuleExpr StartPoint StartPoint elem (Maybe ()) action fixRuleExpr do rules -> Membership (RulesTag rules) v -> RuleExprType rules (RuleExprReturnType rules v) forall rules (v :: Symbol) (proxy :: Symbol -> *). HasRuleExprField rules v => rules -> proxy v -> RuleExprType rules (RuleExprReturnType rules v) getExprField rules ruleDefs Membership (RulesTag rules) v m fixRuleExpr :: RuleExpr action rules tokens elem a -> SyntaxGrammar.RuleExpr NonTerminal Terminal elem (Maybe ()) action fixRuleExpr :: RuleExpr action rules tokens elem a -> RuleExpr StartPoint StartPoint elem (Maybe ()) action fixRuleExpr = \case RuleExpr [Alt action rules tokens elem a] alts -> [Alt StartPoint StartPoint elem (Maybe ()) action a] -> RuleExpr StartPoint StartPoint elem (Maybe ()) action forall k k1 nonTerminal terminal (elem :: k) altDoc (action :: [k] -> k1 -> *) (a :: k1). [Alt nonTerminal terminal elem altDoc action a] -> RuleExpr nonTerminal terminal elem altDoc action SyntaxGrammar.RuleExpr [ Alt action rules tokens elem a -> Alt StartPoint StartPoint elem (Maybe ()) action a forall a. Alt action rules tokens elem a -> Alt StartPoint StartPoint elem (Maybe ()) action a fixAlt Alt action rules tokens elem a origAlt | Alt action rules tokens elem a origAlt <- [Alt action rules tokens elem a] alts ] fixAlt :: Alt action rules tokens elem a -> SyntaxGrammar.Alt NonTerminal Terminal elem (Maybe ()) action a fixAlt :: Alt action rules tokens elem a -> Alt StartPoint StartPoint elem (Maybe ()) action a fixAlt (UnsafeAlt Alt StringLit StartPoint elem (Maybe ()) action a origAlt) = case Alt StringLit StartPoint elem (Maybe ()) action a origAlt of SyntaxGrammar.Alt Expr StringLit StartPoint elem us e Maybe () h action us a act -> Expr StartPoint StartPoint elem us -> Maybe () -> action us a -> Alt StartPoint StartPoint elem (Maybe ()) action a forall k k1 nonTerminal terminal (elem :: k) (us :: [k]) altDoc (action :: [k] -> k1 -> *) (a :: k1). Expr nonTerminal terminal elem us -> altDoc -> action us a -> Alt nonTerminal terminal elem altDoc action a SyntaxGrammar.Alt do Expr StringLit StartPoint elem us -> Expr StartPoint StartPoint elem us forall (us :: [*]). Expr StringLit StartPoint elem us -> Expr StartPoint StartPoint elem us fixExpr Expr StringLit StartPoint elem us e do Maybe () h do action us a act fixExpr :: SyntaxGrammar.Expr IntermNonTerminal Terminal elem us -> SyntaxGrammar.Expr NonTerminal Terminal elem us fixExpr :: Expr StringLit StartPoint elem us -> Expr StartPoint StartPoint elem us fixExpr = (forall x. Membership us x -> Unit StringLit StartPoint elem x -> Unit StartPoint StartPoint elem x) -> Expr StringLit StartPoint elem us -> Expr StartPoint StartPoint elem us forall k (xs :: [k]) (f :: k -> *) (g :: k -> *). (forall (x :: k). Membership xs x -> f x -> g x) -> HFList f xs -> HFList g xs HFList.hmapWithIndex do \Membership us x _ Unit StringLit StartPoint elem x u1 -> Unit StringLit StartPoint elem x -> Unit StartPoint StartPoint elem x forall u. Unit StringLit StartPoint elem u -> Unit StartPoint StartPoint elem u fixUnit Unit StringLit StartPoint elem x u1 fixUnit :: SyntaxGrammar.Unit IntermNonTerminal Terminal elem u -> SyntaxGrammar.Unit NonTerminal Terminal elem u fixUnit :: Unit StringLit StartPoint elem u -> Unit StartPoint StartPoint elem u fixUnit Unit StringLit StartPoint elem u u = case Unit StringLit StartPoint elem u u of SyntaxGrammar.UnitToken StartPoint t -> StartPoint -> Unit StartPoint StartPoint elem elem forall k terminal nonTerminal (elem :: k). terminal -> Unit nonTerminal terminal elem elem SyntaxGrammar.UnitToken StartPoint t SyntaxGrammar.UnitVar StringLit v -> StartPoint -> Unit StartPoint StartPoint elem u forall k nonTerminal terminal (elem :: k) (u :: k). nonTerminal -> Unit nonTerminal terminal elem u SyntaxGrammar.UnitVar do StringLit -> StartPoint getNewV StringLit v rulesTag :: HashMap StringLit StartPoint rulesTag = Proxy# rules -> HashMap StringLit StartPoint forall rules. Rules rules => Proxy# rules -> HashMap StringLit StartPoint genRulesTagMap do Proxy# rules forall k (a :: k). Proxy# a proxy# @rules getNewV :: StringLit -> StartPoint getNewV StringLit v = case StringLit -> HashMap StringLit StartPoint -> Maybe StartPoint forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v HashMap.lookup StringLit v HashMap StringLit StartPoint rulesTag of Just StartPoint newV -> StartPoint newV Maybe StartPoint Nothing -> StringLit -> StartPoint forall a. HasCallStack => StringLit -> a error StringLit "unreachable: rulesTag must include v." type StartPoint = Int type Terminal = Int type NonTerminal = Int type IntermNonTerminal = String class MemberInitials rules initials where memberInitials :: HFList.T (HFList.DictF (HasRuleExprField rules)) initials class Rules rules where generateRules :: HFList.T (HFList.DictF (HasRuleExprField rules)) (RulesTag rules) genStartPoint :: forall initials v. Membership.Membership initials v -> StartPoint genStartPoint :: Membership initials v -> StartPoint genStartPoint Membership initials v m = Membership initials v -> StartPoint forall k (initials :: [k]) (v :: k). Membership initials v -> StartPoint Membership.getMemberId Membership initials v m genRulesTagMap :: forall rules. Rules rules => Proxy# rules -> HashMap.HashMap IntermNonTerminal NonTerminal genRulesTagMap :: Proxy# rules -> HashMap StringLit StartPoint genRulesTagMap Proxy# rules _ = HashMap StringLit StartPoint -> (forall (x :: Symbol). HashMap StringLit StartPoint -> Membership (RulesTag rules) x -> DictF (HasRuleExprField rules) x -> HashMap StringLit StartPoint) -> HFList (DictF (HasRuleExprField rules)) (RulesTag rules) -> HashMap StringLit StartPoint forall k r (xs :: [k]) (f :: k -> *). r -> (forall (x :: k). r -> Membership xs x -> f x -> r) -> HFList f xs -> r HFList.hfoldlWithIndex HashMap StringLit StartPoint forall k v. HashMap k v HashMap.empty forall (x :: Symbol). HashMap StringLit StartPoint -> Membership (RulesTag rules) x -> DictF (HasRuleExprField rules) x -> HashMap StringLit StartPoint go HFList (DictF (HasRuleExprField rules)) (RulesTag rules) forall rules. Rules rules => T (DictF (HasRuleExprField rules)) (RulesTag rules) generateRules where go :: forall v . HashMap.HashMap IntermNonTerminal NonTerminal -> Membership.Membership (RulesTag rules) v -> HFList.DictF (HasRuleExprField rules) v -> HashMap.HashMap IntermNonTerminal NonTerminal go :: HashMap StringLit StartPoint -> Membership (RulesTag rules) v -> DictF (HasRuleExprField rules) v -> HashMap StringLit StartPoint go HashMap StringLit StartPoint vMap Membership (RulesTag rules) v m DictF (HasRuleExprField rules) v HFList.DictF = StringLit -> StartPoint -> HashMap StringLit StartPoint -> HashMap StringLit StartPoint forall k v. (Eq k, Hashable k) => k -> v -> HashMap k v -> HashMap k v HashMap.insert do Proxy# v -> StringLit forall (n :: Symbol). KnownSymbol n => Proxy# n -> StringLit symbolVal' do Proxy# v forall k (a :: k). Proxy# a proxy# @v do Membership (RulesTag rules) v -> StartPoint forall k (initials :: [k]) (v :: k). Membership initials v -> StartPoint Membership.getMemberId Membership (RulesTag rules) v m do HashMap StringLit StartPoint vMap type RuleExpr :: ([Type] -> Type -> Type) -> Type -> Type -> Type -> Type -> Type newtype RuleExpr action rules tokens elem a = RuleExpr { RuleExpr action rules tokens elem a -> [Alt action rules tokens elem a] unRuleExpr :: [Alt action rules tokens elem a] } type Alt :: ([Type] -> Type -> Type) -> Type -> Type -> Type -> Type -> Type newtype Alt action rules tokens elem a = UnsafeAlt { Alt action rules tokens elem a -> Alt StringLit StartPoint elem (Maybe ()) action a unsafeAlt :: SyntaxGrammar.Alt IntermNonTerminal Terminal elem (Maybe ()) action a } type Expr :: Type -> Type -> Type -> [Type] -> Type newtype Expr rules tokens elem us = UnsafeExpr { Expr rules tokens elem us -> Expr StringLit StartPoint elem us unsafeExpr :: SyntaxGrammar.Expr IntermNonTerminal Terminal elem us } class TokensMember tokens t where tokensMembership :: Proxy# '(tokens, t) -> Membership.Membership (TokensTag tokens) t ruleExpr :: [Alt action rules tokens elem a] -> RuleExpr action rules tokens elem a ruleExpr :: [Alt action rules tokens elem a] -> RuleExpr action rules tokens elem a ruleExpr [Alt action rules tokens elem a] alts = [Alt action rules tokens elem a] -> RuleExpr action rules tokens elem a forall (action :: [*] -> * -> *) rules tokens elem a. [Alt action rules tokens elem a] -> RuleExpr action rules tokens elem a RuleExpr [Alt action rules tokens elem a] alts (<:>) :: Expr rules tokens elem us -> action us a -> Alt action rules tokens elem a UnsafeExpr Expr StringLit StartPoint elem us e <:> :: Expr rules tokens elem us -> action us a -> Alt action rules tokens elem a <:> action us a act = Alt StringLit StartPoint elem (Maybe ()) action a -> Alt action rules tokens elem a forall (action :: [*] -> * -> *) rules tokens elem a. Alt StringLit StartPoint elem (Maybe ()) action a -> Alt action rules tokens elem a UnsafeAlt do Expr StringLit StartPoint elem us -> Maybe () -> action us a -> Alt StringLit StartPoint elem (Maybe ()) action a forall k k1 nonTerminal terminal (elem :: k) (us :: [k]) altDoc (action :: [k] -> k1 -> *) (a :: k1). Expr nonTerminal terminal elem us -> altDoc -> action us a -> Alt nonTerminal terminal elem altDoc action a SyntaxGrammar.Alt Expr StringLit StartPoint elem us e Maybe () forall a. Maybe a Nothing action us a act infixl 4 <:> eps :: Expr rules tokens elem '[] eps :: Expr rules tokens elem '[] eps = Expr StringLit StartPoint elem '[] -> Expr rules tokens elem '[] forall rules tokens elem (us :: [*]). Expr StringLit StartPoint elem us -> Expr rules tokens elem us UnsafeExpr Expr StringLit StartPoint elem '[] forall k (a :: k -> *). HFList a '[] HFList.HFNil (<^>) :: Expr rules tokens elem us1 -> Expr rules tokens elem us2 -> Expr rules tokens elem (HFList.Concat us1 us2) UnsafeExpr Expr StringLit StartPoint elem us1 e1 <^> :: Expr rules tokens elem us1 -> Expr rules tokens elem us2 -> Expr rules tokens elem (Concat us1 us2) <^> UnsafeExpr Expr StringLit StartPoint elem us2 e2 = Expr StringLit StartPoint elem (Concat us1 us2) -> Expr rules tokens elem (Concat us1 us2) forall rules tokens elem (us :: [*]). Expr StringLit StartPoint elem us -> Expr rules tokens elem us UnsafeExpr do Expr StringLit StartPoint elem us1 -> Expr StringLit StartPoint elem us2 -> Expr StringLit StartPoint elem (Concat us1 us2) forall k (f :: k -> *) (xs1 :: [k]) (xs2 :: [k]). HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2) HFList.hconcat Expr StringLit StartPoint elem us1 e1 Expr StringLit StartPoint elem us2 e2 infixr 5 <^> var :: KnownSymbol v => proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v] var :: proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v] var proxy v p = Expr StringLit StartPoint elem '[RuleExprReturnType rules v] -> Expr rules tokens elem '[RuleExprReturnType rules v] forall rules tokens elem (us :: [*]). Expr StringLit StartPoint elem us -> Expr rules tokens elem us UnsafeExpr do Unit StringLit StartPoint elem (RuleExprReturnType rules v) -> HFList (Unit StringLit StartPoint elem) '[] -> Expr StringLit StartPoint elem '[RuleExprReturnType rules v] forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> HFList a xs -> HFList a (x : xs) HFList.HFCons Unit StringLit StartPoint elem (RuleExprReturnType rules v) u HFList (Unit StringLit StartPoint elem) '[] forall k (a :: k -> *). HFList a '[] HFList.HFNil where u :: Unit StringLit StartPoint elem (RuleExprReturnType rules v) u = StringLit -> Unit StringLit StartPoint elem (RuleExprReturnType rules v) forall k nonTerminal terminal (elem :: k) (u :: k). nonTerminal -> Unit nonTerminal terminal elem u SyntaxGrammar.UnitVar do proxy v -> StringLit forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> StringLit symbolVal proxy v p varA :: forall v rules tokens elem. KnownSymbol v => Expr rules tokens elem '[RuleExprReturnType rules v] varA :: Expr rules tokens elem '[RuleExprReturnType rules v] varA = Proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v] forall (v :: Symbol) (proxy :: Symbol -> *) rules tokens elem. KnownSymbol v => proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v] var do Proxy v forall k (t :: k). Proxy t Proxy @v tok :: Membership.Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem] tok :: Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem] tok Membership (TokensTag tokens) t p = Expr StringLit StartPoint elem '[elem] -> Expr rules tokens elem '[elem] forall rules tokens elem (us :: [*]). Expr StringLit StartPoint elem us -> Expr rules tokens elem us UnsafeExpr do Unit StringLit StartPoint elem elem -> HFList (Unit StringLit StartPoint elem) '[] -> Expr StringLit StartPoint elem '[elem] forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> HFList a xs -> HFList a (x : xs) HFList.HFCons Unit StringLit StartPoint elem elem u HFList (Unit StringLit StartPoint elem) '[] forall k (a :: k -> *). HFList a '[] HFList.HFNil where u :: Unit StringLit StartPoint elem elem u = StartPoint -> Unit StringLit StartPoint elem elem forall k terminal nonTerminal (elem :: k). terminal -> Unit nonTerminal terminal elem elem SyntaxGrammar.UnitToken do HEnum (TokensTag tokens) -> StartPoint forall k (as :: [k]). HEnum as -> StartPoint HEnum.unsafeHEnum do Membership (TokensTag tokens) t -> HEnum (TokensTag tokens) forall k (a :: k) (as :: [k]). Membership as a -> HEnum as HEnum.henum Membership (TokensTag tokens) t p tokA :: forall t rules tokens elem. TokensMember tokens t => Expr rules tokens elem '[elem] tokA :: Expr rules tokens elem '[elem] tokA = Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem] forall tokens (t :: Symbol) rules elem. Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem] tok do Proxy# '(tokens, t) -> Membership (TokensTag tokens) t forall tokens (t :: Symbol). TokensMember tokens t => Proxy# '(tokens, t) -> Membership (TokensTag tokens) t tokensMembership do Proxy# '(tokens, t) forall k (a :: k). Proxy# a proxy# @'(tokens, t)