Incorrect promotion from index to paramater

[arthur-adjedj]

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

Some inductive types with indices get their indices promoted to parameters in cases where it shouldn't, leading to kernel-level errors afterwards

Context

The issue was first discovered here

Steps to Reproduce

MWE:

inductive All {I : Type u} (P : I → Type v) : List I → Type (max u v) where
  | cons : P x → All P xs → All P (x :: xs)

inductive Iμ {I : Type u}  : I → Type (max u v) where
  | mk : (i : I)  → All Iμ [] → Iμ i

Expected behavior: No error

Actual behavior: The index of Iμ gets promoted to a parameter during elaboration, leading to the following error:

arg #6 of '_nested.All_1.cons' contains a non valid occurrence

Versions

nightly-2024-02-21
Ubuntu

Additional Information

While there are some workarounds to avoid the promotion of indices to parameters, Lean would benefit from having an option to turn that feature off altogether.

Impact

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