+This is not because there is any difficulty typing what the functions
+involved do "from the outside": for instance, the predecessor function
+is a function from numbers to numbers, or τ -> τ, where τ
+is our type for Church numbers (i.e., (σ -> σ) -> σ
+-> σ). (Though this type will only be correct if we decide that
+the predecessor of zero should be a number, perhaps zero.)
+
+Rather, the problem is that the definition of the function requires
+subterms that can't be simply-typed. We'll illustrate with our
+implementation of the predecessor, sightly modified in inessential
+ways to suit present purposes:
+
+ let zero = \s z. z in
+ let snd = \a b. b in
+ let pair = \a b. \v. v a b in
+ let succ = \n s z. s (n s z) in
+ let collect = \p. p (\a b. pair (succ a) a)
+ let pred = \n. n collect (pair zero zero) snd in
+
+Let's see how far we can get typing these terms. `zero` is the Church
+encoding of zero. Using `N` as the type for Church numbers (i.e.,
+<code>N == (σ -> σ) -> σ -> σ</code> for some
+σ, `zero` has type `N`. `snd` takes two numbers, and returns
+the second, so `snd` has type `N -> N -> N`. Then the type of `pair`
+is `N -> N -> (type(snd)) -> N`, that is, `N -> N -> (N -> N -> N) ->
+N`. Likewise, `succ` has type `N -> N`, and `collect` has type `pair
+-> pair`, where `pair` is the type of an ordered pair of numbers,
+namely, <code>pair ≡ (N -> N -> N) -> N</code>. So far so good.
+
+The problem is the way in which `pred` puts these parts together. In
+particular, `pred` applies its argument, the number `n`, to the
+`collect` function. Since `n` is a number, its type is `(σ ->
+σ) -> σ -> σ`. This means that the type of
+`collect` has to match `σ -> σ`. But we concluded above
+that the type of `collect` also had to be `pair -> pair`. Putting
+these constraints together, it appears that `σ` must be the type
+of a pair of numbers. But we already decided that the type of a pair
+of numbers is `(N -> N -> N) -> N`. Here's the difficulty: `N` is
+shorthand for a type involving `σ`. If `σ` turns out to
+depend on `N`, and `N` depends in turn on `σ`, then `σ` is a proper
+subtype of itself, which is not allowed in the simply-typed lambda
+calculus.
+
+The way we got here is that the pred function relies on the right-fold
+structure of the Church numbers to recursively walk down the spine of
+its argument. In order to do that, the argument number had to take
+the operation in question as its first argument. And the operation
+required in order to build up the predecessor must be the sort of
+operation that manipulates numbers, and the infinite regress is
+established.
+
+Now, of course, this is only one of myriad possible implementations of
+the predecessor function in the lambda calculus. Could one of them
+possibly be simply-typeable? It turns out that this can't be done.
+See the works cited by Oleg for details.