Oh, that's another thing that makes me really angry too: GHC's lack of distinction between first-class polymorphism (functions from types to values, à la System

Oh, that's another thing that makes me really angry too: GHC's lack of distinction between first-class polymorphism (functions from types to values, à la System F(ω)) and second-class polymorphism (values, not necessarily functions, that admit more than one type, à la Damas-Milner). But that's a topic for another day. EDIT: Also, I forgot, I haven't actually seen Haskellers use ImpredicativeTypes much. Are you really sure that the predicative subset of System F (just RankN types) has no set models?