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

Paper: https://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf
Zoom: https://umd.zoom.us/j/98723227318?pwd=K0RJZVZZM1Jhd2laMlg1ajgvUjltQT09