RE: Invariants about UnivCo?

...@gmail.com] Sent: 09 October 2017 03:50 To: Richard Eisenberg <r...@cs.brynmawr.edu> Cc: Simon Peyton Jones <simo...@microsoft.com>; ghc-devs@haskell.org Subject: Re: Invariants about UnivCo? Yep, that's the current question: why does preferring `EvCoercion (TransCo UnivCo (Trans

RE: Invariants about UnivCo?

on. Maybe we want the same for coercions? Simon From: Nicolas Frisby [mailto:nicolas.fri...@gmail.com] Sent: 09 October 2017 03:50 To: Richard Eisenberg <r...@cs.brynmawr.edu> Cc: Simon Peyton Jones <simo...@microsoft.com>; ghc-devs@haskell.org Subject: Re: Invariants about UnivCo?

Re: Invariants about UnivCo?

Yep, that's the current question: why does preferring `EvCoercion (TransCo UnivCo (TransCo co UnivCo))` to `EvCast (EvCoercion co) UnivCo` seem to matter? In my scenario, `co` is the evidence for a Given equality type. And the coercion I'm building is also a Given constraint's evidence -- I'm

Re: Invariants about UnivCo?

Thanks for this status report. If I'm to boil it down to the question you seem to be asking: What does changing EvCast ... to EvCoercion ... fix the problem? I'm not sure of the answer at this point, but I want to make sure I understand the question before I go digging for an answer. It's

Re: Invariants about UnivCo?

I can happily report some progress: I'm seeing no more Core lint errors! 1) Thank you both Richard and Simon for your pointers -- -fprint-typechecker-elaboration in particular was a revelation. 2) Simon, I intend to match the spirit of the favor you requested, but not to the letter. My goal with

RE: Invariants about UnivCo?

Some thoughts * Read Note [Coercion holes] in TyCoRep. * As you’ll see, generally we don’t create value-bindings for (unboxed) coercions of type t1 ~# t2. (yes for boxed ones t1 ~ t2). Reasons in the Note. Exception: for superclasses of Givens we do create(co :: a ~# b) =

Re: Invariants about UnivCo?

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

Re: Invariants about UnivCo?

> On Sep 20, 2017, at 8:52 PM, Nicolas Frisby 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:

Re: Invariants about UnivCo?

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

Re: Invariants about UnivCo?

> On Sep 19, 2017, at 9:50 AM, Nicolas Frisby 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