ch:modular-type-classes: ch:modular-type-classes

Problem, observable result, and invariant. Implement the four-constructor running sublanguage of the finite ${\mathsf{MTC}}_0$ resolver, not Kappa’s own implicit search. The command-line result must reproduce the six outputs fixed by the exercise. Before every recursive call, the selected premise is an immediate argument of the requested constructor; before an evidence tree is accepted, an independent traversal checks every node against its realized signature.

Representation. Use separate datatypes for class tags, constructor heads, ground type trees, result patterns, premises, declarations, validation results, evidence trees, and resolution failures. Index declarations operationally by the pair of class and result head. This keeps malformed arities, overlap, missing evidence, and nondecreasing declarations distinct. Encoding all of these as strings would make the validator and resolver share an unverified parser and would obscure the induction on type-tree size.

First complete version. Begin with nullary declarations. Validate that $\mathsf{EqInt}$ is the unique declaration at $(\mathsf{EQ},\mathsf{Int})$, resolve that request, and check that the returned leaf is named EqInt. Only then add constructor declarations. A functor declaration records the immediate argument index selected by each premise. Resolution performs the unique head lookup, recursively resolves premises from left to right, and assembles an explicit evidence tree.

The public fuel bound must cover the represented finite search, not merely the depth of the carrier. One declaration may repeat an immediate-subterm premise many times. If $b$ is the largest premise count and $h$ the carrier-tree size, a deliberately loose geometric bound in $b$ and $h$ covers both tree nodes and premise-list traversal. The corpus includes a forty-premise accepted declaration specifically to reject the tempting linear bound $8h+8$.

Independent evidence checking. Do not trust the resolver’s constructor. Push the root request and returned evidence onto a work list. For each item, look up the declaration again, compare its name and result head, align each child with its premise index, and push the resulting child requests. Reject extra or missing children. Include a deliberately wrong leaf name in the accepted test route; otherwise deleting the name comparison is an observationally silent bug.

Testing and boundary. Run kappa check, kappa test, kappa run, and kappa audit. Replay the three mutations listed in appendix E and restore the accepted source after each one. Exact output checks make wrong classification or evidence visible. These executions test the finite implementation; they do not prove termination, exactness, uniqueness, stability, grounding, or elaboration preservation, and they do not implement the published higher-order systems.