Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This graph perspective encodes naturally in the typeclass system of theorem provers such as Lean, where nodes can be represented as structures (or records) containing the requisite axioms. This design inevitably needs some form of multiple inheritance; a ring is both a semiring and an abelian group. In the presence of dependently-typed typeclasses that themselves consume typeclasses as type-parameters, such as a vector space typeclass which assumes the presence of an existing additive structure, the implementation details of structure multiple inheritance matter. The type of the outer typeclass is influenced by the path taken to resolve the typeclasses it consumes. Unless all possible paths are considered judgmentally equal, this is a recipe for disaster. This paper provides a concrete explanation of how these situations arise (reduced from real examples in mathlib), compares implementation approaches for multiple inheritance by whether judgmental equality is preserved, and outlines solutions (notably: kernel support for $\eta$-reduction of structures) to the problems discovered.

翻译：抽象代数提供了对象集合可满足的大量属性层级，例如构成阿贝尔群或半环。这些分类可组织成宽广且通常无环的有向图。这种图视角自然地编码在定理证明器（如Lean）的类型类系统中，其中节点可表示为包含必要公理的结构（或记录）。该设计不可避免地需要某种形式的多重继承；一个环既是半环又是阿贝尔群。当存在依赖类型类型类（其自身将类型类作为类型参数消耗）时，例如假设存在加法结构的向量空间类型类，结构多重继承的实现细节至关重要。外部类型类的类型受解析其所消耗类型类时采用的路径影响。除非所有可能路径在判断上被视为相等，否则这将是灾难的根源。本文具体解释了这些情况如何产生（从mathlib中的实际示例精简而来），通过是否保留判断相等性比较了多重继承的实现方法，并概述了针对所发现问题的解决方案（特别是：对结构进行$\eta$-归约的内核支持）。