Bidirectional is a nice, pragmatic compromise, but it is a reaction to the difficulty with taking full type inference beyond let-polymorphism. We wouldn't be using bidirectional, if Damas-Hindley-Milner would scale.
Damas-Hindley-Milner inference is also hyper-optimised to a specific point on the design space, and does an excellent job there, but (to echo Conor McBride) I would love to see less conflation of the ideas of execution phase, parametericity, and implicitness going forward.
less conflation of
That's interesting. But I'm not sure what you mean. Would you be able to explain this more, or point me to something I can read on this?