<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:"Verdana","sans-serif";color:#1F497D">I think the issue is this. We have<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"> Strip :: forall k. * -> k<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">When you say <o:p></o:p></span></p>
<p class="MsoNormal" style="text-indent:36.0pt"><span style="font-family:"Courier New"">type instance Strip (Maybe a) = Maybe<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";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:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">
</span><span style="font-family:"Courier New"">type instance Strip (*->*) (Maybe a) = Maybe</span><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";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:"Courier New"">type instance Strip (Maybe a) = Int<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">which would turn into<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">
</span><span style="font-family:"Courier New"">type instance Strip * (Maybe a) = Maybe</span><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">In all cases, an occurrence of (Strip <kind> <type>) will match one of the “type instances” 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:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">Does that answer the question.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";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:"Verdana","sans-serif";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:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D">Simon<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Verdana","sans-serif";color:#1F497D"><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 #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif"">From:</span></b><span lang="EN-US" style="font-size:10.0pt;font-family:"Tahoma","sans-serif""> 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> </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:"Courier New"">{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE PolyKinds #-}<br>
{-# LANGUAGE KindSignatures #-}<br>
{-# LANGUAGE TypeFamilies #-}<br>
{-# LANGUAGE GADTs #-}<br>
{-# LANGUAGE TypeOperators #-}<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 '[] = t<br>
type instance Apply (f :: * -> *) (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 `* -> *`.<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 "`D1' cannot be GADT-like<br>
in its *kind* arguments":<o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">data DStrip :: k -> * where<br>
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>