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.fri...@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 > <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 <simo...@microsoft.com > <mailto:simo...@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-boun...@haskell.org > <mailto:ghc-devs-boun...@haskell.org>] On Behalf Of Nicolas Frisby > Sent: 19 September 2017 16:51 > To: ghc-devs@haskell.org <mailto:ghc-devs@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@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
