[Haskell-cafe] Problems translating Conor McBride's talk into Haskell + DataKind + KindPoly

[Ahn, Ki Yung]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe