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