feat: add withMVarContext

cc @dselsam @kha

src/Init/Lean/Meta/Basic.lean

@@ -344,7 +344,7 @@ do lctx ← getLCtx;
 def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
 getLocalDecl fvar.fvarId!
 
-def getMVarDecl (mvarId : Name) : MetaM MetavarDecl :=
+def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
    | some d => pure d
@@ -717,6 +717,19 @@ do s ← get;
    modify $ fun s => { mctx := s.mctx.incDepth, .. s };
    finally x (modify $ fun s => { cache := savedCache, mctx := savedMCtx, .. s })
 
+/--
+  Execute `x` using the given metavariable `LocalContext` and `LocalInstances`.
+  The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
+  different from the current ones. -/
+@[inline] def withMVarContext {α} (mvarId : MVarId) (x : MetaM α) : MetaM α :=
+do mvarDecl ← getMVarDecl mvarId;
+   localInsts ← getLocalInstances;
+   adaptReader (fun (ctx : Context) => { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances, .. ctx }) $
+     if localInsts == mvarDecl.localInstances then
+       x
+     else
+       resettingSynthInstanceCache x
+
 end Meta
 end Lean
 

src/Init/Lean/MetavarContext.lean

@@ -199,6 +199,11 @@ structure LocalInstance :=
 
 abbrev LocalInstances := Array LocalInstance
 
+def LocalInstance.beq (i₁ i₂ : LocalInstance) : Bool :=
+i₁.fvar == i₂.fvar
+
+instance LocalInstance.hasBeq : HasBeq LocalInstance := ⟨LocalInstance.beq⟩
+
 structure MetavarDecl :=
 (userName       : Name := Name.anonymous)
 (lctx           : LocalContext)