`destructProducts` can add dependencies on implicit variables

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 :boom:, now the first argument of unused is {bad : ℕ × ℕ}.

Zulip thread

leanprover-community / aesop

`destructProducts` can add dependencies on implicit variables #104