Local type inference

We study two partial type inference methods for a language combining subtyp ing and impredicative polymorphism. Both methods are local in the sense tha t missing annotations are recovered using only information from adjacent no des in the syntax tree, without long-distance constraints such as unificati on variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound vari ables in function abstractions by propagating type constraints downward fro m enclosing application nodes. We motivate our design choices by a statisti cal analysis of the uses of type inference in a sizable body of existing ML code.