Corrected inference for simple objects

The corrected 1987 fragment has separate type and row variables, finite partial rows, null, selection, and right-biased update. Constraint characterization is lemma 26.2. The counterexample of proposition 26.7 retains the full countable label universe; labels outside the program are what prevent one unconstrained row variable from combining its two valid input families.

Overwrite equality has the sound and complete four-shape cover of lemma 26.3. A shared row variable is converted to atomic presence obligations, whose exact equivalence is lemma 26.5; this is the termination repair, not a cyclic substitution. The corrected lexicographic descent is lemma 26.6.

Wand’s corrigendum supplies effective finite complete sets and decidable typability for the corrected 1987 simple-object system, as stated in theorem 26.8. It supplies no single principal scheme. The pair $\{{\sigma }_0,{\sigma }_1\}$ is complete for the displayed term $W$, not the global solver’s only output shape.

Wand’s 1991 finite-label concatenation calculus has the finite-complete-set theorem theorem 26.10. Rémy’s 1991 sorted extension/selection calculus instead has unitary unification and principal typings. Neither theorem is transferred across these signatures.

The Kappa corpus in artifacts/ch26-corrected-row-unifier/ generates four branches from an input equation, checks a witness of every shape, exercises the $W$ boundary on rows over $\{a,b\}$, and executes the shared-row solver transition. These finite checks prove no completeness or principality theorem.