Corrected simple-object row inference

The corrected row fragment has the two-sorted grammar $$\tau ::=\alpha \mid \mathsf{Int}\mid \tau \to \tau \mid \mathrm{\Pi }(r),r::=\rho \mid {\varnothing }_{\mathsf{r}}\mid r[a\leftarrow \tau ],\sigma ::=\mathrm{\forall }\overrightarrow{\alpha }\overrightarrow{\rho }.\tau .$$ Type and row variables, quantification, instantiation, and substitution preserve their two sorts. Rows range over the countable label universe, denote finite partial maps, and update is right biased. The primitive schemes are A finite complete set $\{{\theta }_i\}$ solves an equation family $E$ when every member solves $E$, and every solution factors through some ${\theta }_i$ on the variables of $E$. It need not be a singleton.

The invalid injective step $r_1[a\leftarrow {\tau }_1]=r_2[a\leftarrow {\tau }_2]\Rightarrow r_1=r_2$ is replaced by ${\tau }_1={\tau }_2$ and four row-shape branches. Each branch existentially quantifies one common row $r_0$ without $a$ and whichever field witnesses $u_1,u_2$ it displays: A shared-row equation $\rho =\rho [a_1\leftarrow {\tau }_1]\cdots [a_n\leftarrow {\tau }_n]$ is removed and replaced by atomic obligations $\mathsf{has}(\rho ,a_i,{\tau }_i)$, retaining the last type at a repeated label. The special step does not substitute the update chain for $\rho$.

For Wand’s separately named finite-label concatenation calculus, fix $L=\{a_1,\dots ,a_n\}$, use the descriptor sort $d::=\varphi \mid \mathsf{absent}\mid \mathsf{present}(\tau )$, and write ${\mathrm{\Pi }}_L(d_1,\dots ,d_n)$ for record types. The result descriptor $h_i$ at label $a_i$ satisfies $$(g_i=\mathsf{present}({\tau }_i)\wedge h_i=g_i)\vee (g_i=\mathsf{absent}\wedge h_i=f_i).$$ Disjunctive-normal expansion yields finitely many ordinary unification problems and hence a finite complete set. Rémy’s unitary sorted-row calculus is a different signature and contributes no rule to this section.