<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:dt="uuid:C2F41010-65B3-11d1-A29F-00AA00C14882" 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:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
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;}
p.Code, li.Code, div.Code
{mso-style-name:Code;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:22.7pt;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";
font-weight:bold;}
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.apple-converted-space
{mso-style-name:apple-converted-space;}
span.EmailStyle21
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.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:370422484;
mso-list-template-ids:1448373720;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1
{mso-list-id:672146990;
mso-list-type:hybrid;
mso-list-template-ids:-211882814 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;}
@list l2
{mso-list-id:1434936850;
mso-list-template-ids:316544624;}
@list l3
{mso-list-id:1483617849;
mso-list-template-ids:-998864828;}
@list l3:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l3:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
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" style="margin-left:36.0pt">. I went looking in the GHC source, only to discover that you, Simon, <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fblob%2F986643cb3506f2eedce96bf2d2c03873f105fad5%2Fcompiler%2Ftypecheck%2FTcInteract.hs%23L276-277&data=02%7C01%7Csimonpj%40microsoft.com%7C497b4eadac5048bba19f08d717023589%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637003170572848664&sdata=3FxV6%2FaJ8zhkcyRMbZwFoqBOzFmvHwLYY%2FsYUX7hh08%3D&reserved=0">are
apparently deeply suspicious</a> of typechecker plugins that solve derived constraints!<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">What a good thing I left _<i>some</i>_ breadcrumbs to follow!<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">I think my suspicion were about two separate matters<o:p></o:p></p>
<ul type="disc">
<li class="MsoListParagraph" style="mso-list:l1 level1 lfo4">We should not need to delete solved _<i>givens</i>_ from the inert set. We can augment givens with extra facts, but deleting them seems wrong.
<o:p></o:p></li><li class="MsoListParagraph" style="mso-list:l1 level1 lfo4">There should be no Derived constraints in the inert set anyway. They should all be in the WantedConstraints passed to runTcPluginsWanted. They were extracted from the inert set, along with the
Deriveds, by getUnsolvedInerts in solve_simple_wanteds<o:p></o:p></li></ul>
<p class="MsoNormal">I can’t account for what’s happening to your Deriveds, but if you do some more detective work, I’m happy to play consultant.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">Though, for what it’s worth, I think it would be even more helpful if some of the relevant information made its way into the GHC user’s guide, since I found that more discoverable than the wiki page (which took
a comparatively large amount of digging to locate).<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">By definition you are better placed that any of us to know where to put this info -- after all, you know where you looked! It would be a great service to everyone if you wrote a new chapter for
the user guide, drawing on material that already exists -- and then signposted that new chapter from the existing wiki page.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Adding signposts to the wiki page too would be helpful, since it was hard to find.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thanks!<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Simion<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><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"> Alexis King <lexi.lambda@gmail.com>
<br>
<b>Sent:</b> 02 August 2019 05:31<br>
<b>To:</b> Simon Peyton Jones <simonpj@microsoft.com><br>
<b>Cc:</b> ghc-devs@haskell.org<br>
<b>Subject:</b> Re: Properly writing typechecker plugins<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">My thanks to you, Simon, for your prompt response. After reading your message, I realized I perhaps read too far into this sentence on the wiki page:<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal">Defining type families in plugins is more work than it needs to be, because the current interface forces the plugin to search the unsolved constraints for the type family in question (which might be anywhere within the types), <b>then emit
a new given constraint to reduce the type family</b>.<o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Emphasis mine. Although that sentence seems to imply that adding given constraints from a typechecker plugin is both possible and sanctioned, your message, my experimentation, and the GHC source code all seem to agree that is not true,
after all. After realizing that was a dead end, I puzzled for some time on how one is intended to solve nested type families after all, only to realize that a proper solution is simpler than I had realized.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">To make things more concrete, I was confused about how my plugin might solve a constraint like<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-left:30.0pt;margin-right:0cm">
<div>
<p class="MsoNormal">[W] {co_0} :: F (ToLower "Foo") ~# Length "bar"<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">if it knows about ToLower and Length but nothing about F. The solution is actually extremely straightforward to implement, but the idea was not at all obvious to me at first. Namely, it’s possible to just recursively walk the whole type
and solve any known families bottom-up, producing a new constraint:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-left:30.0pt;margin-right:0cm">
<div>
<p class="MsoNormal">[W] {co_1} :: F "foo" ~# 3<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">At the same time, to construct evidence for the first constraint, the recursive function can also build a coercion as it goes, producing<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-left:30.0pt;margin-right:0cm">
<div>
<p class="MsoNormal">co_2 = (F (Univ :: "foo" ~ ToLower "Foo")) ~# (Univ :: 3 ~ Length "bar")<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">which can be used to cast the evidence for the new constraint to evidence for the old one:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-left:30.0pt;margin-right:0cm">
<div>
<p class="MsoNormal">co_0 := co_2 ; {co_1}<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">That all seems to be working well, and it’s much nicer than whatever it was I was trying before. There’s one small wrinkle I’ve bumped into, however, which was preventing the solver from terminating. Specifically, typechecker plugins do
not seem to be able to solve derived constraints.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">To elaborate, my plugin was getting called with the constraint [D] (Length "f" ~ 1), which it was happily turning into [D] (1 ~ 1), but the derived constraint was never removed from the inert set, and it would produce new [D] (1 ~ 1) constraints
forever. I went looking in the GHC source, only to discover that you, Simon, <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fblob%2F986643cb3506f2eedce96bf2d2c03873f105fad5%2Fcompiler%2Ftypecheck%2FTcInteract.hs%23L276-277&data=02%7C01%7Csimonpj%40microsoft.com%7C497b4eadac5048bba19f08d717023589%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637003170572848664&sdata=3FxV6%2FaJ8zhkcyRMbZwFoqBOzFmvHwLYY%2FsYUX7hh08%3D&reserved=0">are
apparently deeply suspicious</a> of typechecker plugins that solve derived constraints! I don’t know if there’s a reason behind that—maybe I’m going about things the wrong way, and I shouldn’t need to solve those derived constraints—but in the meantime, I
added some kludgey mutable state to keep track of the derived constraints my plugin has already attempted to solve so it won’t try to solve them again.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Anyway, that aside, if anyone finds what I’ve written in this email helpful, I can certainly flesh it out a bit more and stick it in a wiki page somewhere. Though, for what it’s worth, I think it would be even more helpful if some of the
relevant information made its way into the GHC user’s guide, since I found that more discoverable than the wiki page (which took a comparatively large amount of digging to locate).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Thanks again,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Alexis<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">On Aug 1, 2019, at 03:01, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">Alexis<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Thanks for writing this up so carefully. I hope that others will join in. And please then put the distilled thought onto the wiki page(s) so they are not lost.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Some quick thoughts from me:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-top:0cm;margin-bottom:0cm;margin-bottom:.0001pt;mso-list:l0 level1 lfo1">
<b>Flattening</b>. I’m pretty sure we pass constraints unflattened because that’s what someone wanted at the time. It could easily be changed, but it might complicate the API. E.g. you might reasonably want to know the mapping from type variable to function
application. There is no fundameental obstacle.<o:p></o:p></li></ul>
<div style="margin-left:36.0pt">
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="margin-top:0cm;margin-bottom:0cm;margin-bottom:.0001pt;mso-list:l3 level1 lfo2">
<b>Letting the plugin add given constraints</b>. This looks a bit like: let the plugin prove lemmas and hand them back to GHC (along with their proof) to exploit. Yes, that seems reasonable too. Again, something new in the API.<o:p></o:p></li></ul>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">I don’t understand enough of your type-class instance question to comment meaningfully, but perhaps others will.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Nothing about the plugin interface is cast in stone. There are quite a few “customers” but few enough that they’ll probably be happy to adapt to changes. Go for it, in consultation with them!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Simon<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<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">
<div>
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span class="apple-converted-space"><span lang="EN-US"> </span></span><span lang="EN-US">ghc-devs <<a href="mailto:ghc-devs-bounces@haskell.org">ghc-devs-bounces@haskell.org</a>><span class="apple-converted-space"> </span><b>On
Behalf Of<span class="apple-converted-space"> </span></b>Alexis King<br>
<b>Sent:</b><span class="apple-converted-space"> </span>01 August 2019 07:55<br>
<b>To:</b><span class="apple-converted-space"> </span><a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<b>Subject:</b><span class="apple-converted-space"> </span>Properly writing typechecker plugins</span><o:p></o:p></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal">Hi all,<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal">I have recently decided to try writing a GHC typechecker plugin so I can get my hands on some extra operations on type-level strings. My plugin works, but only sort of—I know some things about it are plain wrong, and I have a sneaking suspicion
that plenty of other things are not handled properly.<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">First, some context about what I do and don’t already know: I have a high-level understanding of the basic concepts behind GHC’s solver. I understand what evidence is and what purpose it serves, I mostly understand the different flavors
of constraints, and I think I have a decent grasp on some of the operational details of how individual passes work. I’ve spent a little time reading through comments in the GHC source code, along with pieces of the source code itself, but I’m sure my understanding
is pretty patchy.<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">With that out of the way, here are my questions:<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<ol style="margin-top:0cm" start="1" type="1">
<li class="MsoNormal" style="margin-bottom:12.0pt;mso-list:l2 level1 lfo3">First, I’m trying to understand: why are wanted constraints passed to typechecker plugins unflattened? This is my single biggest point of confusion. It certainly seems like the opposite
of what I want. Consider that I have a type family<br>
<br>
type family ToUpper (s :: Symbol) :: Symbol where {}<br>
<br>
that I wish to solve in my plugin. At first, I just naïvely looked through the bag of wanted constraints and looked for constraints of the shape<br>
<br>
t ~ ToUpper s<br>
<br>
but this isn’t good enough, since my plugin regularly receives constraints that look more like<br>
<br>
t ~ SomeOtherTypeFamily (ToUpper s)<br>
<br>
so I have to recursively grovel through every type equality constraint looking for an application of a family I care about. Furthermore, once I’ve found one, I’m not sure how to actually let GHC know that I’ve solved it—do I really have to just generate a new
given constraint and let GHC’s solver connect the dots?<br>
<br>
I have seen <a href="https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fwikis%2Fplugins%2Ftype-checker%23under-discussion-defining-type-families&data=02%7C01%7Csimonpj%40microsoft.com%7C497b4eadac5048bba19f08d717023589%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637003170572858662&sdata=Ap5D%2BqsSiCU4v3YBFy%2BXiwYXqIQEj9oB7GQSypgZRXk%3D&reserved=0"><span style="color:purple">the
note on the typechecker plugins wiki page</span></a> about possibly baking support for type families into the plugin interface, which would indeed be nicer than the status quo, but it seems odd to me that they aren’t just passed to plugins flattened, which
seems like it would spare a lot of effort. Isn’t the flattened representation really what typechecker plugins would like to see, anyway?<o:p></o:p></li><li class="MsoNormal" style="margin-bottom:12.0pt;mso-list:l2 level1 lfo3">But let’s put families aside for a moment. I’m not just solving type families in my plugin, I’m also solving classes. These classes have no methods, but they do have functional dependencies.
For example, I have a class<br>
<br>
class Append (a :: Symbol) (b :: Symbol) (c :: Symbol) | a b -> c, a c -> b, b c -> a<br>
<br>
which is like GHC.TypeLits.AppendSymbol, but the fundeps make GHC a bit happier when running it “backwards” (since GHC doesn’t really know about AppendSymbol’s magical injectivity, so it sometimes complains).<br>
<br>
In any case, I was hoping that GHC’s solver would handle the improvement afforded by the fundeps for me once I provided evidence for Append constraints, but that doesn’t seem to be the case. Currently, I am therefore manually generating derived constraints
based on the functional dependency information, plumbing FunDepOrigin2 through and all. Is there some way to cooperate better with GHC’s solver so I don’t have to duplicate all that logic in my plugin?<br>
<br>
I guess one thing I didn’t try is returning given constraints from my solver instead of just solving them and providing evidence. That is, if my plugin received a<br>
<br>
[W] d1 :: Append "foo" "bar" c<br>
<br>
constraint, then instead of solving the constraint directly, I could leave it alone and instead return a new constraint<br>
<br>
[G] d2 :: Append "foo" "bar" "baz"<br>
<br>
and presumably GHC’s solver would use that constraint to improve and solve d1. But similar to my confusion about type families above, I’m uncertain if that’s the intended method or not, since it seems like it’s sort of circumventing the plugin API.<o:p></o:p></li><li class="MsoNormal" style="mso-list:l2 level1 lfo3">Finally, on a related note, building evidence for these solver-generated typeclass instances is a bit of a pain. They have no methods, but they do sometimes have superclasses. Currently, I’ve been generating
CoreExprs as carefully as I’m able to after reading through the desugaring code: I call dataConWrapId on the result of classDataCon, then use mkTyConApp and mkCoreApps on that directly. It seems to work okay now, but it didn’t always: -dcore-lint thankfully
caught my mistakes, but I’ve been wondering if there’s a safer way to build the dictionary that I’ve been missing.<o:p></o:p></li></ol>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
</div>
<div>
<div>
<p class="MsoNormal">That’s it for now—I’ve just been muddling through until things work. Once I get something that feels closer to right, maybe I’ll put the code somewhere and ask for more low-level comments if anyone would like to take the time to offer them,
but for now, I’m still working on the high-level ideas. The wiki pages I’ve found have been very helpful; my appreciation to all who have contributed to them!<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Many thanks,<o:p></o:p></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal">Alexis<o:p></o:p></p>
</div>
</div>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
</body>
</html>