diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 9db5cf35c7..9bca53421a 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -530,9 +530,21 @@ header ++ indentExpr eType ++ Format.line ++ "but is expected to have type" ++ i
 
 def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
     (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
+/-
+  We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was
+  always of the form:
+  ```
+  failed to synthesize instance
+    CoeT <eType> <e> <expectedType>
+  ```
+  We should revisit this decision in the future and decide whether it may contain useful information
+  or not. -/
+let extraMsg := Format.nil;
+/-
 let extraMsg : MessageData := match extraMsg? with
   | none          => Format.nil
   | some extraMsg => Format.line ++ extraMsg;
+-/
 match f? with
 | none   => throwError $ mkTypeMismatchError header? e eType expectedType ++ extraMsg
 | some f => Meta.throwAppTypeMismatch f e extraMsg
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index ac1e1b9b77..812eab849f 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/tests/lean/doNotation1.lean.expected.out
@@ -4,17 +4,11 @@ doNotation1.lean:20:7: error: invalid reassignment, value has type
   Vector Nat (n + 1)
 but is expected to have type
   Vector Nat n
-failed to synthesize instance
-  CoeT (Vector Nat (n + 1)) (Vector.cons 1 v) (Vector Nat n)
 doNotation1.lean:25:7: error: invalid reassignment, value has type
   Bool
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT Bool true Nat
 doNotation1.lean:24:0: error: type mismatch, 'for' has type
   List Nat
 but is expected to have type
   List Bool
-failed to synthesize instance
-  CoeT (List Nat) r✝.fst (List Bool)
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 8d3d2b35b6..d1d9621441 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -16,8 +16,6 @@ has type
   String
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT String x✝ Nat
 with resulting expansion
   HasAdd.add✝ (x + x✝) x✝¹
 while expanding
diff --git a/tests/lean/matchErrorLocation.lean.expected.out b/tests/lean/matchErrorLocation.lean.expected.out
index 398a2c1ff8..10ccd5b0f0 100644
--- a/tests/lean/matchErrorLocation.lean.expected.out
+++ b/tests/lean/matchErrorLocation.lean.expected.out
@@ -4,5 +4,3 @@ has type
   False
 but is expected to have type
   α
-failed to synthesize instance
-  CoeT False (h he) α
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index aed9d11461..198f1077fc 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -6,8 +6,6 @@ has type
   Nat
 but is expected to have type
   Bool
-failed to synthesize instance
-  CoeT Nat ?m Bool
 sorryAx ?m : ?m
 g ?m ?m : Nat
 20
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index bd31bf8fae..311b6a0a4b 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -6,8 +6,6 @@ has type
   PersistentHashMap Nat Nat
 but is expected to have type
   PersistentHashMap Nat Nat
-failed to synthesize instance
-  CoeT (PersistentHashMap Nat Nat) m (PersistentHashMap Nat Nat)
 phashmap_inst_coherence.lean:12:0: error: application type mismatch
   Lean.runEval fun («_» : Unit) => sorryAx ?m
 argument
diff --git a/tests/lean/server/diags.lean.expected.out b/tests/lean/server/diags.lean.expected.out
index 543f5fa12d..bf351d38a2 100644
--- a/tests/lean/server/diags.lean.expected.out
+++ b/tests/lean/server/diags.lean.expected.out
@@ -1,7 +1,7 @@
 Content-Length: 221
 
-{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1017
+{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 955
 
-{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat\nfailed to synthesize instance\n  CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
+{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 38
 
 {"result":null,"jsonrpc":"2.0","id":1}
diff --git a/tests/lean/server/edits.lean.expected.out b/tests/lean/server/edits.lean.expected.out
index 56efc9d8bc..3d96d6394e 100644
--- a/tests/lean/server/edits.lean.expected.out
+++ b/tests/lean/server/edits.lean.expected.out
@@ -1,8 +1,8 @@
 Content-Length: 221
 
-{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 1017
+{"result":{"serverInfo":{"version":"0.0.1","name":"Lean 4 server"},"capabilities":{"textDocumentSync":{"willSaveWaitUntil":false,"willSave":false,"openClose":true,"change":2},"hoverProvider":true}},"jsonrpc":"2.0","id":0}Content-Length: 955
 
-{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat\nfailed to synthesize instance\n  CoeT String \"NotANat\" Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
+{"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[{"source":"Lean 4 server","severity":3,"range":{"start":{"line":4,"character":0},"end":{"line":4,"character":0}},"message":"n : Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":8,"character":0},"end":{"line":8,"character":0}},"message":"s : String"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":12,"character":0},"end":{"line":12,"character":0}},"message":"Hello world!\n"},{"source":"Lean 4 server","severity":1,"range":{"start":{"line":14,"character":31},"end":{"line":14,"character":31}},"message":"type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat"},{"source":"Lean 4 server","severity":3,"range":{"start":{"line":22,"character":0},"end":{"line":22,"character":0}},"message":"MyNs.u : Unit"}]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 184
 
 {"params":{"version":1,"uri":"file:///home/wojtek/Programming/C%2B%2B/lean4/src/Lean/Server/testDiags.txt","diagnostics":[]},"method":"textDocument/publishDiagnostics","jsonrpc":"2.0"}Content-Length: 883
 
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index d5cae92dbb..f7d198cebb 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -4,16 +4,12 @@ has type
   x✝ = x✝
 but is expected to have type
   x = x
-failed to synthesize instance
-  CoeT (x✝ = x✝) h (x = x)
 shadow.lean:10:0: error: type mismatch
   h
 has type
   x = x
 but is expected to have type
   x = x
-failed to synthesize instance
-  CoeT (x = x) h (x = x)
 shadow.lean:13:0: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out
index 9ab7d5af83..81f3b364ad 100644
--- a/tests/lean/struct1.lean.expected.out
+++ b/tests/lean/struct1.lean.expected.out
@@ -12,8 +12,6 @@ has type
   Bool
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT Bool true Nat
 struct1.lean:38:5: error: omit field 'x' type to set default value
 struct1.lean:41:12: error: type mismatch
   true
@@ -21,8 +19,6 @@ has type
   Bool
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT Bool true Nat
 struct1.lean:44:0: error: invalid 'private' constructor in a 'private' structure
 struct1.lean:47:0: error: invalid 'protected' constructor in a 'private' structure
 struct1.lean:50:0: error: invalid 'protected' field in a 'private' structure
diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out
index 5484cdaf00..d0e45548fa 100644
--- a/tests/lean/typeOf.lean.expected.out
+++ b/tests/lean/typeOf.lean.expected.out
@@ -6,8 +6,6 @@ has type
   Nat
 but is expected to have type
   Bool
-failed to synthesize instance
-  CoeT Nat x Bool
 typeOf.lean:12:0: error: application type mismatch
   HasAdd.add r
 argument
@@ -16,17 +14,11 @@ has type
   Bool
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT Bool r Nat
 typeOf.lean:20:54: error: invalid reassignment, term has type
   Bool
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT Bool (y == 1) Nat
 typeOf.lean:29:53: error: natural number expected, value has type
   Bool
 but is expected to have type
   Nat
-failed to synthesize instance
-  CoeT Bool true Nat