Mutual inductives with instance parameters

[arthur-adjedj]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Lean fails to elaborate mutual inductive type with instance parameters correctly.

Context

None

Steps to Reproduce

class Foo

mutual
  inductive Bar [Foo] where
  inductive Baz [Foo] where
end

Expected behavior: No error

Actual behavior: Error invalid mutually inductive types, parameter name mismatch 'inst._@._hyg.13', expected 'inst._@._hyg.11'

Versions

4.9.0-nightly-2024-05-30

Impact

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