We intoduce System IF, for implicit System F, in which many type applications can be made implicit. It supports decidable type checking and strong normalisation. System IF constitutes a first foray into a new area in the design space of typed lambda calculi, that is interesting in its own right and may prove useful in practice.
