destructProducts can add dependencies on implicit variables

[girving]

Here's (arguably) a bug which may be difficult to fix:

import Aesop
import Mathlib.Data.Nat.Basic

variable {bad : ℕ × ℕ}

set_option trace.aesop true in  -- Shows that `destructProducts` is the culprit
lemma unused {n : ℕ} {p q : ℕ → Prop} (pq : ∀ n, p n → q n) (pn : p n) : q n := by
  aesop (config := { enableSimp := false })  -- Ban `simp` so `destructProducts` has time to fire

#check unused  -- unused {bad : ℕ × ℕ} {n : ℕ} {p q : ℕ → Prop} (pq : ∀ (n : ℕ), p n → q n) (pn : p n) : q n

I'm using aesop close a lemma unused that makes no mention of bad, and bad doesn't occur in the final proof (at least in spirit). However, during aesop's search, it uses destructProducts to take bad apart into components, and 💥, now the first argument of unused is {bad : ℕ × ℕ}.

Zulip thread

[girving]

Possibly this needs to wait on more general changes to implicit variables: leanprover/lean4#2452.