Too many motives for nested inductive types

Description

When checking nested inductive types, the kernel may generate a recursor with too many motives, as well as too many auxiliary recursors.

Steps to Reproduce

set_option genSizeOf false -- Added because of issue #9018

inductive Foo (A : Type)
  | foo : A → Foo A

inductive Bar where
  | bar : Foo Bar → Bar
  | bad : Foo Bar → Bar

#check Bar.rec -- Two motives

inductive Bad where
  | bar : Foo Bad → Bad
  | bad : Foo (id Bad) → Bad

#check Bad.rec -- Three motives !
#check Bad.rec_2 --shouldn't exist!

Expected behavior: Bar and Bad should have the same recursor, with the same motives (e.g one for Bar, one for Foo Bar).

Actual behavior: The Bad recursor gets three motives (one for Bar, one for Foo Bar, and another for Foo (id Bar)), as well as a third recursor Bad.rec_2 which doesn't exist for Bar.

Versions

Lean 4.21.0-rc3 Target: x86_64-unknown-linux-gnu, using live.lean-lang.org.

Additional Information

This bug happens because the kernel, when translating the nested inductive type into a mutual one, populates m_nested_aux with an auxiliary inductive for Foo (id Bar) despite the fact that there already exists one for Foo Bar. The reason this happens is that this check is only up to syntactic equality, not up to defeq.

Impact

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

Reproduce the issue with the Lean examples in the report, then inspect src/kernel/inductive.cpp around m_nested_aux and the linked check near line 981. Verify how the nested-to-mutual translation handles Foo Bar versus Foo (id Bar); done means Bad and Bar generate matching motives and Bad.rec_2 is no longer generated.