Are there any advantages of using Rank2Types in favor of RankNTypes?

Question

As far as I know, a decidable type checking algorithm exists (only) for rank-2 types. Does GHC use somehow this fact, and does it have any practical implications?

Is there also a notion of principal types for rank-2 types, and a type inference algorithm? If yes, does GHC use it?

Are there any other advantages of rank-2 types over rank-n types?

Answer 1

In principle type checking is decidable for rank 2 types. But, that was never going to be included in GHC (overly complicated, doesn't mix well with other features of the type system). So no. Rank2Types is deprecated (okay, it doesn't give you a warning, but it is) so use RankNTypes.

Answer 2

Rank2Types is a synonym for RankNTypes. So right now there are no advantages of rank-2 over rank-n.