fix: grind pattern validation

This PR fixes the `grind` pattern validator. It covers the case where
an instance is not tagged with the implicit instance binder. This
happens in declarations such as
```lean
ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
  [self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
```

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -662,10 +662,23 @@ def getPatternArgKinds (f : Expr) (numArgs : Nat) : MetaM (Array PatternArgKind)
           if pinfos[idx].hasFwdDeps then return .typeFormer else return .relevant
         else
           return .typeFormer
-      else if (← x.fvarId!.getDecl).binderInfo matches .instImplicit then
-        return .instImplicit
       else
-        return .relevant
+        let xDecl ← x.fvarId!.getDecl
+        if xDecl.binderInfo matches .instImplicit then
+          return .instImplicit
+        /-
+        **Note**: Even if the binder is not marked as instance implicit, we may still
+        synthesize it using type class resolution. The motivation is declarations such as
+        ```
+        ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
+            [self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
+        ```
+        Recall that a similar approach is used in `simp`.
+        -/
+        else if (← isClass? xDecl.type).isSome then
+          return .instImplicit
+        else
+          return .relevant
 
 private def getPatternFn? (pattern : Expr) (inSupport : Bool) (root : Bool) (argKind : PatternArgKind) : M (Option Expr) := do
   if !pattern.isApp && !pattern.isConst then
@@ -860,27 +873,34 @@ private def checkCoverage (thmProof : Expr) (numParams : Nat) (bvarsFound : Std.
       for x in xs do
         let fvarId := x.fvarId!
         unless processed.contains fvarId do
-          let xType ← inferType x
+          let xDecl ← fvarId.getDecl
+          let xType := xDecl.type
           if fvarsFound.contains fvarId then
             -- Collect free vars in `x`s type and mark as processed
             fvarsFound := update fvarsFound xType
             processed := processed.insert fvarId
             modified := true
-          else if (← fvarId.getDecl).binderInfo matches .instImplicit then
-            -- If `x` is instance implicit, check whether
-            -- we have found all free variables needed to synthesize instance
-            if (← canBeSynthesized thmVars fvarsFound xType) then
-              fvarsFound := fvarsFound.insert fvarId
-              fvarsFound := update fvarsFound xType
-              processed := processed.insert fvarId
-              modified := true
-          else if (← isProp xType) then
-            -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
-            -- add it to `fvarsFound` and mark it as processed.
-            if checkTypeFVars thmVars fvarsFound xType then
-              fvarsFound := fvarsFound.insert fvarId
-              processed := processed.insert fvarId
-              modified := true
+          else
+            /- **Note**: See comment at `getPatternArgKinds` -/
+            let instImplicit ← if xDecl.binderInfo matches .instImplicit then
+              pure true
+            else
+              pure <| (← isClass? xType).isSome
+            if instImplicit then
+              -- If `x` is instance implicit, check whether
+              -- we have found all free variables needed to synthesize instance
+              if (← canBeSynthesized thmVars fvarsFound xType) then
+                fvarsFound := fvarsFound.insert fvarId
+                fvarsFound := update fvarsFound xType
+                processed := processed.insert fvarId
+                modified := true
+            else if (← isProp xType) then
+              -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
+              -- add it to `fvarsFound` and mark it as processed.
+              if checkTypeFVars thmVars fvarsFound xType then
+                fvarsFound := fvarsFound.insert fvarId
+                processed := processed.insert fvarId
+                modified := true
       if fvarsFound.size == numParams then
         return .ok
       if !modified then

tests/lean/run/grind_pattern_validation_instance.lean

@@ -0,0 +1,58 @@
+/-!
+Test for `grind` pattern validation. It covers the case where
+an instance is not tagged with the implicit instance binder.
+This happens in declarations such as
+```lean
+ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
+  [self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
+```
+-/
+
+def Set (α : Type u) := α → Prop
+
+/-- Membership in a set -/
+protected def Set.Mem (s : Set α) (a : α) : Prop :=
+  s a
+
+instance : Membership α (Set α) :=
+  ⟨Set.Mem⟩
+
+class SetLike (A : Type) (B : outParam Type) where
+  protected coe : A → Set B
+  protected coe_injective : Function.Injective coe
+
+instance [SetLike A B]: CoeTC A (Set B) where coe := SetLike.coe
+
+instance [SetLike A B] : Membership B A :=
+  ⟨fun p x => x ∈ (p : Set B)⟩
+
+class ZeroMemClass (S : Type) (M : outParam Type) [Zero M] [SetLike S M] : Prop where
+  zero_mem : ∀ s : S, (0 : M) ∈ s
+
+class Ring (R : Type) extends Zero R
+
+@[ext]
+structure Subring (M : Type) [Ring M] where
+  carrier : Set M
+  zero_mem' : 0 ∈ carrier
+
+instance {M} [Ring M] : SetLike (Subring M) M where
+  coe := Subring.carrier
+  coe_injective a b h := by ext; assumption
+
+theorem Subring.zero_mem {M} [Ring M] (s : Subring M) : 0 ∈ s :=
+  s.zero_mem'
+
+grind_pattern ZeroMemClass.zero_mem => 0 ∈ s
+
+instance {M} [Ring M] : ZeroMemClass (Subring M) M where
+  zero_mem := Subring.zero_mem
+
+example {R : Type} [Ring R] (S : Subring R) : 0 ∈ S := by
+  grind
+
+example {R : Type} [Ring R] (S : Subring R) : 0 ∈ S := by
+  grind only [ZeroMemClass.zero_mem]
+
+example {R : Type} [Ring R] (S : Subring R) : 0 ∈ S := by
+  grind only [Subring.zero_mem]