tryeach.v

Definition bag := nat.
Existing Class bag.
Instance : bag := 5.
Instance : bag := 6.
Instance : bag := 7.
Instance : bag := 8.
Instance : bag := 9.

Ltac tryeach cls t :=
  let picked := fresh "picked" in
  unshelve (idtac; let v := open_constr:(let picked : cls := _ in _) in exact v);
    [ typeclasses eauto |
      let picked := eval unfold picked in picked in
      let picked := eval unfold picked in picked in
      t picked
    ];
  clear picked.

Goal exists x, x=7.
  eexists.
  Set Typeclasses Debug.
  tryeach bag ltac:(fun x => exact (eq_refl x)).
Qed.