fix: instantiate mvars in types of mvars in abstractMVars (#10612)

This PR fixes an issue reported [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/.60abstractMVars.60.20not.20instantiating.20level.20mvars/near/541918246)
where `abstractMVars` (which is used in typeclass inference and `simp`
argument elaboration) was not instantiating metavariables in the types
of metavariables, causing it to abstract already-assigned metavariables.

This also eliminates an unnecessary `instantiateMVars` and documents the
invariant that the argument to `abstractExprMVars` must have its
metavariables already instantiated.

src/Lean/Meta/AbstractMVars.lean

@@ -67,6 +67,9 @@ private partial def abstractLevelMVars (u : Level) : M Level := do
           modify fun s => { s with nextParamIdx := s.nextParamIdx + 1, lmap := s.lmap.insert mvarId u, paramNames := s.paramNames.push paramId }
           return u
 
+/--
+Abstracts metavariables in `e`. Assumes `instantiateMVars` has been applied to `e`.
+-/
 partial def abstractExprMVars (e : Expr) : M Expr := do
   if !e.hasMVar then
     return e
@@ -88,28 +91,24 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
       if decl.depth != (← getMCtx).depth then
         return e
       else
-        let eNew ← instantiateMVars e
-        if e != eNew then
-          abstractExprMVars eNew
-        else
-          match (← get).emap[mvarId]? with
-          | some e =>
-            return e
-          | none   =>
-            let type   ← abstractExprMVars decl.type
-            let fvarId ← mkFreshFVarId
-            let fvar := mkFVar fvarId;
-            let userName ← if decl.userName.isAnonymous then
-              pure <| (`x).appendIndexAfter (← get).fvars.size
-            else
-              pure decl.userName
-            modify fun s => {
-              s with
-              emap  := s.emap.insert mvarId fvar
-              fvars := s.fvars.push fvar
-              mvars := s.mvars.push e
-              lctx  := s.lctx.mkLocalDecl fvarId userName type }
-            return fvar
+        match (← get).emap[mvarId]? with
+        | some e =>
+          return e
+        | none   =>
+          let type   ← abstractExprMVars (← instantiateMVars decl.type)
+          let fvarId ← mkFreshFVarId
+          let fvar := mkFVar fvarId;
+          let userName ← if decl.userName.isAnonymous then
+            pure <| (`x).appendIndexAfter (← get).fvars.size
+          else
+            pure decl.userName
+          modify fun s => {
+            s with
+            emap  := s.emap.insert mvarId fvar
+            fvars := s.fvars.push fvar
+            mvars := s.mvars.push e
+            lctx  := s.lctx.mkLocalDecl fvarId userName type }
+          return fvar
 
 end AbstractMVars
 

tests/lean/run/abstractMVars.lean

@@ -0,0 +1,23 @@
+import Lean
+/-!
+# Tests of the `Lean.Meta.abstractMVars` procedure
+-/
+
+open Lean Meta
+
+/-!
+The following example used to abstract `levelMVar` even though it was assigned.
+The issue was that the procedure failed to instantiateMVars in the types of metavariables.
+
+Reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/.60abstractMVars.60.20not.20instantiating.20level.20mvars/near/541918246
+-/
+
+/-- info: [] -/
+#guard_msgs in
+run_meta
+  let levelMVar ← mkFreshLevelMVar
+  let mvar ← mkFreshExprMVar (some (mkSort levelMVar))
+  discard <| isDefEq (mkSort levelMVar) (mkSort (mkLevelParam `u))
+  let mvar ← instantiateMVars mvar
+  let abstractResult ← abstractMVars mvar
+  Lean.logInfo m!"{abstractResult.paramNames}"