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