fix: E-matching patterns containing ground universe polymorphic patterns in grind (#9857)

This PR ensures `grind` can E-match patterns containing universe
polymorphic ground sub-patterns. For example, given
```
set_option pp.universes true in
attribute [grind?] Id.run_pure
```
the pattern
```
Id.run_pure.{u_1}: [@Id.run.{u_1} #1 (@pure.{u_1, u_1} `[Id.{u_1}] `[Applicative.toPure.{u_1, u_1}] _ #0)]
```
contains two nested universe polymorphic ground patterns
- `Id.{u_1}`
- `Applicative.toPure.{u_1, u_1}`

This kind of pattern is not common, but it occurs in core.

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

@@ -131,6 +131,33 @@ protected def _root_.Lean.Meta.Grind.GenPatternInfo.assign? (genInfo : GenPatter
   let c ← assignDelayedEqProof? c genInfo.hIdx
   return c
 
+private def matchGroundPattern (pArg eArg : Expr) : GoalM Bool := do
+  /-
+  1) Remark:
+  We need to use `withReducibleAndInstances` because ground patterns are often instances.
+  Here is an example
+  ```
+  instance : Max Nat where
+    max := Nat.max -- Redefined the instance
+
+  example (a : Nat) : max a a = a := by
+    grind
+  ```
+  Possible future improvements:
+  - When `diagnostics` is true, try with `withDefault` and report issue if it succeeds.
+  - (minor) Only use `withReducibleAndInstances` if the argument is an implicit instance.
+    Potential issue: some user write `{_ : Class α}` when the instance can be inferred from
+    explicit arguments.
+  2) Remark:
+  If `pArg` contains universe metavariables, we use `withoutModifyingMCtx` to ensure the metavariables
+  are not assigned. These universe metavariables are created at `internalizePattern` for universe polymorphic
+  ground patterns. They are not common, but they occur in practice.
+  -/
+  if pArg.hasLevelMVar then
+    withoutModifyingMCtx <| withReducibleAndInstances <| isDefEq pArg eArg
+  else
+    isEqv pArg eArg <||> withReducibleAndInstances (isDefEq pArg eArg)
+
 /-- Matches a pattern argument. See `matchArgs?`. -/
 private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM Choice := do
   if isPatternDontCare pArg then
@@ -138,23 +165,7 @@ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM C
   else if pArg.isBVar then
     assign? c pArg.bvarIdx! eArg
   else if let some pArg := groundPattern? pArg then
-    /-
-    We need to use `withReducibleAndInstances` because ground patterns are often instances.
-    Here is an example
-    ```
-    instance : Max Nat where
-      max := Nat.max -- Redefined the instance
-
-    example (a : Nat) : max a a = a := by
-      grind
-    ```
-    Possible future improvements:
-    - When `diagnostics` is true, try with `withDefault` and report issue if it succeeds.
-    - (minor) Only use `withReducibleAndInstances` if the argument is an implicit instance.
-      Potential issue: some user write `{_ : Class α}` when the instance can be inferred from
-      explicit arguments.
-    -/
-    guard (← isEqv pArg eArg <||> withReducibleAndInstances (isDefEq pArg eArg))
+    guard (← matchGroundPattern pArg eArg)
     return c
   else if let some (pArg, k) := isOffsetPattern? pArg then
     assert! Option.isNone <| isOffsetPattern? pArg
@@ -165,7 +176,7 @@ private def matchArg? (c : Choice) (pArg : Expr) (eArg : Expr) : OptionT GoalM C
       let c ← assign? c pArg.bvarIdx! eArg
       genInfo.assign? c eArg
     else if let some pArg := groundPattern? pArg then
-      guard (← isEqv pArg eArg <||> withReducibleAndInstances (isDefEq pArg eArg))
+      guard (← matchGroundPattern pArg eArg)
       genInfo.assign? c eArg
     else if let some (pArg, k) := isOffsetPattern? pArg then
       return { c with cnstrs := .offset (some genInfo) pArg k eArg :: c.cnstrs }

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

@@ -12,6 +12,7 @@ public import Lean.Meta.LitValues
 public import Lean.Meta.Match.MatcherInfo
 public import Lean.Meta.Match.MatchEqsExt
 public import Lean.Meta.Match.MatchEqs
+public import Lean.Util.CollectLevelParams
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Canon
@@ -151,7 +152,7 @@ private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit :=
   mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
 
 /-- Internalizes the nested ground terms in the given pattern. -/
-private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
+private partial def internalizePattern (pattern : Expr) (generation : Nat) (origin : Origin) : GoalM Expr := do
   -- Recall that it is important to ensure patterns are maximally shared since
   -- we assume that in functions such as `getAppsOf` in `EMatch.lean`
   go (← shareCommon pattern)
@@ -161,7 +162,21 @@ where
       return pattern
     else if let some e := groundPattern? pattern then
       let e ← preprocessLight e
-      internalize e generation none
+      let e ← if e.hasLevelParam && origin matches .decl _ then
+        /-
+        If `e` has universe parameters and it is **not** local. That is,
+        it contains the universe parameters of some global theorem.
+        Then, we convert `e`'s universe parameters into universe meta-variables.
+        Remark: it is pointless to internalize the result because it contains these helper meta-variables.
+        Remark: universe polymorphic ground patterns are not common, but they do occur in the
+        core library.
+        -/
+        let ps := collectLevelParams {} e |>.params
+        let us ← ps.mapM fun _ => mkFreshLevelMVar
+        pure <| e.instantiateLevelParamsArray ps us
+      else
+        internalize e generation none
+        pure e
       return mkGroundPattern e
     else pattern.withApp fun f args => do
       return mkAppN f (← args.mapM go)
@@ -203,7 +218,7 @@ def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
   -- Recall that we use the proof as part of the key for a set of instances found so far.
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
-  let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
+  let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation thm.origin)) }
   trace_goal[grind.ematch] "activated `{thm.origin.key}`, {thm.patterns.map ppPattern}"
   modify fun s => { s with ematch.newThms := s.ematch.newThms.push thm }
 

tests/lean/run/grind_univ_poly_ground_pattern.lean

@@ -0,0 +1,3 @@
+/-! Test for E-matching patterns containing nested universe polymorphic ground patterns. -/
+example : Id.run (pure true) = true := by
+  grind only [Id.run_pure]