In programming languages that combine
let r = ref [] in (* generalise r : forall a. a list ref *)
r := [ () ]; (* specialise a := unit *)
true :: !r; (* specialise a := bool *)
If we implement Hindley-Damas-Milner polymorphism naively, then r would have type a list ref for all a. Then, by assigning a list containing the unit value to it, we would specialise it, leading to unsoundness in future uses, like the last line.
To avoid this, languages in the ML family enforce a value restriction: type variables are only generalised (forall a) only in values. For example, ref [] above is not a value, so it would not be generalised.
In languages with polymorphism and algebraic effects and handlers no value restriction is needed [Kammar and Pretnar 2017]. This leads Kammar and Pretnar to '[...] conjecture that it is impossible to simulate full-blown reference cells using effect handlers without other language features.'
There appears to be a textbook discussion of this in TAPL - reference to be found.
An early reference to this in the literature appears in the following paper:
Harper, Robert, and Mark Lillibridge. ‘Polymorphic Type Assignment and CPS Conversion’. LISP and Symbolic Computation 6, no. 3–4 (1993): 361–79. https://doi.org/10.1007/BF01019463. [pdf]
@article{harper_1993,
title = {Polymorphic type assignment and {CPS} conversion},
volume = {6},
doi = {10.1007/BF01019463},
pages = {361--379},
number = {3},
journaltitle = {{LISP} and Symbolic Computation},
author = {Harper, Robert and Lillibridge, Mark},
date = {1993}
}
Kammar, Ohad, and Matija Pretnar. ‘No Value Restriction Is Needed for Algebraic Effects and Handlers’. Journal of Functional Programming 27 (2017). https://doi.org/10.1017/S0956796816000320. [pdf]
@article{kammar_2017,
title = {No value restriction is needed for algebraic effects and handlers},
volume = {27},
doi = {10.1017/S0956796816000320},
journaltitle = {Journal of Functional Programming},
author = {Kammar, Ohad and Pretnar, Matija},
date = {2017},
}