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

[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)

How one would write a function converting a TagList into a TagSet ,
dropping duplicate tags ? I tried a few approaches, but failed. I clearly
lack understanding how to fit it into GHC type system. I know there is a
library  type-level-sets, but it isn't what I would like and I don't
understand how it fits into GHC type system, so it appears to be magical to
me.

Similarly, it would be greatly appreciated if someone could show how to
implement following typeclass

class CmpTag (s1 :: Symbol) (s2 :: Symbol) where
 cmpTag :: Tag con s1 -> Tag con s2 -> OrdTag con (CmpSymbol s1 s2) s1 s2

data OrdTag :: (Symbol -> Constraint) -> Ordering -> Symbol -> Symbol -> *
 where
 TLT ::  CmpSymbol s1 s2 ~ LT           => Tag con s1 -> Tag con s2 ->
OrdTag con LT s1 s2
 TEQ :: (CmpSymbol s1 s2 ~ EQ, s1 ~ s2) => Tag con s  -> Tag con s2 ->
OrdTag con EQ s1 s2
 TGT ::  CmpSymbol s1 s2 ~ GT           => Tag con s1 -> Tag con s2 ->
OrdTag con GT s1 s2
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200424/6266227a/attachment.html>