What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value?

Question

Types and Programming Languages by Pierce says:

22.7 Let polymorphism

A final point worth mentioning is that, in designing full-blown programming languages with let-polymorphism, we need to be a bit careful of the interaction of polymorphism and side-effecting features such as mutable storage cells. A simple example illustrates the danger:

let r = ref (λx. x) in
(r:=(λx:Nat. succ x); (!r)true);

...

It is better to change the typing rule to match the evaluation rule. Fortunately, this is easy: we just impose the restriction (often called the value re striction) that a let-binding can be treated polymorphically—i.e., its free type variables can be generalized—only if its right-hand side is a syntactic value. This means that, in the dangerous example, the type assigned to r when we add it to the context will be X→X, not ∀X.X→X. The constraints imposed by the second line will force X to be Nat, and this will cause the typechecking of the third line to fail, since Nat cannot be unified with Bool.

I am trying to understand the above sentence in bold.

• In the example, is the let binding not treated polymorphically, because ref (λx. x) is not a syntactic value?

• Could you give an example, where the let binding can be treated polymorphically?

Is the above sentence related to the following three sentences in bold? Or are they talking about several different things?

23.8 Fragments of System F

The most popular of these is the let-polymorphism of ML (§22.7), which is sometimes called prenex polymorphism because it can be viewed as a fragment of System F in which type variables range only over quantifier-free types (monotypes) and in which quantified types (polytypes, or type schemes) are not allowed to appear on the left-hand sides of arrows. The special role of let in ML makes the correspondence slightly tricky to state precisely; see Jim (1995) for details.

23.2 Varieties of Polymorphism

More common in practice is the form known as ML-style or let-polymorphism, which restricts polymorphism to top-level let-bindings, disallowing functions that take polymorphic values as arguments, and obtains in return a convenient and natural form of automatic type reconstruction (Chapter 22).

Thanks.