<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;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        font-size:11.0pt;
        font-family:"Calibri",sans-serif;}
pre
        {mso-style-priority:99;
        mso-style-link:"HTML Preformatted Char";
        margin:0cm;
        font-size:10.0pt;
        font-family:"Courier New";}
tt
        {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;
        font-size:11.0pt;
        font-family:"Calibri",sans-serif;}
span.HTMLPreformattedChar
        {mso-style-name:"HTML Preformatted Char";
        mso-style-priority:99;
        mso-style-link:"HTML Preformatted";
        font-family:Consolas;}
span.EmailStyle23
        {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:261231920;
        mso-list-template-ids:592845658;}
@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:796949859;
        mso-list-type:hybrid;
        mso-list-template-ids:-1217788568 134807567 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l1:level1
        {mso-level-tab-stop:none;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@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:977413265;
        mso-list-template-ids:235836528;}
@list l3
        {mso-list-id:1580552384;
        mso-list-template-ids:378150114;}
@list l3:level1
        {mso-level-tab-stop:36.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level2
        {mso-level-tab-stop:72.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level3
        {mso-level-tab-stop:108.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level4
        {mso-level-tab-stop:144.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level5
        {mso-level-tab-stop:180.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level6
        {mso-level-tab-stop:216.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level7
        {mso-level-tab-stop:252.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level8
        {mso-level-tab-stop:288.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
@list l3:level9
        {mso-level-tab-stop:324.0pt;
        mso-level-number-position:left;
        text-indent:-18.0pt;}
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" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">What would you expect of<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<ol style="margin-top:0cm" start="1" type="1">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo3"><span style="font-family:"Courier New";mso-fareast-language:EN-US">\x -> case x of HNil -> blah<o:p></o:p></span></li></ol>
<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">Here the lambda and the case are separated.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New";mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<ol style="margin-top:0cm" start="2" type="1">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo3"><span style="font-family:"Courier New";mso-fareast-language:EN-US">\x -> (x, case x of HNil -> blah)<o:p></o:p></span></li></ol>
<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">Here the lambda and the case are separated more, and x is used twice.<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">What if there are more data constructors that share a common return type?<o:p></o:p></span></p>
<p class="MsoListParagraph"><span style="font-family:"Courier New";mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<ol style="margin-top:0cm" start="3" type="1">
<li class="MsoListParagraph" style="margin-left:0cm;mso-list:l1 level1 lfo3"><span style="font-family:"Courier New";mso-fareast-language:EN-US">data HL2 a where<o:p></o:p></span></li></ol>
<p class="MsoListParagraph" style="text-indent:36.0pt"><span style="font-family:"Courier New";mso-fareast-language:EN-US">HNil1 :: HL2 []<o:p></o:p></span></p>
<p class="MsoListParagraph" style="text-indent:36.0pt"><span style="font-family:"Courier New";mso-fareast-language:EN-US">HNil2 :: HL2 []<o:p></o:p></span></p>
<p class="MsoListParagraph" style="text-indent:36.0pt"><span style="font-family:"Courier New";mso-fareast-language:EN-US">HCons :: …blah…<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New";mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"Courier New";mso-fareast-language:EN-US">\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }<o:p></o:p></span></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-family:"Courier New";mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Here HNil1 and HNil2 both return HL2 [].   Is that “singular”?   What if one was a bit more general than the other?   Do we seek the least common generalisation of the alternatives given?<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">The water gets deep quickly here.  I don’t (yet) see an obviously-satisfying design point that isn’t massively ad-hoc.<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">Simon<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"> ghc-devs <ghc-devs-bounces@haskell.org>
<b>On Behalf Of </b>Alexis King<br>
<b>Sent:</b> 20 March 2021 09:41<br>
<b>To:</b> ghc-devs@haskell.org<br>
<b>Subject:</b> Type inference of singular matches on GADTs<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p>Hi all,<o:p></o:p></p>
<p>Today I was writing some code that uses a GADT to represent heterogeneous lists:<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>data HList as where<o:p></o:p></pre>
<pre>  HNil  :: HList '[]<o:p></o:p></pre>
<pre>  HCons :: a -> HList as -> HList (a ': as)<o:p></o:p></pre>
</blockquote>
<p>This type is used to provide a generic way to manipulate n-ary functions. Naturally, I have some functions that accept these n-ary functions as arguments, which have types like this:<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>foo :: Blah as => (HList as -> Widget) -> Whatsit<o:p></o:p></pre>
</blockquote>
<p>The idea is that <tt><span style="font-size:10.0pt">Blah</span></tt> does some type-level induction on
<tt><span style="font-size:10.0pt">as</span></tt> and supplies the function with some appropriate values. Correspondingly, my use sites look something like this:<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>bar = foo (\HNil -> ...)<o:p></o:p></pre>
</blockquote>
<p>Much to my dismay, I quickly discovered that GHC finds these expressions quite unfashionable, and it invariably insults them:<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>• Ambiguous type variable ‘as0’ arising from a use of ‘foo’<o:p></o:p></pre>
<pre>  prevents the constraint ‘(Blah as0)’ from being solved.<o:p></o:p></pre>
</blockquote>
<p>The miscommunication is simple enough. I expected that when given an expression like<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>\HNil -> ...<o:p></o:p></pre>
</blockquote>
<p>GHC would see a single pattern of type <tt><span style="font-size:10.0pt">HList '[]</span></tt> and consequently infer a type like<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>HList '[] -> ...<o:p></o:p></pre>
</blockquote>
<p>Alas, it was not to be. It seems GHC is reluctant to commit to the choice of <tt>
<span style="font-size:10.0pt">'[]</span></tt> for <tt><span style="font-size:10.0pt">as</span></tt>, lest perhaps I add another case to my function in the future. Indeed, if I were to do that, the choice of
<tt><span style="font-size:10.0pt">'[]</span></tt> would be premature, as <tt><span style="font-size:10.0pt">as ~ '[]</span></tt> would only be available within one branch. However, I do not in fact have any such intention, which makes me quietly wish GHC would
 get over its anxiety and learn to be a bit more of a risk-taker.<o:p></o:p></p>
<p>I ended up taking a look at the OutsideIn(X) paper, hoping to find some commentary on this situation, but in spite of the nice examples toward the start about the trickiness of GADTs, I found no discussion of this specific scenario: a function with exactly
 one branch and an utterly unambiguous pattern. Most examples come at the problem from precisely the opposite direction, trying to tease out a principle type from a collection of branches. The case of a function (or perhaps more accurately, a
<tt><span style="font-size:10.0pt">case</span></tt> expression) with only a single branch does not seem to be given any special attention.<o:p></o:p></p>
<p>Of course, fewer special cases is always nice. I have great sympathy for generality. Still, I can’t help but feel a little unsatisfied here. Theoretically, there is no reason GHC cannot treat<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>\(a `HCons` b `HCons` c `HCons` HNil) -> ...<o:p></o:p></pre>
</blockquote>
<p>and<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<pre>\a b c -> ...<o:p></o:p></pre>
</blockquote>
<p>almost identically, with a well-defined principle type and pleasant type inference properties, but there is no way for me to communicate this to the typechecker! So, my questions:<o:p></o:p></p>
<ol start="1" type="1">
<li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l3 level1 lfo6">
Have people considered this problem before? Is it discussed anywhere already?<o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l3 level1 lfo6">
Is my desire here reasonable, or is there some deep philosophical argument for why my program should be rejected?<o:p></o:p></li><li class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l3 level1 lfo6">
If it <i>is</i> reasonable, are there any obvious situations where a change targeted at what I’m describing (vague as that is) would affect programs negatively, not positively?<o:p></o:p></li></ol>
<p>I realize this gets rather at the heart of the typechecker, so I don’t intend to imply a change of this sort should be made frivolously. Indeed, I’m not even particularly attached to the idea that a change must be made! But I do want to understand the tradeoffs
 better, so any insight would be much appreciated.<o:p></o:p></p>
<p>Thanks,<br>
Alexis<o:p></o:p></p>
</div>
</div>
</body>
</html>