typeclass eauto should offer an option to not shelve subgoals, similar to simple refine

[patrick-nicodemus]

Is your feature request related to a problem?

Section meta.
  Axiom (A : Type).
  Axiom B : A -> Type.
  Existing Class B.
  Axiom X C : Type.
  Axiom f : X -> A.
  Axiom g : forall (x : X), B (f x).
  Existing Instance g.
  Axiom build_C : forall (a: A), B a -> C.
  Goal C.
    notypeclasses refine (build_C _ _).
    (* Goal is B ?Goal, where the first goal is shelved*)
    typeclasses eauto.
    (* does something like "simple eapply g", which
    creates one shelved goal, X *)
  Abort.
End meta.

Because the hole ?x appears in the type of the goal after we apply the goal is shelved aftersimple eapply g. But now there are no remaining unshelved goals, so typeclasses eauto` regards the main goal as solved.

Proposed solution

It would be useful if there was an option for typeclasses eauto to behave at each application in the proof search more like rapply than like simple eapply, so that the goal X is not shelved. Since X is not a declared typeclass, typeclass search would fail on this goal and backtrack, looking for other instances of type B ?a.

Furthermore, a similar flag should be available for the refine tactic, as a way of controlling the behavior of typeclass search within refine. Currently simple refine has the somewhat unintuitive behavior that although it does not shelve any goals, the applications of simple eapply during typeclass search may shelve goals, so it would be desirable to have a simpler version of simple refine that uses something like simple refine during typeclass search.

Alternative solutions

I guess you could work around this by using Hint Extern: rapply <instance> : typeclass_instances instead of declaring it as an instance.

None of the current settings for typeclasses eauto flags such as best_effort or with typeclass_instances seem to affect the code above.