In the presence of polymorphism and mutable cells, value restriction (or a restriction thereof) is necessary to establish type soundness (ie that typed programs are safe), so I'd argue that it achieves this goal.

As for this explanation, I'm not entirely convinced. In the first example, seeing x as two different cells depending on the type is interesting, but I have trouble seeing how it is possible to express its semantics without keeping runtime type information. Is System F compatible with type erasure?