rank 2-polymorphism and type checking

[Koen Claessen]

Simon Peyton-Jones wrote:

 | So I'm interested to know: if GHC allowed
 | arbitrarily-ranked types, who would use them?

I have certainly come across (very practical) situations
where I would like to use rank-n types (with n > 2). One
example is the following.

When using "runST", I often end up with code that looks
like:

  foo =
    runST
    ( do ...
         ...
         ...
    )

Because I think it is a bad idea to use parentheses like
this, I would like to use "$":

  foo =
    runST $
      do ...
         ...
         ...

Alas, the compiler complains, because it wants runST to have
more arguments. So, one could define a special dollar
operator:

  infixr 0 $+

  ($+) :: ((forall s . m s a) -> a) -> (forall s . m s a) -> a
  run $+ m = run m

However, this has a rank-3 type.

I have made the following observation. Richard Bird once
wrote an article where he argues that allowing nested
datatypes is useless unless one allows polymorphic
recursion. I think the same is true for allowing functions
with rank-2 polymorphism. If higher rank polymorphism is not
allowed, then rank-2 polymorphic functions are just not
first-class enough for all kinds of generalizations.

/Koen