Re: [Haskell-cafe] Does GHC recognise that CmpSymbol s1 s2 ~ EQ implies s1 ~ s2 ?

No. As far as I know, GHC has no way of deducing this (although it would be safe to do so). If you need to do this, you could use (s1 :~: s2) and `unsafeCoerce Refl`. It's sad, I know. Happy to expand more if this is too terse! Richard

On Apr 24, 2020, at 12:07 PM, Evgeny Permyakov wrote:

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. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.