fix: instantiate mvars of indices before instantiating fvars

[arthur-adjedj]

When elaborating the headers of mutual indexed inductive types, mvars have to be synthesized and instantiated before replacing the fvars present there. Otherwise, some fvars present in uninstantiated mvars may be missed and lead to an error later.
Closes #3242 (again)

[arthur-adjedj]

WIP

[Kha]

@arthur-adjedj Why is this a draft?

[arthur-adjedj]

I haven't had time to make thorough tests to see if this really solves the issue for good. Knowing the issue popped up once after being already closed, I'd like to make sure this doesn't happen again. I haven't dived into how inductive headers are unified yet, and don't know if some expr mvars aren't expected to be unified later on here. If the expected behavior is that all expr mvars in the headers have already been solved at this point, then this certainly is the right solution, and I'd be happy to get this merged.
I'm not available to investigate this right now, but plan on looking into this in the coming days.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4717 build failed against this PR. (2024-08-09 22:09:05) View Log
• 💥 Mathlib branch lean-pr-testing-4717 build failed against this PR. (2024-08-09 23:16:02) View Log
• 🟡 Mathlib branch lean-pr-testing-4717 build this PR didn't complete normally. (2024-08-12 15:54:00) View Log
• ✅ Mathlib branch lean-pr-testing-4717 has successfully built against this PR. (2024-08-12 16:59:02) View Log
• ✅ Mathlib branch lean-pr-testing-4717 has successfully built against this PR. (2024-08-13 11:46:22) View Log
• ✅ Mathlib branch lean-pr-testing-4717 has successfully built against this PR. (2024-08-16 16:21:39) View Log

[arthur-adjedj]

Despite multiple rebases, the CI on mathlib/batteries seems to keep on failing, and I'm not sure why. Looking at the errors, I don't think the failures are due to the changes made in that PR. I'd like to see at least one CI run work "correctly" on this to ensure no breakage was made, but otherwise, I'm confident this PR makes the right fixes, and will be marking it as ready for review.

[arthur-adjedj]

awaiting-review

[nomeata]

I see likely unwanted differences in

git diff nightly-testing-2024-08-09..lean-pr-testing-4717

With

git checkout -p nightly-testing-2024-08-09 --

I’m removing all changes but the one to the toolchain, let’s give it a shot.

What also often works if our scripts failed to update the pr testing branch through rebases (not uncommon) is to delete that branch in mathlib4 and re-trigger the CI here to recreate it freshly.

[nomeata]

Glad it's green now. Don’t forget to update the PR description, as it will become the commit message.

[arthur-adjedj]

Thanks for the notice ! That's now fixed.

[nomeata]

Looks good to me, I don’t think I understand the intricacies any better than you. Would you mind leaving a comment in the code with whatever insights you have so that the next person looking at the code won’t have to re-discover it?