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.