fix: oversight in isReadOnlyOrSyntheticOpaque

[JovanGerb]

Explanation

In the case that assignSyntheticOpaque := true and the given metavariable is syntheticOpaque and the depth of the metavariable is not the current depth, isReadOnlyOrSyntheticOpaque returns false, even though the metavariable is read-only because of being declared at a smaller depth. This causes the metavariable to (wrongly) be able to be instantiated by isDefEq.

This bug was found at the proof of RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover, which involves a type class synthesis for CommRing ?m.2404, and the synthesis manages to instantiate this metavariable into different values, even though synthInstance? increases the metavariable depth. This synthesis fails after 1 second.

I found the bug while modifying the instance synthesis code: the modified code spent several minutes on this failed synthesis.

Test

The problem can be verified with the test:

run_meta do
  let m ← mkFreshExprMVar (Expr.sort levelOne) MetavarKind.syntheticOpaque
  withAssignableSyntheticOpaque do
  withNewMCtxDepth do
  let eq ← isDefEq m (.const ``Nat [])
  Lean.logInfo m! "{eq}"

this unification used to succeed, giving true, and this fix makes it return false.

Impact on Mathlib

This fix causes a change in the behaviour of congr, convert and friends, which breaks a couple of proofs in mathlib. Most of these are fixed by supplying more arguments.

I fixed these proofs, and benched mathlib. The result is that most files are unaffected, but some files are significantly improved. This is most prominent in Mathlib.RingTheory.Jacobson, where the number of instructions has decreased by 28%. The overall improvement is a 0.3% reduction in instructions.

Zulip message

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4206 build failed against this PR. (2024-05-17 21:18:50) View Log
• 💥 Mathlib branch lean-pr-testing-4206 build failed against this PR. (2024-05-17 21:55:37) View Log
• 💥 Mathlib branch lean-pr-testing-4206 build failed against this PR. (2024-05-17 22:52:40) View Log
• 💥 Mathlib branch lean-pr-testing-4206 build failed against this PR. (2024-05-18 01:10:50) View Log
• 💥 Mathlib branch lean-pr-testing-4206 build failed against this PR. (2024-05-18 04:20:07) View Log
• 💥 Mathlib branch lean-pr-testing-4206 build failed against this PR. (2024-05-18 05:39:41) View Log
• 🟡 Mathlib branch lean-pr-testing-4206 build against this PR was cancelled. (2024-05-18 06:54:03) View Log
• ✅ Mathlib branch lean-pr-testing-4206 has successfully built against this PR. (2024-05-18 07:24:11) View Log
• ✅ Mathlib branch lean-pr-testing-4206 has successfully built against this PR. (2024-05-18 14:04:27) View Log

[JovanGerb]

Do my changes on the Lean-pr-testing-4206 branch automatically get merged on the nightly-testing branch of mathlib?

[kim-em]

@JovanGerb, they don't automatically get merged. I really need to set up a bot that generates notifications about merged PRs that have associated lean-pr-testing-NNNN branches downstream.

In the meantime, if this happens again, the right thing to do is ping me on zulip so I know to look for it!