Semi-unification and polymorphic recursion

Arrow terms are $M,N::=\alpha \mid M\to N$. A finite family $\{M_i{⪯}_{\mathsf{su}}{N}_i{\}}_{i=1}^n$ is solved by one outer substitution $S$ and one matcher $R_i$ for each inequality: $$R_i(S(M_i))=S(N_i)(1\le i\le n).$$ Equations may be retained as $S(P)=S(Q)$, or encoded as $(P,P){⪯}_{\mathsf{su}}(P,Q)$ using one fixed binary constructor.

The Milner–Mycroft calculus adds the following rule to the HM rules above:

$\mathrm{\Gamma },x:\sigma {⊢}_{\mathsf{MM}}e:\sigma$

$\mathrm{\Gamma }{⊢}_{\mathsf{MM}}\mathsf{fix}x.e:\sigma$

Its first-order presentation protects in $\overline{\rho }$ one variable monotype for every ambient nongeneric variable, together with the monotypes of enclosing lambda-bound variables:

$A(x)=\tau$$(\tau ,\overline{\rho }){⪯}_{\mathsf{su}}({\tau }^{\prime },\overline{\rho })$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}x:{\tau }^{\prime }$

$A,x:{\tau }_1;(\overline{\rho },{\tau }_1){⊢}_{\mathsf{FO}}e:{\tau }_2$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}\lambda x.e:{\tau }_1\to {\tau }_2$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}{e}_1:{\tau }_2\to \tau$$A;\overline{\rho }{⊢}_{\mathsf{FO}}{e}_2:{\tau }_2$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}{e}_1{e}_2:\tau$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}{e}_1:{\tau }_1$$A,x:{\tau }_1;\overline{\rho }{⊢}_{\mathsf{FO}}{e}_2:{\tau }_2$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}\mathsf{let}x=e_1\mathsf{in}{e}_2:{\tau }_2$

$A,x:{\tau }_x;\overline{\rho }{⊢}_{\mathsf{FO}}e:{\tau }_b$$({\tau }_x,\overline{\rho }){⪯}_{\mathsf{su}}({\tau }_b,\overline{\rho })$$({\tau }_b,\overline{\rho }){⪯}_{\mathsf{su}}({\tau }_x,\overline{\rho })$$({\tau }_b,\overline{\rho }){⪯}_{\mathsf{su}}(\tau ,\overline{\rho })$

$A;\overline{\rho }{⊢}_{\mathsf{FO}}\mathsf{fix}x.e:\tau$

The generator $\mathsf{SEI}$ assigns a fresh root $a_p$ to every syntax occurrence and a disjoint binder monotype $b_p$ to every lambda or fix at $p$. If immediate subterms have roots $q,r$, its five local constraints are Subproblems use the environment and protected-tuple extensions stated in definition 5.11; occurrence variables in distinct subproblems are fresh.