(kernel) declaration has free variables error when extending class with typeclass parameter and extends

[SabrinaJewson]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The following Lean 4 code produces an error:

class A
class B
class C [A] extends B
class D extends A, B, C
--                    ^ (kernel) declaration has free variables 'D.toC'

Context

This came about when I was defining my own classes for abstract algebra, which heavily build on other classes and use extends to minimize field repetition caused by inheritance diamonds.

Steps to Reproduce

1. Write the code above into a Lean file
2. Attempt to compile it

Expected behavior: No error.

Actual behavior: The type checker gives the described error.

Versions

Lean (version 4.3.0-nightly-2023-10-01, commit e6292bc, Release) on Linux 6.3.13

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[digama0]

Note that this has never worked (extends classes cannot be dependent on each other)

[SabrinaJewson]

That’s surprising to me, because the following does work:

class A
class B [A]
class C extends A, B