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