deriving DecidableEq gives kernel error for higher universes

Stream: mathlib4

[Bhavik Mehta]

Here's my example:

import Mathlib

inductive example_type : Type 1
  | A | B | C
  deriving DecidableEq

This came up in a student project; it works fine for Type

[Joachim Breitner]

Good catch. Probably nothing deep, please file an issue.
(Are enumeration types at higher types useful?)

[Bhavik Mehta]

lean4#9541