Finding minimum type error sources
ISSN der Zeitschrift
Software-engineering and management 2015
Gesellschaft für Informatik e.V.
Automatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler reports the first location with a type conflict as the source of the error. However, this is often not the true error source. We present a general algorithm that helps to produce more meaningful type error reports. The algorithm finds all minimum error sources, where the definition of minimum is given by a compiler-specific ranking criterion (e.g. minimizing the program changes needed to fix the error). The approach works by reducing the search for minimum error sources to an optimization problem that we formulate in terms of weighted maximum satisfiability modulo theories (MaxSMT). This formulation allows us to build on SMT solvers to support rich type systems and, at the same time, abstract from the concrete ranking criterion. We have implemented an instance of our algorithm targeted at OCaml programs. Our evaluation shows that our approach significantly improves upon the quality of type error reports produced by state of the art compilers. This work appeared at OOPSLA 2014 where it won a Best Paper Award.