Qualified types and coherent dictionary elaboration

${\mathrm{QTC}}_0$ is rank-one HM with unary class predicates and monotypes generated by variables, $\mathsf{Int}$, $\mathsf{Bool}$, $\mathsf{String}$, lists, and arrows. Its finite class environment has an acyclic superclass graph, primitive constructor-headed instances whose premises lie at proper type subterms, and a finite superclass-closed effective table ${\mathcal{I}}^{\uparrow }$. For each requested class, all effective result heads are pairwise nonunifiable. Canonical source predicate contexts are variable-headed; constructor-headed requests are decomposed or rejected by the total fixed-order normalizer. Bindings enter the environment only through successful normalization and ambiguity checking; later substitutions act by the partial canonical action $S\star \mathrm{\Gamma }$.

Each primitive instance and reachable superclass contributes one effective clause along a fixed shortest path. Exact local evidence precedes an ordered shortest superclass projection, and local evidence precedes the unique effective global candidate selected by ${\mathsf{pick}}_{\mathcal{C}}$. A projection from local class $K^{\prime }$ to requested superclass $K$ has type $K_D^{\prime }(A)\to K_D(A)$. The total predicate normalizer uses one priority agenda, shares completed instance evidence across requests, and returns an irredundant variable-headed set with the same solvable ground instances as its input; otherwise it returns the first fixed-priority constructor-headed rejection. Resolution terminates, is functional, and constructs well-typed evidence by lemma 11.1. Normalization is deterministic, ground-equivalent to its admitted input, and irredundant by lemma 11.2. The same lemma proves substitution naturality of the returned templates and the factorization $R⊩SP\Rightarrow R⊩SQ$ for a normalization $P\mapsto Q$; these clauses justify composition of $S\star \mathrm{\Gamma }$. The maximal generalization split is lemma 11.3.

Qualified W uses the chapter 3 MGU, canonical predicate transport through $S\star \mathrm{\Gamma }$, conservative let generalization, and the visible ambiguity check. Its exact soundness and principal qualified-scheme boundary are theorem 11.4, theorem 11.5. Principality is conditional on successful canonical-environment actions, normalization, and ambiguity checks. No result is claimed for overlap, ambiguous schemes, higher rank, or defaulting.

The evidence-explicit core distinguishes type, dictionary, and ordinary abstraction. W-indexed elaboration preserves target typing by theorem 11.6; $S^{†}u$ records the corresponding action on target syntax and evidence templates. Forward erasure simulation and existential reverse lifting yield the operational correspondence of theorem 11.7; no injectivity of brace erasure is assumed. Algorithmic coherence is theorem 11.8; the one-step bridge is lemma 13.17. The premise-free annotated ground compatibility slice is proposition 13.21.

${\mathrm{ATS}}_0$ adds saturated associated-synonym applications, equality schemes generated by instances, conversion under entailed equality, and inference that returns pending equalities as well as class constraints and a substitution. The chapter’s local target sketch passes the selected associated type explicitly alongside the class dictionary; the source paper states that an evidence translation is available but omits its rules. Under the imported well-formed-program restrictions, the exact endpoint is soundness of inference, theorem 13.23. Completeness and principality are not imported, and the QTC principality theorem does not extend across this boundary.

The separately displayed COCHIS syntax, deterministic/focused resolution, unambiguity, valid substitutions, and termination hypotheses delimit the imported preservation, soundness, coherence/stability, algorithmic, and safety results in theorem 11.10. Its termination-to-value conclusion uses System F strong normalization in addition to preservation, progress, canonical forms, and operational simulation. No COCHIS principality result is imported.

The Kappa companion recorded in appendix E checks seven printed validation/resolution observations, including a superclass-closed global candidate. Three hidden assertions check exact-local priority, the work bound with three distinct siblings, and rejection of a primitive/effective closure conflict; four semantic mutations guard the corresponding mechanisms. It does not prove any universal inference, elaboration, or coherence theorem.