# Why is the polymorphic weight 1

I am reading through through a paper called HMF: Simple Type Inference for First-Class Polymorphism by Daan Leijen of Microsoft Research.

In the paper it describes how to calculate the polymorphic weight of an expression:

I am having trouble understanding why the above example [[forall a. [forall b. a -> b]]] has a weight of 1 rather than two. there are two type abstractions where both type variable are not free in their bodies, should these not be added together?

[[forall a. [forall b. a -> b]]] has a weight of 1
It doesn't. It has a polymorphic weight of 1. The polymorphic weight strips the binder before it looks at the weight. For the $\rho$ you chose:
$[\![\forall \overline{\alpha} . \rho]\!] = wt(\rho) = 1 \neq 2 = wt(\forall \overline{\alpha} . \rho)$