Traditional type inference aims at reconstructing type declarations given some type definitions. We present a rule-based constraint rewriting algorithm that reconstructs both type declarations and type definitions.

Our algorithm reconstructs uniform polymorphic definitions of algebraic data types and simultaneously infers the types of all expressions and functions (supporting polymorphic recursion) in the program. The declarative nature of the algorithm allows us to easily show that it has a number of highly desirable properties such as soundness, completeness and various optimality properties. Moreover, we show how to easily extend and adapt it to suit a number of different language constructs and type system features.

This is joint work with Maurice Bruynooghe, previously presented at PPDP 2006.