[Haskell-cafe] SystemF, universal quantification, and rigid type variables

[David Rush]

In short, I'm trying to decide if there is a real difference between the 
types:

    (forall a.a) -> b
    a -> b

and frankly, I'm not seeing a difference. But ghc apparently does

*SystemF.Tests> :t ((\u (x::forall a. a) y -> u x y) (\x y -> y))  True

<interactive>:1:49:
    Couldn't match type `a' with `Bool'
      `a' is a rigid type variable bound by
          a type expected by the context: a at <interactive>:1:1
    In the second argument of `\ u (x :: forall a. a) y
                                 -> u x y', namely
      `True'
    In the expression:
      ((\ u (x :: forall a. a) y -> u x y) (\ x y -> y)) True
*SystemF.Tests> 

Since this is a 'rigid type variable' complaint, I am inclined to think that 
this is a limitation of ghc, rather than a particular issue with the logic of 
System F. I'd actually love to be wrong. Is there an actual difference 
between the types?

- david rush