<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
@font-face
{font-family:"Segoe UI";
panose-1:2 11 5 2 4 2 4 2 2 3;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
code
{mso-style-priority:99;
font-family:"Courier New";}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
p.Code, li.Code, div.Code
{mso-style-name:Code;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
margin-bottom:.0001pt;
font-size:9.0pt;
font-family:"Courier New";}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle21
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;
font-weight:normal;
font-style:normal;
text-decoration:none none;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri",sans-serif;
mso-fareast-language:EN-US;}
.MsoPapDefault
{mso-style-type:export-only;
margin-top:6.0pt;
margin-right:0cm;
margin-bottom:6.0pt;
margin-left:0cm;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:2012296539;
mso-list-type:hybrid;
mso-list-template-ids:129289452 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-18.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:12.0pt">Some thoughts<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo1"><span style="font-size:12.0pt">Read Note [Coercion holes] in TyCoRep.<o:p></o:p></span></li></ul>
<p class="MsoListParagraph"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo1"><span style="font-size:12.0pt">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<o:p></o:p></span></li></ul>
<p class="MsoListParagraph"><span style="font-size:12.0pt">where d is some dictionary with a superclass of type (a ~# b).<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:12.0pt">Side note: the use of “cobox” is wildly unhelpful. These Ids are specifically
<b>unboxed</b>! I’m going to change it to just “co”.<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo1">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.<o:p></o:p></li></ul>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo1">Do -ddump-tc -fprint-typechecker-elaboration; that should show you the evidence binds.<o:p></o:p></li></ul>
<p class="MsoNormal"><o:p> </o:p></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<o:p></o:p></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo1">Extra assertions, such as that above<o:p></o:p></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l0 level1 lfo1"><b><span style="font-family:"Courier New"">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<o:p></o:p></li></ul>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Richard and I know too much! – your learning curve is very valuable and I don’t want to lose it.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></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.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Simon<o:p></o:p></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-devs [mailto:ghc-devs-bounces@haskell.org]
<b>On Behalf Of </b>Nicolas Frisby<br>
<b>Sent:</b> 19 September 2017 16:51<br>
<b>To:</b> ghc-devs@haskell.org<br>
<b>Subject:</b> Invariants about UnivCo?<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
[I summarize with some direct questions at the bottom of this email.]<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<o:p> </o:p></p>
</div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;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.<o:p></o:p></p>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<o:p> </o:p></p>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;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">https://github.com/nfrisby/coxswain/issues/3#issuecomment-330577609</a><o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Here's the relevant bit:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292E">The latest unresolved </span><code><span style="font-size:9.0pt;font-family:Consolas;color:#24292E">-dcore-lint</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292E"> error
is an out-of-scope </span><code><span style="font-size:9.0pt;font-family:Consolas;color:#24292E">cobox</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292E"> co var. I'm certainly not creating it <em><span style="font-family:"Segoe UI",sans-serif">directly</span></em> (there
are no </span><code><span style="font-size:9.0pt;font-family:Consolas;color:#24292E">U(plugin:coxswain,...</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292E"> in the Core Lint warning), but I have to wonder if my somewhat
loose use of </span><code><span style="font-size:9.0pt;font-family:Consolas;color:#24292E">UnivCo</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292E"> 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><span style="font-size:9.0pt;font-family:Consolas;color:#24292E">UnivCo</span></code><span style="font-size:10.5pt;font-family:"Segoe UI",sans-serif;color:#24292E"> for
source comments looking for anything it should <em><span style="font-family:"Segoe UI",sans-serif">not</span></em> be used for, but I didn't find an obvious explanation along those lines.</span> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I haven't yet been able to effectively distill the test case.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I'm doing this all at -O0.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> [G] cobox_a67J = CO Sym cobox_a654,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> [G] cobox_a67M<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> = cobox_a67J `cast` U(plugin:coxswain,...)<o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">cobox_a654 is introduced by a GADT pattern match. <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Questions:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<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?)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">2) Is my plugin asking for this kind of trouble by using UnivCo to cast coboxes?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<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?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<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?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Thank you for your time. -Nick<o:p></o:p></p>
</div>
</div>
</div>
</div>
</body>
</html>