Improving Error Messages for Dependent Types

Dependently typed languages allow programmers to establish the correctness of their code, accessing the full power of higher-order logic via the Curry-Howard correspondence. However, a major barrier to their widespread adoption is their complexity. Since they impose a rigid type discipline, a significant portion of development time is spent reading, understanding, and responding to compiler error messages.

For Hindley-Milner style functional languages, such as Haskell or ML, several techniques have been developed to improve the quality of error messages. Our work adapts these techniques to dependently typed languages. We present replay graphs, which provide a representation of a unification algorithm run as a graph, allowing for the use of heuristics to generate error messages and repair hints, and counter-factual unification, which makes unification resistant to bias, so that when conflicting assumptions are encountered, the first one is not necessarily assumed to be correct.