Slow code generation for an instance declaration

[genereuxx]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following instance declaration of Int2.Field, code generation doesn't seem to terminate.

Context

This is an issue encountered since the switch from lean3 to lean4. It was tested on two different computers, both of them macos, and also live.lean-lang.org.

Notes

• I have tried to make an mwe that doesn't import Mathlib but it requires a little bit a work as Field depends on many things.
• Potential culprits are fields describing natural actions of rational number on fields. I could make an mwe without them and the code generation was instant. I am a not 100% sure as I had to prune other things than just those fields.
• Marking this instance declaration as noncomputable lets the file build normally.
• Removing proofs inside the instance declaration and proving them as lemmas makes the file build normally. (e.g. mul_assoc)

Steps to Reproduce

import Mathlib.Algebra.Field.Defs

inductive Int2 : Type
  | zero
  | one

def Int2.add : Int2 → Int2 → Int2
  | Int2.zero, a         => a
  | Int2.one,  Int2.zero => Int2.one
  | Int2.one,  Int2.one  => Int2.zero

instance Int2.Add : Add Int2 := Add.mk Int2.add

instance Int2.Zero : Zero Int2 := Zero.mk Int2.zero

instance Int2.Neg : Neg Int2 := Neg.mk fun a ↦ a

instance Int2.AddGroup : AddGroup Int2 :=
  { add            := (· + ·)
    zero           := 0
    neg            := fun a ↦ a
    add_assoc      :=
      by
        intro a b c
        cases a <;>
          cases b <;>
          cases c <;>
          rfl
    zero_add       :=
      by
        intro a
        cases a <;>
          rfl
    add_zero       :=
      by
        intro a
        cases a <;>
          rfl
    neg_add_cancel :=
      by
        intro a
        cases a <;>
          rfl
    nsmul         := nsmulRec
    zsmul         := zsmulRec }

def Int2.mul : Int2 → Int2 → Int2
  | Int2.one,  a => a
  | Int2.zero, _ => Int2.zero

instance Int2.Field : Field Int2 :=
  { Int2.AddGroup with
    one            := Int2.one
    mul            := Int2.mul
    inv            := fun a ↦ a
    add_comm       :=
      by
        intro a b
        cases a <;>
          cases b <;>
          rfl
    exists_pair_ne :=
      by
        apply Exists.intro Int2.zero
        apply Exists.intro Int2.one
        simp
    zero_mul       :=
      by
        intro a
        rfl
    mul_zero       :=
      by
        intro a
        cases a <;>
          rfl
    one_mul        :=
      by
        intro a
        rfl
    mul_one        :=
      by
        intro a
        cases a <;>
          rfl
    mul_inv_cancel :=
      by
        intro a h
        cases a
        { apply False.elim
          apply h
          rfl }
        { rfl }
    inv_zero       := by rfl
    mul_assoc      := by
      intro a b c
      cases a <;>
      cases b <;>
      cases c <;>
      rfl
    mul_comm       :=
      by
        intro a b
        cases a <;>
          cases b <;>
          rfl
    left_distrib   :=
      by
        intro a b c
        cases a <;>
          cases b <;>
          rfl
    right_distrib  :=
      by
        intro a b c
        cases a <;>
          cases b <;>
          cases c <;>
          rfl
    nnqsmul        := _
    qsmul          := _ }

Expected behavior: The file builds without issue.

Actual behavior: The file never finishes loading.

Versions

4.15.0-rc1
macOS 13.4 (22F66) (live.lean-lang.org has also been tried)