impredicative polymorphism: seen on HCAR

[Isaac Dupree]

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