Dunfield-Krishnaswami handles higher ranked polymorphism but is probably most famous for just being a very nice presentation of bidirectional typechecking. Algo

Dunfield-Krishnaswami handles higher ranked polymorphism but is probably most famous for just being a very nice presentation of bidirectional typechecking. Algorithm W (Hindley-Milner) is only able to infer first-order polymorphism occurring at generalization points (usually "let"s).