<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;}
/* 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:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
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.EmailStyle19
{mso-style-type:personal;
font-family:"Calibri",sans-serif;
color:windowtext;
font-weight:normal;
font-style:normal;
text-decoration:none none;}
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-size:10.0pt;}
@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:280778;
mso-list-type:hybrid;
mso-list-template-ids:2017127922 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;}
@list l1
{mso-list-id:1943102208;
mso-list-type:hybrid;
mso-list-template-ids:-1120117064 134807553 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l1: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 l1: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 l1: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 l1: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 l1: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 l1: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 l1: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 l1: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 l1: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="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
Nick writes<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
Here's a small indicative example. In the "simplify Givens" step, the plugin receives<o:p></o:p></p>
<p class="Code" style="margin-left:72.0pt"> [G] (p `Union` Singleton A) ~ (q `Union` Singleton B)<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:6.0pt;margin-right:0cm;margin-bottom:6.0pt;margin-left:36.0pt">
and I would ideally simplify that to<o:p></o:p></p>
<p class="Code" style="margin-left:72.0pt"> [G] p ~ (x `Union` Singleton B)<o:p></o:p></p>
<p class="Code" style="margin-left:72.0pt"> [G] q ~ (x `Union` Singleton A)<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt">If we think of Union as a type-level function (which it is?), then the step you outline above is similar to what happens during “flattening” of the Givens. We get this:<o:p></o:p></span></p>
<p class="Code">[G] fsk1 ~ p `Union` Singleton B (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk2 ~ q `Union` Singleton A (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk1 ~ fsk2 (CTyEqCan)<span style="font-size:12.0pt"><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:l1 level1 lfo2"><span style="font-size:12.0pt">The newly generated skolems are called “flatten-skolems” or fsks for short.<o:p></o:p></span></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2"><span style="font-size:12.0pt">The new skolems are kept in the `inert_fsks` field of the `InertSet`. <o:p></o:p></span></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2"><span style="font-size:12.0pt">A new one is created by `TcSMonad.newFlattenSkolem`<o:p></o:p></span></li><li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo2"><span style="font-size:12.0pt">All fsks are eliminated by TsSMonad.unflattenGivens<o:p></o:p></span></li></ul>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal">Returning to your point, you are exploiting a property of sets that allows you to say that if<o:p></o:p></p>
<p class="MsoNormal"> p U X = q U Y<o:p></o:p></p>
<p class="MsoNormal">Then suppose r = p <span style="font-family:Symbol">Ç</span> q
<o:p></o:p></p>
<p class="MsoNormal">then p = r U Y, q = r U X<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">And now we can eliminate all uses of p, q in favour of r. But if you do this in a type system, we have a problem: where is ‘r’ bound? E.g. if you have<o:p></o:p></p>
<p class="Code">f :: forall p q. (p `Union` A) ~ (q `Union` B) => blah<o:p></o:p></p>
<p class="MsoNormal">Then p, q are bound by the forall, but r is not. To put it another way, what well-typed Core program would you like to generate?<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">You could do this:<o:p></o:p></p>
<p class="Code">[G] fsk1 ~ p `Union` Singleton B (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk2 ~ q `Union` Singleton A (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk3 ~ p `Intersect` q (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk4 ~ fsk3 `Union` Singleton B (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk5 ~ fsk3 `Union` Singleton A (CFunEqCan)<o:p></o:p></p>
<p class="Code">[G] fsk1 ~ fsk2 (CTyEqCan)<o:p></o:p></p>
<p class="Code">[G] p ~ fks4 (CTyEqCan)<o:p></o:p></p>
<p class="Code">[G] q ~ fsk5 (CTyEqCan)<o:p></o:p></p>
<p class="MsoNormal"><span style="font-size:12.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal">The ‘r’ is just fsk3. It’ll be eliminated by unflattenGivens, so there is no problem with scoping.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">I have no idea whether that’ll help you prove the things you want to prove!<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"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></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" style="margin-left:36.0pt"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> ghc-devs <<a href="mailto:ghc-devs-bounces@haskell.org">ghc-devs-bounces@haskell.org</a>>
<b>On Behalf Of </b>Nicolas Frisby<br>
<b>Sent:</b> 24 June 2018 19:01<br>
<b>To:</b> <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<b>Subject:</b> Can a TC plugin create new skolem vars when simplifying Givens?<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><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:36.0pt">
I'm still spending the occasional weekend working on a type checker plugin for row types (actually "set" types at first, but I haven't thought of a less ambiguous term for that).<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:36.0pt">
<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:36.0pt">
One point of complexity in the plugin has to do with creating fresh variables when simplifying Givens. Some constraints are traditionally simplified by introducing a fresh variable. For Wanted constraints, that's easy (newFlexiTyVar). For Givens, though, I
haven't figured out how to do it.<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:36.0pt">
<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:36.0pt">
This email is just to ask these two questions:<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:36.0pt">
<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:36.0pt">
1) Is there a function to add a new skolem variable when simplifying Givens?<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:36.0pt">
<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:36.0pt">
2) Assuming not, is there a strong reason for there to never be such a function?<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:36.0pt">
<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:36.0pt">
Here's a small indicative example. In the "simplify Givens" step, the plugin receives<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:36.0pt">
<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:36.0pt">
[G] (p `Union` Singleton A) ~ (q `Union` Singleton B)<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:36.0pt">
<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:36.0pt">
and I would ideally simplify that to<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:36.0pt">
<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:36.0pt">
[G] p ~ (x `Union` Singleton B)<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:36.0pt">
[G] q ~ (x `Union` Singleton A)<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:36.0pt">
<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:36.0pt">
for some fresh skolem variable x. But I don't see how to properly create a fresh skolem variable in the Givens. If these were Wanteds, I would just use newFlexiTyVar.<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:36.0pt">
<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:36.0pt">
I think this is analogous to a hypothetical type checker plugin that eta expands tuples. If we were to simplify<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:36.0pt">
<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:36.0pt">
[G] ... (x :: (k1,k2)) ...<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:36.0pt">
<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:36.0pt">
to<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:36.0pt">
<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:36.0pt">
[G] ... '(x1 :: k1,x2 :: k2) ...<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:36.0pt">
<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:36.0pt">
we'd have to generate x1 and x2 somehow. The only method I'm aware of for that is to use Fst x and Snd x instead (ie type families). That might be acceptable for the tuple expansion example, but I'm very reticent to use something like that for the set types
plugin.<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:36.0pt">
<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:36.0pt">
I have a plan to get by without creating these variables when simplifying Givens, but it's not simple. I'd be delighted if it were possible to create them. Hence my two questions listed above.<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:36.0pt">
<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:36.0pt">
Thank you for your time. -Nick<o:p></o:p></p>
</div>
</div>
</div>
</div>
</body>
</html>