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. I understand these to be Rank 2 terms: (\(x::(forall a. a)). 0) :: (forall. (forall a. a) -> Int) The explicit forall annotation on the bound and binding variable x causes the program to infer a Rank 2 polytype as indicated by the "-> Int" following the (forall a. a), while noting the absence of a type variable following the left-most forall printed by the program, correct? (\(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> b) Also Rank 2, only one arrow to the right of (forall a. a -> a) counts. The universal quantifier on type variable b ranges over the type variable a, correct? I understand this to be a Rank 3 term: (\(f::(forall a. a -> a)). \(x::(forall b. b)). f (f x)) :: (forall c. (forall a. a -> a) -> (forall b. b) -> c) The arrows to the right of the universally quantified a and b expressions qualify this as Rank 3. Type variable c ranges over type variables a and b, correct? Thanks for your help in better understanding this information. I'm home schooling myself on Haskell and community support is a big help. 1. Practical Type Inference for Arbitrary-Rank Types. 2.http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/ -- Rick