So, I think, that it should be clarified by someone, who knows OCaml and
English much better than me, what is the difference between this two
cases. And it would be great if it will be described in the manual,
too.
The problem is that most people expecting "let x : 'a = 12" to fail did not (and often will never) read that manual section. Documenting is enough when people notice they don't know something (and look for the answer). It doesn't work very well when people guess what something is (so they don't feel a need to look it up), but consistently guess wrong.
I agree with Andreas that the current situation is unsatisfying, and that his proposed change would be a net improvement. Roberto says that we should teach the stuff better, but our constantly-repeated experience is that people consistently *guess* that type annotations enforce polymorphism -- before seeking for help from teachers on that point. As to why this happen, I'm not sure (but I don't think we need to have the cause to agree that the issue requires a change), but I would hazard Ivan's explanation that they expect that from the meaning of type variables in type signatures, either inferred in the toplevel or explicitly written in .mli. After all, most OCaml programs have so few type annotations that people only encounter type variables in those type signatures. The suggestion to use '_a for flexible variables seems reasonable.
However, I think that the current syntax of implicitly-introduced variables with heuristically-defined scoping rules is bad in any case. My own toy experiment with explicit syntaxes always use an explicit binding syntax for both rigid and flexible variables (eg. "forall a b c in ..." and "some a b c in ..."). In this regard, the ('a 'b . ty) or (type a) syntaxes are definite improvements -- if only we had applied those explicit binding forms to GADT constructor types as well... So I think that even with Andreas' proposed change, people would still be surprised by things like the following:
let id : 'a -> 'a = fun x -> x
let dup (x : 'a) ('a * 'a) =
let result = (x, x) in
(id : 'a -> 'a) result (* fails, while (id : 'b -> 'b) works *)