Deep recursion error depending on order of multiplication

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

@sgouezel discovered that defining npow x (n + 1) = npow x n * x can cause a "deep recursion detected at replace" error, while npow x (n + 1) = x * npow x n does not. As a consequence, we have to define npow and nsmul to multiply/add on the left. The definition of rat.mul does not look asymmetrical either, so I'm not quite sure where the asymmetry is coming from. Although we have a workaround, this is surprising and annoying behaviour, and might cause similar difficult-to-diagnose errors in the future.

Steps to Reproduce

Example code (using mathlib f9c787da6):

import data.rat.basic

def mypow1 {α : Type*} [comm_semiring α] : ℕ → α → α
| 0 x := 1
| (n+1) x := mypow1 n x * x

def haspow1 : has_pow ℚ ℕ := ⟨λ x n, mypow1 n x⟩
def my_op1 {α : Type*} [comm_semiring α] : α → α := λ a, mypow1 10000 a
lemma foo1 (a : ℚ) : my_op1 a = @has_pow.pow ℚ ℕ haspow1 a 10000  := rfl -- deep recursion detected at replace

def mypow2 {α : Type*} [comm_semiring α] : ℕ → α → α
| 0 x := 1
| (n+1) x := x * mypow2 n x

def haspow2 : has_pow ℚ ℕ := ⟨λ x n, mypow2 n x⟩
def my_op2 {α : Type*} [comm_semiring α] : α → α := λ a, mypow2 10000 a
lemma foo2 (a : ℚ) : my_op2 a = @has_pow.pow ℚ ℕ haspow2 a 10000  := rfl -- works

-- The error also occurs when defining `mypow3` tail-recursively:
def mypow3 {α : Type*} [comm_semiring α] : ℕ → α → α → α
| 0 x acc := acc
| (n+1) x acc := mypow3 n x (acc * x)

def haspow3 : has_pow ℚ ℕ := ⟨λ x n, mypow3 n x 1⟩
def my_op3 {α : Type*} [comm_semiring α] : α → α := λ a, mypow3 10000 a 1
lemma foo3 (a : ℚ) : my_op3 a = @has_pow.pow ℚ ℕ haspow3 a 10000 := rfl -- deep recursion detected at replace

Expected behavior: lemmas foo1, foo2 and foo3 type-check succesfully

Actual behavior: only foo2 type-checks, the others fail

Reproduces how often: foo1 and foo3 break for large enough exponents (≥10000 in this testcase), foo2 stays working for much larger exponents (three times as many digits).

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

$ lean --version
Lean (version 3.28.0, commit 5a3bb32c05bc, Release)
$ uname -a
Linux $HOST 5.11.11-arch1-1 #1 SMP PREEMPT Tue, 30 Mar 2021 14:10:17 +0000 x86_64 GNU/Linux

Reproduce the three minimal definitions and lemmas from the issue with Lean 3.28, starting by comparing the multiplication orders and the tail-recursive case. Trace the elaboration or replacement path that emits “deep recursion detected at replace”; done means all three foo lemmas type-check for the reported large exponent without relying on operand order.