Extending Hindley-Milner to type mutable references I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used to declare a variable as opposed to a bare assignment.

However, I'm now trying to add mutability into the language, specifically in the syntactical form

let mut x = 1


where x is now a rebindable variable. This is effectively the same as

let x = ref 1 in ...


in ML, but my type-checker inserts the dereference operator (!) automatically. So something like ref is never directly used. Any instance of x has a ! applied to it. So, if you do

let mut x = 1
let y = x
x = 2


Then x is still rebindable, and has the value of 2, but y is immutable and has the value 1. 

I am having great difficulty extending my implementation of Hindley-Milner 's unification to support mutable references. The main paper I was reading was Standard ML-NJ Weak Polymorphism and Imperative Constructs by John Mitchell, as I was hoping to get an inference algorithm that had similar behavior to OCaml's weak polymorphism implementation.

This paper is pretty good and explains most things well enough, but it lacks a formal description of the type inference algorithm for its language. Are there any good resources on extending Hindley-Milners unification algorithm, that is, not the type system, with mutable references. I know the two go hand in hand, but I'm just having a really hard time jumping from the type inference rules from the paper I'm using to extending my implementation. I'm wondering if there is at least a description of an algorithm that unifies types in a language that supports mutable references.

Lastly, I saw this question here asking something similar. The asker states "I only find solutions for a language with mutable references but without genuine imperative control structures", I would like to see those references! I completely understand how to extend my language to have imperative control structures once I get my mutable references working, but this is where I am stuck now.
To get behaviour similar to Ocaml, simply avoid generalizing the type of mutable variables. 

With ordinary let-bindings, you generalize if you bind a value, and don't generalize otherwise. With mutable variable bindings, you never generalize. 

The standard ML-like behaviour is then: 

let xs = []          // xs : forall a. list a 

let as = 1 :: xs     // as : list int   -- instantiate a to int
let bs = true :: xs  // bs : list bool  -- instantiate a to bool


The mutable variable typing will go:

let mut xs = []     // xs : list ?a  -- a is an unification variable

let as = 1 :: xs    // as : list int  AND ALSO
                    // xs : list int, since ?a gets resolved to int
let bs = true :: xs // TYPE ERROR, since xs : list int