Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism

Jana Dunfield, Neelakantan R. Krishnaswami

Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference,…