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-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe