Extremely verbose aesop panic

Stream: general

[Eric Wieser]

The following code (in mathlib master) produces 1595 panics:

import Mathlib.Data.Finset.Basic

example
    (n : List ℕ → List ℕ)
    (hn : ∀ A, n A = A.filter (fun p => true)) :
    0 ≤ 0 := by
  exact (0, not_not.1 $ by aesop)

all of which are

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:920:14: unknown metavariable

[Eric Wieser]

Waiting for an LSP message eventually gives

aesop: internal error: extracted proof has metavariables.
  Proof: Eq.mpr (id Init.Classical._auxLemma.2)
    (?m.2081 (Eq.mp (forall_congr fun A => congrArg (Eq (n A)) (List.filter_true A)) h₂'))
  Unassigned metavariables: [_uniq.6175, _uniq.6176]

[Eric Wieser]

It seems this is somehow caused by

@[simp, aesop safe apply (rule_sets := [finsetNonempty])]
theorem singleton_nonempty (a : α) : ({a} : Finset α).Nonempty :=
  ⟨a, mem_singleton_self a⟩

as the above example panics only after that lemma

[Eric Wieser]

Minimized to be mathlib-free at https://github.com/leanprover-community/aesop/issues/153