perf: deduplicate ← instantiateMVars (← inferType mvar) in TC search

[JovanGerb]

Closes #4284

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1c0787e.
There were no significant changes against commit 287d46e.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4379 has successfully built against this PR. (2024-06-06 18:38:13) View Log

[leodemoura]

Dear @JovanGerb ,

We have noticed that you have been submitting many PRs, and it is great to see your enthusiasm. Thank you for filing issues and proposing fixes. We are always looking for new contributors.
We want to share some guidelines based on our previous experiences. All successful external Lean contributors have started by making uncontroversial and small contributions. This approach helps build trust between the contributor and the core development team.
We strongly believe that critical modules that have been modified by multiple contributors become more challenging to maintain. For example, the type class resolution module has already been updated by Daniel, Gabriel, and myself. Daniel was the original author and is no longer part of the core team. Gabriel is a seasoned Lean developer who carefully studied this delicate module before making contributions.
We don't want to discourage you, but we would greatly appreciate it if you read our contribution guidelines and started by making contributions to simpler modules.
We’d encourage you avoid core modules and functionality initially, and maybe focus on low risk contributions (error messages, leaf tactics). Contributing to Mathlib is also a good way to build experience and reputation. We understand your eagerness to help with lean, and sympathize, but experience shows that it works better for everyone involved to take it slowly before, eventually maybe, touching core files.

Best wishes,
Leo and Sebastian (@Kha)

[JovanGerb]

Dear @leodemoura and @Kha,

Thank you for your kind message. I can undestand that making significant changes to core Lean requires trust and careful consideration. And the benefits of the change need to outweigh the cost of worsened maintanability.
I think this applies most to my suggested changes in type class synthesis caching (#4272) and the fix for eta-unreduced metavariable assignments (#4387).
Then there are some less disruptive changes such as fixing the implementation of isClassQuickConst? (#4319) and this PR, which seem to me to not negatively impact maintainability (although I'm not the right person to judge this) and which still give a noticeable improvement. There is also the fix for metavariable assignments in trace.Meta.synthInstance (#4285), which improves the trace messages. The fix at #4282 might improve performance, but I haven't checked this.
Finally there are changes that don't impact the performance or user experience, and only improve readability of the code itself, such as removing redundant parts from the code (#4388, #4288, #4287 and #4283). Are such changes welcome or are they considered to be too insignificant?
In #4277 I made many independent changes to type class synthesis, which I know is against the contribution guidelines, but I did it to see how the performance would improve by doing all those changes together. It now turns out that the improvement is already captured by the change in this PR. I can make separate PRs for the other parts of that PR if that is helpful.
Finally I'd like to say that I really like Lean both as a programming language and as a theorem prover, and that I'm happy to be in a position where I can help make it even better.

Best whishes,
Jovan

[Kha]

Thanks for your understanding. Maintainability of the code is one important aspect, but reviewing work is another one I would like to highlight. For a critical module like TC synth, there are basically no uncontroversial changes because every change must be reviewed with the full context of the module in mind, which usually means there is at most one potential reviewer and that person likely does not have that context ready in their mind right now.

Are such changes welcome or are they considered to be too insignificant?

So even positive but insignificant changes to such modules can be distractive and will be considered very low priority. For significant changes, as Leo wrote one should start at less critical places.