Context-Dependent Type Error Diagnosis for Functional Languages

Customizable type error diagnosis has been proposed as a solution to
achieve domain-specific type error diagnosis for embedded domain
specific languages. A proven approach is to phrase type inferencing
as a constraint-solving problem, so that we can manipulate the order
in which constraints are solved, and associate domain-specific type
error messages with specific constraints to be communicated to the
programmer in case type checking fails. A major challenge in this
area lies in scaling this idea up uniformly to a fully-featured (functional)
language, that is, languages that go beyond the polymorphic
λ-calculus.
In this paper, we show how within the general framework Constraint
Handling Rules we can achieve such uniformity and generality,
while at the same time providing the necessary type error
customizability in a natural way. A proof-of-concept implementation
is provided for a Haskell-like language, including support for type
classes, GADTs and higher-ranked types. However, our approach applies
to any language for which a constraint-based non-backtracking
formulation of the type system is available.