Seminal: searching for ML type-error messages

We present a new way to generate type-error messages in a poly-morphic, implicitly, and strongly typed language (specifically Caml). Our method separates error-message generation from type-checking by taking a fundamentally new approach: we present to programmers small term-level modifications that cause an ill-typed program to become well-typed. This approach aims to improve feedback to programmers with no change to the underlying type-checker nor the compilation of well-typed programs. We have added a prototype implementation of our approach to the Objective Caml system by intercepting type-checker error mes-sages and using the type-checker on candidate changes to see if they succeed. This novel front-end architecture naturally decom-poses into (1) enumerating local changes to the abstract syntax tree that may remove type errors, (2) searching for places to try the changes, (3) using the type-checker to evaluate the changes, and (4) ranking the changes and presenting them to the user