[Haskell] Type inference for arbitrary rank types

[Edsko de Vries]

Hi,

I am currently studying the paper "Practical Type Inference for
Arbitrary Rank Types" by Simon Peyton Jones and Mark Shields, and I've
been wondering about the final version of the typing rules (figure 7,
"Bidirectional version of Odersky-Laufer") (although I suppose the
question is slightly more general than this figure).

In this figure, there are rules for annotated abstractions (AABS1 and
AABS2) and annotated terms (ANNOT). What I'm wondering about: are the
rules AABS1 and AABS2 really necessary? As in, if you would remove those
two rules, does there exist a program that can be typed with the
original set of rules than cannot be typed with the set of rules with
AABS1/2 removed? It seems to me that any program that can be typed using
AABS1/2, can also be typed with ANNOT.

More importantly, in the absence of lexically scoped type variables, a
type such as 

  forall a. (forall b. (a, b) -> (b, a)) -> [a] -> [a]    (*)

(the example given on page 11, section 4.1 in the paper) cannot even be
typed using AABS1/2, but must be typed with ANNOT.

Perhaps I am missing something here though, because in Odersky and
Laufer's original paper, they do not do "local type inference" (they
don't specify a bidirectional version), which would make type (*)
impossible to specify in their original system?

Thanks,

Edsko