New stack overflow on simps dealing with UInt64

[girving]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

After updating to leanprover/lean4:v4.6.0-rc1, I get new crashes when using simp. Here is a no-import example:

theorem UInt64.add_def (a b : UInt64) : a + b = ⟨a.val + b.val⟩ := rfl

theorem UInt64.toNat_add (m n : UInt64) : (m + n).toNat = (m.toNat + n.toNat) % UInt64.size := by
  simp only [UInt64.toNat, UInt64.add_def]
  simp only [HAdd.hAdd, Add.add, Fin.add, Nat.add_eq]

which if run in VSCode results in

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

Context

I got several of these crashes in my https://github.com/girving/ray repo after updating Lean and Mathlib (4 or 5 total), all in code proving things about UInt64 or an Int64 type built on top of UInt64.

Zulip discussion

Steps to Reproduce

1. Try to build the example above.

Expected behavior: It builds.

Actual behavior: It crashes with a stack overflow.

Versions

% lean --version
Lean (version 4.6.0-rc1, aarch64-apple-darwin, commit 5cc0c3f145ff, Release)

macOS 14.2.1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[fpvandoorn]

I also had this issue when updating to latest Lean/mathlib recently. The issue seems to be with having a looping set of simp-lemmas (in your example, Nat.add_eq conflicts with unfolding HAdd/Add).

[fpvandoorn]

Here are some examples that show roughly the boundary between the panic occurring and not occuring.

namespace error

def a : Nat := 0
@[simp] theorem h1 : 0 = a := rfl
@[simp] theorem h2 : a = 0 := rfl

example (x : Nat) : x = 0 := by
  simp only [h1, h2] -- causes a panic

end error

namespace works
def a : Bool := false
@[simp] theorem h1 : a = false := rfl
@[simp] theorem h2 : false = a := rfl

example (x : Bool) : x = false := by
  simp only [h1, h2] -- gives a normal error (expected)
end works

namespace also_works

def a : Nat := 0
def b : Nat := 0
@[simp] theorem h1 : b = a := rfl
@[simp] theorem h2 : a = b := rfl

example (x : Nat) : x = a := by
  simp only [h1, h2] -- gives a normal error (expected)

end also_works

[leodemoura]

Stack overflow does not happen anymore. The new error message is

error: tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information

If we add set_option diagnostics true, Lean now produces information that is sufficient to diagnosing the loop.
I am marking it as closing soon.

[fpvandoorn]

Yes, the issue is solved on my side