The theorem of completeness of type inference states the following:
Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$,
In other words, I have some term "t"
whose type is "S" under the assumptions in Gamma,
assuming the constraints "C" is met.
The "x" denotes that we assign the typed variable "x" to this inference.
And sigma is a mapping of type variables to types.
If:
$\sigma(\Gamma)\vdash \sigma(t) : T$, and
When assume a mapping that Gamma has some t whose type is "T". When we apply
sigma to that Gamma, our assumptions are still valid
$dom(\sigma)\cap\mathcal{X} = \emptyset$
We want the domain of the type mappings to be disjoint from our type variables.
then there is some solution:
$(\sigma', T)= T$ and
The tuple (sigma', T) is equivalent to T
$\sigma'\backslash\mathcal{X}=\sigma$
sigma' set minus type variables will be equal to sigma
What I don't fully understand (and the Pierce book is so very opaque) is why the need for the $\sigma'$ to prove that the program is typeable. What exactly is happening in that transition from $\sigma \rightarrow \sigma'$.
Or am I being as dense as I think, and this theorem is able to simultaneously look at the step rules I have defined for my language and resolve the term to a concrete value. And Completeness implicitly uses those rules, thus the need for $\sigma'$