RFC: in TC resolution, ← instantiateMVars (← inferType mvar) is computed 2 or 3 times over for every new goal

[JovanGerb]

Proposal

These three lines do this same computation:

lean4/src/Lean/Meta/SynthInstance.lean

Line 286 in f05a827

let mvarType ← instantiateMVars mvarType

lean4/src/Lean/Meta/SynthInstance.lean

Line 243 in f05a827

let mvarType ← instantiateMVars mvarType

lean4/src/Lean/Meta/SynthInstance.lean

Line 474 in f05a827

let mvarType ← instantiateMVars (← inferType mvar)

I propose to do it once, and pass this result as an argument to all these functions.

[kim-em]

Is there evidence that this change by itself would have a performance impact?

[JovanGerb]

I hadn't tested it separately yet, but here's a PR for it now: #4379
Fixing only this also involved moving the withMCtx around a bit, because the instantiateMVars needs to be in the relevant metavariable context. I have an issue for this here #4286

[JovanGerb]

The result of the test on Mathlib is that this change is responsible for all of the performance improvement in #4277.