Solution (source code)

= Solution

The nowhere-defined partial function is represented by
$$
F=\lambda n.\Omega.
$$
For every Church numeral $c_m$, the term $Fc_m$ reduces to $\Omega$ and hence to no numeral. If $F$ had type $Nat\to Nat$, the strong normalization theorem would make every reduction sequence from $F$ finite, contradicting the visible infinite reduction inside $\Omega$. Thus this partial function is lambda-definable by an untypable term of the required kind.