I think it depends on the algorithm & implementation, but in at least some cases type inference adds very little code over type checking. (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. And depending on the language, you've got to have some non-trivial machinery for handling function overloads, which can require inference-y reasoning anyway (like calling an overloaded function immediately with the result of another overloaded function).)

On the other hand, non-local inference can make things more complicated in some situations, depending on how hard you try. For instance, Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context and return to the member access later. For example, consider the following Rust code where the compiler could figure out the types with some additional complexity but doesn't bother:

  fn main() {
      let a = (1..10).collect();
      println!("{:?}", a.len());
      let b: Vec<i32> = a;
  }

  error[E0282]: type annotations needed

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

>Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context

My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.

Your comment has me feeling quite bullish on TypeScript type inference

HM is pretty easy implement actually. You just need a unification function, the rest is just a laundry list of rules available everywhere, like Wikipedia. Source: I implemented a typed python dialect as a college project that used HM.

> How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables).

Just the opposite: type inference forces the type systems to remain simpler. Without type inference you could make them more complicated.

Implementation would be simpler, but only by a small degree. To be honest, HM is relatively straightforward to actually implement.

There's some really cool programming language theory that makes things like type inference easier than you think. It's still hard but there's rules and math and stuff for all of it.

You can't actually have a statically-typed language without type inference. Otherwise if you tell the compiler `(5 + 2) : String`, how would it report a type error?

That’s not type inference, just type propagation - tons simpler.

Sorry but what's the difference? Inference is a way to infer the type of any given expression. How does type propagation contrast?

Propagation is way easier, and basically just requires tracking types of values & parameters. To infer the type of `a` in

    var a = 1;

I just need to figure out the type of `1`, then realize that the type of `a` is the same.

slightly harder would be typing union / intersection types - e.g. this:

    var a = some_test() ? "foo" : new Bar();

Java would "infer" (kind-of) the type of `a` to be something like `Serializable & Comparable<? extends Serializable & Comparable<...>>` as both `Serializable` and `Comparable` are supertypes of both `String` and `Bar` (well, depends on `Bar` of course). This starts to show how much trickier things can get.

Now, imagine knowing nothing about what can be stored in the variable, and only seeing how it's used - this is the case for function parameters.

    (x) -> x + 1;

Is `x` a `float`? An `int`? A `long`? Maybe a vector? Basically, imagine the most complex type you can write in a given language, and then consider, the compiler would need to be able to prove that this is the only (or at least the most specific) type you could use.

Hmm, all of your examples can be inferred by Hindley-Milner. Of course, for the second one it would be a type error assuming that `Bar` is not a subtype of `String`. I'm not seeing how type propagation of a complex expression could be any simpler or easier than full-fledged type inference of that expression. For example,

    let x = "foo" |> bar |> baz 5

What's the type of `x`? You might say that we can figure it out by propagation, but how's that different from inference?

Indeed, what I'm saying is that inference is more powerful (i.e. better) than propagation. Most compilers only implement propagation, not full inference, allowing programmers to skip type annotations on local variables (since their types can be propagated from parameters and expressions), but not on parameters.

Basically, there's two complications with type inference. One is type variables that you need to then "solve" - in my last example above, the type of parameter `x` would start as a type parameter α (usually denoted by Greek letters in type systems literature), then it would be "unified" with `int` when used "like" an int (i.e. passed to a function `+ : (int, int) -> int`).

This is what happens in a language with a "simple" type system like OCaml, with no subtyping. (OCaml is slightly more complicated, but still all equations that it needs to solve only involve equality (I think)). If your type system features subtyping, things get a bit more complidated.

    (x) -> new List(x + 1, concat("test", x))

This now generates two constraints, `α <: int` and `α <: string`, that the compiler needs to solve. One solution would be an intersection type `string & int`. Does this type make sense? Does it even exist? Will the programmer understand it? The question isn't only finding the solution, but also which solution is "the best" - how to even define "the best"? I'm not aware of any good answers to this question (not even MLSub, it only works for simple cases).

The other big issue type inference deals with, is generalization. If, at the end of inferring an expression's type, there are no equations involving a type variable (a bit of a simplification, but let's go with it), then it can be "generalized" - turned into polymorphic type.

    (x) -> new List(x)

We might be able to assign the type `forall α . α -> list[α]` (or, a this would be written in Java / C++, `<T> T -> List<T>`), but again this depends on multiple conditions (is `x` used elsewhere? does it escape the scope? is `List` mutable?), and can get much more complicated with more features (e.g. upper and lower bounds, like Java's `<U extends Number>`)

In your example, figuring the type of `x` is trivial compared to above - just take the return type of `baz`.

Local variables seems to be the sweet-spot for me, especially when I'm working on a project with others.