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

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).