Invariants about UnivCo?

[Nicolas Frisby]

Bah. I misparsed the note; it doesn't rule out casting coboxes.

However, it does refer to Note [Bind new Givens immediately] in TcRnTypes,
which indicates that maybe I should be explicitly binding an evidence
variable when adjusting given constraints of type t1 ~# t2...

Thanks for the castCoercionKind tip

On Wed, Sep 20, 2017 at 7:59 PM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

> On Sep 20, 2017, at 8:52 PM, Nicolas Frisby <nicolas.frisby at gmail.com>
> wrote:
>
> * Note [Coercion evidence terms] in TcEvidence.hs lists an INVARIANT that
> the evidence for t1 ~# t2 must be built with EvCoercion. I'm very confident
> that I am instead building it with a by-fiat EvCast: this is what I meant
> by "by using UnivCo to cast coboxes" in my previous email.
>
>
> Hm. If you break an INVARIANT, anything can happen. Perhaps you've hit it.
> I think instead of using EvCast, you should use Coercion.castCoercionKind,
> but I'm not sure without knowing more details.
>
> Richard
>
>
> I'm optimistic that fixing this up will help. Does it sound promising/ring
> any bells for you?
>
> Thanks. -Nick
>
> On Wed, Sep 20, 2017 at 7:47 PM Richard Eisenberg <rae at cs.brynmawr.edu>
> wrote:
>
>>
>> > On Sep 19, 2017, at 9:50 AM, Nicolas Frisby <nicolas.frisby at gmail.com>
>> wrote:
>> >
>> > Questions:
>> >
>> > 1) Is there a robust way to ensure that covar's uniques are always
>> printed? (Is the pprIface reuse  with a free cobox part of the issue here?)
>>
>> Try rebasing. I ran into a similar issue not long ago and revised the
>> code around printing coercions. Also, -fprint-explicit-kinds might help. An
>> occurrence of a tyvar is also an implicit occurrence of all the free
>> variables in its kinds.
>>
>> >
>> > 2) Is my plugin asking for this kind of trouble by using UnivCo to cast
>> coboxes?
>>
>> No. `UnivCo`s should work fine. You might potentially be asking for
>> "shoot the gorillas" problems (it has been suggested that we refrain from
>> "launching the rockets", as that event seems a mite too likely these days,
>> unsafeCoerceIO or no; I propose this new formulation, inspired by an
>> utterance by Simon PJ about how when you're tackling bugs, sometimes you
>> shoot one gorilla only to find more behind it... but then he remarked that
>> one, of course, would never want to actually shoot a gorilla.), but I think
>> Core Lint should be OK.
>>
>> >
>> > 3) If I spent the effort to create non-UnivCo coercions where possible,
>> would that likely help? This is currently an "eventually" task, but I
>> haven't seen an urgency for it yet. I could bump its priority if it might
>> help. E.G. I'm using UnivCo to cast entire givens when all I'm doing is
>> reducing a type family application somewhere "deep" within the given's
>> predtype. I could, with considerable effort, instead wrap a single,
>> localized UnivCo within a bunch of non-UnivCo "lifting" coercion
>> constructors. Would that likely help?
>>
>> I don't think this line of inquiry will be helpful.
>>
>> >
>> > 3) Is there a usual suspect for this kind of situation where a cobox
>> binding is seemingly dropped (by the typechecker) even though there's an
>> occurrence of it?
>>
>> Not for me.
>>
>> I hope this helps!
>> Richard
>>
>> >
>> > Thank you for your time. -Nick
>> > _______________________________________________
>> > ghc-devs mailing list
>> > ghc-devs at haskell.org
>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170921/924d0640/attachment-0001.html>