Re: [Haskell-cafe] Need help with advanced type-level programming

On Sat, 25 Apr 2020, Ximin Luo wrote:

Evgeny Permyakov:

...

Consider following code

data Tag :: (Symbol -> Constraint) -> Symbol -> * where  Tag :: (KnownSymbol s, con s) => Tag con s

data TagList :: (Symbol -> Constraint) -> [Symbol] -> * where  LNil :: TagList con '[]  LCon :: Tag con s -> TagList con ss -> TagList con (s ': ss)

data TagSet :: (Symbol -> Constraint ) -> [Symbol] -> * where  SNil :: TagSet con '[]  SSin :: Tag con s -> TagSet con '[s]  SCon :: CmpSymbol ht mt ~ LT => Tag con ht -> TagSet con (mt ': ts) -> TagSet con (ht ': mt ': ts)

If your problem is about maintaining sets of constraints, that might be easier to achieve by just maintaining sets of constraints.