From 37870635e47090c75c17ba02165d66237b8f03fa Mon Sep 17 00:00:00 2001
From: Parth Shastri <31370288+cppio@users.noreply.github.com>
Date: Wed, 8 Jan 2025 10:16:42 -0500
Subject: [PATCH] fix: reduce `Eq.rec` when mvars are present

---
 src/Lean/Meta/WHNF.lean           |  2 --
 tests/lean/6562.lean              | 24 ++++++++++++++++++++++++
 tests/lean/6562.lean.expected.out |  0
 3 files changed, 24 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/6562.lean
 create mode 100644 tests/lean/6562.lean.expected.out

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 97009be71fcc..958e52af1a1a 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -125,8 +125,6 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorTypeI := majorType.getAppFn
   if !majorTypeI.isConstOf recVal.getMajorInduct then
     return major
-  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
-    return major
   else do
     let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure major
     let newType ← inferType newCtorApp
diff --git a/tests/lean/6562.lean b/tests/lean/6562.lean
new file mode 100644
index 000000000000..feaf3adaf5cf
--- /dev/null
+++ b/tests/lean/6562.lean
@@ -0,0 +1,24 @@
+/-! Patterns with metavariables should still satisfy defeqs -/
+
+example : (x : Nat) → (Eq.refl x).symm.ndrec (motive := fun _ => Bool) false = false → Unit
+  | _, rfl => ()
+
+inductive Mem (a : α) : List α → Type
+  | head (as : List α) : Mem a (a::as)
+  | tail (b : α) {as : List α} : Mem a as → Mem a (b::as)
+
+def del : @Mem α a as → List α
+  | .head as => as
+  | .tail b mem => b :: del mem
+
+def memOfDel : (mem : Mem c as) → Mem a (del mem) → Mem a as
+  | .head _, mem => .tail _ mem
+  | .tail _ mem, .head _ => .head _
+  | .tail _ mem, .tail _ mem' => .tail _ (memOfDel mem mem')
+
+def memOfDel' : (mem : Mem c as) → Mem a (del mem) → Mem a as
+  | .head _, mem => .tail _ mem
+  | .tail b mem, (mem' : Mem a (b :: del mem)) =>
+    match mem' with
+    | .head _ => .head _
+    | .tail _ mem' => .tail _ (memOfDel' mem mem')
diff --git a/tests/lean/6562.lean.expected.out b/tests/lean/6562.lean.expected.out
new file mode 100644
index 000000000000..e69de29bb2d1