The new type checker, based on a constraint-generating but bidirectional approach, can type a lot more programs than the older, Algorithm W-derived checker. As an example, consider the following definition. […]

OCaml (which uses rather standard Hindley-Milner-Damas type inference) can type-check this definition just fine.

Certainly, but still I am a bit confused by this blog post that seems to imply that this function is not typable with traditional HM algorithms for prenex polymorphism, while it does seem to work just fine. Is there an error in the blog post itself, and the author meant to insert an example making essential use of higher-order polymorphism? Or was there a bug in the previous type-checker that could have been fixed while keeping the same inference specification, instead of moving to higher-rank bidirectional algorithms?

Perhaps I didn’t make this clear enough, but I did not mean to imply this was a fault with Algorithm W in general, but rather a fault of my implementation of HM inference.

Or was there a bug in the previous type-checker that could have been fixed while keeping the same inference specification, instead of moving to higher-rank bidirectional algorithms?

Indeed, but I chose to do both at once. (I had previously tried to add rank-N polymorphism to the old type checker before figuring out it was broken beyond saving)

Edit: Also, I only realize now but: when you write “ε-contraction” (epsilon-contraction), you mean “η-contraction” (eta-contraction), as a transformation from (fun x -> t x) to just (t), right?

OCaml (which uses rather standard Hindley-Milner-Damas type inference) can type-check this definition just fine.

hindley-milner or bust

That isn’t a rank-n type. Things become much trickier once you start nesting foralls, which is where bidirectional type checking shines.

Certainly, but still I am a bit confused by this blog post that seems to imply that this function is not typable with traditional HM algorithms for prenex polymorphism, while it does seem to work just fine. Is there an error in the blog post itself, and the author meant to insert an example making essential use of higher-order polymorphism? Or was there a bug in the previous type-checker that could have been fixed while keeping the same inference specification, instead of moving to higher-rank bidirectional algorithms?

Perhaps I didn’t make this clear enough, but I did not mean to imply this was a fault with Algorithm W in general, but rather a fault of my implementation of HM inference.

Indeed, but I chose to do both at once. (I had previously tried to add rank-N polymorphism to the old type checker before figuring out it was broken beyond saving)

I see, thanks for the clarification!

Edit: Also, I only realize now but: when you write “ε-contraction” (epsilon-contraction), you mean “η-contraction” (eta-contraction), as a transformation from

`(fun x -> t x)`

to just`(t)`

, right?Er.. Yes, thanks. Greek was never my forte, maybe I should stick to the Latin alphabet. (Edit: fixed.)