  Gradually typed languages allow programmers to mix statically and dynamically
typed code, enabling them to incrementally reap the benefits of static typing
as they add type annotations to their code. However, this type migration
process is typically a manual effort with limited tool support. This paper
examines the problem of \emph{automated type migration}: given a dynamic
program, infer additional or improved type annotations.
  Existing type migration algorithms prioritize different goals, such as
maximizing type precision, maintaining compatibility with unmigrated code, and
preserving the semantics of the original program. We argue that the type
migration problem involves fundamental compromises: optimizing for a single
goal often comes at the expense of others. Ideally, a type migration tool would
flexibly accommodate a range of user priorities.
  We present TypeWhich, a new approach to automated type migration for the
gradually-typed lambda calculus with some extensions. Unlike prior work, which
relies on custom solvers, TypeWhich produces constraints for an off-the-shelf
MaxSMT solver. This allows us to easily express objectives, such as minimizing
the number of necessary syntactic coercions, and constraining the type of the
migration to be compatible with unmigrated code.
  We present the first comprehensive evaluation of GTLC type migration
algorithms, and compare TypeWhich to four other tools from the literature. Our
evaluation uses prior benchmarks, and a new set of ``challenge problems.''
Moreover, we design a new evaluation methodology that highlights the subtleties
of gradual type migration. In addition, we apply TypeWhich to a suite of
benchmarks for Grift, a programming language based on the GTLC. TypeWhich is
able to reconstruct all human-written annotations on all but one program.
