In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term.  In Church-style, they are intrinsic to the term and are truly there.  Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.