feat: improve error messages for level metavariables

[JovanGerb]

When a def/theorem contains a metavariable, an error is thrown at the correct syntax, showing the context of the metavariable, and some text depending on whether the metavariable is implicit, or a placeholder.

However, when there is a universe metavariable, this doesn't work as nicely, and an error is thrown at the start of the (mutual) definition. This is confusing because it doesn't point the user to the code causing the error, and it can confuse people who don't know much about universe levels.

So, I've implemented errors for universe levels analogously to expression metavariables. And when there are errors for both kinds of metavariables, then both errors are thrown, with the expression metavariable errors being logged first.

The errors for expression metavariables start with

don't know how to synthesize implicit argument
don't know how to synthesize placeholder

So analogously the errors for universe metavariables start with

don't know how to synthesize universe {levelName} of '{constName}'
don't know how to synthesize universe placeholder

I would suggest to replace don't know how to with failed to as it means the same, but is shorter. I also would suggest using the word infer instead of synthesize, because we don't was to confuse this with type class synthesis errors.

To implement this, I removed the code that turns level metavariables into level parameters in the values of the predefinitions, and I removed the function checkForHiddenUnivLevels, which is what throws the current universe errors. Then, I extended the function logUnassignedUsingErrorInfos to also include the new level metavariable errors.

A nice side effect is that the silently failing example at #2226 now isn't silent anymore. This is because the error thrown at checkForHiddenUnivLevels wasn't visible (due to being a throwError, and not a logError, as evidenced by #4463)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4450 build failed against this PR. (2024-06-14 02:17:22) View Log

[JovanGerb]

Should I create a new PR in order to get mathlib CI working again? (I merged with a more recent version of nightly-with-mathlib)

[Kha]

Thank you for the PR but this is a lot of new code for a somewhat niche issue. We are not currently ready to maintain this code and as always, starting with smaller PRs further away from the foundation is the way to go.