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