Bottom up Hindley-Milner type inference: Applying a substitution to an implicit constraint

Question

I am trying to implement the 'Bottom up' type inference algorithm which can be found in Generalizing Hindley-Milner Type Inference Algorithms

Page 6 explains how an implicit constraint is

t1 should be an instance of the type scheme that is obtained by generalizing type t2 with respect to the set of monomorphic type variables M

However, on page 9, during the explanation of how to apply a substitution to an implicit constraints, I am told to apply a substitution to this set of monomorphic type variables. The problem is that if i have the substitution [t1 := t2 -> t3] then M is no longer a set of type variables.

What am I misunderstanding here?

Answer 1

I got in touch with the authors of the paper and when they told me the answer I did kick myself a bit:

The substitution function has the form S : Substitution -> a -> a so when applying this to a set of type variables then the result will be a set of type variables.

So when applying [t1 := t2 -> t3] instead of replacing with t2 -> t3 I replace with ftv(t2 -> t3) aka [t2, t3] (where ftv is a function to get the free type variables in a type).

Answer 2

If the set of monomorphic type variables is encoded as a set of monotypes (as opposed to bare variable names) then freevars in freevars(M) on page 9 doesn't need (yet another) overloading, ditto the application of substitutions.

In this respect the typing of SOLVE seems slightly broken: in the definition of activevars, freevars is applied to M, while in SOLVE freevars is not applied to M ("freevars(t2) - M"), and M can't possibly contain type schemes, i.e. have bound variables. So is M a set a free variables names (no need to apply freevars before a set operation with other freevars(t)) or is it a set of monotypes (need to apply freevars)?