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 <[email protected]> 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 >> [email protected] >> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe> >> > > > > ______________________________**_________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe> >
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
