fix: improve precision of synthesis failure spans in interpolated strings (#9004)

This PR ensures that type-class synthesis failure errors in interpolated
strings are displayed at the interpolant at which they occurred.

Author: jrr6

src/Init/Meta.lean

@@ -1430,7 +1430,7 @@ def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → S
   let mut i := 0
   let mut result := Syntax.missing
   for elem in chunks do
-    let elem ← match elem.isInterpolatedStrLit? with
+    let elem ← withRef elem <| match elem.isInterpolatedStrLit? with
       | none     => mkElem elem
       | some str => mkElem (Syntax.mkStrLit str)
     if i == 0 then

tests/lean/interactive/strInterpSynthError.lean

@@ -0,0 +1,30 @@
+/-!
+# String interpolation synthesis diagnostic spans
+
+The spans for type-class synthesis errors in interpolated strings to be localized to the
+interpolants at which synthesis failure occurs.
+-/
+
+structure Foo where
+structure Bar where
+
+def foo := Foo.mk
+def bar := Bar.mk
+
+instance : ToString Foo := ⟨fun _ => "foo"⟩
+
+example := s!"a {foo} b {bar} c"
+            --^ collectDiagnostics
+               --^ collectDiagnostics
+                       --^ collectDiagnostics
+
+example := s!"{bar} a"
+            --^ collectDiagnostics
+             --^ collectDiagnostics
+                  --^ collectDiagnostics
+
+
+example := s!"a {bar}"
+            --^ collectDiagnostics
+               --^ collectDiagnostics
+                  --^ collectDiagnostics

tests/lean/interactive/strInterpSynthError.lean.expected.out

@@ -0,0 +1,33 @@
+{"version": 1,
+ "uri": "file:///strInterpSynthError.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 15, "character": 25},
+    "end": {"line": 15, "character": 28}},
+   "message":
+   "failed to synthesize\n  ToString Bar\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 15, "character": 25},
+    "end": {"line": 15, "character": 28}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 20, "character": 15},
+    "end": {"line": 20, "character": 18}},
+   "message":
+   "failed to synthesize\n  ToString Bar\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 20, "character": 15},
+    "end": {"line": 20, "character": 18}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 26, "character": 17},
+    "end": {"line": 26, "character": 20}},
+   "message":
+   "failed to synthesize\n  ToString Bar\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "fullRange":
+   {"start": {"line": 26, "character": 17},
+    "end": {"line": 26, "character": 20}}}]}