[Haskell-cafe] Aren't type system extensions fun?

[Andrew Coppin]

Haskell 98 provides a simple and clean type system, which I feel I 
understand very well.

GHC provides a vast zoo of strange and perplexing type system 
extensions, which I don't understand at all. (Well, some of it is simple 
enough - e.g., multiparameter type classes. But GADTs? FDs? ATs? Hmm...)

Anyway, it seems there is a large set of such type system extensions 
that involve writing "forall" all over the place. I have by now more or 
less managed to comprehend the fact that

  data Thing = forall x. Thing x

allows a type variable to appear on the RHS that is *not* present on the 
LHS, thus "hiding" the type of something inside the structure. And for 
some reason, they call this "existential quantification" [which I can't 
spell never mind pronounce].

Today I was reading a potentially interesting paper, and I stumbled 
across something referred to as a "rank-2 type". Specifically,

  class Typable x => Term x where
    gmapT :: (forall y. Term y => y -> y) -> x -> x

At this point, I am at a complete loss as to how this is any different from

  gmapT :: Term y => (y -> y) -> x -> x

Can anybody enlighten me?

This is probably the first real use I've ever seen of so-called rank-2 
types, and I'm curios to know why people think they need to exist. 
[Obviously when somebody vastly more intelligent than me says something 
is necessary, they probably know something I don't...]

At this point, I don't think I even wanna *know* what the hell a rank-N 
type is... o_O