TC search considers Opaque constants transparent & Hint Opaque solution requires annoying workaround

[Janno]

Description of the problem

In the example below one can see that a constant marked Opaque is considered transparent for TC search and that one cannot simply mark it Hint Opaque without first making it Transparent (and then making it Opaque again afterwards). I suppose both of these are bugs but the latter wouldn't be a big issue if the TC search considered Opaque constants Hint Opaque by default.

Class Inh (A : Prop) := inh : A.

Definition True' : Prop := True.
Opaque True'.

Instance Inh_True' : Inh True' | 1 := id I.
Instance Inh_True : Inh True | 100 := I.

Set Typeclasses Debug.
Set Typeclasses Debug Verbosity 2.

Goal True.
  apply inh.                (* wrongly picks [Inh_True'] *)
Qed.

Existing Instance Inh_True | 0.

Goal True'.
  apply inh.                    (* wrongly picks [Inh_True] *)
Qed.

Existing Instance Inh_True | 100. (* Restore initial instance priorities *)

(* Cannote declare [True'] opaque for TC search because it is already opaque :( *)
Fail Hint Opaque True' : typeclass_instances.

(* But we can change that. *)
Transparent True'.
Hint Opaque True' : typeclass_instances.
Opaque True'.

Goal True.
  apply inh.                (* correctly picks [Inh_True] *)
Qed.

Existing Instance Inh_True | 0.

Goal True'.
  apply inh.                    (* correctly picks [Inh_True'] *)
Qed.

Let me know if I should pull these apart into two issues.

Coq Version

8.11, master

[Janno]

@ppedrot any chance this is as easy to fix as the one about axioms?

[ppedrot]

This has strong interactions with the stuff I've been working on recently, so expect progress on this soon.

[SkySkimmer]

#12573 may help