Redundant alternative in deriving Ord

Stream: lean4

[ohhaimark]

I have the following:

abbrev Var := Int

inductive Ty where
  | int
  | bool

@[reducible] def Ty.type : Ty → Type
  | .int => Int
  | .bool => Bool

inductive Expr : Ty → Type where
  | litInt : Int → Expr .int
  | litBool : Bool → Expr .bool
  | varInt : Var → Expr .int
  | add : Expr .int → Expr .int → Expr .int
  | minus : Expr .int → Expr .int
  | lt : Expr .int → Expr .int → Expr .bool
  | eq : Expr .int → Expr .int → Expr .bool
deriving Ord

but I have this error on the deriving: redudant alternative. I'd really like to not have to manually write this Ord instance.
I'm on leanprover/lean4:v4.7.0-rc2

[ohhaimark]

Smaller repro

inductive Ty where
  | int
  | bool
inductive Expr : Ty → Type where
  | a : Expr .int
  | b : Expr .bool
deriving Ord

[ohhaimark]

Well now I realize I don't need that Ord instance, but still a bug.

[Kim Morrison]

@ohhaimark, could you please open an issue on the Lean repo?

[ohhaimark]

https://github.com/leanprover/lean4/issues/3706

[ohhaimark]

Where does lean implement deriving tactics? More specifically, where can I find Ord's?

[Chris Bailey]

https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Deriving/Ord.lean