sample terms and interpreting program output from Tc Monad

Hi All:

I'm still working through the following paper [1] and I wondered whether
you could help me confirm my understanding of some sample terms and
program output from the Tc Monad. For those interested, the language is
specified in Parser.lhs available in the protoype here [2].

I understand these to be Rank 0 terms:

(\(x::Int) . x) (0 :: Int) :: (forall. Int) -- value

(\(x::Int). x) :: (forall. Int -> Int)

(\(x::a). x) :: (forall. a -> a)

Although the program prints forall, the absence of a type variable
indicates Rank 0, correct?

I understand these to be Rank 1 terms:

(\x. x) :: (forall a. a -> a) -- This is not the same as the third
example above, right? This one identifies the type variable a, the one
above does not. Also, there's no explicit annotation, it's inferred.

(\x. \y. x) :: (forall a b. b -> a -> b) -- Still rank 1.

Although there's no explicit annotation, the program infers the type
variables and prints the forall and the appropriate type variables for
the Rank 1 polytypes.