I wonder if this is a reference to "I need you to understand that people don't have conversations where they randomly recommend operating systems to one another"

But to the actual point of the article: my understanding is that there are areas where you can use bidirectional typing (e.g. languages that have subclasses) where HM style type inference might become undecidable.

Personally I am a bit skeptical about whether complex type inference doesn't do more harm than good in some cases. A valid alternative approach is to just make type declarations required. Sure infer trivial types like when doing variable assignment but other than that just expect types to be provided. This drastically cuts down on complexity and enforces more readable programs. And it gives you much better error messages.

Or go the opposite way: If you want a language that feels dynamic and leads to prototyping, well a type system that is total and complete might be too heavy. Instead of only allowing programs that are proven to be typed correctly you might want to allow all programs that you can not proved to be wrong. Lean into gradual typing. Everything goes at first and the typing becomes as strict as the programmer decides based on how much type information they add.

Those are both very valid approach. Not every language needs that level of type inference.

You should also ask “Does my language need subtyping such as subclasses?” And if the answer to both is yes, you should probably forget about Hindley Milner, or at least pick something far away from it on the spectrum.

Unification is simple, not very hard to implement and more powerful. Bidir gives better error messages and is more "predictable".

I personnaly lean strongly towards unification. I think you can get good enough error messages and what you lose with bidir is not worse it. But clearly the Rust core team disagreed. They clearly don't mind annotations.

Anyway, here is my non answer: it's a trade off.