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 <r...@cs.brynmawr.edu> wrote: > On Sep 20, 2017, at 8:52 PM, Nicolas Frisby <nicolas.fri...@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 <r...@cs.brynmawr.edu> > wrote: > >> >> > On Sep 19, 2017, at 9:50 AM, Nicolas Frisby <nicolas.fri...@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@haskell.org >> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> >>
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs