AbstractBidirectional typechecking has become popular in advanced type systems because it works in many situations where inference is undecidable. In this paper, I show how to cleanly handle parametric polymorphism in a bidirectional setting. The key contribution is a bidirectional type system for a subset of ML that supports firstclass (higherrank and even impredicative) polymorphism, and is complete for predicative polymorphism (including MLstyle polymorphism and higherrank polymorphism). The system's power comes from bidirectionality combined with a "greedy" method of finding polymorphic instances inspired by Cardelli's early work on System F_{<:}. This work demonstrates that bidirectionality is a good foundation for traditionally vexing features like firstclass polymorphism. 
Reader’s guideThis paper develops an idea noted as future work in my dissertation ("Be greedy", pp. 236238). (The application to firstclass polymorphism was unexpected.)An earlier draft encompasses this work and several related systems with intersection and union types.

@InProceedings{Dunfield09:polymorphism, author = {Jana Dunfield}, title = {Greedy Bidirectional Polymorphism}, booktitle = {ML Workshop (ML '09)}, pages = {1526}, month = aug, year = 2009, note = {\url{http://www.cs.queensu.ca/~jana/papers/poly/}} }