Better type check error messages for expressions involving polymorphic functions

[sharkdp]

We try to avoid showing constraint-solver error messages wherever we can, because they will probably always be worse than direct type-checker errors. Unfortunately, there are still some cases where they show up. A simplified example looks like this:

>>> fn id(x) = x

  fn id<A>(x: A) -> A = x

>>> 1 meter + id(1 second)
error: Could not solve the following constraints:
  Length / Time = Scalar
.. while trying to infer types in the (elaborated) statement:
  1 metre + id(1 second)

 = Consider adding type annotations to get more precise error messages.

Here, we instantiate id :: T0 -> T0 with a fresh type variable T0, add a Time ~ T0 constraint for the argument, and a Length ~ T0 constraint for the return type. But we fail to stop immediately and instead go into the constraint solver stage where those two constraints are turned into a single Length ~ Time and subsequently into a Length / Time = Scalar dtype constraint, which can not be solved.

[sharkdp]

This is a highly non-trivial problem, so I'm collecting a few resources:

• https://ecommons.cornell.edu/server/api/core/bitstreams/1f5f5381-1004-4756-adb0-dfb2bf509163/content
• Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference, https://arxiv.org/abs/2402.12637
• https://www.researchgate.net/publication/2853723_Improved_Type_Error_Reporting#full-text
• https://ics-websites.science.uu.nl/docs/vakken/mapa/downloads/type-error-diagnosis.pdf, https://www.youtube.com/watch?v=bPrM1gONdII
• https://www.reddit.com/r/ProgrammingLanguages/comments/i2hfti/comment/g06inhf/
• https://dspace.library.uu.nl/bitstream/handle/1874/7297/full.pdf - Top Quality Type Error Messages

[rben01]

So in the provided example, the goal is to be able to go back and attach the constraint solver error to the + (which must have two arguments of the same type)? Or more concretely, to develop heuristics about which generic parameter unifications should have highest precedence? i.e., that f<A>(x: A) -> A should be solved earlier in the constraint solving process than add<A>(x: A, y: A) -> A because it is “more deterministic” — although I'm having trouble articulating exactly how (bottom up vs. top down?). It seems like one simple heuristic (that needs verification) is that unifying an input generic parameter with an output generic parameter should take higher precedence than unifying two input generic parameters. Perhaps also that constraints should be solved in the order that the expressions would be evaluated (the latest expression to be evaluated should have its constraints’ failures be the ones reported).