Type inference is essential for programming languages, yet complete
and global inference quickly becomes undecidable in the presence of rich type
systems like System~F. Pierce and Turner proposed local type
inference (LTI) as a scalable,
partially annotated alternative by relying on information local to
applications. While LTI has been widely adopted in practice, there
are significant gaps between theory and practice, with its theory
being underdeveloped and specifications for LTI being complex and restrictive.

We propose \emph{Local Contextual Type Inference}, a principled
redesign of LTI grounded in contextual typing—a recent formalism
which captures type information flow. We present \emph{Contextual
System~F} (Fc), a variant of System~F with implicit and
first-class polymorphism. We formalize Fc using a declarative
type system, prove soundness, completeness, and
decidability, and introduce matching subtyping as a bridge between
declarative and algorithmic inference. This work offers the first
mechanized treatment of LTI, while at the same time removing
important practical restrictions and also demonstrating the power of
contextual typing in designing robust, extensible and simple to
implement type inference algorithms.