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 these paths are considered judgmentally equal, this is a recipe for disaster. This paper provide 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 to the problems discovered.

翻译：抽象代数提供了一个庞大的性质层次结构，用于描述一组对象可满足的各类特性，例如构成阿贝尔群或半环。这些分类可组织成一张宽广且通常无环的有向图。这种图结构自然地编码在定理证明器（如Lean）的型类系统中，其中节点可表示为包含必要公理的结构（或记录）。这种设计不可避免地需要某种形式的多重继承：一个环既是半环又是阿贝尔群。当存在依赖类型的型类（这些型类本身将其他型类作为类型参数消耗）时，例如向量空间型类假定存在一个加法结构，结构多重继承的实现细节便至关重要。外层型类的类型会受到解析其所消耗型类时路径的影响。除非所有这些路径在判断相等性上被视为等价，否则这将是一场灾难。本文具体解释了这些情况是如何出现的（根据mathlib中的实际示例简化而来），通过判断相等性是否保留来比较多重继承的实现方法，并概述了所发现问题的解决方案。