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

[Ahn, Ki Yung]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: tmp.lhs
Type: text/x-literate-haskell
Size: 2320 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121025/9532469f/attachment.lhs>