ch:row-polymorphism: ch:row-polymorphism
Problem and result. Implement the chapter’s mutually recursive constrained inserter and solver. The first accepted run must solve crossing open tails, print every named clause, replay the answer under its residual predicates, and reject empty insertion, an occurs input, and duplicate formation.
Representation. In artifacts/ch7-rows/corpus.kp, represent monotypes, strict row spines, lacks predicates, equations, and sorted substitutions by separate nominal datatypes. Keep row spines for insertion. Use finite label maps only inside contextual equality, so comparison cannot erase the recursive clause that produced a solution.
Stage 1: predicates and formation. Implement deterministic normalization first. An empty-row lacks predicate vanishes, a distinct head is peeled, an equal head yields bottom, and an open tail remains residual. Define strict formation from the normalized set and make the public solver reject an ill-formed input before allocating a fresh tail.
Stage 2: one complete insertion. Give the inserter exactly four branches. I-Var exposes the requested field behind a fresh tail and emits its lacks obligation; I-Empty rejects; I-Match solves the field-type equation; and I-Skip recursively inserts below a distinct head and reattaches that head. Return a substitution, normalized predicates, residual row, fresh supply, step count, and the list of clauses actually executed. At this stage test both an open variable and the empty row.
Stage 3: the mutually recursive solver. Add U-Done, leading identity deletion U-Delete, U-Empty, variable elimination with sorted occurs checks, constructor decomposition, and U-Row. The last clause calls insertion on the right row, applies its substitution to the remaining equations, and puts the left-tail equation first. Every recursive call normalizes predicates and prepends its executed clause to the returned trace. Keep resource exhaustion distinct from logical failure.
Stage 4: the first end-to-end run. Solve the displayed crossing equation from example 4.24. Print the clause trace returned by that solver run: U-Delete -> U-Done with an empty substitution.
Stage 5: remaining acceptance cases. Add explicit tests for the row occurs check, contradictory lacks normalization, and a literal duplicate row. The same corpus then layers the qualified-W and record/variant evaluator cases on the already tested solver; those later cases must not replace the direct solver oracle. Its generalization fixture must keep every predicate in the scheme while also returning each environment-fixed predicate as residual.
A failing version. Apply mutant-accept-empty-insertion.patch only to a disposable copy. It replaces I-Empty’s rejection by a fabricated empty residual. Kappa still accepts the program, but the direct empty-insertion oracle prints FAIL insertion into empty is rejected.
Acceptance test. Run check, test, run, and audit. Require the exact five-clause trace, successful equation replay and factorization, all eleven PASS lines, the summary All 11 Chapter 7 corpus cases passed., and an empty audit. Require the accepted source hash and mutant hash recorded in appendix E; the check-clean mutant must fail its test oracle.
Mathematical boundary. The run executes every insertion branch and the crossing path through the solver. Finite tests do not prove termination, factorization, principality, evidence coherence, qualified-W correctness, or source safety.