From eece499da9e7aea7789f6cda0b37f4540902a58c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 27 Jun 2023 16:39:19 -0700
Subject: [PATCH] fix: fixes #2282

---
 src/Lean/Meta/DiscrTree.lean |  6 ++++--
 tests/lean/run/2282.lean     | 15 +++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/2282.lean

diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 33cc4aefe9..001bb2d202 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -436,8 +436,10 @@ def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree
 
 private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
   let e ← reduceDT e root (simpleReduce := s)
-  if let some v := toNatLit? e then
-    return (.lit v, #[])
+  unless root do
+    -- See pushArgs
+    if let some v := toNatLit? e then
+      return (.lit v, #[])
   match e.getAppFn with
   | .lit v         => return (.lit v, #[])
   | .const c _     =>
diff --git a/tests/lean/run/2282.lean b/tests/lean/run/2282.lean
new file mode 100644
index 0000000000..24d4e4ab27
--- /dev/null
+++ b/tests/lean/run/2282.lean
@@ -0,0 +1,15 @@
+class Zero'.{u} (α : Type u) where
+  zero : α
+
+instance Zero'.toOfNat0 {α} [Zero' α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero' α›.1
+
+instance Nat.zero' : Zero' Nat where
+  zero := 0
+
+example :
+    0 = if (b : Bool) then
+      (@OfNat.ofNat.{0} Nat 0 (@Zero'.toOfNat0.{0} Nat (Nat.zero')))
+    else
+      Nat.zero := by
+  simp