Higher-rank polymorphism is a special case of impredicative polymorphism, where the type constructor is (->)
instead of any arbitrary constructor like []
.
The basic problems with impredicativity are that it makes type checking hard and type inference impossible in the general case—and indeed we can’t infer types of a higher rank than 2: you have to provide a type annotation. This is the ostensible reason for the existence of the Rank2Types
extension separate from RankNTypes
, although in GHC they’re synonymous.
However, for the restricted case of (->)
, there are simplified algorithms for checking these types and doing the necessary amount of inference along the way for the programmer’s convenience, such as Complete and Easy Bidirectional Type Checking for Higher-rank Polymorphism—compare that to the complexity of Boxy Types: Inference for Higher-rank Types and Impredicativity.
The actual reasons in GHC are partly historical: there had been an ImpredicativeTypes
extension, which was deprecated because it never worked properly or ergonomically. Part of the problem was that we didn’t yet have the TypeApplications
extension, so there was no convenient way to explicitly supply a polymorphic type as a type argument, and the compiler attempted to do more inference than it ought to. In GHC 9.2, ImpredicativeTypes
has come out of retirement, thanks to GHC proposal 274 and an algorithm, Quick Look, that infers a predictable subset of impredicative types.
In the absence of ImpredicativeTypes
, there have been alternatives for a while: with RankNTypes
, you can “hide” other forms of impredicativity by wrapping the polymorphic type in a newtype
and explicitly packing & unpacking it to tell the compiler exactly where you want to generalise and instantiate type variables.
newtype Id = Id { unId :: forall a. a -> a }
f :: [Id]
f = [Id id] -- generalise
(unId (head f) (), unId (head f) 'x') -- instantiate to () and Char
[]
. The function only requiresRankNTypes
to be enabled. (Strictly speaking,Rank2Types
would suffice, were it not superseded byRankNTypes
.) It's[]
which is special, not(->)
. – Noblewoman(->)
that's special:Maybe (forall a . a)
is a subtype offorall a . Maybe a
in that every value of the first type is admissible when the second is expected but not vice-versa; ie impredicative polymorphism is disallowed forMaybe
and[]
for exactly the same reason. – Bonbon