In Types and Programming Languages by Pierce,
ML-style let-polymorphism was ﬁrst described by Milner (1978). A num- ber of type reconstruction algorithms have been proposed, notably the clas- sic Algorithm W (Damas and Milner) of Damas and Milner (1982; also see Lee and Yi, 1998). The main diﬀerence between Algorithm W and the pre- sentation in this chapter is that the former is specialized for “pure type reconstruction”—assigning principal types to completely untyped lambda- terms—while we have mixed type checking and type reconstruction, permit- ting terms to include explicit type annotations that may, but need not, contain variables. This makes our technical presentation a bit more involved (espe- cially the proof of completeness, Theorem 22.3.7, where we must be careful to keep the programmer’s type variables separate from the ones introduced by the constraint generation rules), but it meshes better with the style of the other chapters.
What are the difference and relation between type checking and type reconstruction?
Does type checking apply only to terms with explicit type annotations which don't contain type variables?
Does type reconstruction apply only to terms either without explicit type annotations, or with explicit type annotations containing type variables?