ch:datatype-declarations: ch:datatype-declarations
Problem, result, and invariant. Decide the finite regular declaration grammar without confusing ordinary constructor arguments with function domains inside those arguments, and produce the induction hypothesis for every field that is accepted. Maintain the invariant that a family in the block is accepted exactly at positive sign with open function-domain ancestry, never as an argument of a recursive family application, and never inside an argument of an earlier family; and the invariant that a field mentioning the block never receives the trivial hypothesis.
Representation tradeoff. One representation returns a Boolean and lets the caller name the failure. That is the tempting shortcut, and it is wrong here: the printed diagnostic would then be a constant rather than a result. The companion instead carries Sign, an ancestry flag, and the path travelled so far, and returns either Pass or a Diagnosis holding the first failing path together with the state that rejected it. The traversal stays small enough to inspect completely, and every printed path is computed. A second traversal computes the induction hypothesis each accepted binder yields, so the companion checks both halves of the declaration rule rather than only the half that says yes or no.
First complete version. Define base, block-family application, arrow, pair, and earlier-family nodes. Base nodes pass. A block-family application tests positive sign and the open flag, then rejects if any of its own arguments mentions the block. At an arrow, check the domain with flipped sign and closed ancestry, then check the codomain with the original state. Pair components preserve the state. An earlier family passes at either sign exactly when none of its arguments mentions the block.
The part that is easy to leave out. A verdict is only half the job. Implement the hypothesis type as well, and print it for every binder of an accepted block. A field of type accepted while the eliminator hands that field nothing is wrong in a way no verdict reveals. Recurse on the same derivation the check produced: trivial once the block has left the type, the motive at a direct occurrence, a
Remaining cases. Take two positive fixtures: the mutual tree–forest block, and a branching block whose fields exercise all four hypothesis clauses. Add the four rejections one at a time. The rendered diagnostic reports the last path step together with the sign or the ancestry flag that rejected it, and names a nested occurrence, or one under an earlier family, as such. The finite corpus does not implement universe solving or Tarjan decomposition; those inputs are frozen by the fixture constructor.
Observable result. The accepted program prints two accepted declarations, the four hypothesis types of the second one, four path-specific rejections, and All 7 Chapter 122 corpus cases passed.
Three failing versions. Treat a function domain as a codomain by preserving both sign and open ancestry. The mutation still typechecks, but negative-bad and double-negative both become accepted. Then, separately, reverse the sign at a domain but leave the ancestry flag open. That mutation still rejects negative-bad, so sign tracking alone appears sufficient; it accepts double-negative, where two reversals restore a positive sign under an arrow. That is why the double-negation fixture is in the corpus: the checker carries two pieces of state, and one fixture separates only one of them. Finally, return the trivial hypothesis at a function field. Every verdict is unchanged and only the hypothesis line moves — which is the whole reason to print it.
Acceptance test. Run the four commands in subappendix E.5. Require a passing check, one passing inline test, the exact eight-line semantic transcript, and an empty audit. Replay each mutation, require the inline test to fail on its own fixture, restore the accepted source, and rerun all four commands.
Mathematical boundary. The recursive predicate computes the judgment of definition 122.4 on the represented finite syntax and exposes the boundary used by theorem 122.15. Its run is not a model construction and does not prove normalization, consistency, or correctness of a nested-datatype checker.