Hi,<br><br>Please use GHC 7.6 for experimenting with PolyKinds/DataKinds; the<br>implementation in 7.4 was not fully complete. Your code compiles fine in 7.6.<br><br><br>Cheers,<br>Pedro<br><br><div class="gmail_quote">On Fri, Oct 26, 2012 at 3:10 AM, Ahn, Ki Yung <span dir="ltr">&lt;<a href="mailto:kyagrd@gmail.com" target="_blank">kyagrd@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Promotion works for user defined lists such as<br>
<br>
data List a = Nil | Cons a (List a)<br>
<br>
And, if I use (List Bool) instead of [Bool] everything works out.<br>
It&#39;s only the Haskell list type constructor [] is being a problem.<br>
<br>
In the &quot;Giving Haskell a promotion&quot; paper, it says that Haskell lists are &quot;natively promoted&quot;. I believe this means that it is treated specially somehow. I don&#39;t know how it is implemented but what GHC 7.4.1 does specially for Haskell lists has some problems. So, it&#39;s clearly not a limitation of DataKind and PolyKind extension, but that special routine for [] is the issue.<br>


<br>
I might have to write bug report.<div><div class="h5"><br>
<br>
On 2012년 10월 25일 18:07, Ahn, Ki Yung wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Most part of Conor&#39;s talk at ICFP, until just before the last stage<br>
where he heavily uses true value dependency for compiler correctness all<br>
the code seemed to be able to translate into Haskell with the new hot<br>
DataKinds and PolyKinds extension.<br>
<br>
I tried it in GHC 7.4.1 and it was possible to do it, but I got stuck<br>
and I had to make the generic list structure mono-kinded with kind<br>
signatures rather not use the PolyKinds extension.<br>
<br>
I wonder if this is just a but of GHC 7.4.1&#39;s implementation of<br>
PolyKinds, or a limitation of the DataKind design.<br>
<br>
I attached a literate Haskell script with this message that illustrates<br>
this problem.<br>
<br>
Thanks in advance for any comments including whether it runs in later<br>
versions or still has problems, and discussions about the DataKinds and<br>
PolyKinds extension.<br>
<br>
Ki Yung<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote>
<br>
<br>
<br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>