My installed GHC is looping when building your TcRnDriver, oddly. I'm going to wait for the HP release to (hopefully) get a GHC version that works properly so I can try out your code.
However, I did notice that (coqPassCoreToCore == id). This doesn't seem right - perhaps you haven't updated the branch with the pre-extracted Coq code recently? I am in a position to answer one of my own questions: > 1. What is the %%a syntax in the dotproduct' function? I would > understand what was going on if that was ~~ instead. This is the syntax for cross-stage persistence. In the example, c is of type Char in the environment, but we want to compare it to a variable bound within a <[ bracket ]>, so we must use %% to lift that thing bound at level 0 to something bound at level 1. I guess that equally this could be done implicitly (which I think is what TH does) at the cost of having variables at level n shadow variables at level m < n. Cheers, Max _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
