> To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same In fac

> To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same In fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).