fix: instantiateMVars slowdown in the language server

[Kha]

Fixes #5614

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5805 has successfully built against this PR. (2024-10-22 12:36:57) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9157c1f2792ddcf792b2b212185a2449078356b5 --onto 66dbad911eaaec4cd512662bd5cc67a2a16d2484. (2024-10-24 08:49:08)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit b8a5c2d.
There were significant changes against commit 9157c1f:

  Benchmark           Metric                 Change
  =============================================================
+ big_omega.lean MT   branch-misses          -35.6%   (-76.8 σ)
+ big_omega.lean MT   branches               -29.5% (-2209.9 σ)
+ big_omega.lean MT   instructions           -29.8% (-3617.5 σ)
+ big_omega.lean MT   task-clock             -48.8%   (-14.1 σ)
+ big_omega.lean MT   wall-clock             -48.8%   (-14.1 σ)
+ parser              task-clock              -2.7%   (-11.9 σ)
+ parser              wall-clock              -2.7%   (-11.8 σ)
+ stdlib              instantiate metavars   -14.3%  (-112.8 σ)
- stdlib              share common exprs       2.2%    (11.5 σ)