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.

Of course you understand this, but for the benefit of the audience:

HM can do this because it dramatically restricts the allowable complexity of every single name in the program. This is rarely a problem, though, as typically you, as a programmer, only ever intend for names in the program to be so complex. The result is that HM simply ensures that your program is one which makes enough sense all of the time.

Which is sometimes painful for people when they first start.