You are confusing two different things: gradual typing, and type inference.
Type inference infers a static type for every expression in a program. Hindley-Milner is such a type inference algorithm.
Gradual typing allows you to partition your program into typed and untyped parts. The untyped parts need not even be typable under your type system.
Type inference and gradual typing can be combined. See:
Siek and Vachharajani: Gradual typing with unification-based inference
http://dl.acm.org/citation.cfm?id=1408688
The idea of that paper is that you want to do type inference for the statically typed part of your program in a gradual type system.
Strictly speaking Hindley-Milner is the type system that itself admits tractable inference using the usual unification techniques via the Damas-Milner family of algorithms. Gradual typing itself uses type inference in the Damas-Milner family, although it diverges with it's notion of consistency.
Scala doesn't/cannot use Hindley-Milner, I doubt it could be any easier to apply it to Python. (Clojure core.typed doesn't use hindley milner either afaik. There've been experiments on that front though)
The problem is that HM doesn't integrate super well with dynamic typing. They already tried doing that with Scheme a while ago (search for Soft Typing) but the end result was very complex and hard to use.
That's false. This is gradual typing, which is more recent. Gradual typing allows dynamicity, while HM fails if not every type can be statically inferred. Furthermore, IIRC there are reasons why HM is less/not suited for imperative languages, but they escape me at the moment.
