Per-class typeclass transparency data

[JasonGross]

Sometimes I want to set transparency data per-instance or per-class. For example if I have a class Foo := foo : Bar, I may want it to be the case that hints from Bar don't apply when the goal is Foo (even more importantly, Foo may have phantom parameters that should block unification), but when resolving hints for other classes, I want the hints to apply even if their Foo argument is a context variable whose type is Bar.

Related to #14126

[JasonGross]

Example:

From Coq Require Import String.
Export StringSyntax.
Definition with_default (name : string) {A} (x : A) := A.
#[global] Arguments with_default _ {_} _, _ _ _.
Existing Class with_default.
#[global] Typeclasses Opaque with_default.
#[global] Hint Opaque with_default : typeclass_instances.
Ltac fill_default _ :=
  lazymatch goal with
  | [ |- @with_default ?name ?A ?x ]
    => match goal with
       | [ H : @with_default ?name' ?A' _ |- _ ] => constr_eq A A'; constr_eq name name'; fail 1
       | _ => exact x
       end
  end.
#[global] Hint Extern 0 (with_default _ _) => fill_default () : typeclass_instances.
#[global] Hint Extern 0 => lazymatch goal with
                           | [ |- with_default _ _ ] => fail
                           | _ => progress unfold with_default
                           end : typeclass_instances.


Class Foo (x : with_default "foo" bool true) := foo : True.
Instance: forall x, Foo x := fun x => I.
Fail Instance: forall x : bool, Foo x := _. (* should succeed without Fail *)
Definition check_no_assum : with_default "foo" bool true -> with_default "bar" bool true := _.
Check eq_refl : check_no_assum = fun x => true. (* succeeds *)
Section __1.
  #[local] Typeclasses Transparent with_default. (* should be for everything but [with_default] goals *)
  Instance: forall x : bool, Foo x := _. (* succeeds *)
  Definition check_no_assum1 : with_default "foo" bool true -> with_default "bar" bool true := _.
  Fail Check eq_refl : check_no_assum1 = fun x => true. (* should succeed without Fail *)
End __1.
Section __2.
  #[local] Hint Transparent with_default : typeclass_instances. (* should be for everything but [with_default] goals *)
  Instance: forall x : bool, Foo x := _. (* succeeds *)
  Definition check_no_assum2 : with_default "foo" bool true -> with_default "bar" bool true := _.
  Fail Check eq_refl : check_no_assum2 = fun x => true. (* should succeed without Fail *)
End __2.

[JasonGross]

Even more nuanced, it might be useful to be able to mix transparency data with Hint Mode, per-class and even per-instance. Something like "this slot should treat all constants as opaque, while this other slot should treat all constants as transparent". There's a bit of a question of priority of transparency info, though.