feat: apply’s error message should show implicit arguments as needed

[nomeata]

luckily the necessary functionality already exists in the form of
addPPExplicitToExposeDiff. But it is not cheap, and we should not run this code
when the error message isn’t shown, so we should do this lazily.

We already had MessageData.ofPPFormat to assemble the error message lazily, but it
was restricted to returning FormatWithInfo, a data type that doesn’t admit a nice
API to compose more complex messages (like Format or MessageData has; an attempt to
fix that is in #3926).

Therefore we split the functionality of .ofPPFormat into .ofFormatWithInfo and .ofLazy,
and use .ofLazy to compute the more complex error message of apply.

Fixes #3232.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 75e68e7565708361e117c5f56b66fdbe013de667 --onto 1c20b5341956fb77fcf2c2601e64075e51d5f858. (2024-04-16 18:01:06)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 75e68e7565708361e117c5f56b66fdbe013de667 --onto d3e004932c1f5ac3946850692940512d381c7634. (2024-04-18 20:36:23)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 22ce2fea9b93b53a338114dde67c27e881aa1b24 --onto 62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a. (2024-04-22 12:31:05)
• ✅ Mathlib branch lean-pr-testing-3929 has successfully built against this PR. (2024-05-08 11:27:37) View Log
• ✅ Mathlib branch lean-pr-testing-3929 has successfully built against this PR. (2024-05-08 12:09:06) View Log
• 🟡 Mathlib branch lean-pr-testing-3929 build against this PR was cancelled. (2024-05-17 09:08:54) View Log
• 💥 Mathlib branch lean-pr-testing-3929 build failed against this PR. (2024-05-17 09:14:04) View Log
• 🟡 Mathlib branch lean-pr-testing-3929 build against this PR was cancelled. (2024-05-17 19:34:45) View Log
• 🟡 Mathlib branch lean-pr-testing-3929 build this PR didn't complete normally. (2024-05-17 20:30:39) View Log

[Vtec234]

Hi! I have re-fetched the pretty-printing infrastructure into my mental cache and I think I agree that this is the right-est solution. Just to confirm though, why did you discard #3926? Is it because that still doesn't allow for lazily-produced MessageData, only FormatWithInfos, and furthermore introduced yet another appendable message type?

[nomeata]

Hi! I have re-fetched the pretty-printing infrastructure into my mental cache and I think I agree that this is the right-est solution.

Thanks! It's good to have a second pair of eyes!

Just to confirm though, why did you discard #3926? Is it because that still doesn't allow for lazily-produced MessageData, only FormatWithInfos, and furthermore introduced yet another appendable message type?

Yes! The way FormarWithInfo works makes appending then rather tedious (shifting indices), and it's not just appending but also string interpolation that would have to be duplicated. It didn't seem desirable to have three similar data structures around.

[Vtec234]

Now mathlib fails, and searching for the error message on the phone is annoying. But probably nothing worrying and we can merge?

I have made adaptations to batteries and to mathlib4, and written a changelog. If these build, I think we should be good.

But, it would still be good to benchmark as MessageData is used quite ubiquitously.

[Vtec234]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8316658.
There were no significant changes against commit 883a3e7.

[nomeata]

Mathlib seems to be happy as well, thanks. Any last thoughts before I press the button?

[Vtec234]

LGTM!

[nomeata]

Thanks for your help getting this over the finishing line.

We should probably now make the omega error lazy. I'm curious if that will show up in mathlib.