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

David Rush kumoyuki at gmail.com
Fri Mar 7 10:05:24 UTC 2014

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

    (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

    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
    In the expression:
      ((\ u (x :: forall a. a) y -> u x y) (\ x y -> y)) True

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

More information about the Haskell-Cafe mailing list