Hint Mode + should not shelve dependent subgoals that only appear in + positions

[samuelgruetter]

We were trying to use Hint Mode + to tell typeclass search that the key and value arguments of a map typeclass are to be considered as inputs, ie typeclass search should only act on goals of the form map K V where both K and V are known, but not on goals of the form map ?key ?value, because this might later lead to surprising error messages if typeclass search picks any map implementation with potentially the wrong key and value types.

Here's a minimized example (in Coq 8.13.2):

Axiom B: Type.

Class word := {
  wrep : Type;
}.
Coercion wrep : word >-> Sortclass.

Class map (key value: Type) := { }.
Hint Mode map + + : typeclass_instances.

Class goal := { }.

Instance mk_goal{word: word}{map: map word B}: goal := { }.

Instance default_word: word. Admitted.
Instance default_map: map default_word B := { }.

Set Printing Implicit.

Check mk_goal.
(* can infer both missing arguments:
@mk_goal default_word default_map
     : goal
*)

Check (_ : goal).
(* fails to infer any arguments, even though mk_goal is in the typeclass hints:
?g : goal
     : goal
where
?g : [ |- goal]
*)

Hint Mode map - - : typeclass_instances.

Check (_ : goal).
(* now it works:
@mk_goal default_word default_map : goal
     : goal
*)

If I use Hint Mode +, Coq fails to infer a (_ : goal), and I have to use Hint Mode - in order to get it to work again.

It is also interesting that Check mk_goal can infer the missing arguments, whereas Check (_: goal) cannot, so why is this?

Using Set Typeclasses Debug Verbosity 2 and comparing the output of the two, I think I found out why:
Check mk_goal first looks for a word, finds default_word, and then looks for a map default_word B, which succeeds as well.
On the other hand, Check (_: goal) starts by finding mk_goal, which opens two subgoals, and since the first subgoal appears as a dependency in the second subgoal, the first subgoal is shelved, and typeclass search works on the second subgoal, which appears as (map ?key B). Now, since we have a Hint Mode map + + : typeclass_instances, the two arguments of map are treated as inputs to typeclass search, and since one of them is unknown, this subgoal is "suspended", and resolution continues "on the remaining goals", but there are none (because the shelved ones are not considered), so it tries one more time, and then sees that it has reached "a fixed point when the set of remaining suspended goals does not change", so no solution is found.
This explanation is derived from combining the output of Set Typeclasses Debug Verbosity 2 with the explanation in this paragraph in the the manual:

The mode hints (see Hint Mode) associated with a class are taken into account by typeclasses eauto. When a goal does not match any of the declared modes for its head (if any), instead of failing like eauto, the goal is suspended and resolution proceeds on the remaining goals. If after one run of resolution, there remains suspended goals, resolution is launched against on them, until it reaches a fixed point when the set of remaining suspended goals does not change.

A simple solution to this problem is to simply do Hint Mode map - - : typeclass_instances, because then typeclass search succeeds on the (map.map ?word byte) subgoal, but then we can't benefit from the Hint Mode + feature any more.

I also tried Set Typeclasses Dependency Order, but that didn't help.

It seems to me that if Hint Mode + is set, after applying mk_goal, typeclass search should detect that even though the first subgoal appears as a depencency of the second subgoal, it must not be shelved, because it only appears in an input (+) position, so solving the second subgoal will not determine the first subgoal.

So at my current state of understanding, I'd tend to call this a bug, but maybe I misunderstood how Hint Mode is supposed to be used, or there is already a flag that makes this example work? Some guidance by typeclass experts would be appreciated :)

[SkySkimmer]

Something like Hint Extern 1 goal => unshelve refine mk_goal : typeclass_instances. instead of the simple eapply @mk_goal-ish behaviour of Instance works.

Possibly related to #13952 but not fixed by it.

[samuelgruetter]

Something like Hint Extern 1 goal => unshelve refine mk_goal : typeclass_instances. instead of the simple eapply @mk_goal-ish behaviour of Instance works.

That makes sense, but if I was to use this as a workaround, I'd have to apply it once for each instance that depends on a map. I'd prefer a workaround/option/flag that I only have to apply (at most) once for each Hint Mode + command, would that be possible?