Make sure that `Make` instances are consistent and "constant time".

A follow up of !836 (merged) to fix two things:

1. Various Make instances still had expensive/recursive/non-constant-time Affine/Absorbing premises.
2. There were some inconsistencies between the instances for the modalities and the conjunctions, for example, where emp ∧ P was turned into P if P is affine, but <affine> P remained just <affine> P regardless of whether P is affine.

To fix these things, this MR introduces classes QuickAffine and QuickAbsorbing. These classes are aliases for [Affine] and [Absorbing], but their instances are severely restricted. They only inspect the top-level symbol or check if the whole BI is affine---thus fixing (1). Aside, we use these classes for both all Make instances, thus ensuring consistent behavior and fixing (2).

As a consequence of this MR, one test fails:

Lemma demo_3 P1 P2 P3 :
  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.

What happens is that after framing, the subterm (P3 ∧ ⌜x = 0⌝) ∨ P3 is turned into (emp ∧ ⌜x = 0⌝) ∨ emp. Before, the instance for ∨ would be fired, since emp ∧ ⌜x = 0⌝ is affine, thus turning the whole subterm into emp. I don't see how we can support this example without performing a recursive search to check if terms are affine.

That said, this test seems artificial/contrived, so I am not bothered that it fails. This MR is an improvement for Iron, due to fixing (2), a single iSplit can be removed somewhere.