We present a new way to generate type-error messages in a polymorphic, implicitly, and strongly typed language (specifically Caml). Our method separates error-message generation from typechecking 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 typechecker 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 messages and using the type-checker on candidate changes to see if they succeed. This novel front-end architecture naturally decomto (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. Categori...
Benjamin S. Lerner, Dan Grossman, Craig Chambers