chore: move file

We already report a more informative issue when `proveEq` fails.

src/Lean/Meta/Tactic/Grind.lean

@@ -42,7 +42,6 @@ builtin_initialize registerTraceClass `grind.eqc
 builtin_initialize registerTraceClass `grind.internalize
 builtin_initialize registerTraceClass `grind.ematch
 builtin_initialize registerTraceClass `grind.ematch.pattern
-builtin_initialize registerTraceClass `grind.ematch.pattern.search
 builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
 builtin_initialize registerTraceClass `grind.eqResolution
@@ -71,6 +70,7 @@ builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
+builtin_initialize registerTraceClass `grind.debug.ematch.activate
 builtin_initialize registerTraceClass `grind.debug.ematch.pattern
 builtin_initialize registerTraceClass `grind.debug.beta
 builtin_initialize registerTraceClass `grind.debug.internalize
@@ -81,7 +81,6 @@ builtin_initialize registerTraceClass `grind.debug.mbtc
 builtin_initialize registerTraceClass `grind.debug.ematch
 builtin_initialize registerTraceClass `grind.debug.proveEq
 builtin_initialize registerTraceClass `grind.debug.pushNewFact
-builtin_initialize registerTraceClass `grind.debug.ematch.activate
 builtin_initialize registerTraceClass `grind.debug.appMap
 builtin_initialize registerTraceClass `grind.debug.ext
 

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

@@ -300,7 +300,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       let report : M Unit := do
         reportIssue! "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
       unless (← withDefault <| isDefEq mvarIdType vType) do
-        let some heq ← proveEq? vType mvarIdType
+        let some heq ← withoutReportingMVarIssues <| proveEq? vType mvarIdType
           | report
             return ()
         /-

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

@@ -337,35 +337,54 @@ private def foundBVar (idx : Nat) : M Bool :=
 private def saveBVar (idx : Nat) : M Unit := do
   modify fun s => { s with bvarsFound := s.bvarsFound.insert idx }
 
-private def getPatternFn? (pattern : Expr) : Option Expr :=
-  if !pattern.isApp && !pattern.isConst then
-    none
-  else match pattern.getAppFn with
-    | f@(.const declName _) => if isForbidden declName then none else some f
-    | f@(.fvar _) => some f
-    | _ => none
+inductive PatternArgKind where
+  | /-- Argument is relevant for E-matching. -/
+    relevant
+  | /-- Instance implicit arguments are considered support and handled using `isDefEq`. -/
+    instImplicit
+  | /-- Proofs are ignored during E-matching. Lean is proof irrelevant. -/
+    proof
+  | /--
+    Types and type formers are mostly ignored during E-matching, and processed using
+    `isDefEq`. However, if the argument is of the form `C ..` where `C` is inductive type
+    we process it as part of the pattern. Suppose we have `as bs : List α`, and a pattern
+    candidate expression `as ++ bs`, i.e., `@HAppend.hAppend (List α) (List α) (List α) inst as bs`.
+    If we completely ignore the types, the pattern will just be
+    ```
+    @HAppend.hAppend _ _ _ _ #1 #0
+    ```
+    This is not ideal because the E-matcher will try it in any goal that contains `++`,
+    even if it does not even mention lists.
+    -/
+    typeFormer
+    deriving Repr
+
+def PatternArgKind.isSupport : PatternArgKind → Bool
+  | .relevant => false
+  | _ => true
 
 /--
-Returns a bit-mask `mask` s.t. `mask[i]` is true if the corresponding argument is
+Returns an array `kinds` s.ts `kinds[i]` is the kind of the corresponding argument.
+
 - a type (that is not a proposition) or type former (which has forward dependencies) or
 - a proof, or
 - an instance implicit argument
 
-When `mask[i]`, we say the corresponding argument is a "support" argument.
+When `kinds[i].isSupport` is `true`, we say the corresponding argument is a "support" argument.
 -/
-def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
+def getPatternArgKinds (f : Expr) (numArgs : Nat) : MetaM (Array PatternArgKind) := do
   let pinfos := (← getFunInfoNArgs f numArgs).paramInfo
   forallBoundedTelescope (← inferType f) numArgs fun xs _ => do
     xs.mapIdxM fun idx x => do
       if (← isProp x) then
-        return false
+        return .relevant
       else if (← isProof x) then
-        return true
+        return .proof
       else if (← isTypeFormer x) then
         if h : idx < pinfos.size then
           /-
           We originally wanted to ignore types and type formers in `grind` and treat them as supporting elements.
-          Thus, we would always return `true`. However, we changed our heuristic because of the following example:
+          Thus, we wanted to always return `.typeFormer`. However, we changed our heuristic because of the following example:
           ```
           example {α} (f : α → Type) (a : α) (h : ∀ x, Nonempty (f x)) : Nonempty (f a) := by
             grind
@@ -374,33 +393,53 @@ def getPatternSupportMask (f : Expr) (numArgs : Nat) : MetaM (Array Bool) := do
           a type or type former is considered a supporting element only if it has forward dependencies.
           Note that this is not the case for `Nonempty`.
           -/
-          return pinfos[idx].hasFwdDeps
+          if pinfos[idx].hasFwdDeps then return .typeFormer else return .relevant
         else
-          return true
+          return .typeFormer
+      else if (← x.fvarId!.getDecl).binderInfo matches .instImplicit then
+        return .instImplicit
       else
-        return (← x.fvarId!.getDecl).binderInfo matches .instImplicit
+        return .relevant
 
-private partial def go (pattern : Expr) : M Expr := do
+private def getPatternFn? (pattern : Expr) (inSupport : Bool) (argKind : PatternArgKind) : MetaM (Option Expr) := do
+  if !pattern.isApp && !pattern.isConst then
+    return none
+  else match pattern.getAppFn with
+    | f@(.const declName _) =>
+      if isForbidden declName then
+        return none
+      if inSupport then
+        if argKind matches .typeFormer | .relevant then
+          if (← isInductive declName) then
+            return some f
+        return none
+      return some f
+    | f@(.fvar _) =>
+      if inSupport then return none else return some f
+    | _ =>
+      return none
+
+private partial def go (pattern : Expr) (inSupport : Bool) : M Expr := do
   if let some (e, k) := isOffsetPattern? pattern then
-    let e ← goArg e (isSupport := false)
+    let e ← goArg e inSupport .relevant
     if e == dontCare then
       return dontCare
     else
       return mkOffsetPattern e k
-  let some f := getPatternFn? pattern
+  let some f ← getPatternFn? pattern inSupport .relevant
     | throwError "invalid pattern, (non-forbidden) application expected{indentExpr pattern}"
   assert! f.isConst || f.isFVar
   unless f.isConstOf ``Grind.eqBwdPattern do
-   saveSymbol f.toHeadIndex
+    saveSymbol f.toHeadIndex
   let mut args := pattern.getAppArgs.toVector
-  let supportMask ← getPatternSupportMask f args.size
+  let patternArgKinds ← getPatternArgKinds f args.size
   for h : i in [:args.size] do
     let arg := args[i]
-    let isSupport := supportMask[i]?.getD false
-    args := args.set i (← goArg arg isSupport)
+    let argKind := patternArgKinds[i]?.getD .relevant
+    args := args.set i (← goArg arg (inSupport || argKind.isSupport) argKind)
   return mkAppN f args.toArray
 where
-  goArg (arg : Expr) (isSupport : Bool) : M Expr := do
+  goArg (arg : Expr) (inSupport : Bool) (argKind : PatternArgKind) : M Expr := do
     if !arg.hasLooseBVars then
       if arg.hasMVar then
         pure dontCare
@@ -408,25 +447,23 @@ where
         pure <| mkGroundPattern arg
     else match arg with
       | .bvar idx =>
-        if isSupport && (← foundBVar idx) then
+        if inSupport && (← foundBVar idx) then
           pure dontCare
         else
           saveBVar idx
           pure arg
       | _ =>
-        if isSupport then
-          pure dontCare
-        else if let some _ := getPatternFn? arg then
-          go arg
+        if let some _ ← getPatternFn? arg inSupport argKind then
+          go arg inSupport
         else
           pure dontCare
 
 def main (patterns : List Expr) : MetaM (List Expr × List HeadIndex × Std.HashSet Nat) := do
-  let (patterns, s) ← patterns.mapM go |>.run {}
+  let (patterns, s) ← patterns.mapM (go (inSupport := false)) |>.run {}
   return (patterns, s.symbols.toList, s.bvarsFound)
 
 def normalizePattern (e : Expr) : M Expr := do
-  go e
+  go e (inSupport := false)
 
 end NormalizePattern
 
@@ -668,11 +705,11 @@ private def isPatternFnCandidate (f : Expr) : CollectorM Bool := do
   | _ => return false
 
 private def addNewPattern (p : Expr) : CollectorM Unit := do
-  trace[grind.ematch.pattern.search] "found pattern: {ppPattern p}"
+  trace[grind.debug.ematch.pattern] "found pattern: {ppPattern p}"
   let bvarsFound := (← getThe NormalizePattern.State).bvarsFound
   let done := (← checkCoverage (← read).proof (← read).xs.size bvarsFound) matches .ok
   if done then
-    trace[grind.ematch.pattern.search] "found full coverage"
+    trace[grind.debug.ematch.pattern] "found full coverage"
   modify fun s => { s with patterns := s.patterns.push p, done }
 
 /-- Collect the pattern (i.e., de Bruijn) variables in the given pattern. -/
@@ -696,10 +733,11 @@ Returns `true` if pattern `p` contains a child `c` such that
 3- `c` is not an offset pattern.
 4- `c` is not a bound variable.
 -/
-private def hasChildWithSameNewBVars (p : Expr) (supportMask : Array Bool) (alreadyFound : Std.HashSet Nat) : CoreM Bool := do
+private def hasChildWithSameNewBVars (p : Expr)
+    (argKinds : Array NormalizePattern.PatternArgKind) (alreadyFound : Std.HashSet Nat) : CoreM Bool := do
   let s := diff (collectPatternBVars p) alreadyFound
-  for arg in p.getAppArgs, support in supportMask do
-    unless support do
+  for arg in p.getAppArgs, argKind in argKinds do
+    unless argKind.isSupport do
     unless arg.isBVar do
     unless isOffsetPattern? arg |>.isSome do
       let sArg := diff (collectPatternBVars arg) alreadyFound
@@ -711,31 +749,33 @@ private partial def collect (e : Expr) : CollectorM Unit := do
   if (← get).done then return ()
   match e with
   | .app .. =>
+    trace[grind.debug.ematch.pattern] "collect: {e}"
     let f := e.getAppFn
-    let supportMask ← NormalizePattern.getPatternSupportMask f e.getAppNumArgs
+    let argKinds ← NormalizePattern.getPatternArgKinds f e.getAppNumArgs
     if (← isPatternFnCandidate f) then
       let saved ← getThe NormalizePattern.State
       try
-        trace[grind.ematch.pattern.search] "candidate: {e}"
+        trace[grind.debug.ematch.pattern] "candidate: {e}"
         let p := e.abstract (← read).xs
         unless p.hasLooseBVars do
-          trace[grind.ematch.pattern.search] "skip, does not contain pattern variables"
+          trace[grind.debug.ematch.pattern] "skip, does not contain pattern variables"
           return ()
         let p ← NormalizePattern.normalizePattern p
         if saved.bvarsFound.size < (← getThe NormalizePattern.State).bvarsFound.size then
-          unless (← hasChildWithSameNewBVars p supportMask saved.bvarsFound) do
+          unless (← hasChildWithSameNewBVars p argKinds saved.bvarsFound) do
             addNewPattern p
             return ()
-        trace[grind.ematch.pattern.search] "skip, no new variables covered"
+        trace[grind.debug.ematch.pattern] "skip, no new variables covered"
         -- restore state and continue search
         set saved
-      catch _ =>
-        trace[grind.ematch.pattern.search] "skip, exception during normalization"
+      catch ex =>
+        trace[grind.debug.ematch.pattern] "skip, exception during normalization{indentD ex.toMessageData}"
         -- restore state and continue search
         set saved
     let args := e.getAppArgs
-    for arg in args, support in supportMask do
-      unless support do
+    for arg in args, argKind in argKinds do
+      trace[grind.debug.ematch.pattern] "arg: {arg}, support: {argKind.isSupport}"
+      unless argKind.isSupport do
         collect arg
   | .forallE _ d b _ =>
     if (← pure e.isArrow <&&> isProp d <&&> isProp b) then
@@ -746,6 +786,7 @@ private partial def collect (e : Expr) : CollectorM Unit := do
 private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Array Expr) : MetaM (Option (List Expr × List HeadIndex)) := do
   let go : CollectorM (Option (List Expr)) := do
     for place in searchPlaces do
+      trace[grind.debug.ematch.pattern] "place: {place}"
       let place ← preprocessPattern place
       collect place
       if (← get).done then
@@ -782,8 +823,8 @@ where
         return some e
       else
         let args := e.getAppArgs
-        for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do
-          unless flag do
+        for arg in args, argKind in (← NormalizePattern.getPatternArgKinds f args.size) do
+          unless argKind.isSupport do
             if let some r ← visit? arg then
               return r
         return none

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

@@ -313,7 +313,8 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
     mkENode e generation
     activateTheoremPatterns declName generation
   | .mvar .. =>
-    reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
+    if (← reportMVarInternalization) then
+      reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
     mkENode' e generation
   | .mdata .. =>
     reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"

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

@@ -68,6 +68,13 @@ structure Context where
   when performing lookahead.
   -/
   cheapCases : Bool := false
+  /-
+  If `reportMVarIssue` is `true`, `grind` reports an issue when internalizing metavariables.
+  The default value is `true`. We set it to `false` when invoking `proveEq` from the `instantiateTheorem`
+  at in the E-matching module. There, the terms may contain metavariables, and we don't want to bother
+  user with "false-alarms". If the instantiation fails, we produce a more informative issue anyways.
+  -/
+  reportMVarIssue : Bool := true
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -147,6 +154,16 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 abbrev GrindM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
+@[inline] def mapGrindM [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM α → GrindM α) {α} (x : m α) : m α :=
+  controlAt GrindM fun runInBase => f <| runInBase x
+
+/--
+`withoutReportingMVarIssues x` executes `x` without reporting metavariables found during internalization.
+See comment at `Grind.Context.reportMVarIssue` for additional details.
+-/
+def withoutReportingMVarIssues [MonadControlT GrindM m] [Monad m] : m α → m α :=
+  mapGrindM <| withTheReader Grind.Context fun ctx => { ctx with reportMVarIssue := false }
+
 /-- Returns the user-defined configuration options -/
 def getConfig : GrindM Grind.Config :=
   return (← readThe Context).config
@@ -177,6 +194,9 @@ def getMainDeclName : GrindM Name :=
 def cheapCasesOnly : GrindM Bool :=
   return (← readThe Context).cheapCases
 
+def reportMVarInternalization : GrindM Bool :=
+  return (← readThe Context).reportMVarIssue
+
 def saveEMatchTheorem (thm : EMatchTheorem) : GrindM Unit := do
   if (← getConfig).trace then
     modify fun s => { s with trace.thms := s.trace.thms.insert { origin := thm.origin, kind := thm.kind } }

tests/lean/grind/hashmap_list.lean

@@ -1,18 +0,0 @@
-import Std.Data.HashMap
-
-reset_grind_attrs%
-
-open Std
-
-attribute [grind →] List.length_pos_of_mem
-attribute [grind] HashMap.size_insert
-
--- Fails with issue:
--- [issue] type error constructing proof for List.length_pos_of_mem
---     when assigning metavariable ?l with
---       m.insert 1 2
---     has type
---       HashMap Nat Nat : Type
---     but is expected to have type
---       List Nat : Type
-example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 3 4).size ≤ m.size := by grind

tests/lean/grind/mvar.lean

@@ -1,14 +0,0 @@
-open List
-
--- Failing with:
--- [issue] unexpected metavariable during internalization
---       ?α
---     `grind` is not supposed to be used in goals containing metavariables.
-  -- [issue] type error constructing proof for Array.eq_empty_of_append_eq_empty
-  --     when assigning metavariable ?xs with
-  --       l₁
-  --     has type
-  --       List α : Type u_1
-  --     but is expected to have type
-  --       Array ?α : Type ?u.430
-theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by grind (gen := 6)

tests/lean/run/grind_ematch1.lean

@@ -83,15 +83,25 @@ error: `@[grind →] theorem using_grind_fwd.StransBad` failed to find patterns
 @[grind→] theorem StransBad (a b c d : Nat) : S a b ∨ R a b → S b c → S a c ∧ S b d := sorry
 
 
-set_option trace.grind.ematch.pattern.search true in
+set_option trace.grind.debug.ematch.pattern true in
 /--
-info: [grind.ematch.pattern.search] candidate: S a b
-[grind.ematch.pattern.search] found pattern: S #4 #3
-[grind.ematch.pattern.search] candidate: R a b
-[grind.ematch.pattern.search] skip, no new variables covered
-[grind.ematch.pattern.search] candidate: S b c
-[grind.ematch.pattern.search] found pattern: S #3 #2
-[grind.ematch.pattern.search] found full coverage
+info: [grind.debug.ematch.pattern] place: S a b ∨ R a b
+[grind.debug.ematch.pattern] collect: S a b ∨ R a b
+[grind.debug.ematch.pattern] arg: S a b, support: false
+[grind.debug.ematch.pattern] collect: S a b
+[grind.debug.ematch.pattern] candidate: S a b
+[grind.debug.ematch.pattern] found pattern: S #4 #3
+[grind.debug.ematch.pattern] arg: R a b, support: false
+[grind.debug.ematch.pattern] collect: R a b
+[grind.debug.ematch.pattern] candidate: R a b
+[grind.debug.ematch.pattern] skip, no new variables covered
+[grind.debug.ematch.pattern] arg: a, support: false
+[grind.debug.ematch.pattern] arg: b, support: false
+[grind.debug.ematch.pattern] place: S b c
+[grind.debug.ematch.pattern] collect: S b c
+[grind.debug.ematch.pattern] candidate: S b c
+[grind.debug.ematch.pattern] found pattern: S #3 #2
+[grind.debug.ematch.pattern] found full coverage
 [grind.ematch.pattern] Strans: [S #4 #3, S #3 #2]
 -/
 #guard_msgs (info) in

tests/lean/run/grind_eq_pattern.lean

@@ -1,14 +1,14 @@
 reset_grind_attrs%
 
 /--
-info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend _ _ _ _ #2 #0]
+info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #2 #0]
 -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 attribute [grind] List.append_ne_nil_of_left_ne_nil
 
 /--
-info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend _ _ _ _ #1 #2]
+info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2]
 -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in

tests/lean/run/grind_hashmap_list.lean

@@ -0,0 +1,12 @@
+import Std.Data.HashMap
+set_option grind.warning false
+reset_grind_attrs%
+
+open Std
+
+attribute [grind →] List.length_pos_of_mem
+attribute [grind] HashMap.size_insert
+
+set_option trace.grind.issues true in
+example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 3 4).size ≥ m.size := by
+  grind

tests/lean/run/grind_mvar.lean

@@ -0,0 +1,12 @@
+open List
+reset_grind_attrs%
+set_option grind.warning false
+
+attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero
+attribute [grind] Vector.getElem?_append getElem?_dropLast
+
+#guard_msgs (info) in -- should not report any issues
+set_option trace.grind.issues true
+theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by
+   fail_if_success grind (gen := 6)
+   grind -ext only [List.dropLast_append_cons, List.dropLast_singleton, List.append_nil]

tests/lean/run/grind_pattern1.lean

@@ -1,20 +1,20 @@
 set_option trace.grind.ematch.pattern true
 
 /--
-info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem _ `[Nat] #4 _ _ (@Array.push _ #3 #2) #1 _]
+info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem (Array #4) `[Nat] _ _ _ (@Array.push _ #3 #2) #1 _]
 -/
 #guard_msgs in
 grind_pattern Array.getElem_push_lt => (xs.push x)[i]
 
 
 /--
-info: [grind.ematch.pattern] List.getElem_attach: [@getElem _ `[Nat] _ _ _ (@List.attach #3 #2) #1 _]
+info: [grind.ematch.pattern] List.getElem_attach: [@getElem (List (@Subtype #3 _)) `[Nat] (@Subtype _ _) _ _ (@List.attach _ #2) #1 _]
 -/
 #guard_msgs in
 grind_pattern List.getElem_attach => xs.attach[i]
 
 /--
-info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 _ _ (@HAppend.hAppend _ _ _ _ #1 (@List.cons _ #0 (@List.nil _))) #0]
+info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 (List _) _ (@HAppend.hAppend (List _) (List _) (List _) _ #1 (@List.cons _ #0 (@List.nil _))) #0]
 -/
 #guard_msgs in
 grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
@@ -54,13 +54,13 @@ instance [Boo α β] : Boo (List α) (Array β) where
 
 theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl
 
-/-- info: [grind.ematch.pattern] fEq: [@f _ _ _ _ #0] -/
+/-- info: [grind.ematch.pattern] fEq: [@f (List #4) (Array #3) _ _ #0] -/
 #guard_msgs in
 grind_pattern fEq => f a
 
 theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl
 
-/-- info: [grind.ematch.pattern] fEq2: [@f _ _ _ _ #1] -/
+/-- info: [grind.ematch.pattern] fEq2: [@f (List #5) (Array #4) _ _ #1] -/
 #guard_msgs in
 grind_pattern fEq2 => f a
 
@@ -71,12 +71,12 @@ theorem gEq [Boo α β] (a : List α) : (g (β := Array β) a).1 = a := rfl
 
 /--
 error: invalid pattern(s) for `gEq`
-  [@g _ _ _ #0]
+  [@g (List #3) _ _ #0]
 the following theorem parameters cannot be instantiated:
   β : Type
   inst✝ : Boo α β
 ---
-info: [grind.ematch.pattern] gEq: [@g _ _ _ #0]
+info: [grind.ematch.pattern] gEq: [@g (List #3) _ _ #0]
 -/
 #guard_msgs in
 grind_pattern gEq => g a

tests/lean/run/grind_pattern2.lean

@@ -62,7 +62,7 @@ theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[
 
 
 /--
-info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem _ `[Nat] _ _ _ #2 #5 _) (@getElem _ `[Nat] _ _ _ #2 #4 _)]
+info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem (Array _) `[Nat] _ _ _ #2 #5 _) (@getElem (Array _) `[Nat] _ _ _ #2 #4 _)]
 -/
 #guard_msgs in
 grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁)