# Substitution of monomorphic type variables in generalized Hindley–Milner

I am trying to understand the constraints-based Hindley–Milner type inference algorithm described in the Generalizing Hindley-Milner paper. The function $$\text{S}\small{\text{OLVE}}$$ is defined as follows:

$$\begin{array}{l} \text{S}\small{\text{OLVE}} :: Constraints → Substitution \\ \text{S}\small{\text{OLVE}} (\emptyset) = [\ ] \\ \text{S}\small{\text{OLVE}} (\{ \tau_1 \equiv \tau_2 \} \cup C) = \text{S}\small{\text{OLVE}} (\mathcal{S} C) \circ \mathcal{S} \\ \quad \quad \quad \text{where}\ \mathcal{S} = \text{mgu}(\tau_1, \tau_2) \\ \text{S}\small{\text{OLVE}} (\{ \tau_1 \leq_M \tau_2 \} \cup C) = \text{S}\small{\text{OLVE}} (\{ \tau_1 \preceq \text{generalize}(M, \tau_2) \} \cup C) \\ \quad \quad \quad \text{if}\ (\text{freevars}(\tau_2) − M) \cap \text{activevars}(C) = \emptyset \\ \text{S}\small{\text{OLVE}} (\{ \tau \preceq \sigma \} \cup C) = \text{S}\small{\text{OLVE}} (\{\tau \equiv \text{instantiate}(\sigma)\} \cup C) \\ \end{array}$$

Most of this is clear, but where I am confused is around how substitution is defined for the monomorphic set $$M$$. The paper explains that

For implicit instance constraints, we make note of the fact that the substitution also has to be applied to the sets of monomorphic type variables.

$$S(\tau_1 \leq_M \tau_2) =_{def} \mathcal{S} \tau_1 \leq_{\mathcal{S} M} \mathcal{S} \tau_2$$

but I don't find any details of how $$\mathcal{S} M$$ is defined. Based on Example 3, I think we should get something like:

$$\text{S}\small{\text{OLVE}} (\{\tau_4 \leq_{\{ \tau_1 \}} \tau_3, \text{Bool} \rightarrow \tau_3 \equiv \tau_1 \}) \\ = \text{S}\small{\text{OLVE}} (\{\tau_4 \leq_{\{ \tau_3 \}} \tau_3 \}) \circ[\tau_1 := \text{Bool} \rightarrow \tau_3]$$

In this step, unifying $$\text{Bool} \rightarrow \tau_3$$ and $$\tau_1$$ gives a substitution $$\mathcal{S} = [ \tau_1 := \text{Bool} \rightarrow \tau_3 ]$$, and $$M = \{ \tau_1 \}$$, and so apparently $$\mathcal{S} \{ \tau_1 \} = \{ \tau_3 \}$$, but how do we arrive at that? Maybe there is something obvious I have overlooked here.

• Could it be that $\mathcal{S}M$ in $\mathcal{S}\tau_1\leq_{\mathcal{S}M}\mathcal{S}\tau_2$ is not a different relation, but means the set of type variables that the substitution $\mathcal{S}$ brings in scope? – frabala Jun 9 '20 at 22:37