help with diagnosis of slow declaration

Stream: mathlib4

[Kevin Buzzard]

Apologies for the large MWE; it's mathlib-only but to minimise it from FLT I needed 150 lines of API for restricted products.

I find this code pretty weird (although I've seen this phenomenon before; I just want to understand it better). After the boilerplate there are two declarations at the end. The last-but-one declaration is padicRingEquiv:

noncomputable
def padicRingEquiv : FiniteAdeleRing (𝓞 ℚ) ℚ ≃+* Πʳ (p : Nat.Primes), [ℚ_[p], subring p] where
  __ := [something]

which is a ring isomorphism between two rings, and this compiles very quickly. The last declaration is padicEquiv:

noncomputable
def padicEquiv : FiniteAdeleRing (𝓞 ℚ) ℚ ≃ₐ[ℚ] Πʳ (p : Nat.Primes), [ℚ_[p], subring p] where
  __ := [the same thing]
  commutes' q := by [some proof]

which is a $\mathbb{Q}$-algebra isomorphism between the same rings, and the construction is simply the same ring equiv and then a proof that the $\mathbb{Q}$-algebra structures are compatible.

If I sorry the commutes' proof then padicEquiv compiles really quickly, and if I fill in the proof then it compiles super-slowly. But the problem isn't the proof, which the profiler indicates is still compiling quickly. The problem is what happens afterwards: the orange bars disappear (in particular the orange bars on the proof disappear) apart from the one-line bar on the def padicEquiv line and it stays for 30 seconds. My understanding of what is going on is that some part of the system accepts the declaration, and then the kernel checks it and the kernel has a really hard time convincing itself that the declaration is actually OK. The profiler says

[Elab.async] [0.061745] Lean.addDecl ▼
  [Kernel] [0.061631] ✅️ typechecking declarations [padicEquiv._proof_1]
[Elab.async] [0.066556] Lean.addDecl ▼
  [Kernel] [0.066531] ✅️ typechecking declarations [padicEquiv._proof_2]
[Elab.async] [29.744237] Lean.addDecl ▼
  [Kernel] [29.744206] ✅️ typechecking declarations [padicEquiv._proof_3]
[Elab.async] [0.048560] Lean.addDecl ▼
  [Kernel] [0.048416] ✅️ typechecking declarations [padicEquiv]

so clearly the issue is with padicEquiv._proof_3. I've tried #printing the proof but it doesn't round trip.

What are the possible causes for such a situation? Am I abusing defeq somewhere? How does one go about debugging this? All I can get from the profiler is "something is taking 29 seconds on a fast machine". Are we now getting to the point where there are tools which I can use which give some kind of indication as to what exactly is being abused in this definition?

[Aaron Liu]

maybe try inserting as_aux_lemma => in the middle of the proof I've found that it helps sometimes

[Aaron Liu]

oh you have code I can try stuff on it

[Aaron Liu]

it becomes fast if I replace the final simp with simp -implicitDefEqProofs

[Aaron Liu]

so probably you have a rfl-proof that's slow when you instantiate it

[Aaron Liu]

this has caused problem before #lean4 > `deep recursion detected` with 16-bit bitvec's @ 💬

[Kevin Buzzard]

Aaron Liu said:

it becomes fast if I replace the final simp with simp -implicitDefEqProofs

Oh nice find! Thanks! So I'll just do this and ignore the issue :-) Or will it bite me again later?

[Aaron Liu]

I think it might prevent simp from calling dsimp in certain places, but it shouldn't have any negative consequences if it works