Coercion logic

Richard Eisenberg eir at cis.upenn.edu
Thu Oct 22 13:57:56 UTC 2015


The Coercible solver has evolved steadily. It should know that (Coercible a b <=> Coercible b a). Do you have a concrete example of where it's not doing this? Have you tested against HEAD?

Thanks,
Richard

On Oct 22, 2015, at 9:56 AM, David Feuer <david.feuer at gmail.com> wrote:

> At present, any time we write a function with a `Coercible`
> constraint, we must take great care to choose `Coercible a b` or
> `Coercible b a` depending on which will ultimately lead to fewer silly
> conversions. This is particularly sad because the whole Coercible
> mechanism guarantees that these have exactly the same run-time
> representation, and because People Wiser Than Me believe Coercible
> should *always* remain symmetric. My (admittedly reptilian) brain
> wonders what it would take to tell the type checker that
> 
> forall a b . Coercible a b ~ Coercible b a
> 
> and have it over with.
> 
> David Feuer
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



More information about the ghc-devs mailing list