Type substitution ($S$)

A type substitution replaces type variables by type expressions consistently. For example, $S=\{\alpha \mapsto \mathrm{int}\}$ gives $S(\alpha \to \alpha )=\mathrm{int}\to \mathrm{int}$. Applying a type substitution to a type scheme must respect its bound type variables; separate instantiation first replaces those bound placeholders by fresh ones.