Great paper: Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism

I start discussing this great paper by Dunfield and Krishnaswami, about how to extend a particular approach to type inference to handle polymorphism.