[mafribe]

   research in academia is that 
   it's disproportionately focused 
   on even stronger types that are 
   even harder to compute. 

Type inference for simple types in sequential computation is a solved problem, Milner and Damas showed how to do it in [1] in 1982. However, most extensions of Damas/Milner cross from decidable type inference to undecidability, so some annotation is often necessary, e.g. Scala, Rust, Haskell (kinding).

Most work on expressive typing systems (e.g. dependent types) has a different aim, namely using types for the verification of arbitrary program properties. This is undecidable, but we want (and need) as much automation as possible to lower the cost of verification, whence a lot of research is about partially automated type inference for very expressive typing systems. For most standard front-end dev, verification is not an issue since

- the field has fairly low correctness requirements that can easily achieved with testing

- typically you don't have strong specifications to verify against. No formal spec, no verification.

[1] L. Damas, R. Milner: Principal type-schemes for functional programs, http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_typ...