[thunderseethe]

> The real question is unification vs bidir

Quite the opposite, imo. Unification does not exclude bidir and the two fit together very well. You can have one system with both Unification and bidir and get all the advantages of both.

[StopDisinfo910]

Not really, no. You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Hybrid systems are bidir for parts, unification for others.

But, I maintain that what the article calls HM is trully unification independantly of what's above. This is not about algorithm W. It's actually about the tension between solving types as a large constraint problem or using annotations to check.

[thunderseethe]

> 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.