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
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@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
No, I've not tested against head. I'd not heard anything new about that! That sounds exciting. Sorry about the noise if it's all finished already. David On Thu, Oct 22, 2015 at 9:57 AM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
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@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
participants (2)
-
David Feuer -
Richard Eisenberg