Invariants about UnivCo?

Nicolas Frisby nicolas.frisby at gmail.com
Thu Sep 21 02:52:15 UTC 2017


Thanks for the reply Richard, I really appreciate it.

Your email actually buzzed my phone just as I was opening my laptop to
draft this email. I'm optimistic that I may have identified part of the
issue.

* 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.

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/469238aa/attachment.html>


More information about the ghc-devs mailing list