feat: add support for stuck class projection function applications at getStuckMVar?

closes #1408

src/Lean/Meta/WHNF.lean

@@ -10,6 +10,7 @@ import Lean.Structure
 import Lean.Util.Recognizers
 import Lean.Meta.Basic
 import Lean.Meta.GetConst
+import Lean.Meta.FunInfo
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchPatternAttr
 
@@ -257,20 +258,46 @@ mutual
     match e with
     | .mdata _ e  => getStuckMVar? e
     | .proj _ _ e => getStuckMVar? (← whnf e)
-    | .mvar .. => do
+    | .mvar .. =>
       let e ← instantiateMVars e
       match e with
-      | Expr.mvar mvarId => pure (some mvarId)
+      | .mvar mvarId => return some mvarId
       | _ => getStuckMVar? e
     | .app f .. =>
       let f := f.getAppFn
       match f with
-      | .mvar mvarId   => return some mvarId
+      | .mvar .. =>
+        let e ← instantiateMVars e
+        match e.getAppFn with
+        | .mvar mvarId => return some mvarId
+        | _ => getStuckMVar? e
       | .const fName _ =>
         match (← getConstNoEx? fName) with
         | some <| .recInfo recVal  => isRecStuck? recVal e.getAppArgs
         | some <| .quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs
-        | _                        => return none
+        | _  =>
+          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.get? 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

tests/lean/run/1408.lean

@@ -0,0 +1,13 @@
+inductive Foo (n : Nat)
+
+class Bar (n: Nat) (α : Type u) (β: outParam (Type u)) where
+  bar: Foo n → Fin (n+1) → α → β
+
+instance: Bar n (Foo (n+1)) (Foo n) := sorry
+
+example  (t: Foo (n+2)) (s₁: Foo (n+1)) (s₂: Foo n) (t': Foo n) (hk: k < n + 1) (hm: m < n + 2):
+  Bar.bar s₂ ⟨k, hk⟩ (Bar.bar s₁ ⟨m, ‹_›⟩ t) = t' := sorry
+
+variable (t: Foo (n+2)) (s₁: Foo (n+1)) (s₂: Foo n) (t': Foo n) (hk: k < n + 1) (hm: m < n + 2)
+example:
+  Bar.bar s₂ ⟨k, hk⟩ (Bar.bar s₁ ⟨m, ‹_›⟩ t) = t' := sorry