Prevent [finite_countable] from solving unrelated evars

stdpp/base.v

@@ -198,6 +198,19 @@ Global Existing Instance TCDiag_diag.
 Global Hint Mode TCDiag ! ! ! - : typeclass_instances.
 Global Hint Mode TCDiag ! ! - ! : typeclass_instances.
 
+(** Perform at most one step of typeclass search, without affecting unrelated goals due to
+https://github.com/coq/coq/issues/6583.
+
+Useful for emulating [Hint Immediate] during TC search. Example (from [finite.v]):
+<<
+Global Hint Extern 1 (Countable _) =>
+  notypeclasses refine finite_countable; solve_tc_onestep : typeclass_instances.
+>>
+See docs for Iris's [iSolveTC] for further background.
+ *)
+Ltac solve_tc_onestep :=
+  solve [once (typeclasses eauto 1)].
+
 (** Given a proposition [P] that is a type class, [tc_to_bool P] will return
 [true] iff there is an instance of [P]. It is often useful in Ltac programming,
 where one can do [lazymatch tc_to_bool P with true => .. | false => .. end]. *)

stdpp/finite.v

@@ -25,7 +25,8 @@ Next Obligation.
   rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
   destruct (list_find_Some (x =.) xs i y); naive_solver.
 Qed.
-Global Hint Immediate finite_countable : typeclass_instances.
+Global Hint Extern 1 (Countable _) =>
+  notypeclasses refine finite_countable; solve_tc_onestep : typeclass_instances.
 
 Definition find `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} : option A :=
   list_find P (enum A) ≫= decode_nat ∘ fst.