diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 6163893251..284f30ea96 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1862,7 +1862,7 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
     tryUnificationHints t s <||> tryUnificationHints s t
 
 /--
-Result type for `isDefEqDelta`
+Result type for `isDefEqDeltaStep`
 -/
 inductive DeltaStepResult where
   | eq | unknown
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index e42ef2a79e..312aa51f99 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -271,87 +271,6 @@ private def reduceQuotRec (recVal  : QuotVal) (recArgs : Array Expr) (failK : Un
   | QuotKind.ind  => process 4 3
   | _             => failK ()
 
--- ===========================
-/-! # Helper function for extracting "stuck term" -/
--- ===========================
-
-mutual
-  private partial def isRecStuck? (recVal : RecursorVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
-    if recVal.k then
-      -- TODO: improve this case
-      return none
-    else do
-      let majorIdx := recVal.getMajorIdx
-      if h : majorIdx < recArgs.size then do
-        let major := recArgs[majorIdx]
-        let major ← whnf major
-        getStuckMVar? major
-      else
-        return none
-
-  private partial def isQuotRecStuck? (recVal : QuotVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
-    let process? (majorPos : Nat) : MetaM (Option MVarId) :=
-      if h : majorPos < recArgs.size then do
-        let major := recArgs[majorPos]
-        let major ← whnf major
-        getStuckMVar? major
-      else
-        return none
-    match recVal.kind with
-    | QuotKind.lift => process? 5
-    | QuotKind.ind  => process? 4
-    | _             => return none
-
-  /-- Return `some (Expr.mvar mvarId)` if metavariable `mvarId` is blocking reduction. -/
-  partial def getStuckMVar? (e : Expr) : MetaM (Option MVarId) := do
-    match e with
-    | .mdata _ e  => getStuckMVar? e
-    | .proj _ _ e => getStuckMVar? (← whnf e)
-    | .mvar .. =>
-      let e ← instantiateMVars e
-      match e with
-      | .mvar mvarId => return some mvarId
-      | _ => getStuckMVar? e
-    | .app f .. =>
-      let f := f.getAppFn
-      match f with
-      | .mvar .. =>
-        let e ← instantiateMVars e
-        match e.getAppFn with
-        | .mvar mvarId => return some mvarId
-        | _ => getStuckMVar? e
-      | .const fName _ =>
-        match (← getEnv).find? fName with
-        | some <| .recInfo recVal  => isRecStuck? recVal e.getAppArgs
-        | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
-        | _  =>
-          unless e.hasExprMVar do return none
-          -- Projection function support
-          let some projInfo ← getProjectionFnInfo? fName | return none
-          -- This branch is relevant if `e` is a type class projection that is stuck because the instance has not been synthesized yet.
-          unless projInfo.fromClass do return none
-          let args := e.getAppArgs
-          -- First check whether `e`s instance is stuck.
-          if let some major := args[projInfo.numParams]? then
-            if let some mvarId ← getStuckMVar? major then
-              return mvarId
-          /-
-          Then, recurse on the explicit arguments
-          We want to detect the stuck instance in terms such as
-          `HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) n (OfNat.ofNat Nat 2 ?m)`
-          See issue https://github.com/leanprover/lean4/issues/1408 for an example where this is needed.
-          -/
-          let info ← getFunInfo f
-          for pinfo in info.paramInfo, arg in args do
-            if pinfo.isExplicit then
-              if let some mvarId ← getStuckMVar? arg then
-                return some mvarId
-          return none
-      | .proj _ _ e => getStuckMVar? (← whnf e)
-      | _ => return none
-    | _ => return none
-end
-
 -- ===========================
 /-! # Weak Head Normal Form auxiliary combinators -/
 -- ===========================
@@ -689,6 +608,114 @@ where
         | .yesWithDeltaI => k (← whnfAtMostI c)
       | _ => unreachable!
 
+-- ===========================
+/-! # Helper function for extracting "stuck term" -/
+-- ===========================
+
+mutual
+  private partial def isRecStuck? (recVal : RecursorVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
+    if recVal.k then
+      -- TODO: improve this case
+      return none
+    else do
+      let majorIdx := recVal.getMajorIdx
+      if h : majorIdx < recArgs.size then do
+        let major := recArgs[majorIdx]
+        let major ← whnf major
+        getStuckMVar? major
+      else
+        return none
+
+  private partial def isQuotRecStuck? (recVal : QuotVal) (recArgs : Array Expr) : MetaM (Option MVarId) :=
+    let process? (majorPos : Nat) : MetaM (Option MVarId) :=
+      if h : majorPos < recArgs.size then do
+        let major := recArgs[majorPos]
+        let major ← whnf major
+        getStuckMVar? major
+      else
+        return none
+    match recVal.kind with
+    | QuotKind.lift => process? 5
+    | QuotKind.ind  => process? 4
+    | _             => return none
+
+  private partial def isProjStuck? (projInfo : ProjectionFunctionInfo) (f : Expr) (args : Array Expr) : MetaM (Option MVarId) := do
+    -- This branch is relevant if `e` is a type class projection that is stuck because the instance has not been synthesized yet.
+    unless projInfo.fromClass do return none
+    -- First check whether `e`s instance is stuck.
+    if let some major := args[projInfo.numParams]? then
+      if let some mvarId ← getStuckMVar? major then
+        return mvarId
+    /-
+    Then, recurse on the explicit arguments
+    We want to detect the stuck instance in terms such as
+    `HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) n (OfNat.ofNat Nat 2 ?m)`
+    See issue https://github.com/leanprover/lean4/issues/1408 for an example where this is needed.
+    -/
+    let info ← getFunInfo f
+    for pinfo in info.paramInfo, arg in args do
+      if pinfo.isExplicit then
+        if let some mvarId ← getStuckMVar? arg then
+          return some mvarId
+    return none
+
+  private partial def isDefnStuck? (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) : MetaM (Option MVarId) := do
+    -- We simply report "stuck" iff one of the arguments is stuck on an MVar.
+    -- For matchers, we can do slightly better by only checking the discriminants.
+    -- C.f. `Lean.Meta.DiscrTree.getKeyArgs`.
+    match ← getMatcherInfo? c.name with
+    | some info =>
+      -- We cannot afford to unfold the matcher here.
+      -- We simply report "stuck" iff one of the discriminants is stuck on an MVar.
+      for arg in revArgs.reverse[info.getDiscrRange.lower:info.getDiscrRange.upper] do
+        if let some mvarId ← getStuckMVar? arg then
+          return some mvarId
+      return none
+    | none =>
+      -- We need to unfold here, otherwise we would need to report `Nat.succ ?m` as stuck on `?m`,
+      -- regressing e.g., 5333.lean.
+      deltaBetaDefinition c lvls revArgs (fun _ => return none) getStuckMVar?
+
+  /-- Return `some (Expr.mvar mvarId)` if metavariable `mvarId` is blocking reduction. -/
+  partial def getStuckMVar? (e : Expr) : MetaM (Option MVarId) := do
+    match e with
+    | .mdata _ e  => getStuckMVar? e
+    | .proj _ _ e => getStuckMVar? (← whnf e)
+    | .mvar .. =>
+      let e ← instantiateMVars e
+      match e with
+      | .mvar mvarId => return some mvarId
+      | _ => getStuckMVar? e
+    | .app f .. =>
+      let f := f.getAppFn
+      match f with
+      | .mvar .. =>
+        let e ← instantiateMVars e
+        match e.getAppFn with
+        | .mvar mvarId => return some mvarId
+        | _ => getStuckMVar? e
+      | .const fName lvls =>
+        match (← getEnv).find? fName with
+        | some <| .recInfo recVal  => isRecStuck? recVal e.getAppArgs
+        | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
+        | some <| c@(.defnInfo ..) =>
+          /- For some weird reason, hoisting this check to the top of the function breaks a DefEq
+          check in `3807.lean`. -/
+          unless e.hasExprMVar do return none
+          if let some projInfo ← getProjectionFnInfo? fName then
+            isProjStuck? projInfo f e.getAppArgs
+          else
+            isDefnStuck? c lvls e.getAppRevArgs
+        | _  => return none
+      | .proj _ _ e => getStuckMVar? (← whnf e)
+      | _ => return none
+    | _ => return none
+end
+
+-- ===========================
+/-! # Helper function for unfolding definitions -/
+-- ===========================
+
 /--
   Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldingMatch` (*) and `markSmartUnfoldingMatchAlt` (**).
   For example, consider the following definition
@@ -877,6 +904,10 @@ def unfoldDefinition (e : Expr) : MetaM Expr := do
   let some e ← unfoldDefinition? e | throwError "failed to unfold definition{indentExpr e}"
   return e
 
+-- ===========================
+/-! # More Weak Head Normal Form auxiliary combinators -/
+-- ===========================
+
 @[specialize] partial def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
   whnfEasyCases e fun e => do
     let e ← whnfCore e
diff --git a/tests/lean/run/unfoldingStuckOnMVar.lean b/tests/lean/run/unfoldingStuckOnMVar.lean
new file mode 100644
index 0000000000..4d007802ab
--- /dev/null
+++ b/tests/lean/run/unfoldingStuckOnMVar.lean
@@ -0,0 +1,77 @@
+/-!
+# Definitional equality on a definition the unfolding of which is stuck on an MVar
+-/
+
+namespace One
+
+def Pred (σs : List Type) := match σs with
+  | [] => Prop
+  | σ::σs => σ → Pred σs
+
+def Blah (x : Nat) := x
+
+def trp {α : Type} {σs : List Type} (P Q : α → Pred σs) : Prop := sorry
+
+theorem spec {α : Type} {σs : List Type} {a : α} (P : α → Pred σs) :
+  trp P P := sorry
+
+/--
+info: spec fun p s =>
+  p.fst = some p.snd ∧ s = 4 : trp (fun p s => p.fst = some p.snd ∧ s = 4) fun p s => p.fst = some p.snd ∧ s = 4
+-/
+#guard_msgs in
+#check (spec (σs := [Nat]) (fun p s => p.1 = p.2 ∧ s = 4)
+        : @trp (MProd (Option Nat) Nat) [Nat] _ _)
+
+/-!
+This used to have a failure on `(fun p s => p.1 = p.2 ∧ s = 4)` because the definitional equality
+  ?m.547 p → Prop =?= Pred ?m.504
+used to return `false` instead of being stuck on `?m.504`.
+-/
+set_option trace.Meta.isDefEq.stuckMVar true in
+/--
+info: spec fun p s =>
+  p.fst = some p.snd ∧ s = 4 : trp (fun p s => p.fst = some p.snd ∧ s = 4) fun p s => p.fst = some p.snd ∧ s = 4
+---
+trace: [Meta.isDefEq.stuckMVar] found stuck MVar ?m.504 : List Type
+[Meta.isDefEq.stuckMVar] found stuck MVar ?m.504 : List Type
+-/
+#guard_msgs in
+#check (spec (fun p s => p.1 = p.2 ∧ s = 4)
+        : @trp (MProd (Option Nat) Nat) [Nat] _ _)
+
+end One
+
+namespace I8766
+
+
+def SPred (σs : List Type) := match σs with
+  | [] => Prop
+  | σ :: σs => σ → SPred σs
+
+class WP (m : Type → Type) (σs : outParam (List Type)) where
+
+instance : WP (EStateM ε σ) [σ] where
+
+def Triple [WP m σs] (x : m α) (P Q : SPred σs) := True
+
+/-!
+Similarly to the above, reduction of `SPred ?m.1250` is stuck on `?m.1250`.
+It will eventually be solved once `WP (EStateM ε σ) [σ]` has been synthesized.
+-/
+set_option trace.Meta.isDefEq.stuckMVar true in
+/--
+info: ∀ (ε σ α : Type) (s : σ) (prog : EStateM ε σ α) (P : σ → Prop), Triple prog (fun s' => s' = s) P → P s : Prop
+---
+trace: [Meta.isDefEq.stuckMVar] found stuck MVar ?m.1138 : List Type
+[Meta.isDefEq.stuckMVar] found stuck MVar ?m.1138 : List Type
+---
+trace: [Meta.isDefEq.stuckMVar] found stuck MVar ?m.1138 : List Type
+[Meta.isDefEq.stuckMVar] found stuck MVar ?m.1138 : List Type
+[Meta.isDefEq.stuckMVar] found stuck MVar ?m.1138 : List Type
+-/
+#guard_msgs in
+#check ∀ ε σ α s (prog : EStateM ε σ α) (P : σ → Prop),
+    Triple prog (fun s' => s' = s) P → P s
+
+end I8766