Possibly we just a have a different idea of what a lambda calculus is: I was thinking of Church's untyped lambda calculus, which is a much weirder beast than System FC.
Even if you restrict lambda calculus to mean untyped lambda calculus, it's common practice to discard the types once type-checking has completed and continue the compilation without them.
