fix: Meta.Closure: topologically sort abstracted vars

[nomeata]

This PR topologically sorts abstracted vars in
Meta.Closure.mkValueTypeClosure if MVars are being abstracted.
Fixes #10705

[nomeata]

!bench

[leanprover-radar]

Benchmark results for 2cf8794 against efbbb0b are in! @nomeata

[leanprover-bot]

Here are the benchmark results for commit 2cf8794.
There were significant changes against commit efbbb0b:

  Benchmark                          Metric         Change
  ==================================================================
+ workspaceSymbols with new ranges   branches        -1.1% (-43.5 σ)
+ workspaceSymbols with new ranges   instructions    -1.5% (-46.7 σ)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-23 10:33:35)

[eric-wieser]

It's not immediately clear to me why a sort is needed here; presumably we could store the variables in the order we visit them or similar (as revert does)? Or is the point that we do actually want a different (topologically-compatilble) order that is somehow more efficient for reducing term sizes?

[nomeata]

It's not immediately clear to me why a sort is needed here; presumably we could store the variables in the order we visit them

This might be true if we visited the types of fvars before adding them, but the existing code puts them on a separate to-process-queue:

      let newFVarId ← mkFreshFVarId
      pushToProcess ⟨fvarId, newFVarId⟩
      return mkFVar newFVarId

This was introduced in 555a3f0 and I since don't fully understand the implications I’d rather leave it like this.

Also, adding the infrastructure to sort these would allow me to make progress on #10723 and then maybe remove the hacks where termination checking has to unfold abstracted proofs.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-10926 has successfully built against this PR. (2025-10-23 12:20:56) View Log
• ✅ Mathlib branch lean-pr-testing-10926 has successfully built against this PR. (2025-10-23 16:53:06) View Log

[nomeata]

presumably we could store the variables in the order we visit them

Also, isn’t this what you tried in #10702? I thought you said it didn't work.

I gave it another shot at #10932 but it didn’t work out of the box, so parking it there for now.

[nomeata]

Maybe we’ll find a more elegant fix later, but for now this fixes the bug and seems to work.