Strict data rows and qualified row inference

The two-sorted grammar is A lacks predicate is $\rho \mathrm{\backslash }\ell$. Normalize it by Predicate contexts are normalized finite sets of residual variable predicates. Entailment and strict row formation are

$\xi \mathrm{\backslash }\ell \in P$

$P⊩\xi \mathrm{\backslash }\ell$

$P⊩{ϵ}_{\rho }\mathrm{\backslash }\ell$

$P⊩\rho \mathrm{\backslash }\ell$$m\ne \ell$

$P⊩\{m:\tau \mid \rho \}\mathrm{\backslash }\ell$

$P⊢\xi \mathsf{row}$

$P⊢{ϵ}_{\rho }\mathsf{row}$

$P⊢\rho \mathsf{row}$$P⊢\tau \mathsf{type}$$P⊩\rho \mathrm{\backslash }\ell$

$P⊢\{\ell :\tau \mid \rho \}\mathsf{row}$

Type formation is

$P⊢\tau \mathsf{type}$$P⊢\upsilon \mathsf{type}$

$P⊢\tau \to \upsilon \mathsf{type}$

$P⊢\rho \mathsf{row}$

$P⊢\mathsf{Rec}(\rho )\mathsf{type}$

$P⊢\rho \mathsf{row}$

$P⊢\mathsf{Var}(\rho )\mathsf{type}$

The type-variable and three base-type cases are axioms. Row equality exchanges adjacent distinct labels only; $a{\equiv }_P{a}^{\prime }$ additionally requires both sides formed under $P$. An admissible substitution $S:P\to Q$ is sorted, has $Q$-formed images, normalizes $P[S]$, and satisfies $Q⊩\mathsf{nf}(P[S])$.

Qualified schemes are $$\chi ::=P\Rightarrow \tau ,\sigma ::=\mathrm{\forall }\overline{\alpha }\overline{\xi }.P\Rightarrow \tau .$$ For $$X=\mathrm{ftv}(P,\tau )\setminus \mathrm{ftv}(\mathrm{\Gamma }),P^{\mathsf{g}}=\{p\in P\mid \mathrm{ftv}(p)\subseteq X\},P^{\mathsf{r}}=P\setminus P^{\mathsf{g}},$$ put ${\mathrm{Gen}}_{\mathrm{\Gamma }}(P\Rightarrow \tau )=\mathrm{\forall }X.P\Rightarrow \tau$. Qualified typing is

$\mathrm{\Gamma }(x)=\mathrm{\forall }\overline{\alpha }\overline{\xi }.Q\Rightarrow {\tau }_0$$P⊩\mathsf{nf}(Q[T])$$P⊢{\tau }_0[T]\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{q}x:P\Rightarrow {\tau }_0[T]$

$c:\mathrm{\forall }\overline{\alpha }\overline{\xi }.Q\Rightarrow {\tau }_0\in {\mathrm{\Sigma }}_0$$P⊩\mathsf{nf}(Q[T])$$P⊢{\tau }_0[T]\mathsf{type}$

$\mathrm{\Gamma }{⊢}_{q}c:P\Rightarrow {\tau }_0[T]$

$\mathrm{\Gamma },x:{\tau }_1{⊢}_{q}e:P\Rightarrow {\tau }_2$

$\mathrm{\Gamma }{⊢}_q\lambda x.e:P\Rightarrow {\tau }_1\to {\tau }_2$

$\mathrm{\Gamma }{⊢}_q{e}_1:P_1\Rightarrow {\tau }_1\to {\tau }_2$$\mathrm{\Gamma }{⊢}_q{e}_2:P_2\Rightarrow {\tau }_1$$\mathsf{nf}(P_1\cup P_2)=P$

$\mathrm{\Gamma }{⊢}_q{e}_1{e}_2:P\Rightarrow {\tau }_2$

$\mathrm{\Gamma }{⊢}_q{e}_1:P_1\Rightarrow {\tau }_1$$\mathrm{\Gamma },x:{\mathrm{Gen}}_{\mathrm{\Gamma }}(P_1\Rightarrow {\tau }_1){⊢}_q{e}_2:P_2\Rightarrow {\tau }_2$$\mathsf{nf}(P_1^{\mathsf{r}}\cup P_2)=P$

$\mathrm{\Gamma }{⊢}_q\mathsf{let}x=e_1\mathsf{in}{e}_2:P\Rightarrow {\tau }_2$

$\mathrm{\Gamma }{⊢}_{q}e:P\Rightarrow \tau$$\tau {\equiv }_P{\tau }^{\prime }$

$\mathrm{\Gamma }{⊢}_{q}e:P\Rightarrow {\tau }^{\prime }$

The saturated record and variant terms add Their complete typing rules are

$\mathrm{\Gamma }{⊢}_q\{\}:\varnothing \Rightarrow \mathsf{Rec}({ϵ}_{\rho })$

$\mathrm{\Gamma }{⊢}_{q}r:P\Rightarrow \mathsf{Rec}(\{\ell :\tau \mid \rho \})$

$\mathrm{\Gamma }{⊢}_{q}r.\ell :P\Rightarrow \tau$

$\mathrm{\Gamma }{⊢}_{q}r:P\Rightarrow \mathsf{Rec}(\{\ell :\tau \mid \rho \})$

$\mathrm{\Gamma }{⊢}_{q}r-\ell :P\Rightarrow \mathsf{Rec}(\rho )$

$\mathrm{\Gamma }{⊢}_{q}a:P_1\Rightarrow \tau$$\mathrm{\Gamma }{⊢}_{q}r:P_2\Rightarrow \mathsf{Rec}(\rho )$$\mathsf{nf}(P_1\cup P_2\cup \{\rho \mathrm{\backslash }\ell \})=P$

$\mathrm{\Gamma }{⊢}_q\{\ell =a\mid r\}:P\Rightarrow \mathsf{Rec}(\{\ell :\tau \mid \rho \})$

$\mathrm{\Gamma }{⊢}_{q}a:P_0\Rightarrow \tau$$\mathsf{nf}(P_0\cup \{\rho \mathrm{\backslash }\ell \})=P$

$\mathrm{\Gamma }{⊢}_q⟨\ell =a⟩:P\Rightarrow \mathsf{Var}(\{\ell :\tau \mid \rho \})$

$\mathrm{\Gamma }{⊢}_{q}u:P_0\Rightarrow \mathsf{Var}(\rho )$$\mathsf{nf}(P_0\cup \{\rho \mathrm{\backslash }\ell \})=P$

$\mathrm{\Gamma }{⊢}_q{\mathsf{embed}}_{\ell }u:P\Rightarrow \mathsf{Var}(\{\ell :\tau \mid \rho \})$

$\mathrm{\Gamma }{⊢}_{q}u:P_0\Rightarrow \mathsf{Var}(\{\ell :\tau \mid \rho \})$$\mathrm{\Gamma },x:\tau {⊢}_q{e}_1:P_1\Rightarrow \upsilon$$\mathrm{\Gamma },y:\mathsf{Var}(\rho ){⊢}_q{e}_2:P_2\Rightarrow \upsilon$$\mathsf{nf}(P_0\cup P_1\cup P_2)=P$

$\mathrm{\Gamma }{⊢}_q{\mathsf{case}}_{\ell }u\mathsf{of}\{⟨\ell =x⟩\mapsto e_1;y\mapsto e_2\}:P\Rightarrow \upsilon$

Values and the complete source evaluation contexts are Besides beta and let, the primitive roots are together with matching case reduction to $e_1[v/x]$ and unequal-tag case reduction to $e_2[⟨m=v⟩/y]$. Compatibility is $E⟨e⟩⟶E⟨e^{\prime }⟩$.

Constrained insertion and solving have judgments $${\mathsf{insert}}_P(\ell :\tau ,\rho )=(I,Q,{\rho }^{-}),\mathsf{solve}(P;E)=(U,Q),$$ and are mutually recursive. Insertion has four clauses: an open tail $\xi$ is replaced by $\{\ell :\tau \mid \zeta \}$, adding $\zeta \mathrm{\backslash }\ell$; empty fails; a matching head solves its field-type equation; and a distinct head recurses on the tail and is reattached. Every fresh tail is global to the run.

The solver normalizes $P$ before every call, uses the empty and reflexive clauses first, then sorted variable elimination with occurs check, orientation, rigid type decomposition, empty-row cases, and finally row-extension exposure. The last clause is exactly $$\frac{{\mathsf{insert}}_P(\ell :\tau ,q)=(I,P_1,q^{-})\mathsf{solve}(P_1;(\rho [I]\doteq q^{-},E[I]))=(V,Q)}{\mathsf{solve}(P;(\{\ell :\tau \mid \rho \}\doteq q,E))=(I;V,Q)}.$$ These clauses are tried in this order, and rigid subequations are prepended left to right. A variable–variable equation eliminates the left variable; the symmetric orientation is used only when the left side is not a variable.

Qualified W returns ${\mathsf{W}}_r(\mathrm{\Gamma },e)=(P,S,\tau )$. Its variable, constant, lambda, application, and let clauses are the HM clauses with qualified instantiation, normalized predicate unions, solver calls, and the residual $P_1^{\mathsf{r}}$ retained at let. The exact new clauses are: empty returns $(\varnothing ,\mathrm{id},\mathsf{Rec}({ϵ}_{\rho }))$; extension infers payload then record and solves the record shape with a fresh tail lacking $\ell$; selection and restriction solve against $\mathsf{Rec}(\{\ell :\alpha \mid \xi \})$; injection introduces a fresh tail and its lacks predicate; embedding solves the old variant row and leaves the new payload type fresh; case solves the scrutinee shape, infers the matching branch, then the residual branch under all prior substitutions, and finally solves the branch-result equation. Its returned case substitution is $S_0;U_0;S_1;S_2;V$, in that order. These are precisely the clauses of definition 4.29; no effect-row equation is admitted here.

With a fixed total label order, lacks evidence is

$d_{\xi ,\ell }:\xi \mathrm{\backslash }\ell \in \mathrm{\Delta }$

$\mathrm{\Delta }⊢d_{\xi ,\ell }:\xi \mathrm{\backslash }\ell$

$\mathrm{\Delta }⊢0:{ϵ}_{\rho }\mathrm{\backslash }\ell$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$

$\mathrm{\Delta }⊢d:\{m:\tau \mid \rho \}\mathrm{\backslash }\ell$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$

$\mathrm{\Delta }⊢d+1:\{m:\tau \mid \rho \}\mathrm{\backslash }\ell$

The named syntax translation on row types is Let $\mathsf{canTy}$ recursively sort every strict row index. Target type conversion is explicit:

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:\theta$$\mathsf{canTy}(\theta )=\mathsf{canTy}({\theta }^{\prime })$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:{\theta }^{\prime }$

Target schemes are $\mathrm{\forall }X.\mathsf{Off}(P)\Rightarrow \theta$, with explicit static instantiation and evidence abstraction:

$\mathrm{\Gamma }(x)=\sigma$

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:\sigma$

$c:\theta \in {\mathrm{\Sigma }}_0$

$\mathrm{\Delta };\mathrm{\Gamma }⊢c:\theta$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:\mathrm{\forall }X.\mathsf{Off}(P)\Rightarrow \theta$$T\text{sorted and formed}$$\mathrm{\Delta }⊢\overline{d}:\mathsf{Off}(P[T])$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t[T]\overline{d}:\theta [T]$

$\mathrm{\Delta },\overline{d}:\mathsf{Off}(P);\mathrm{\Gamma }⊢t:\theta$$X\cap \mathrm{ftv}(\mathrm{\Delta },\mathrm{\Gamma })=\varnothing$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathrm{\Lambda }X.\lambda \overline{d}.t:\mathrm{\forall }X.\mathsf{Off}(P)\Rightarrow \theta$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t_1:\sigma$$\mathrm{\Delta };\mathrm{\Gamma },x:\sigma ⊢t_2:\theta$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{let}x=t_1\mathsf{in}{t}_2:\theta$

Writing a monotype as the corresponding empty scheme, the ordinary target rules are

$\mathrm{\Gamma }(x)=\theta$

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:\theta$

$c:\theta \in {\mathrm{\Sigma }}_0$

$\mathrm{\Delta };\mathrm{\Gamma }⊢c:\theta$

$\mathrm{\Delta };\mathrm{\Gamma },x:\theta ⊢t:\upsilon$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x.t:\theta \to \upsilon$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:\theta \to \upsilon$$\mathrm{\Delta };\mathrm{\Gamma }⊢u:\theta$

$\mathrm{\Delta };\mathrm{\Gamma }⊢tu:\upsilon$

The nullary array rule and six saturated evidence-carrying data rules are

$\mathrm{\Delta };\mathrm{\Gamma }⊢[]:\mathsf{Array}({ϵ}_{\rho })$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$$\mathrm{\Delta };\mathrm{\Gamma }⊢r:\mathsf{Array}(\{\ell :\alpha \mid \rho \})$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{lookup}dr:\alpha$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$$\mathrm{\Delta };\mathrm{\Gamma }⊢r:\mathsf{Array}(\{\ell :\alpha \mid \rho \})$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{delete}dr:\mathsf{Array}(\rho )$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$$\mathrm{\Delta };\mathrm{\Gamma }⊢a:\alpha$$\mathrm{\Delta };\mathrm{\Gamma }⊢r:\mathsf{Array}(\rho )$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{insert}dar:\mathsf{Array}(\{\ell :\alpha \mid \rho \})$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$$\mathrm{\Delta };\mathrm{\Gamma }⊢a:\alpha$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{tag}da:\mathsf{Sum}(\{\ell :\alpha \mid \rho \})$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$$\mathrm{\Delta };\mathrm{\Gamma }⊢u:\mathsf{Sum}(\rho )$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{widen}du:\mathsf{Sum}(\{\ell :\alpha \mid \rho \})$

$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$$\mathrm{\Delta };\mathrm{\Gamma }⊢u:\mathsf{Sum}(\{\ell :\alpha \mid \rho \})$$\mathrm{\Delta };\mathrm{\Gamma }⊢f:\alpha \to \beta$$\mathrm{\Delta };\mathrm{\Gamma }⊢g:\mathsf{Sum}(\rho )\to \beta$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{split}dufg:\beta$

The target reductions use evidence as zero-based array/tag offsets and are the lookup, delete, insert, tag, widen, and split roots displayed in definition 7.51. Evidence-passing compilation accepts a principal result only when $\mathrm{ftv}(P)\subseteq \mathrm{ftv}(\mathrm{\Gamma },\tau )$; this unambiguity side condition is part of the compiler interface, not the source typing judgment.