<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=iso-8859-1">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
        {font-family:Tahoma;
        panose-1:2 11 6 4 3 5 4 4 2 4;}
@font-face
        {font-family:Verdana;
        panose-1:2 11 6 4 3 5 4 4 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","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;}
span.EmailStyle17
        {mso-style-type:personal-reply;
        font-family:"Verdana","sans-serif";
        color:#1F497D;}
.MsoChpDefault
        {mso-style-type:export-only;
        font-family:"Calibri","sans-serif";
        mso-fareast-language:EN-US;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
        {page:WordSection1;}
--></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:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">I think the issue is this.&nbsp; We have<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Strip :: forall k. * -&gt; k<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">When you say &nbsp;<o:p></o:p></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-family:&quot;Courier New&quot;">type instance Strip (Maybe a) = Maybe<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">GHC infers the kind arguments (as with all hidden argument) to get<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><span style="font-family:&quot;Courier New&quot;">type instance Strip (*-&gt;*) (Maybe a) = Maybe</span><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">It would be fine to have another type instance like this<o:p></o:p></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-family:&quot;Courier New&quot;">type instance Strip (Maybe a) = Int<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">which would turn into<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><span style="font-family:&quot;Courier New&quot;">type instance Strip * (Maybe a) = Maybe</span><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:&quot;Courier New&quot;"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">In all cases, an occurrence of (Strip &lt;kind&gt; &lt;type&gt;) will match one of the &#8220;type instances&#8221; only if, well, it matches, including the kind.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">Does that answer the question.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">I would love someone to write some user guidance notes about this kind of thing, perhaps as a new sub-page of<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><a href="http://www.haskell.org/haskellwiki/GHC/Type_system">http://www.haskell.org/haskellwiki/GHC/Type_system</a><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D">Simon<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:&quot;Verdana&quot;,&quot;sans-serif&quot;;color:#1F497D"><o:p>&nbsp;</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 #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US" style="font-size:10.0pt;font-family:&quot;Tahoma&quot;,&quot;sans-serif&quot;">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:&quot;Tahoma&quot;,&quot;sans-serif&quot;"> glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org]
<b>On Behalf Of </b>José Pedro Magalhães<br>
<b>Sent:</b> 30 October 2012 10:29<br>
<b>To:</b> GHC users<br>
<b>Subject:</b> Kind refinement in type families with PolyKinds<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p>&nbsp;</o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt">Hi all,<br>
<br>
I'm wondering why the following does not work:<o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:&quot;Courier New&quot;">{-# LANGUAGE DataKinds&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; #-}<br>
{-# LANGUAGE PolyKinds&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; #-}<br>
{-# LANGUAGE KindSignatures&nbsp;&nbsp;&nbsp;&nbsp; #-}<br>
{-# LANGUAGE TypeFamilies&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; #-}<br>
{-# LANGUAGE GADTs&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; #-}<br>
{-# LANGUAGE TypeOperators&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; #-}<br>
<br>
module Bug where<br>
<br>
-- Type equality<br>
data a :=: b where Refl :: a :=: a<br>
<br>
-- Applying a type to a list of arguments<br>
type family Apply (t :: k) (ts :: [*]) :: *<br>
type instance Apply t&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; '[]&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; = t<br>
type instance Apply (f :: * -&gt; *) (t ': ts) = f t<br>
<br>
-- Stripping a type from all its arguments<br>
type family Strip (t :: *) :: k<br>
type instance Strip (Maybe a) = Maybe<br>
<br>
-- Reapplying a stripped type is the identity<br>
x :: Apply (Strip (Maybe a)) (a ': '[]) :=: Maybe a<br>
x = Refl</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
If I ask GHCi for the kind of `Strip (Maybe Int)`, I get `k`, whereas I would expect `* -&gt; *`.<br>
That explains why the `Apply` type family is not reduced further.<br>
<br>
I understand that this might be related to GADTs not being allowed to refine kinds;<br>
the following datatype fails to compile with the error &quot;`D1' cannot be GADT-like<br>
in its *kind* arguments&quot;:<o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:&quot;Courier New&quot;">data DStrip :: k -&gt; * where<br>
&nbsp; D1 :: DStrip Maybe</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
But then, shouldn't the type instance for `Strip` above trigger the same error?<br>
<br>
<br>
Thanks,<br>
Pedro<o:p></o:p></p>
</div>
</div>
</body>
</html>