The May 2008 Haskell Communities and Activities Report, GHC http://www.haskell.org/communities/05-2008/html/report.html#ghc:
Impredicative polymorphism. We are not happy with GHC’s current implementation of impredicative polymorphism, which is rather complicated and ad hoc. Dimitrios (with Simon and Stephanie) wrote a paper about a new and better approach: http://research.microsoft.com/~simonpj/papers/boxy . At the same time, Daan Leijen has been working on his closely-related design: http://research.microsoft.com/users/daan/pubs.html . Daan’s design has a much simpler implementation, in exchange for an (arguably) less-predictable specification. Which of these two should we implement? Let us know!
I read the papers... Dimitrios's *paper* is easier for me to understand than Daan's. In fact they seem quite similar. I have no idea of any examples where they would behave differently. I don't use impredicative polymorphism much (but maybe because of my perception that the existing implementations are poorly designed, and that it can usually be avoided by an amount of abstraction that's useful anyway). So I'd say, implement the easier solution. Is there a paper or documentation somewhere, presenting a practical argument for why impredicative polymorphism is important in real programs (beyond runST $) -- for example, a real program that uses it and has clearer code because of it? I don't really mind writing let/function type-signatures that have weird types (unless they're long and repeat information that doesn't need to be, which is a different problem). I wonder how often these proposals require type-signatures on lambdas passed to higher-order functions, though... A side-effect is for those of us who want to have any concern for future compatibility with non-GHC type systems (or the long future of GHC's, even), whether one of the proposals would be likely to be easier for someone else to implement in a different compiler. -Isaac