HM type inference works perfectly fine with separate compilation and/or partial files (whichever you mean). See the OCaml tooling for a concrete demosntration.

HM type inference works perfectly fine with separate compilation and/or partial files (whichever you mean). See the OCaml tooling for a concrete demosntration. Subtyping is a fairly large domain, and it really depends what you mean. There are cases where it works fine (again, see OCaml) and other where it's more problematic (see Scala). In any case it's not really HM anymore, it needs to be more.