Modular type classes and implicit modules

${\mathsf{MTC}}_0$ has finite constructor trees, atomic class signatures with a distinguished carrier, named paths and total constructor-headed module functors, explicit adoption, head-directed evidence resolution, and the displayed equality/show elaboration fragment. Premises select immediate constructor arguments and environments are nominally nonoverlapping.

Under those hypotheses, resolution terminates and is sound, complete, unique, and stable under admissible extension; inserted evidence is well typed, elaboration preserves source typing, and solvable residual constraints ground to closed evidence. These are theorems of the finite chapter calculus, not of full OCaml or arbitrary type-class search.

Figures 22–23 of the extended presentation of [DHCK07] prove mutual algorithmic-to-declarative inference soundness under validity, future-world, instantiation, and canonical residual-solution hypotheses, plus a ground top-level consequence. The imported theorem is neither completeness nor a global coherence theorem.

The design of [WBY15] elaborates omitted module parameters by constrained module-expression search with decrease and uniqueness checks. The chapter transfers its concrete design and pinned prototype specimen, not an unpublished whole-OCaml coherence theorem.

For [OBL^+18], the chapter records System F type preservation (Theorem 3.1), monomorphic well-scoped uniqueness (Propositions 3.6–3.7), synth/check procedure soundness (Proposition 3.8), and the explicitly conjectural semi-completeness result (Conjecture 3.9).

The Kappa companion in artifacts/ch16-mtc-resolution/ executes the finite resolver, evidence checker, error classifications, and three semantic mutation gates. It does not mechanize the published higher-order module or SI metatheory.