fix Known with not-Known Make instances

iris/proofmode/class_instances_make.v

@@ -85,10 +85,14 @@ Proof. by rewrite /MakeOr. Qed.
   to avoid [emp] in goals involving affine BIs, we give [make_affinely_affine]
   a lower cost than [make_affinely_True].
 - [make_affinely_default] adds the modality. This is the default instance since
-  it can always be used, and thus has the highest cost. *)
+  it can always be used, and thus has the highest cost.
+  (For this last point, the cost of the [KnownMakeAffinely] instances does not
+  actually matter, since this is a [MakeAffinely] instance, i.e. an instance of
+  a different class. What really matters is that the [known_make_affinely]
+  instance has a lower cost than [make_affinely_default].) *)
 
 Global Instance make_affinely_affine P :
-  QuickAffine P → MakeAffinely P P | 0.
+  QuickAffine P → KnownMakeAffinely P P | 0.
 Proof. apply affine_affinely. Qed.
 Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 1.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
@@ -105,10 +109,14 @@ Proof. by rewrite /MakeAffinely. Qed.
   it does not really matter since goals in affine BIs typically do not contain
   occurrences of [emp] to start with.
 - [make_absorbingly_default] adds the modality. This is the default instance
-  since it can always be used, and thus has the highest cost. *)
+  since it can always be used, and thus has the highest cost.
+  (For this last point, the cost of the [KnownMakeAbsorbingly] instances does not
+  actually matter, since this is a [MakeAbsorbingly] instance, i.e. an instance of
+  a different class. What really matters is that the [known_make_absorbingly]
+  instance has a lower cost than [make_absorbingly_default].) *)
 
 Global Instance make_absorbingly_absorbing P :
-  QuickAbsorbing P → MakeAbsorbingly P P | 0.
+  QuickAbsorbing P → KnownMakeAbsorbingly P P | 0.
 Proof. apply absorbing_absorbingly. Qed.
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 1.
 Proof.

iris/proofmode/classes_make.v

@@ -35,7 +35,10 @@ evar, then [MakeX] will not instantiate it arbitrarily.
 The reason for this is that if given an evar, these classes would typically
 try to instantiate this evar with some arbitrary logical constructs such as
 [emp] or [True]. Therefore, we use a [Hint Mode] to disable all the instances
-that would have this behavior. *)
+that would have this behavior.
+
+In practice this means that usually only the default instance should use [MakeX],
+and most specialized instances should use [KnownMakeX]. *)
 From iris.bi Require Export bi.
 From iris.prelude Require Import options.