<div dir="ltr"><div>Consider following code <br></div><div><br></div><div><span style="font-family:monospace">data Tag :: (Symbol -> Constraint) -> Symbol -> * where<br> Tag :: (KnownSymbol s, con s) => Tag con s<br><br>data TagList :: (Symbol -> Constraint) -> [Symbol] -> * where<br> LNil :: TagList con '[]<br> LCon :: Tag con s -> TagList con ss -> TagList con (s ': ss)<br><br>data TagSet :: (Symbol -> Constraint ) -> [Symbol] -> * where<br> SNil :: TagSet con '[]<br> SSin :: Tag con s -> TagSet con '[s]<br> SCon :: CmpSymbol ht mt ~ LT => Tag con ht -> TagSet con (mt ': ts) -> TagSet con (ht ': mt ': ts)<br></span></div><div><br></div><div>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.<br></div><div><br></div><div>Similarly, it would be greatly appreciated if someone could show how to implement following typeclass </div><div><br></div><div><span style="font-family:monospace">class CmpTag (s1 :: Symbol) (s2 :: Symbol) where<br> cmpTag :: Tag con s1 -> Tag con s2 -> OrdTag con (CmpSymbol s1 s2) s1 s2</span></div><div><span style="font-family:monospace"><br></span></div><div><span style="font-family:monospace">data OrdTag :: (Symbol -> Constraint) -> Ordering -> Symbol -> Symbol -> *  where<br> TLT ::  CmpSymbol s1 s2 ~ LT           => Tag con s1 -> Tag con s2 -> OrdTag con LT s1 s2<br> TEQ :: (CmpSymbol s1 s2 ~ EQ, s1 ~ s2) => Tag con s  -> Tag con s2 -> OrdTag con EQ s1 s2<br> TGT ::  CmpSymbol s1 s2 ~ GT           => Tag con s1 -> Tag con s2 -> OrdTag con GT s1 s2<br></span><br></div></div>