What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value? Types and Programming Languages by Pierce says:


  22.7 Let polymorphism
  
  A ﬁnal 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-eﬀecting
  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 uniﬁed
  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 quantiﬁer-free types
  (monotypes) and in which quantiﬁed 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.
You seem to have been confounded by many related and similar but crucially different concepts! Let me attempt to explain them one at a time.

Parametric polymorphism is the ability to write types that quantify universally over type variables using the $\forall$ quantifier. It is similar to template polymorphism in C++, or generics in Java. For example, the type $\forall \alpha . \alpha  \rightarrow \alpha$ means "for each and every type $\alpha$, given an expression of type $\alpha$, this function returns an expression of type $\alpha$. This is (almost) equivalent to writing the Java method signature public &lt;T&gt; T foo(T bar).

Parametric polymorphism is parametric in that for each and every possible type $\alpha$, the function behaves in the same way. This gives us powerful free theorems about the behavior of a function, e.g., a function with type $\forall \alpha . \alpha  \rightarrow \alpha$ could only be the identity function, as you were given something of an unknown type, the only thing that you could do with it is to return it unchanged (unless you cheat by non-termination).

Hindley-Milner is a special and restricted form of parametric polymorphism, in that it only allows $\forall$ to appear at the beginning of a type. That is, you cannot have types like $\forall \alpha . (\forall \beta . \beta \rightarrow \beta) \rightarrow \alpha$. The reason why people love Hindley-Milner is that type reconstruction (or type inference), or reconstructing the type of an expression without type annotations, is always deciable and principal (meaning that the type reconstructed is always the most general type possible).

The value restriction is a restriction in programming languges with both Hindley-Milner type systems and mutable storage. With the value restriction, a polymorphic type would only be inferred for a definition if the right-hand side of the definition is a syntactic value. The idea is to prevent problems with mutable store:

Consider the following ML program:

let r = ref []
r := [3]; r
let l = List.map (function true -&gt; 1 | false -&gt; 2) !r


Without the value restriction, the type 'a list ref would be inferred for r. However, the second line makes the contents of r have the type int list, nevertheless r still keeps the (incorrectly) polymorphic type 'a list ref and the third line would result in an uncaught type error!

The value restriction prohibits definitions whose right-hand side is not a syntactic value from being inferred a polymorphic type. In the program above, r would no longer have a polymorphic type since ref [] is not a syntactic value. The second line will fix the type to r to int list ref, causing the third line to correctly report a type error.

For more about value restriction, the first and second part of Jacques Garrigue's paper Relaxing the Value Restriction explains it rather concisely. There is also Andrew Wright and Matthias Felleisen's paper A Syntactic Approach to Type Soundness in which the value restriction was first invented.