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 -&gt; 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?
You asked why


  [[forall a. [forall b. a -&gt; 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)$