Hindley-Milner and other type systems do it by restricting the class of programs you are allowed to write. Essentially what they do is if they can't infer the t

Hindley-Milner and other type systems do it by restricting the class of programs you are allowed to write. Essentially what they do is if they can't infer the type of a variable they terminate with an error. The class of programs that you are allowed to write is still reasonably big and Turing complete, but as research to make the type system more expressive shows, people want to go beyond that (higher kinds, GADTs, dependent types, polymorphic variants / structural records, subtyping, etc.). Type inference for a dynamically typed language can't terminate with an error if it can't infer the type, it has to be conservative in the other direction: if it can't infer the type of a variable it must assume that it can be anything.