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

[Henning Thielemann]

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.