Improving Error Messages for Dependent Types with Constraint-based Unification

Abstract

Dependently typed programming languages provide a powerful tool for proving code correct. However, these languages are complex, and programming in them is often difficult. Certain features, such as pattern matching or inferring values using metavariables, rely on a unification procedure performed during type-checking. When this process fails, the error messages provided are often confusing, and do not accurately indicate which programmer error caused the failure.

For functional languages with simple typing, error messages have been improved by expressing type-checking as a constraint-solving problem, performing global analysis on a constraint-graph. While these attempts have been successful, there are a number of differences between dependent and simple types. Parametric polymorphism is expressed using implicit parameters, rather than polymorphic types. Moreover, since there is no distinction between types and terms, typechecking may require code to be evaluated. This means that the existing techniques for error generation do not directly apply to dependent-types.

This thesis presents background information on dependent-type checking, functional error-message reporting, constraint-based typechecking, and higher-order unification. We frame some of the challenges for adapting existing techniques to more advanced languages.

In an initial attempt to improve error messages, this thesis proposes a dependently-typed system with replay-graphs, for combining higher-order unification with type graphs. Additionally, a system of counter-factual constraint-solving is proposed, which finds multiple solutions for various subsets of unification constraints.

The results of implementing these techniques is presented, with examples both of where they produce improved error messages on type-incorrect programs, and where they produce poor messages.