Historic Relationship between Typed Lambda Calculus and Lisp?
First, your friend is wrong about the history of the $\lambda$-calculus. Church created the untyped calculus first, which he intended as a foundation for mathematics. Fairly quickly, it was discovered that the logic derived from this calculus was inconsistent (because non-terminating programs existed).  Eventually Church developed the simple theory of types as well, and many other things besides, but that wasn't the original point of the system.

An excellent overview of the history is found in this paper.

Second, the simply-typed lambda calculus is a quite restrictive language. You need some form of recursive type to write any interesting kind of program in it. Certainly, it would be impossible to write the kinds of programs in McCarthy's original paper with the $\lambda$-calculi based type systems understood in 1958. Cutting-edge programming type systems at that point were the ones found in Fortran and COBOL.