Invariants about UnivCo?
nicolas.frisby at gmail.com
Thu Sep 21 03:08:32 UTC 2017
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>
> On Sep 20, 2017, at 8:52 PM, Nicolas Frisby <nicolas.frisby at gmail.com>
> * 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.
> 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>
>> > On Sep 19, 2017, at 9:50 AM, Nicolas Frisby <nicolas.frisby at gmail.com>
>> > 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
>> 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!
>> > 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...
More information about the ghc-devs