Improving Type Error Messages in OCaml

Abstract

Cryptic type error messages are a major obstacle to learning OCaml or other ML-based languages. In many cases, error messages cannot be interpreted without a sufficiently-precise model of the type inference algorithm. The problem of improving type error messages in ML has received quite a bit of attention over the past two decades, and many different strategies have been considered. Unfortunately, the problem only admits imperfect solutions. On the one hand, reporting everything that contributes to the error leads to messages that are way too verbose. On the other hand, relying on heuristics or relying on the bias inherent to unification for selecting the most plausible causes of the error often attracts the programmer's attention away from the actual location of the error.

In this work, we try to nevertheless improve the state of the art. We present a modification to the traditional ML type inference algorithm implemented in OCaml that, by significantly reducing the left-to-right bias, allows us to report error messages that are more helpful to the programmer. Our algorithm remains fully predictable and continues to produce relatively-concise error messages that always help making some progress towards fixing the code. We implemented our approach as a patch to the OCaml compiler in just a few hundred lines of code. We believe that this patch should benefit not just to beginners, but also to experienced programs developing large-scale OCaml programs.

Paper

Arthur Charguéraud
ETPCS: Post-proceedings of the ML/OCaml 2014 workshops, November 2015