use withTermInfoContext' inside withInfoHole to prevent the custom info to override the term info

Author: datokrat

src/Lean/Elab/SyntheticMVars.lean

@@ -37,10 +37,11 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
         let mvarDecl     ← getMVarDecl mvarId
         let expectedType ← instantiateMVars mvarDecl.type
         withInfoHole mvarId do
-          let result ← resumeElabTerm stx expectedType (!postponeOnError)
-          /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
-            That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
-          let result ← withRef stx <| ensureHasType expectedType result
+          let result ← withTermInfoContext' .anonymous stx do
+            let result ← resumeElabTerm stx expectedType (!postponeOnError)
+            /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
+              That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
+            withRef stx <| ensureHasType expectedType result
           /- We must perform `occursCheck` here since `result` may contain `mvarId` when it has synthetic `sorry`s. -/
           if (← occursCheck mvarId result) then
             mvarId.assign result