From bf8b66c6a52a268d647fa07466ac34a1dde64814 Mon Sep 17 00:00:00 2001
From: Arthur Adjedj <arthur.adjedj@gmail.com>
Date: Thu, 21 Mar 2024 11:29:22 +0100
Subject: [PATCH] fix: ignore unused alternatives in `Ord` derive handler
 (#3725)

Closes #3706

This derive handler's implementation is very similar to `BEq`'s, which
already ignores unused alternative so as to work correctly on indexed
inductive types. This PR simply implements the same solution as the one
present in
[`BEq.lean`](https://github.com/leanprover/lean4/blob/2c15cdda044e77bb8c3937c63501850790e60dc6/src/Lean/Elab/Deriving/BEq.lean#L94).

After some tests, it doesn't seem like any other derive handler present
in Core suffers from the same issue (though some handlers don't work on
indexed inductives for other reasons).
---
 src/Lean/Elab/Deriving/Ord.lean |  1 +
 tests/lean/run/3706.lean        | 13 +++++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 tests/lean/run/3706.lean

diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
index 47a4bcfc1e..1b67f532ad 100644
--- a/src/Lean/Elab/Deriving/Ord.lean
+++ b/src/Lean/Elab/Deriving/Ord.lean
@@ -84,6 +84,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   for i in [:ctx.typeInfos.size] do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual
+     set_option match.ignoreUnusedAlts true
      $auxDefs:command*
     end)
 
diff --git a/tests/lean/run/3706.lean b/tests/lean/run/3706.lean
new file mode 100644
index 0000000000..da8acce2a5
--- /dev/null
+++ b/tests/lean/run/3706.lean
@@ -0,0 +1,13 @@
+/--Ensure that `deriving Ord` works on indexed inductive types.-/
+inductive Ty where
+  | int
+  | bool
+inductive Expr : Ty → Type where
+  | a : Expr .int
+  | b : Expr .bool
+deriving Ord
+
+inductive Vec (α : Type u) : Nat → Type u
+  | nil  : Vec α 0
+  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+deriving Ord