Try implementing "A practical framework for type inference error explanation"

[byorgey]

Giving good error messages when type inference fails is notoriously tricky. In A Practical Framework for Type Inference Error Explanation, Loncaric et al. give a framework for essentially doing type error slicing (pointing to the places in the code that contributed to a type error) while treating type inference more or less as a black box. The idea is to take the set of constraints generated by type inference and try to find a minimal (or at least small-ish) subset such that removing them causes the constraint solver to succeed, and point to the places where those constraints were generated. The results seem on par with other approaches to the problem, with a much simpler and more language-agnostic implementation. I'd like to try implementing this, partly because it might give us nice error messages, and partly because I am shamelessly using Swarm as a laboratory for learning about cool PL techniques.

I have read carefully through the paper and it seems like implementing it shouldn't be too bad. In particular, it would require:

• Rewrite the type inference algorithm to generate a set of constraints instead of solving them on the fly, then have a separate constraint solver which solves them. We should still be able to use unification-fd for the constraint solver, but the point is that we need to be able to run the constraint solver multiple times on different subsets of the constraints.
  • Concretely, we should just be able to change the concrete typechecking monad, and the semantics of things like =:=: currently it just calls the unification operator from unification-fd, but we could change our monad to have something like Writer (Set Constraint) and then change =:= to just add something to this set. Most of our actual inference code should not have to change at all.
  • In practice we might like to keep the current behavior which does unification on the fly (so we can fail fast, and at least have a default error message to show, and/or have a flag that can turn the experimental new error generation behavior on and off), but also track a set of generated constraints on the side.
• Instrument the constraint solver to track "unsat cores", as outlined in the paper.
  • A first, stupid yet easy way is to just find any set of unsatisfiable constraints initially and then iterate the solver to find an unsat core.
  • The paper also outlines some methods for tracking unsat cores during the solving directly.
• Implement the MYCROFT algorithm as outlined in the paper.

[byorgey]

I think it's still worth doing #99 first, since that should be much simpler. I don't really know if and when I will get around to this.