<div dir="ltr">Bah. I misparsed the note; it doesn't rule out casting coboxes.<div><br></div><div>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...</div><div><br></div><div>Thanks for the castCoercionKind tip</div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Sep 20, 2017 at 7:59 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><blockquote type="cite"><div>On Sep 20, 2017, at 8:52 PM, Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com" target="_blank">nicolas.frisby@gmail.com</a>> wrote:</div><div><div dir="ltr"><div><br></div><div>* 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 "<span style="color:rgb(117,117,117)">by using UnivCo to cast coboxes</span>" in my previous email.</div></div></div></blockquote><div><br></div></div></div><div style="word-wrap:break-word"><div><div>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.</div></div></div><div style="word-wrap:break-word"><div><div><br></div><div>Richard</div></div></div><div style="word-wrap:break-word"><div><br><blockquote type="cite"><div><div dir="ltr"><div><br></div><div>I'm optimistic that fixing this up will help. Does it sound promising/ring any bells for you?</div><div><br></div><div>Thanks. -Nick</div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Sep 20, 2017 at 7:47 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
> On Sep 19, 2017, at 9:50 AM, Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com" target="_blank">nicolas.frisby@gmail.com</a>> wrote:<br>
><br>
> Questions:<br>
><br>
> 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?)<br>
<br>
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.<br>
<br>
><br>
> 2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes?<br>
<br>
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.<br>
<br>
><br>
> 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?<br>
<br>
I don't think this line of inquiry will be helpful.<br>
<br>
><br>
> 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?<br>
<br>
Not for me.<br>
<br>
I hope this helps!<br>
Richard<br>
<br>
><br>
> Thank you for your time. -Nick<br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
<br>
</blockquote></div>
</div></blockquote></div></div></blockquote></div>