fix: type class issues

[leodemoura]

Summary:

• Take synthPendingDepth into account when caching TC results
• Add maxSynthPendingDepth option with default := 2.
• Add support for tracking synthPending failures when using set_option diagnostics true

closes #2522 closes #3313 closes #3927

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4114 build failed against this PR. (2024-05-09 01:32:33) View Log
• 💥 Mathlib branch lean-pr-testing-4114 build failed against this PR. (2024-05-09 02:27:02) View Log
• 🟡 Mathlib branch lean-pr-testing-4114 build this PR didn't complete normally. (2024-05-09 03:05:09) View Log
• ❌ Mathlib branch lean-pr-testing-4114 built against this PR, but testing failed. (2024-05-09 04:06:25) View Log

[kim-em]

Speedcenter results on Mathlib (comparing against nightly-testing-2024-05-08, i.e. no changes except this change to Lean, and the two minor adaptations in Mathlib) are available at http://speed.lean-fro.org/mathlib4/compare/74df3d57-7d3a-4c8a-870b-ed5b8ccd5802/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=fd58d1bdbcaeb92b91d2d047c4a4d4572fda2162.

Unfortunately they are bad: +1.3% instructions, +2.4% wall clock.

[kim-em]

Closing in favour of #4119