Violating memory safety with Haskell's value restriction

Summary

17 May 2025 A common issue in impure ML-style languages with polymorphism and mutable references is the possibility of polymorphic references. In a hypothetical impure language that had both these features, but no mitigations against polymorphic references, the following code would be extremely unsafe. unsafeCoerce :: a -> b unsafeCoerce x = let dangerous = ref Nothing dangerous := Just x case dangerous of Nothing -> error "unreachable" Just y -> y This code creates a reference dangerous with an initial value of Nothing, writes x to it, and then reads from it again. But because this language doesn’t prevent polymorphic references and Nothing has type forall a. Maybe a, dangerous is actually generalized to forall a. Ref (Maybe a). This means that in the line that writes to it, dangerous is instantiated to Maybe a, whereas in the line that reads from it, it is instantiated to Maybe b, although the value stored in it still has type a, breaking type safety and consequently memory safety! Scary, right? You might think that you could prevent this by just preventing generalization of reference types, but references can be hidden behind closures, so languages need a slightly blunter hammer: the value restriction. The value restriction says that a let binding can only ever be given a polymorphic type if its bound expression is syntactically a “value”, i.e. an expression that obviously will not perform any computation. 5 is a value. So is Nothing. But sqrt 42 and (crucially) ref Nothing are not values and will not be generalized. Haskell’s let bindings do not have a value restriction. So, does this mean that Haskell’s type system is deeply unsound and we just never noticed? No! If we translate the original example to Haskell, we will hit a type error, telling us that dangerous was not generalized. unsafeCoerce :: a -> b unsafeCoerce x = do dangerous <- newIORef Nothing writeIORef dangerous (Just x) result <- readIORef dangerous case result of Nothing -> error "unreachable" Ju...