There are some important requirements if you want to have "full type inference" in your language. In order: 1 - For each term in the language, there must be an

There are some important requirements if you want to have "full type inference" in your language. In order: 1 - For each term in the language, there must be an unique "best type" that describes it. (principal type property) 2 - If principal types exist, then you also need to show that a type inference algorithm exists. (decidability of types) 3 - If the type inference algorithm exists, it must execute in a reasonable amount of time Many of the type system features that one might want to add to a language can violate one of these properties, specially when you start combining them together into a single type system. In particular, subtyping is particularly tricky. Finally, there is also a problem that you can never get away from with full global type inference schemes: type error messages tend to take the form of "type A is not equal to B" instead of "found type A, expected type B". Then a type constraint cannot be met, the error message cannot tell you which of the two sides is the wrong one. Additionally, the way that type constraints propagate means that the error message might not necessarily point to the true source of the type error. For these reasons, even in language with full type inference it is usually a good idea to at least have type annotations for top level functions.