This is not unique to Coalton. Any HM-based language that defines mutation primitives has it, including Haskell and OCaml. These languages don't "solve" it a sense most people think, instead they provide some sort of restriction or workaround to the HM theory to make mutation constructs feasible. There's a huge space of possible solutions, including ensuring functional purity with monads (Haskell) to using weak polymorphism (OCaml) to using Wright's value restriction (eliminate invalid mutations, but also eliminate tons of reasonable, valid programs).

Coalton developers know of the HM deficiency and described it very well here [2]. It looks like they're building out more important parts of the language that affect their users more seriously (e.g., adding records) before making a hugely consequential design decision around mutation, which people don't seem to bump into much.

It doesn't seem to have stopped them from building interesting software in the slightest. [3]

[1] https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...

[2] https://github.com/coalton-lang/coalton/issues/84

[3] https://coalton-lang.github.io/20220906-quantum-compiler/