RankN Types
Brief Explanation
In Haskell 98, all free variables in a type are implicitly universally quantified, e.g.
const :: a > b > a
Thus Haskell 98 permits only rank1 types.
The proposal is to allow explicit universal quantification within types using a forall
keyword, so types can have the forms

type
>
type 
forall
vars. [context=>
] type  monotype
where monotype is a Haskell 98 type.
Note that forall
's are not allowed inside type constructors other than >
.
forall
s and contexts in the second argument of >
may be floated out, e.g. the following types are equivalent:
succ :: (forall a. a > a) > (forall b. b > b)
succ :: forall b. (forall a. a > a) > b > b
It is not possible to infer higherrank types in general; type annotations must be supplied by the programmer in many cases.
References
 Arbitraryrank polymorphism in the GHC User's Guide.
 Practical type inference for arbitraryrank types, Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields, July 2005. To appear in Journal of Functional Programming.
 Boxy types: type inference for higherrank types and impredicativity, Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, ICFP 2006.
 Semantics of Types and Classes in the Haskell 98 Report
 PolymorphicComponents would also be allowed higherrank types
 Rank2Types are a special case
Tickets
#60  add RankNTypes or Rank2Types 

Details
HindleyMilner type systems (e.g. in Haskell 98) may be specified by rules deriving the type of an expression from those of its constituents, providing a simple way to reason about the types of expressions. The rules may also be used as a bottomup procedure for inferring principal types, with inferred types matched against any signatures supplied, but many other traversals yield the same answer. A mixture of bottomup inference and topdown checking often produces more informative error messages.
Bidirectional type inference
For arbitraryrank types, a particular bidirectional traversal is specified by the type rules (see Fig. 8 on p25 of the arbitraryrank paper), to make use of programmersupplied annotations. In particular,
 functions and expressions with type signatures are checked topdown.
 parameter variables without explicit signatures are assigned monotypes in upwards inference, but may inherit arbitraryrank types in downwards checking.
 in an application (whether inferred or checked), the type of the function is inferred bottomup, and the argument checked topdown against the inferred argument type.
The generalization preorder must be recursively defined, with contravariance for >
types (see Fig. 7 on p22 of
the arbitraryrank paper).
The system has the following properties:
 Programs containing no
forall
s are typeable if and only if they are typeable in Haskell 98.  Inference produces principal types, though checking may accept more types.
 Both checking and inference are monotonic with respect to the generalization preorder.
However it does not permit
runST $ do { ... }
as that requires impredicative types.
Boxy types
Boxy types generalize bidirectional inference, and also allow impredicative types (type variables may be instantiated to polytypes, and polytypes may occurs as arguments of type constructors).
Pros
 More convenient than encodings using PolymorphicComponents
Cons
 More complex than Rank2Types, which cover the most common cases (and can encode the rest, though clumsily).
 No clear programmerlevel description of the restrictions that apply. To quote the boxytypes paper:
The type system is arguably too complicated for Joe Programmer to understand, but that is true of many type systems, and perhaps it does not matter too much: in practice, Joe Programmer usually works by running the compiler repeatedly, treating the compiler as the specification of the type system. Indeed, a good deal of the complexity of the type system (especially Section 6) is there to accommodate programs that "ought" to work, according to our understanding of Joe's intuitions.