feat: set priority in monadic class instances

[JovanGerb]

This PR adds the high priority to some instances with monad transformers, most notably to MonadExceptOf ε (ExceptT ε m). This means that in ExceptT α MetaM, throw will throw the α instead of the Exception.

These instances now have high priority:

• MonadReaderOf ρ (ReaderT ρ m)
• MonadWithReaderOf ρ (ReaderT ρ m)
• MonadStateOf σ (StateT σ m)
• MonadStateOf σ (EStateT ε σ m)
• MonadExceptOf ε (ExceptT ε m)
• MonadExceptOf ε (EStateT ε σ m)
• MonadExceptOf ε (ExceptCpsT ε m)
• MonadCallStackOf κ (CallStackT κ m)
• MonadCycleOf κ (CycleT κ m)

And these instance now have low priority:

• MonadExceptOf Unit (OptionT m)
• [MonadExcept ε m] {α : Type v} : OrElse (m α)

The last one makes sure that the OrElse instance has lower priority than instOrElseOfAlternative (this change doesn't affect the synthesis order, because the order of the files in which the instances were declared was already 'correct').

In Prelude.lean, instead of setting the priority to high or low, it has to be set to 10000 or 100, which is the same.

The increased priority of MonadExceptOf ε (ExceptT ε m) affected a few files that had to be fixed.

Closes #4212

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-09 19:19:03) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 99070bf304931c4ff22e31d6943e72858af65800 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-04 16:09:35)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 906aa1be4b29c423a97d6909bc315fa236529a79 --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-16 15:57:56)

[JovanGerb]

The test that broke had the number from the name generator offset by 8.
The line local infix:65 (priority := high) "*" => mul previously used to increment the name generator by 1560, and now this became 1568. I don't understand where these 8 extra names come from, but I equally don't understand why a simple infix declaration needs to use so ridiculously many names.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-09 22:09:04) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-10 23:25:37) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5291 has successfully built against this PR. (2024-09-11 01:25:32) View Log

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6aa0c46b04e78011af49eb4f272ea07e9173e584 --onto adfd6c090ef7d6bdcc8f69c5dd6f919b1b71cab3. (2024-09-12 11:37:11)

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 90ac0f7.
There were significant changes against commit 6aa0c46:

  Benchmark   Metric       Change
  ========================================
- rbmap       task-clock     2.2% (23.0 σ)
- rbmap       wall-clock     2.3% (24.8 σ)

[kim-em]

I'm concerned that there's an unexplained performance regression revealed by !bench. Can you determine if that is real or not, and if so try to localize the exact change that causes it?

[JovanGerb]

Can you benchmark it again? There seems to be nothing in the rbmap.lean benchmarking test related to the changes in this PR.

[JovanGerb]

@kim-em, can you have a look at this one again? I don't know how to verify that the slowdowns weren't real.

I've now updated the PR to the new toolchain, but I'm not sure how to get it to build the accompanying Batteries and Mathlib.

[kim-em]

@JovanGerb, you'll need to rebase this PR onto origin/nightly-with-mathlib. Then you can run !bench again.

[JovanGerb]

It seems I don't understand how git works, so I've opened it as a new PR: #6725

[JovanGerb]

@JovanGerb, you'll need to rebase this PR onto origin/nightly-with-mathlib. Then you can run !bench again.

I tried to !bench the new PR, but it seems that I still cannot do that myself.

[Kha]

Instructions at least are unchanged, most likely noise