The following theorem fails to type-check in the kernel:

theorem y : id (Nat.gcd 314159 10000) = Nat.gcd 314159 10000 := rfl
-- (kernel) deep recursion detected

Presumably this happens because we provide a too constructive proof of Acc (· < ·) 314159, which allows the kernel to unfold the definition 314159 times. (theorized by @digama0)

as reported by @thorimur