It's kind of sad to me that (almost) complete type inference has been around since the [70s](https://en.wikipedia.org/wiki/Hindley–Milner_type_system) and it's still not mainstream. (unless you consider F# or OCaml mainstream languages)

Type annotations at the signature level are documentation, so I'm not so sure if global type inference is really better than local type inference. Also HM type inference doesn't play nice with type systems with subtyping or method overloading.

OCaml does have subtyping (albeit with a clear separation between that and implementation inheritance) and method overloading, but its type inference accommodates those. Or am I missing something?

Seriously asking: How does it work for undecidable cases? Nominal subtyping may cause ambiguity where both supertype and subtype match. Overloading may cause ambiguity where more than one overload matches, and depending on the overload we can infer different types.

BTW I didn't say it was impossible, only that it doesn't play nice and probably is no longer a pure HM system. The search space is definitely much bigger with overloading and subtyping.

It still has classes, and implementation inheritance with method overloading, but they're completely decoupled from subtyping (so e.g. subclasses are not necessarily subtypes - a class can use self-type in an argument position). And types themselves are structural, with row variables and polymorphism. If you need to define an equivalent of a named interface, you just define a type alias, like any other. And when you define a class, you get an auto-generated type alias for the structural type of objects that it will instantiate. [1]

End result actually looks surprisingly familiar to someone coming from C++ or Java, at the first glance. It's really a shame that it's not something that OCaml is famous for; it deserves to be. I wish I could have an object model that expressive in C#.

[1] https://caml.inria.fr/pub/docs/manual-ocaml/objectexamples.h...