Canonical structure

Canonical structure is a typeclass-like mechanism in the Coq proof assistant that enables automatic inference of algebraic and ordering structures for concrete types. Developed as part of the Mathematical Components project, canonical structures allow the Coq type system to automatically resolve which algebraic structure (group, ring, field, module) a given type carries, eliminating the need for explicit instance arguments in proofs and definitions. Unlike typeclasses in languages such as Haskell, canonical structures in Coq are resolved at elaboration time through unification with explicitly declared canonical instances, making the inference process both predictable and inspectable. This predictability is essential for large-scale formalizations where implicit instance resolution must not introduce uncontrolled complexity.

The choice of canonical structures over typeclasses in MathComp was not aesthetic preference. It was architectural discipline: inference should be transparent, not magical.