Comment by skybrian
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 great when the type constraints are inequalities.