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

[Richard Eisenberg]

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 <permeakra at gmail.com> 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.