[heavenlyblue]

    "f(x) + g(x)"

This example is way too trivial to explain why type systems are generally undecidable. Let's imagine:

    def f/g(x):
      if isinstance(x, str):
       return 6
      elif isinstance(x, int):
       return 'a'

It is decidable for any type of x that is previously known. More importantly, type systems were essentially created to be able to prove whether a given expression is decidable or not.

    x = 1
    print_int(x)
    x="a"
    print_string(x)

This is solved by A-normal form (https://en.wikipedia.org/wiki/A-normal_form). Or by a more general concept that is available outside functional languages, SSA (https://en.wikipedia.org/wiki/Static_single_assignment_form).

You can make a point that this code is hard to modify in dynamic languages, but it is an issue with the code style rather than type systems. For example - IntelliJ IDEA would highlight such Pythonic code as incorrectly typed, since you have changed the type and therefore the variable itself.

I find the general argument against complexities in the type systems such as Haskell to be quite amusing, to be fair. Most of the time you are not dealing with code that is undecidable - and that's why type systems are interesting.

[z3t4]

the real world is not strictly typed, i think types are for the compiler rather then humans. Im however a big fan of runtime bound checking so that the program always have a sane state.