If you want to see a really beautiful type inference, take a look at Hindley-Milner. Not only is it global (it infers all the types in your program) but it's al

If you want to see a really beautiful type inference, take a look at Hindley-Milner. Not only is it global (it infers all the types in your program) but it's also surprisinlyg simple--it's basically just a straightforward constraint satisfaction problem. In particular, take a look at how it has been extended by real languages, especially OCaml. OCaml has some very cool sub-typing features but manages to maintain global inference, unlike Scala. (Largely by choosing structural rather than nominative sub-typing.) So some languages have had better type inference for longer than Scala has been around.