As far as I can tell they are using local inference, which is basically just unification. The set of possible types seems pretty narrow[1] as well so I don't see much room to go wrong. You're right that there is a lot of mathematical theory about type systems and that inference can easily go wrong (be undecidable) but that is mostly for type systems that try to do inference for higher rank polymorphism and other things, which it doesn't seem like Hack is. Also I guess the language is supposed to be a superset of "valid" PHP, although I don't know whether this is true without modifying the PHP program much.
Local inference isn't just unification. In particular, most local inference algorithms are designed to work with subtyping, which doesn't work in ML-like type systems.
I assume that "local inference" means, in practice, "no let-polymorphism". That's what causes most of the headaches with extensions to Hindley-Milner (including the undecidability of subtyping).
http://hacklang.org/manual/en/hack.annotations.types.php