Coercion logic

[David Feuer]

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 at 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 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
>