assertInstancesCommute loops when there are several unnamed assumptions

[dwrensha]

Reported by @YaelDillies:

• [Merged by Bors] - feat: Positivity extension for Finset.prod mathlib4#9365 (comment)
• [Merged by Bors] - feat: Positivity extension for Finset.prod mathlib4#9365 (comment)

[thorimur]

I'm not sure this is actually about unnamed assumptions per se. I think it's because let _ ← ... elaborates differently from let _i ← ..., and the former instead effectively becomes let <newname> := .... Note that writing let _i := ← synthInstanceQ ... causes the same maximum recursion depth issue in the linked PR; also note that the local context contains let decls (displaying :=) in both problematic cases.

MWE:

import Lean
import Qq

open Qq Lean.Meta

example : MetaM Unit := do
  have P : Q(Prop) := sorry
  let x := ← synthInstanceQ q(Decidable $P) -- or `let _ ← synthInstanceQ ...`
  assertInstancesCommute -- maximum recursion depth reached