fix: incorrect grind param warning

This PR the redundant `grind` parameter warning message. It now checks
the `grind` theorem instantiation constraints too.

src/Lean/Elab/Tactic/Grind/Param.lean

@@ -52,8 +52,8 @@ public def addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Nam
       let thm₁ ← Grind.mkEMatchTheoremForDecl declName (.eqLhs gen) params.symPrios
       let thm₂ ← Grind.mkEMatchTheoremForDecl declName (.eqRhs gen) params.symPrios
       if warn &&
-          params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns &&
-          params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns then
+          params.ematch.containsWithSamePatterns thm₁.origin thm₁.patterns thm₁.cnstrs &&
+          params.ematch.containsWithSamePatterns thm₂.origin thm₂.patterns thm₂.cnstrs then
         warnRedundantEMatchArg params.ematch declName
       return { params with extra := params.extra.push thm₁ |>.push thm₂ }
     | _ =>
@@ -63,7 +63,7 @@ public def addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Nam
         Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
       else
         Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
-      if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns then
+      if warn && params.ematch.containsWithSamePatterns thm.origin thm.patterns thm.cnstrs then
         warnRedundantEMatchArg params.ematch declName
       return { params with extra := params.extra.push thm }
   | .defn =>

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

@@ -358,7 +358,7 @@ structure EMatchTheoremConstraint where
   numMVars   : Nat
   /-- The actual `rhs`. -/
   rhs        : Expr
-  deriving Inhabited, Repr
+  deriving Inhabited, Repr, BEq
 
 /-- A theorem for heuristic instantiation based on E-matching. -/
 structure EMatchTheorem where
@@ -391,10 +391,13 @@ instance : TheoremLike EMatchTheorem where
 /-- Set of E-matching theorems. -/
 abbrev EMatchTheorems := Theorems EMatchTheorem
 
-/-- Returns `true` if there is a theorem with exactly the same pattern is already in `s` -/
-def EMatchTheorems.containsWithSamePatterns (s : EMatchTheorems) (origin : Origin) (patterns : List Expr) : Bool :=
+/--
+Returns `true` if there is a theorem with exactly the same pattern and constraints is already in `s`
+-/
+def EMatchTheorems.containsWithSamePatterns (s : EMatchTheorems) (origin : Origin)
+    (patterns : List Expr) (cnstrs : List EMatchTheoremConstraint) : Bool :=
   let thms := s.find origin
-  thms.any fun thm => thm.patterns == patterns
+  thms.any fun thm => thm.patterns == patterns && thm.cnstrs == cnstrs
 
 def EMatchTheorems.getKindsFor (s : EMatchTheorems) (origin : Origin) : List EMatchTheoremKind :=
   let thms := s.find origin

tests/lean/run/grind_pattern_cnstr.lean

@@ -33,3 +33,11 @@ grind_pattern extract_extract => (as.extract i j).extract k l where
 set_option trace.grind.ematch.instance true in
 example (as : Array Nat) (h : #[].extract i j = as) : False := by
   grind only [= extract_empty, usr extract_extract]
+
+#guard_msgs (warning, drop error) in
+example (as bs : List Nat) (h : as.filterMap some = bs) : False := by
+  grind (instances := 50) [= List.filterMap_filterMap] -- No warning because stdlib version has a constraint
+
+#guard_msgs (warning, drop error) in
+example (as bs : List Nat) (h : as.filterMap some = bs) : False := by
+  grind (instances := 50) [List.filterMap_filterMap] -- No warning because stdlib version has a constraint