Hi, Please use GHC 7.6 for experimenting with PolyKinds/DataKinds; the implementation in 7.4 was not fully complete. Your code compiles fine in 7.6. Cheers, Pedro On Fri, Oct 26, 2012 at 3:10 AM, Ahn, Ki Yung wrote:

Promotion works for user defined lists such as

data List a = Nil | Cons a (List a)

And, if I use (List Bool) instead of [Bool] everything works out. It's only the Haskell list type constructor [] is being a problem.

In the "Giving Haskell a promotion" paper, it says that Haskell lists are "natively promoted". I believe this means that it is treated specially somehow. I don't know how it is implemented but what GHC 7.4.1 does specially for Haskell lists has some problems. So, it's clearly not a limitation of DataKind and PolyKind extension, but that special routine for [] is the issue.

I might have to write bug report.

On 2012년 10월 25일 18:07, Ahn, Ki Yung wrote:

...

Most part of Conor's talk at ICFP, until just before the last stage where he heavily uses true value dependency for compiler correctness all the code seemed to be able to translate into Haskell with the new hot DataKinds and PolyKinds extension.

I tried it in GHC 7.4.1 and it was possible to do it, but I got stuck and I had to make the generic list structure mono-kinded with kind signatures rather not use the PolyKinds extension.

I wonder if this is just a but of GHC 7.4.1's implementation of PolyKinds, or a limitation of the DataKind design.

I attached a literate Haskell script with this message that illustrates this problem.

Thanks in advance for any comments including whether it runs in later versions or still has problems, and discussions about the DataKinds and PolyKinds extension.

Ki Yung

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe

______________________________**_________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe