That's the main issue with advanced type systems that feature things like union types, generics/polymorphism, subtyping... It's hard to specify the line between type inference guessing correctly what the programmer wants, and type inference now catching a programmer's bug. This is the reason that most Hindley-Milner type systems (e.g. OCaml's) don't allow recursive types (which come up e.g. for typing the Y combinator).

Another example is:

    function equal<T>(lhs: T, rhs: T): boolean {
      return lhs === rhs;
    }

    var e = equal(42, 'hello');

Here, there obviously is a type for `T`: `any` (the toplevel dynamic type) or `number|string`.

This problem is caused by the requirement that type inference is "complete", i.e. that it correctly infers types for all programs that have a valid typing (i.e. that would work if the programmer specified all types).