Invariants about UnivCo?

Mon Oct 9 02:50:16 UTC 2017

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
simplifying Givens.

The only hard indication I currently have of what "goes wrong" is the
ASSERT failure described in the previous email.

I'm planning to spend some time investigating. I would appreciate any
cycles you spend on it!

On Sun, Oct 8, 2017, 18:53 Richard Eisenberg <rae at cs.brynmawr.edu> wrote:

> 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 always
> possible a Note is wrong!
>
> Thanks for this!
>
> Richard
>
> On Oct 7, 2017, at 8:19 PM, Nicolas Frisby <nicolas.frisby at gmail.com>
> wrote:
>
> 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 this project is to write a typechecker plugin
> for achieving row types _without_ editing GHC's source code. I'm keeping an
> annotated bibliography of things I've studied (papers, guide/wiki/blog,
> source Notes, etc). (It's nice to put a bunch of related notes in the same
> text file!) I'm also logging my epiphanies, which I do intend to write-up
> in some kind of document (probably on the dev wiki). I'm planning a section
> for suggesting which Notes should be adjusted/expanded, but I don't
> anticipate feeling comfortable enough to actually edit the Notes myself.
> This is unfortunately just a hobby project. My intent is to offer you,
> Richard, and other experts the details of what wasn't clear to me.
>
> 3) I confirmed that the lack of cobox uniques in the dump output was
> indeed due to `ppr_co' deferring to `ppr @IfaceType'; it does that (at
> least) for every coercion with a head of `TyConAppCo'. With a tiny kludgy
> patch I was able to persist those uniques just for debugging purposes.
>
> 4) My top-level error is an "out of scope cobox" Lint error, but (once I
> patched the dumper) the output of -fprint-typechecker-elaboration showed
> sufficient bindings for all of the cobox occurrences, even the one that the
> Lint error was flagging! Stymied, I finally did a -DDEBUG build of the
> ghc-8.2.2-rc1 tag and used that. It ultimately lead to me finding my
> mistakes. (New wisdom: always use a DEBUG build when authoring a plugin.
> (... Duh.))
>
> 4a) ASSERT failures showed that I was invoking `substTy' without correctly
> initializing the `InScopeSet'. I also was ignorant that I should be using
> `extendTvSubstAndInScope' instead of just `extendTvSubst'. I don't think
> this was relevant to my particular Lint error, but I fixed it if only to
> see further ASSERT failures.
>
> 4b) Fixing my `InScopeSet's ASSERT failure revealed another:
> `extendIdSubst' was being called with a CoVar! That's something that my
> plugin code absolutely does not do, so at that point I knew that some
> higher-level operation I was doing was knocking the rest of GHC's pipeline
> off the rails. (In particular, I traced this ASSERT callstack to
> extendIdSubst called from simpleOptExpr called from
> mkInlineUnfoldingWithArity called from DsBinds. I stopped there.)
>
> 5) The first suspect turned out to be the culprit: I was using my plugin's
> by-fiat coercions in the most naive possible way, always simply `EvCast ev
> (fiatCoercion ty0 ty1)`. In particular, I was even doing that to create new
> Given unlifted equality witnesses from existing Given unlifted equality
> witnesses when simplifying Given constraints (e.g. for example reducing a
> plugin-specific type family application on one side of an unlifted equality
> type ~#).
>
> In summary, I see no more ASSERT failures or Lint errors having now
> changed my plugin to prefer `EvCoercion (TransCo U (TransCo co U))` to
> `EvCast (EvCoercion co) U`. The actual diff excerpt is here:
> https://github.com/nfrisby/coxswain/issues/3#issuecomment-334972227
>
> I have not figured out exactly why that change matters, but it does seem a
> reasonable preference to require. In particular, Note [Coercion evidence
> terms] in TcEvidence.hs explicitly says that `EvCast (EvCoercion co1) co2`
> is a valid form of evidence for ~#. So perhaps that Note deserves
> elaboration --- I'm guessing the missing part may be specific to Givens?
>
> -Nick
>
> On Thu, Sep 21, 2017 at 2:59 AM Simon Peyton Jones <simonpj at microsoft.com>
> wrote:
>
>> 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) = sc_sel1 d
>>
>> where d is some dictionary with a superclass of type (a ~# b).
>>
>>
>>
>> Side note: the use of “cobox” is wildly unhelpful.  These Ids are
>> specifically *unboxed*!  I’m going to change it to just “co”.
>>
>>
>>
>>    - You appear to have bindings like[G]  cobox_a67J = CO Sym
>>    cobox_a654.  That is suspicious.  Who is creating them?  It may not
>>    actually be wrong but it’s suspicious.  The time it’d be outright wrong is
>>    if you dropped the ev-binds on the floor.
>>
>>
>>
>> Ha!  runTcSEqualites makes up an ev_binds_var, and solves the equalities
>> – but it should be the case that no value bindings end up in the
>> ev_binds_var.  (reason: we are solving equalities in a type signature, so
>> there is no place to put the evidence bindigns)   I suggest you add a
>> DEBUG-only assertion to check this.
>>
>>
>>
>>    - Do -ddump-tc -fprint-typechecker-elaboration; that should show you
>>    the evidence binds.
>>
>>
>>
>> Can I ask you a favour?  Separately from your branch, can you start a
>> branch of small patches to GHC that include
>>
>>    - Extra assertions, such as that above
>>    - *Notes* that explain things you wish you’d known earlier, with
>>    references to those Notes from the places you were studying when you that
>>    information would have been useful
>>
>>
>>
>> Richard and I know too much! – your learning curve is very valuable and I
>> don’t want to lose it.
>>
>>
>>
>> Keeping this separate from your branch is useful : you can commit (via
>> Phab) these updates right away, so they aren’t predicated on adding row
>> types to GHC.
>>
>>
>>
>> Simon
>>
>>
>>
>> *From:* ghc-devs [mailto:ghc-devs-bounces at haskell.org] *On Behalf Of *Nicolas
>> Frisby
>> *Sent:* 19 September 2017 16:51
>> *To:* ghc-devs at haskell.org
>> *Subject:* Invariants about UnivCo?
>>
>>
>>
>> [I summarize with some direct questions at the bottom of this email.]
>>
>>
>>
>> I spent time last night trying to eliminate -dcore-lint errors from my
>> record and variant library using the coxswain row types plugin. I made some
>> progress, but I'm currently stuck, as discussed on this github Issue.
>>
>>
>>
>> https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609
>> <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnfrisby%2Fcoxswain%2Fissues%2F3%23issuecomment-330577609&data=02%7C01%7Csimonpj%40microsoft.com%7Cde0675bbb584495a2f8008d4ff764c72%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636414330952932223&sdata=lPLcpIlb%2BhivQdCUoVOPUgYDHeEDaMX660NQS%2BQyyBw%3D&reserved=0>
>>
>>
>>
>> Here's the relevant bit:
>>
>>
>>
>> The latest unresolved -dcore-lint error is an out-of-scope cobox co var.
>> I'm certainly not creating it *directly* (there are no
>> U(plugin:coxswain,... in the Core Lint warning), but I have to wonder if
>> my somewhat loose use of UnivCo is violating some assumptions somewhere
>> that's causing GHC to drop the co var binding or overlook this occurrence
>> of it on a renaming/subst pass. I checked UnivCo for source comments
>> looking for anything it should *not* be used for, but I didn't find an
>> obvious explanation along those lines.
>>
>>
>>
>> I haven't yet been able to effectively distill the test case.
>>
>>
>>
>> I'm doing this all at -O0.
>>
>>
>>
>> With `-ddump-tc-trace`, I can see the offending cobox (cobox_a67M) is
>> present in an "implication evbinds" listing after a "solveImplication end
>> }" delimiter, but that's the last obvious binding of it.
>>
>>
>>
>>                          [G] cobox_a67J = CO Sym cobox_a654,
>>
>>                          [G] cobox_a67M
>>
>>                            = cobox_a67J `cast` U(plugin:coxswain,...)
>>
>>
>>
>> cobox_a654 is introduced by a GADT pattern match.
>>
>>
>>
>> I'm also not seeing obvious occurrences of cobox_a67M, but I think the
>> reason is that I'm seeing several (Sym cobox) with no uniques printed (even
>> with `-dppr-debug`). Those are probably the cobox in question, but I can't
>> confirm.
>>
>>
>>
>> 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?)
>>
>>
>>
>> 2) Is my plugin asking for this kind of trouble by using UnivCo to cast
>> coboxes?
>>
>>
>>
>> 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?
>>
>>
>>
>> 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?
>>
>>
>>
>> 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/20171009/3c05b33d/attachment-0001.html>