Issues related to the relaxed value restriction has become relevant again after the introduction of GADTs, since these don’t admit positive variance, as required by the relaxation. The way forward may be to restore variance checking; even failing that a new pseudo-variance could indicate that the type is merely state-free for that parameter. Though, inspired by that paper one could consider a somewhat more esoteric but imperative-friendly option:
The by-name binding in the paper induce an evaluation per occurrence. It seems sufficient to evaluate the let-term at each type in order to guarantee safety. Such a “by-type” semantic would generalise the by-value semantic, admitting the same type generalisation as by-name. Though, since it does not generalise the relaxed value restriction it should be a separate let-construct if added to OCaml.
E.g., without suggesting this specific syntax
let [_] get_cell, set_cell, clear_cell =
let r = ref None in
((fun () -> !r), (fun x -> r := Some x), (fun x -> r := None))
val ['a] get_cell : (unit -> 'a option)
val ['a] set_cell : ('a -> unit)
val ['a] clear_cell : (unit -> unit)
would create a reference per instance of 'a.
This would have a performance penalty linear in the number of type instances instead of linear in the number of calls. There would be challenges to the implementation though. A run-time representation of types seems necessary in order to memoise the state at each used type. Since types can be generated at run time, at least due to first-order modules, there are potential space leaks and instances which cannot be identified for initialization at compile-time.
Without being familiar with its implementation, I’d imagine this might trespass into modular-implicits territory due to the instance-creation and implied type argument.