ch:type-classes: ch:type-classes
Problem, result, and invariant. Implement the finite EqList(EqFromOrd(OrdInt)), project EqFromOrd(dOrd), construct a projected global superclass instance, reject an overlapping effective table, reject the nondecreasing constructor self-premise, and report the missing Show Bool request. The exact acceptance oracle is seven PASS lines followed by All 7 Chapter 13 corpus cases passed.
Maintain three invariants. A public resolution call closes and validates the whole effective table before search. Exact local evidence has priority over a superclass projection, and all local evidence has priority over the unique global effective candidate. For each requested class, closed effective heads are pairwise nonunifiable. Each accepted instance premise requests an immediate proper subterm of the result type; the work budget also pays for every sibling in the premise list.
Representation. Use separate datatypes for class tags, type heads, full type trees, result patterns, premises, declarations, local evidence, evidence trees, and failure causes. Constructor heads carry their arity, while a premise stores the immediate argument index it requests. This separation lets validation reject overlap, malformed arity, and nondecreasing premises before resolution. Representing declarations as strings would be shorter, but the search would then share an unchecked parser with its validator and the proper-subterm measure would be invisible.
First complete version. Begin with the premise-free Ord Int declaration. Superclass closure derives the effective Eq Int candidate whose builder is EqFromOrd applied to OrdInt. Next add Eq (List a) with one ArgumentPremise Eq 0. One-way head matching selects that unique effective declaration; the premise resolver selects the list element and recursively builds Ord a => Ord (List a) along Ord -> Eq; its projected effective clause supplies the open-substitution case used by the chapter’s normalization proof.
Add local evidence in two passes. The exact pass scans the whole list before the superclass pass begins. The latter may turn a local Ord Int dictionary into EqFromOrd(dOrd). This order is deliberate: a nearer superclass candidate must not defeat an exact Eq Int entry later in the list. Only after both local passes fail may global effective lookup run. Reject a primitive Eq Int declaration together with Ord Int, since closure makes their Eq Int result heads overlap; never resolve this conflict by declaration order.
Validation and the work bound. Validate each declaration against all previously accepted heads. Duplicate class/head pairs are ambiguous. A variable-headed result and a SelfPremise are nondecreasing and therefore cyclic at this fragment. For an argument premise, check that its index is below the result constructor’s arity.
Let Eq a, Ord a, and Show a; a bound based only on type depth fails this case despite the valid table.
Keep raw recursive helpers private. Export the input/output datatypes and one resolve function that always validates before calculating the bound and searching.
A failing version. The tempting local resolver returns the first superclass projection it sees. On a list containing dOrd before the exact dEq, it returns EqFromOrd(dOrd) instead of dEq. The exact-before-super assertion exposes this error. A second tempting implementation allocates a fixed amount of fuel per type layer; the hidden three-sibling declaration exhausts it.
Acceptance test and boundary. Run the four commands recorded in appendix E. Require the seven printed cases, the hidden priority, sibling-bound, and closure-conflict assertions, an empty audit, and rejection of all four documented mutations. The program illustrates the mechanisms of lemma 11.1, lemma 11.2; it does not prove those lemmas, qualified inference principality, dictionary elaboration, operational correspondence, or coherence.