What are the difference and relation between type checking and type reconstruction? 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?

Thanks.
What are the difference and relation between type checking and type
  reconstruction?


Type reconstruction is a class of problem that involves coming up with a type for a term. For example given a term $\lambda x. x$ can you find the type for this term. Or in general answering the question:

Does a $T$ exist such that the judgement $\Gamma \vdash M : T$ is derivable, where
$M$ is the term and $\Gamma$ is the type environment.

Type checking on the other hand is a process where the question is: 

Given a $T$ and an $M$ can $\Gamma \vdash M : T$ be a valid judgement.


  Does type checking apply only to terms with explicit type annotations which don't contain type variables?


No. You can have a type checking problem that asks whether $\lambda x. x$ has a type $\tau \to \tau$ where $\tau$ is a type variable.


  Does type reconstruction apply only to terms either without explicit type annotations, or with explicit type annotations containing type variables?


As type reconstruction problem is about computing the correct type for a term, if you have an explicit type annotation for a term, you would classify it as a type checking problem.