Apparently it only gets away without annotations if the language doesn’t support subtyping? Here’s an explanation about why bidirectional type checking is better for that:

https://www.haskellforall.com/2022/06/the-appeal-of-bidirect...

It seems to me that type-checking that relies on global constraint-solving is usually a bad idea. Annotated function types result in less confusion about what a function does.

Indeed. Unification-based type inference doesn't work well when the type constraints are all inequalities.