fix: whnf

2026-04-16 00:54:06 +00:00 · 2026-03-03 09:13:44 -08:00
1 changed files with 2 additions and 2 deletions
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -348,7 +348,7 @@ mutual
            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
+              if let some mvarId ← getStuckMVar? (← whnf major) then
                return mvarId
            /-
            Then, recurse on the explicit arguments
@@ -366,7 +366,7 @@ mutual
          else if let some auxInfo ← getAuxParentProjectionInfo? fName then
            unless auxInfo.fromClass do return none
            if let some major := args[auxInfo.numParams]? then
-              if let some mvarId ← getStuckMVar? major then
+              if let some mvarId ← getStuckMVar? (← whnf major) then
                return mvarId
            return none
          else