> I wonder if this is a reference to "I need you to understand that people don't have conversations where they randomly recommend operating systems to one another"
It is!
> my understanding is that there are areas where you can use bidirectional typing (e.g. languages that have subclasses) where HM style type inference might become undecidable
There are! Afaik most languages end up with a bidirectional system in practice for this reason. Haskell started out HM and has shifted to bidir because it interacts better with impredicative types (and visible type applications). Bidir can handle fancy features like subtyping and all sorts of nifty stuff.
It is!
> my understanding is that there are areas where you can use bidirectional typing (e.g. languages that have subclasses) where HM style type inference might become undecidable
There are! Afaik most languages end up with a bidirectional system in practice for this reason. Haskell started out HM and has shifted to bidir because it interacts better with impredicative types (and visible type applications). Bidir can handle fancy features like subtyping and all sorts of nifty stuff.