  We present spine-local type inference, a partial type inference system for
inferring omitted type annotations for System F terms based on local type
inference. Local type inference relies on bidirectional inference rules to
propagate type information into and out of adjacent nodes of the AST and
restricts type-argument inference to occur only within a single node.
Spine-local inference relaxes the restriction on type-argument inference by
allowing it to occur only within an {application spine and improves upon it by
using contextual type-argument inference. As our goal is to explore the design
space of local type inference, we show that, relative to other variants,
spine-local type inference enables desirable features such as first-class
curried applications, partial type applications, and the ability to infer types
for some terms not otherwise possible. Our approach enjoys usual properties of
a bidirectional system of having a specification for our inference algorithm
and predictable requirements for typing annotations, and in particular
maintains some the advantages of local type inference such as a relatively
simple implementation and a tendency to produce good-quality error messages
when type inference fails.
