Vytiniotis, DimitriosWeirich, Stephanie CPeyton Jones, Simon2023-05-222023-05-222006-09-012006-12-08https://repository.upenn.edu/handle/20.500.14332/6314Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established ideas: unification-based inference, and bidirectional propagation of type annotations. The result is a type system that conservatively extends Hindley-Milner, and yet supports both higher-rank types and impredicativity.impredicativityhigher-rank typestype inferencePresentation