fix: type class issues with `maxSynthPendingDepth := 1`

[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

Identical to #4114 but with maxSynthPendingDepth := 1

closes #4114

cc @semorrison

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4119 build failed against this PR. (2024-05-10 01:22:48) View Log
• 💥 Mathlib branch lean-pr-testing-4119 build failed against this PR. (2024-05-10 02:02:52) View Log
• 💥 Mathlib branch lean-pr-testing-4119 build failed against this PR. (2024-05-10 02:12:11) View Log
• 💥 Mathlib branch lean-pr-testing-4119 build failed against this PR. (2024-05-10 06:51:44) View Log
• ❌ Mathlib branch lean-pr-testing-4119 built against this PR, but linting failed. (2024-05-10 21:01:04) View Log
• ✅ Mathlib branch lean-pr-testing-4119 has successfully built against this PR. (2024-05-11 00:08:28) View Log
• ✅ Mathlib branch lean-pr-testing-4119 has successfully built against this PR. (2024-05-11 00:35:09) View Log
• ✅ Mathlib branch lean-pr-testing-4119 has successfully built against this PR. (2024-05-11 01:32:44) View Log
• 🟡 Mathlib branch lean-pr-testing-4119 build against this PR was cancelled. (2024-05-14 01:37:25) View Log
• 🟡 Mathlib branch lean-pr-testing-4119 build against this PR was cancelled. (2024-05-14 01:42:49) View Log
• 💥 Mathlib branch lean-pr-testing-4119 build failed against this PR. (2024-05-14 01:47:45) View Log
• 🟡 Mathlib branch lean-pr-testing-4119 build against this PR was cancelled. (2024-05-14 02:55:02) View Log
• 🟡 Mathlib branch lean-pr-testing-4119 build against this PR was cancelled. (2024-05-14 03:08:01) View Log
• 💥 Mathlib branch lean-pr-testing-4119 build failed against this PR. (2024-05-14 04:03:07) View Log

[kim-em]

(Mathlib build will come good again after the toolchain rebuilds after the rebase ... It's okay locally so likely I'll merge this without waiting for a final check.)