Timeout in simp only due to decide:=true

Stream: general

[Eric Wieser]

This causes a timeout unless you tell simp only not to decide:

import Mathlib.Order.LocallyFinite
import Mathlib.Data.Int.Interval
import Mathlib.Tactic
def square (m : ℤ) : Finset (ℤ × ℤ) :=
  ((Finset.Icc (-m) (m)) ×ˢ (Finset.Icc (-m) (m))).filter fun x =>
    max x.1.natAbs x.2.natAbs = m

lemma square_eq (n : ℕ) : square n.succ =
    Finset.Icc ((-n.succ,-n.succ) : ℤ × ℤ) (n.succ,n.succ) \
    Finset.Icc (-(n),-(n)) (n,n) := by
  induction n with
  | zero =>
    simp only -- times out
    -- need `simp (config := {decide := false}) only`
    sorry
  | succ n ih =>
    sorry

It's not clear to me what makes this hard to decide; rfl closes the goal instantly.

[Scott Morrison]

There have been several aborted attempts at changing the default in simp to decide := false. Maybe it's time for someone to try again.