Type systems are indispensable in modern higher-order, polymorphic languages. An important explanation for Haskell's and ML's popularity is their advanced type system, which helps a programmer in finding program errors before the program is run. Although the type system in a polymorphic language is important, the reported error messages are often poor. The goal of this research is to improve the quality of error messages for ill-typed expressions.

In a unification-based system type conflicts are often detected far from the source of the conflict. To indicate the actual source of a type conflict an analysis of the complete program is necessary. For example, if there are three occurrences where x::Int and only one where x::Bool, we expect that there is something wrong with the occurrence of x::Bool. The order in which subexpressions occur should not influence the reported error. Unfortunately, this is not the case for unification-based systems.

This article presents another approach to inferring the type of an expression. A set of typing rules is given together with a type assignment algorithm. From the rules and the program at hand we construct a set of constraints on types. This set replaces the unification of types in a unification-based system. If the set is inconsistent, some constraints are removed from the set and error messages are constructed. Several heuristics are used to determine which constraint is to be removed. With this approach we increase the chance that the actual source of a type conflict is reported. As a result we are able to produce more precise error messages.