What was wrong with SML?
I think that in some sense the <i>correct</i> solution to the reference type problem is the Scala solution, which depends on subtyping.  This is pretty tricky to reason through, and adding subtyping makes type inference a lot more difficult, so it&#x27;s hardly surprising that SML avoided this, but it provides a much more satisfying solution.  (OCaml later embraced subtyping, but in the particular case of mutable references, it instead adopted the same value-restriction approach as SML.)<p>Here&#x27;s the way I understand it; be warned that I&#x27;m just starting to understand this stuff, so I might have got something wrong.  I&#x27;d welcome corrections.<p>S is a subtype of T (S &lt;: T) iff you can use an object of type S wherever you need an object of type T.  This gives us a partial order on types, in the sense that<p><pre><code>    ∀T: T &lt;: T
    ∀S:∀T: S &lt;: T ∧ T &lt;: S ⇒ S = T
    ∀S:∀T:∀U: S &lt;: T ∧ T &lt;: U ⇒ S &lt;: U
</code></pre>
which all follow from the above informal definition.  Sometimes we make it a lattice, for example by adding a ⊤ type (&quot;top&quot;) that everything is a subtype of and a ⊥ type (&quot;bottom&quot;) that is a subtype of everything.<p>In general in the presence of subtyping we can only infer type <i>bounds</i> on most things, not exact types.  For example, consider that {3} &lt;: ℤ &lt;: ℝ &lt;: ℂ; if we see a function being applied to the value 3, we can infer that it must be at least applicable to {3}, but a function that is applicable to ℤ or ℝ would also work.<p>Given this informal definition, surprisingly, α → α (the type of the identity function) is a &quot;subtype&quot; of bool → bool, not vice versa.  That is, α → α &lt;: bool → bool.  Whenever we want a function of type bool → bool, we can use a function of type α → α, but not vice versa.<p>α → α is a weird type because it includes an implicit universal quantifier: ∀α: α → α.  As it turns out, the judgment above that α → α &lt;: bool → bool is not because α &lt;: bool or bool &lt;: α.  It&#x27;s because bool → bool is what you get when you instantiate the quantifier with a particular value, α = bool.<p>There&#x27;s <i>also</i> a function-specific rule for subtyping, and it&#x27;s a real mindbender: B → C &lt;: A → D if A &lt;: B and C &lt;: D.  We say functions&#x27; argument types are <i>contravariant</i> and their results are <i>covariant</i>.  Considering the A &lt;: B case, if we need a function from integers to booleans, we can use a function from real numbers to booleans—we just won&#x27;t happen to invoke it with any non-integer real numbers, but it will still work, assuming there aren&#x27;t incompatible binary representations at play (as in the case of the OCaml +. and + operators MJD mentions.).  Considering the C &lt;: D case, we can also use a function from integers to true: it will never return a value we cannot use as a boolean.<p>We can decompose the operation of taking a reference to x, ref x, into a step of creating a reference r and then applying the reseating operation r := x to it.  This operation is valid iff the assignee is of a subtype of the referent type; that is, (r : T ref) := (x : S) is valid iff S &lt;: T.  That&#x27;s because later when we read r we will be using its value as a T, so any subtype of T is fine.  So for ref (fn x ⇒ x), we have that S = α → α, so we can derive the type bound that T must be some <i>supertype</i> of α → α.  As mentioned above, this includes bool → bool, but it also includes ℤ → ℤ, (ℤ × ℂ) → (ℤ × ℂ), and the polymorphic type α → α itself.  So reseating a reference is contravariant: we can write a value we know is an integer <i>or anything more specific</i> (a subtype such as a positive integer) into a reference we know to hold an integer <i>or anything more general</i> (a supertype such as a real number).<p>The dereferencing operation !r turns out to instead be covariant: !(r: S ref): T is valid iff S &lt;: T.  That is, we&#x27;re going to use the result as type T, so the reference can hold any subtype of T.  So if we see ((!m) 23) we have (!m) : {23} → ⊤, from which we can deduce a type bound (m : U) where U &lt;: ({23} → ⊤) ref.  That is, the type of the referent of m is a subtype of a &quot;function that can take 23 and return something&quot;.  For example, (ℤ → string) &lt;: ({23} → ⊤), because {23} &lt;: ℤ and functions are contravariant in their arguments, and string &lt;: ⊤ (because every type is a subtype of ⊤), so if m has type (ℤ → string) ref, we&#x27;re good.  (bool → bool) ref would not work, because (bool → bool) ref is not a subtype of ({23} → ⊤) ref, because bool → bool is not a subtype of {23} → ⊤, because, even though bool &lt;: ⊤, {23} is not a subtype of bool.<p>How does this resolve the problem?  If m is of type (α → α) ref, ((!m) 23) <i>would</i> work; for example, if m happens to be a reference to the identity function, it evaluates to 23.  (In many languages that&#x27;s the only function of type α → α, in the interests of making the Curry–Howard correspondence meaningful.)  But if we&#x27;ve previously seen (m := not), we have an incompatible type bound: (not : bool → bool), so we know that m is of type (bool → bool) ref or a ref to <i>some supertype of</i> bool → bool, U ref where bool → bool &lt;: U.  And, as I said above, it is <i>not</i> the case that bool → bool &lt;: α → α; it&#x27;s the other way around.<p>This seems to give us a nice, clean solution to the problem of types for references.  Aside from being confusing as hell, the cost is that instead of inferring a <i>type</i> for every expression we can now only infer an <i>infinite set of possibilities</i> for its type.  This sounds ridiculous but it is precisely what OCaml does for polymorphic variants and objects (though not mutable refs; details are in <a href="https:&#x2F;&#x2F;v2.ocaml.org&#x2F;manual&#x2F;polymorphism.html" rel="nofollow">https:&#x2F;&#x2F;v2.ocaml.org&#x2F;manual&#x2F;polymorphism.html</a>).  With polymorphic variants:<p><pre><code>    # let f a = match a with 1 -&gt; `P (3, 4) | _ -&gt; `Q (5) ;;
    val f : int -&gt; [&gt; `P of int * int | `Q of int ] = &lt;fun&gt;
    # let g b = match b with `P (c, d) -&gt; c + d | `Q (c) -&gt; c ;;
    val g : [&lt; `P of int * int | `Q of int ] -&gt; int = &lt;fun&gt;
</code></pre>
The &quot;&lt;&quot; here means that what&#x27;s being given is an &quot;upper bound&quot;: it&#x27;s perfectly acceptable to apply g to an expression whose type is a <i>subtype</i> of the type given, like this:<p><pre><code>    # `Q 2 ;;
    - : [&gt; `Q of int ] = `Q 2
    # g (`Q 2) ;;
    - : int = 2
</code></pre>
But the &quot;&gt;&quot; on f&#x27;s return type is a &quot;lower bound&quot;: you can only use f in a context where its return type <i>is a subtype of</i> the expected type.  Including the same type, so we can pass it to g:<p><pre><code>    # g (f 1);;
    - : int = 7
    # g (f 2);;
    - : int = 5
</code></pre>
Similarly we can write a function that calls a couple of methods on its arguments:<p><pre><code>    # let mf o = (o#foo ; o#bar + 1) ;;
    val mf : &lt; bar : int; foo : &#x27;a; .. &gt; -&gt; int = &lt;fun&gt;
</code></pre>
Here OCaml infers that the object needs to have a method &quot;bar&quot; returning int and a method &quot;foo&quot; of some type, but the .. makes this an upper-bound object type: it&#x27;s okay for the object to be of some subtype that has more methods.  And similarly if you construct an object with some methods, it can be used in a context that requires some supertype that doesn&#x27;t have all of them.  (There&#x27;s a very close analogy between an object with a certain set of methods and a function that can be applied to terms with a certain finite set of polymorphic variant tags.)<p>The subtyping approach would seem to provide a logical solution to the problem of mutability, but it isn&#x27;t the approach OCaml took, for reasons I don&#x27;t understand.  It&#x27;s confusing and difficult to understand, but less so than OCaml&#x27;s current set of rules.  I suspect the answer is that OCaml had to be backward-compatible with earlier versions of Caml before subtyping was added, but possibly it&#x27;s instead to keep the type inference problem decidable or something.