> You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification.

Could you expand on this? I do not follow. You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. It is not often done because people are coming around to the idea that global type inference causes spooky action at a distance, but nothing prevents it from working.

> I maintain that what the article calls HM is trully unification

In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck.