From fddc8b06ac97fa61d8137d25d15956b76be95323 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Mar 2022 10:33:11 -0800
Subject: [PATCH] fix: missing case at `getStuckMVar?`

Fix issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'rewrite'.20failed.20but.20it.20should.20work/near/274870747
---
 src/Lean/Meta/WHNF.lean         | 12 +++++++-----
 tests/lean/run/kronRWIssue.lean | 12 ++++++++++++
 2 files changed, 19 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/kronRWIssue.lean

diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 5e86c604e1..86f68e10c8 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -224,24 +224,26 @@ mutual
     | _             => return none
 
   /-- Return `some (Expr.mvar mvarId)` if metavariable `mvarId` is blocking reduction. -/
-  partial def getStuckMVar? : Expr → MetaM (Option MVarId)
+  partial def getStuckMVar? (e : Expr) : MetaM (Option MVarId) := do
+    match e with
     | Expr.mdata _ e _       => getStuckMVar? e
-    | Expr.proj _ _ e _      => do getStuckMVar? (← whnf e)
-    | e@(Expr.mvar ..) => do
+    | Expr.proj _ _ e _      => getStuckMVar? (← whnf e)
+    | Expr.mvar .. => do
       let e ← instantiateMVars e
       match e with
       | Expr.mvar mvarId _ => pure (some mvarId)
       | _ => getStuckMVar? e
-    | e@(Expr.app f _ _) =>
+    | Expr.app f .. =>
       let f := f.getAppFn
       match f with
       | Expr.mvar mvarId _       => return some mvarId
-      | Expr.const fName fLvls _ => do
+      | Expr.const fName fLvls _ =>
         let cinfo? ← getConstNoEx? fName
         match cinfo? with
         | some $ ConstantInfo.recInfo recVal  => isRecStuck? recVal fLvls e.getAppArgs
         | some $ ConstantInfo.quotInfo recVal => isQuotRecStuck? recVal fLvls e.getAppArgs
         | _                                => return none
+      | Expr.proj _ _ e _ => getStuckMVar? (← whnf e)
       | _ => return none
     | _ => return none
 end
diff --git a/tests/lean/run/kronRWIssue.lean b/tests/lean/run/kronRWIssue.lean
new file mode 100644
index 0000000000..dc74a3a5a0
--- /dev/null
+++ b/tests/lean/run/kronRWIssue.lean
@@ -0,0 +1,12 @@
+class Foo (α : Type) where
+  decEq : DecidableEq α
+
+instance instDecidableEq {α} [Foo α] : DecidableEq α := Foo.decEq
+instance instFooNat : Foo Nat := ⟨by infer_instance⟩
+
+def kron (i j : α) [DecidableEq α] : Nat := if (i=j) then 1 else 0
+
+theorem kron_right_mul (α : Type) [foo : Foo α]  (i j : α) (x : Nat) : x * kron i j = kron i j * x := sorry
+
+example {i j : Nat} : i * kron i j = kron i j * i := by
+  rw [kron_right_mul]