Strange simpNF error "at a distance"

Stream: mathlib4

[Michael Rothgang]

#21422 adds two new classes to mathlib - and causes the simpNF linter to error in a file far downstream, that is seemingly unrelated. The logs seem to indicate that simplifying the LHS of some lemma now times out, which makes the simpNF fail. That lemma looks completely unrelated to the area I'm modifying, though.

Can anybody help me to even approach this problem - how would I even start to investigate?

[Yaël Dillies]

import Mathlib

set_option diagnostics true in
example : LHS_of_the_lemma_that_simp_nf_times_out_on = sorry := by simp

[Michael Rothgang]

Thanks for the pointer! I tried this (on the relevant branch); it does not seem to yield useful information: putting

set_option diagnostics true in
example (I : Ideal (MvPolynomial σ k)) : vanishingIdeal (zeroLocus I) = sorry := by simp

at the end of Mathlib/RingTheory/Nullstellensatz.lean (i.e., the LHS of the lemma that times out in CI) yields

[diag] Diagnostics ▼
  [reduction] unfolded declarations (max: 156, num: 8): ▶
  [reduction] unfolded instances (max: 975, num: 38): ▼
    [] Field.toCommRing ↦ 975     [] CommRing.toRing ↦ 912     [] Ring.toSemiring ↦ 717     [] CommSemiring.toSemiring ↦ 657     [] EuclideanDomain.toCommRing ↦ 550     [] Field.toEuclideanDomain ↦ 550     [] Semiring.toNonUnitalSemiring ↦ 484     [] NonUnitalSemiring.toNonUnitalNonAssocSemiring ↦ 444     [] Semiring.toNonAssocSemiring ↦ 404     [] NonAssocSemiring.toNonUnitalNonAssocSemiring ↦ 400     [] NonUnitalNonAssocSemiring.toAddCommMonoid ↦ 366     [] CommRing.toCommSemiring ↦ 349     [] Field.toSemifield ↦ 342     [] Semifield.toCommSemiring ↦ 342     [] AddCommMonoid.toAddMonoid ↦ 318     [] DivisionRing.toRing ↦ 269     [] AddMonoid.toAddZeroClass ↦ 88     [] AddZeroClass.toZero ↦ 84     [] MulZeroClass.toZero ↦ 84     [] NonUnitalNonAssocSemiring.toMulZeroClass ↦ 84     [] PartialOrder.toPreorder ↦ 84     [] LinearOrder.toPartialOrder ↦ 80     [] Preorder.toLT ↦ 48     [] Finset.instUnion ↦ 40     [] AddMonoid.toAddSemigroup ↦ 36     [] AddMonoidAlgebra.commRing ↦ 35     [] instCommRingMvPolynomial ↦ 35     [] AddMonoidAlgebra.nonUnitalNonAssocSemiring ↦ 34     [] AddMonoidAlgebra.nonUnitalSemiring ↦ 34     [] AddMonoidAlgebra.nonUnitalCommSemiring ↦ 30     [] Lattice.toSemilatticeSup ↦ 30     [] NonUnitalCommSemiring.toNonUnitalSemiring ↦ 30     [] SemilatticeSup.toPartialOrder ↦ 30     [] Finsupp.instAddCommMonoid ↦ 28     [] Finsupp.instAddMonoid ↦ 28     [] AddCommGroup.toAddGroup ↦ 22     [] AddGroup.toSubNegMonoid ↦ 22     [] SubNegMonoid.toAddMonoid ↦ 22
  [reduction] unfolded reducible declarations (max: 96, num: 11): ▶
  [def_eq] heuristic for solving `f a =?= f b` (max: 60, num: 1): ▶

The instance searches do not traverse anything related to ENorm. (In fact, reverting the ENorm change does not change anything in the output.)

[Jovan Gerbscheid]

I can see that the following is attempted in the simp, and it is very close to a heartbeat error, because adding set_option trace.Meta.synthInstance true makes it get a heartbeat error.

import Mathlib

variable (σ k : Type*) [Field k] [IsAlgClosed k] [Finite σ] (I : Ideal (MvPolynomial σ k))

#synth I.IsPrime

So I'm guessing your PR somehow managed to barely push it over the heartbeat limit.

[Jovan Gerbscheid]

fix: change the order of the arguments in IsArtinianRing.isMaximal_of_isPrime so that [IsArtinianRing R] comes after [p.IsPrime]. (#21449)

[Jovan Gerbscheid]

Because in this case all the computation is wasted on trying to synthesize the IsArtinianRing, while the IsPrime instance is just not available.

[Michael Rothgang]

Thanks a lot for diagnosing this. You're my hero!