Issue with Aesop

Stream: general

[Artie Khovanov]

Aesop is producing terms that blow up from a fairly simple-looking state using only built-in rules. This is making it time out on a task I think it should be able to handle.

MWE:

import Mathlib

set_option trace.aesop true in
theorem fails {R : Type*} [AddMonoid R] [Mul R]
    {a s : R} (ha : a ≠ 0)
    (ih : s ∈ AddSubsemigroup.closure {x | ∃ y, y ≠ 0 ∧ y * y = x}) :
    a * a + s ∈ AddSubsemigroup.closure {x | ∃ y, y ≠ 0 ∧ y * y = x} := by
  aesop -- Tactic `simp` failed with a nested error: (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached

set_option trace.aesop true in
theorem works {R : Type*} [AddMonoid R] [Mul R]
    {a s : R} (ha : a ≠ 0)
    (ih : s ∈ AddSubsemigroup.closure {x | ∃ y, y ≠ 0 ∧ y * y = x}) :
    a * a + s ∈ AddSubsemigroup.closure {x | ∃ y, y ≠ 0 ∧ y * y = x} := by
  apply add_mem -- aesop safe apply 90%
  apply AddSubsemigroup.mem_closure_of_mem -- aesop safe apply 90%
  · aesop
  · aesop

The failing trace (and the succeeding trace) has terms that look like

(fun {s} ↦ ∃ y, ⋂ (_ : {x | ∃ y, ¬y = 0 ∧ y * y = x} ⊆ ↑y), ↑y = fun {s} ↦ ↑(AddSubsemigroup.closure {x | ∃ y, ¬y = 0 ∧ y * y = x}) (a * a + s)) ∈ Set.range fun t ↦ ⋂ (_ : t ∈ {S | {x | ∃ y, ¬y = 0 ∧ y * y = x} ⊆ ↑S}), ↑t

which recursively blow up in every subgoal, tanking the performance. The rule that produces them is
Rule: [75.0000%] unsafe|tactic|global|Aesop.BuiltinRules.applyHyps.

[Artie Khovanov]

(@Jannis Limperg)