Propagation of location information in constrained type
inference

Abstract: The Timber type system is an extension of the classical Hindley-Milner
type system, incorporating both qualified types and first class
polymorphism. Since we also have subtyping, type errors in this system
manifest themselves as unsatisfiable constraints rather than as
non-unifiable types as in the Hindley-Milner system.

In this thesis, we present a theoretical model for propagating the
source of a constraint so that it can be presented to the user in case
of an error. We also present examples from an implementation of our
system for the Timber compiler. We propagate the location information
by adding annotations to the syntax tree and then preserve that
information as we build the predicates and types needed for type checking.

We conclude that the approach to annotation taken here is one
possible solution for the propagation of location information in
constrained type inference.