By semantic
 CmpSymbol s1 s2 ~ EQ should be equivalent to s1 ~ s2 for s1 , s2 :: Symbol

Does GHC recognize it? If not, is there some trick to obtain evidence of the second constraint from the first ? I'm talking about context of type class instance declarations.