SML doesn't have subtyping or variance AFAIK so that can't really explain the issue. The way I like to look at it is to translate to System F. The standard tran

SML doesn't have subtyping or variance AFAIK so that can't really explain the issue. The way I like to look at it is to translate to System F. The standard translation would give: let m : ∀α. ref (α → α) = Λα. ref [α → α] (λx. x) in (m [bool]) := not; print ((!(m [int])) 23) end This actually has different behavior because the ref allocation is under a big lambda (Λ). Each time it is applied it would generate a new ref cell. So it would generate a `ref (bool → bool)` starting with `λx. x` and assign `not` to it. Then generate a separate `ref (int → int)` (again starting with `λx. x`) and dereference and apply it. Thus this would print `23`. (The naive model of) SML runs into problems because it erases the big lambdas and so evaluates `Λα. ref [α → α] (λx. x)` to a single ref cell of type `∀α. ref (α → α)` Sidenote: Variance does have some relation here, I couldn't think of a way to trigger bad behavior without a type that uses the type variable invariantly.