<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">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!</div><div class=""><br class=""></div><div class="">Thanks for this!</div><div class=""><br class=""></div><div class="">Richard</div><br class=""><div><blockquote type="cite" class=""><div class="">On Oct 7, 2017, at 8:19 PM, Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com" class="">nicolas.frisby@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">I can happily report some progress: I'm seeing no more Core lint errors!<div class=""><br class=""></div><div class="">1) Thank you both Richard and Simon for your pointers -- <span style="color:rgb(33,33,33);font-family:Calibri,sans-serif;font-size:14.6667px" class="">-fprint-typechecker-</span><span style="color:rgb(33,33,33);font-family:Calibri,sans-serif;font-size:14.6667px" class="">elaboration</span> in particular was a revelation.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">4) My top-level error is an "out of scope cobox" Lint error, but (once I patched the dumper) the output of <span style="color:rgb(33,33,33);font-family:Calibri,sans-serif;font-size:14.6667px" class="">-fprint-typechecker-</span><span style="color:rgb(33,33,33);font-family:Calibri,sans-serif;font-size:14.6667px" class="">elaboration</span> 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.))</div><div class=""><br class=""></div><div class="">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.<br class=""><br class="">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.)</div><div class=""><br class=""></div><div class="">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 ~#).<br class=""><br class="">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: <a href="https://github.com/nfrisby/coxswain/issues/3#issuecomment-334972227" class="">https://github.com/nfrisby/coxswain/issues/3#issuecomment-334972227</a><br class=""></div><div class=""><br class=""></div><div class="">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?</div><div class=""><br class=""></div><div class="">-Nick</div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="">On Thu, Sep 21, 2017 at 2:59 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" class="">simonpj@microsoft.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple" class="">
<div class="m_-3607345558727168865WordSection1"><p class="MsoNormal"><span style="font-size:12.0pt" class="">Some thoughts<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
<ul style="margin-top:0cm" type="disc" class="">
<li class="m_-3607345558727168865MsoListParagraph" style="margin-left:0cm"><span style="font-size:12.0pt" class="">Read Note [Coercion holes] in TyCoRep.<u class=""></u><u class=""></u></span></li></ul><p class="m_-3607345558727168865MsoListParagraph"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
<ul style="margin-top:0cm" type="disc" class="">
<li class="m_-3607345558727168865MsoListParagraph" style="margin-left:0cm"><span style="font-size:12.0pt" class="">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<u class=""></u><u class=""></u></span></li></ul><p class="m_-3607345558727168865MsoListParagraph"><span style="font-size:12.0pt" class="">where d is some dictionary with a superclass of type (a ~# b).<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:12.0pt" class="">Side note: the use of “cobox” is wildly unhelpful. These Ids are specifically
<b class="">unboxed</b>! I’m going to change it to just “co”.<u class=""></u><u class=""></u></span></p><p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
<ul style="margin-top:0cm" type="disc" class="">
<li class="m_-3607345558727168865MsoListParagraph" style="margin-left:0cm">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.<u class=""></u><u class=""></u></li></ul><p class="MsoNormal"><u class=""></u> <u class=""></u></p><p class="MsoNormal" style="margin-left:36.0pt">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.<u class=""></u><u class=""></u></p><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
<ul style="margin-top:0cm" type="disc" class="">
<li class="m_-3607345558727168865MsoListParagraph" style="margin-left:0cm">Do -ddump-tc -fprint-typechecker-elaboration; that should show you the evidence binds.<u class=""></u><u class=""></u></li></ul><p class="MsoNormal"><u class=""></u> <u class=""></u></p><p class="MsoNormal">Can I ask you a favour? Separately from your branch, can you start a branch of small patches to GHC that include<u class=""></u><u class=""></u></p>
<ul style="margin-top:0cm" type="disc" class="">
<li class="m_-3607345558727168865MsoListParagraph" style="margin-left:0cm">Extra assertions, such as that above<u class=""></u><u class=""></u></li><li class="m_-3607345558727168865MsoListParagraph" style="margin-left:0cm"><b class=""><span style="font-family:"Courier New"" class="">Notes</span></b> 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<u class=""></u><u class=""></u></li></ul><p class="MsoNormal"><u class=""></u> <u class=""></u></p><p class="MsoNormal">Richard and I know too much! – your learning curve is very valuable and I don’t want to lose it.<u class=""></u><u class=""></u></p><p class="MsoNormal"><u class=""></u> <u class=""></u></p><p class="MsoNormal">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.<u class=""></u><u class=""></u></p><p class="MsoNormal"><u class=""></u> <u class=""></u></p><p class="MsoNormal">Simon<u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt" class="">
<div class="">
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm" class=""><p class="MsoNormal"><b class=""><span lang="EN-US" class="">From:</span></b><span lang="EN-US" class=""> ghc-devs [mailto:<a href="mailto:ghc-devs-bounces@haskell.org" target="_blank" class="">ghc-devs-bounces@haskell.org</a>]
<b class="">On Behalf Of </b>Nicolas Frisby<br class="">
<b class="">Sent:</b> 19 September 2017 16:51<br class="">
<b class="">To:</b> <a href="mailto:ghc-devs@haskell.org" target="_blank" class="">ghc-devs@haskell.org</a><br class="">
<b class="">Subject:</b> Invariants about UnivCo?<u class=""></u><u class=""></u></span></p>
</div>
</div></div></div></div><div lang="EN-GB" link="blue" vlink="purple" class=""><div class="m_-3607345558727168865WordSection1"><div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt" class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
<div class="">
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
[I summarize with some direct questions at the bottom of this email.]<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
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.<u class=""></u><u class=""></u></p>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<a href="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" target="_blank" class="">https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609</a><u class=""></u><u class=""></u></p>
</div>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Here's the relevant bit:<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292e" class="">The latest unresolved </span><code class=""><span style="font-size:9.0pt;font-family:Consolas;color:#24292e" class="">-dcore-lint</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292e" class=""> error
is an out-of-scope </span><code class=""><span style="font-size:9.0pt;font-family:Consolas;color:#24292e" class="">cobox</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292e" class=""> co var. I'm certainly not creating it <em class=""><span style="font-family:"Segoe UI",sans-serif" class="">directly</span></em> (there
are no </span><code class=""><span style="font-size:9.0pt;font-family:Consolas;color:#24292e" class="">U(plugin:coxswain,...</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292e" class=""> in the Core Lint warning), but I have to wonder if my somewhat
loose use of </span><code class=""><span style="font-size:9.0pt;font-family:Consolas;color:#24292e" class="">UnivCo</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292e" class=""> 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 </span><code class=""><span style="font-size:9.0pt;font-family:Consolas;color:#24292e" class="">UnivCo</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292e" class=""> for
source comments looking for anything it should <em class=""><span style="font-family:"Segoe UI",sans-serif" class="">not</span></em> be used for, but I didn't find an obvious explanation along those lines.</span> <u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">I haven't yet been able to effectively distill the test case.<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">I'm doing this all at -O0.<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">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.<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class="">
<div class=""><p class="MsoNormal"> [G] cobox_a67J = CO Sym cobox_a654,<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"> [G] cobox_a67M<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"> = cobox_a67J `cast` U(plugin:coxswain,...)<u class=""></u><u class=""></u></p>
</div>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">cobox_a654 is introduced by a GADT pattern match. <u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">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.<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">Questions:<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">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?)<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes?<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">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?<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">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?<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">Thank you for your time. -Nick<u class=""></u><u class=""></u></p>
</div>
</div>
</div></div></div></blockquote></div>
_______________________________________________<br class="">ghc-devs mailing list<br class=""><a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<br class=""></div></blockquote></div><br class=""></body></html>