approach 1 *seems* to work

This reverts commit 3f82bdf176.

src/Lean/Elab/SyntheticMVars.lean

@@ -36,17 +36,33 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
       withSavedContext savedContext do
         let mvarDecl     ← getMVarDecl mvarId
         let expectedType ← instantiateMVars mvarDecl.type
-        withInfoHole mvarId do
+        let ret ← 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 ← do
+            if (← getInfoState).enabled then
+              let savedInfoTrees ← getResetInfoTrees
+              -- withRef stx <| ensureHasType expectedType result
+              Prod.fst <$> MonadFinally.tryFinally' (withRef stx <| ensureHasType expectedType result) fun _ => do
+                modifyInfoState fun state =>
+                  if savedInfoTrees.size > 0 then
+                    let mod (t : InfoTree) : InfoTree :=
+                      match t with
+                      | .node i ts => .node i (ts.append state.trees)
+                      | _ => t -- TODO?
+                    { state with trees := savedInfoTrees.modify (savedInfoTrees.size - 1) mod }
+                  else
+                    { state with trees := savedInfoTrees }
+            else
+              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
             return true
           else
             return false
+        pure ret
     catch
      | ex@(.internal id _) =>
        if id == postponeExceptionId then

src/Lean/Elab/Term/TermElabM.lean

@@ -1183,6 +1183,23 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     else
       throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{extraErrorMsg}{useTraceSynthMsg}"
 
+structure CoeExpansionTrace where
+  expandedCoeDecls : List Name
+deriving TypeName
+
+partial def _root_.Lean.Elab.InfoTree.format' (tree : InfoTree) (ctx? : Option ContextInfo := none) : TermElabM Format := do
+  match tree with
+  | .hole id     => return .nestD f!"• ?{toString id.name}"
+  | .context i t => t.format' <| i.mergeIntoOuter? ctx?
+  | .node i cs   =>
+    let ctx := ctx?.getD { env := (← getEnv), fileMap := (← getFileMap), ngen := NameGenerator.mk `dummy 0 }
+    let fmt ← i.format ctx
+    if cs.size == 0 then
+      return .nestD f!"• {fmt}"
+    else
+      let ctx? := i.updateContext? ctx?
+      return .nestD f!"• {fmt}{Std.Format.prefixJoin .line (← cs.toList.mapM fun c => c.format' ctx?)}"
+
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
     (mkErrorMsg? : Option (MVarId → (expectedType e : Expr) → MetaM MessageData) := none)
     (mkImmedErrorMsg? : Option ((errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData) := none) : TermElabM Expr := do
@@ -1190,7 +1207,12 @@ def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgH
   try
     withoutMacroStackAtErr do
       match ← coerce? e expectedType with
-      | .some eNew => return eNew
+      | .some eNew =>
+        pushInfoLeaf (.ofCustomInfo {
+          stx := ← getRef
+          value := Dynamic.mk <| CoeExpansionTrace.mk []
+        })
+        return eNew
       | .none => failure
       | .undef =>
         let mvarAux ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
@@ -1500,7 +1522,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
   | (elabFn::elabFns) =>
     try
       -- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
-      withTermInfoContext' elabFn.declName stx (expectedType? := expectedType?)
+      let ret ← withTermInfoContext' elabFn.declName stx (expectedType? := expectedType?)
         (try
           elabFn.value stx expectedType?
         catch ex => match ex with
@@ -1533,6 +1555,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
               postponeElabTermCore stx expectedType?
             else
               throw ex)
+      pure ret
     catch ex => match ex with
       | .internal id _ =>
         if id == unsupportedSyntaxExceptionId then

tests/lean/run/test.lean

@@ -0,0 +1,5 @@
+structure X
+def X.x (_ : X) : BaseIO Bool := sorry
+
+def f : IO Unit := do
+  let _ ← ([] : List X).findM? fun p => p.x