Completeness of Constraint Typing (type inference) question regarding $\sigma'$

Question

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'$

Answer 1

Assuming that this is from Chapter 22 of Pierce's book, what's going on is that Pierce had to strengthen the statement of the theorem slightly to deal with all the fresh constraint variables tracked in $\mathcal{X}$.

The naive statement of completeness would be is that

If $\Gamma \vdash t:S|_{\mathcal{X}}C$ and $(\sigma, T)$ is a solution for $(\Gamma, t)$, then $(\sigma, T)$ is a solution for $(\Gamma, t, S, C)$.

Basically, this says that if $(\sigma, T)$ is a solution to the type inference problem, then it will be a solution of the generated constraints $C$. However, the inference rules in Figure 22-1 sometimes will create some new contraint variables (for example, rule CT-App), all of which are recorded in $\mathcal{X}$.

If the domain of $\sigma$ overlapped with the new variables constraint generation introduced, then you're in trouble, because now we have the possibility of inconsistencies between $\sigma$ and the constraints in $C$. So, instead Pierce proves that:

If $\Gamma \vdash t:S|_{\mathcal{X}}C$ and $(\sigma, T)$ is a solution for $(\Gamma, t)$ and $\mathrm{dom}(\sigma) \cap \mathcal{X} = \emptyset$, then there exists a $\sigma'$ such that $(\sigma', T)$ is a solution for $(\Gamma, t, S, C)$ and $\sigma'/\mathcal{X} = \sigma$.

So he says that if $(\sigma, T)$ is a solution for $(\Gamma, t)$ that doesn't overlap with $\mathcal{X}$, then there is a solution $(\sigma', T)$ for $(\Gamma, t, S, C)$ such that $\sigma'$ is an extension of $\sigma$ to cover the variables in $\mathcal{X}$.