The Hindley-Milner "infer as much as possible" approach presents jagged-seeming edges to the user experience because the "possible" part -- restriction imposed not by language authors, but by the logic itself -- isn't always intuitive.
Conversation
Replying to
Becoming increasingly convinced that bidirectional, local type inference with explicit quantification is the way to go. Less interested in Hindley-Milner these days - seems to be too hard to extend in provide good error messages.
we've been thinking vaguely about using local type inference with type holes (see our POPL'17 paper) with a HM layer on top suggesting type hole fillings when possible
1