Lean4
/-- Diamond inheritance cannot depend on `outParam`s in the following circumstances:
* there are three classes `Top`, `Middle`, `Bottom`
* all of these classes have a parameter `(α : outParam _)`
* all of these classes have an instance parameter `[Root α]` that depends on this `outParam`
* the `Root` class has two child classes: `Left` and `Right`, these are siblings in the hierarchy
* the instance `Bottom.toMiddle` takes a `[Left α]` parameter
* the instance `Middle.toTop` takes a `[Right α]` parameter
* there is a `Leaf` class that inherits from both `Left` and `Right`.
In that case, given instances `Bottom α` and `Leaf α`, Lean cannot synthesize a `Top α` instance,
even though the hypotheses of the instances `Bottom.toMiddle` and `Middle.toTop` are satisfied.
There are two workarounds:
* You could replace the bundled inheritance implemented by the instance `Middle.toTop` with
unbundled inheritance implemented by adding a `[Top α]` parameter to the `Middle` class. This is
the preferred option since it is also more compatible with Lean 4, at the cost of being more work
to implement and more verbose to use.
* You could weaken the `Bottom.toMiddle` instance by making it depend on a subclass of
`Middle.toTop`'s parameter, in this example replacing `[Left α]` with `[Leaf α]`.
-/
def «out-param inheritance» : LibraryNote✝ :=
()
