I agree that the result, while cool, is not readable. An obvious next step would be to demonstrate how the type-checked lambda-heavy implementation can be refactored into something that also makes sense to a human.
> just because the types check out doesn't mean it's free from bugs
That's certainly true in the general case. In fact, the author gives a type-checked-but-wrong example of "we need an Int, so just return zero."
But in some specific cases, as the author writes, "One of those facts we can infer [from a type signature] is often the the only possible implementation." The article demonstrates that "possible" includes "also makes use of all the values available (or else the signature would be simpler)."