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