¶Gradual types
a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines
[Siek2015]
[Siek2015] “Refined Criteria for Gradual Typing”
A good overview paper of Castagna et al's work:
[Castagna2022] “Programming with Union, Intersection, and Negation Types”
Two papers describing type variables and specialization inference in more detail: