Prevent [finite_countable] from solving unrelated evars

Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw. Fixes #160 (closed).

The problem is that Hint Immediate translates to (something like) simple apply @finite.finite_countable ; trivial in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.

Missing (I assume):

• trivial only uses hints with cost 0, but typeclasses eauto 0 does not appear to work, so typeclasses eauto 1 is the closest thing I see. This might be a problem.
• Testcase
• Changelog? Probably not needed since this is a bugfix
• Mention this in upstream issue.

Also see Coq issue https://github.com/coq/coq/issues/16893.

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]. *)

[Ralf Jung]

Note, iSolveTC does not exist any more, it got moved to std++

[Paolo G. Giarrusso]

Ack:

-See docs for Iris's [iSolveTC] for further background.
+See docs for [tc_solve] for further background.

But I thought this MR was essentially rejected in favor of waiting for a Coq fix to https://github.com/coq/coq/issues/16893 ? If you're interested then please let me know.

[Ralf Jung]

I'm not sure, I don't really understand the work-around.^^