From 5491cacb9eac9e46e0225cb3f3ae540ade17ae98 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 10:15:35 +0200
Subject: [PATCH] Make `BiLaterContractive` a class instead of a notation.

This avoids unnecessary search on failed attempts. `Contractive` is notation for
`Proper`, so previously, this caused a bunch of setoid instances to be used. In
turn, this resulted in TC debug output that is hard to read.
---
 iris/base_logic/bi.v | 2 +-
 iris/bi/extensions.v | 4 ++--
 iris/bi/monpred.v    | 2 +-
 iris/si_logic/bi.v   | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 2ff462f72..5f8257722 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -165,7 +165,7 @@ Global Instance uPred_pure_forall M : BiPureForall (uPredI M).
 Proof. exact: @pure_forall_2. Qed.
 
 Global Instance uPred_later_contractive {M} : BiLaterContractive (uPredI M).
-Proof. apply later_contractive. Qed.
+Proof. exact: @later_contractive. Qed.
 
 Global Instance uPred_persistently_impl_plainly M : BiPersistentlyImplPlainly (uPredI M).
 Proof. exact: persistently_impl_plainly. Qed.
diff --git a/iris/bi/extensions.v b/iris/bi/extensions.v
index e54908d50..f665cae03 100644
--- a/iris/bi/extensions.v
+++ b/iris/bi/extensions.v
@@ -25,8 +25,8 @@ Class BiLöb (PROP : bi) :=
 Global Hint Mode BiLöb ! : typeclass_instances.
 Global Arguments löb_weak {_ _} _ _.
 
-Notation BiLaterContractive PROP :=
-  (Contractive (bi_later (PROP:=PROP))) (only parsing).
+Class BiLaterContractive (PROP : bi) :=
+  later_contractive :> Contractive (bi_later (PROP:=PROP)).
 
 (** The class [BiPersistentlyForall] states that universal quantification
 commutes with the persistently modality. The reverse direction of the entailment
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index fa923f412..f5a8e0d07 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -728,7 +728,7 @@ Section bi_facts.
 
   Global Instance monPred_later_contractive :
     BiLaterContractive PROP → BiLaterContractive monPredI.
-  Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
+  Proof. intros ? n. unseal=> P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
   Global Instance monPred_bi_löb : BiLöb PROP → BiLöb monPredI.
   Proof. rewrite {2}/BiLöb; unseal=> ? P HP; split=> i /=. apply löb_weak, HP. Qed.
   Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI.
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 9f3755aca..0b4d63892 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -125,7 +125,7 @@ Global Instance siProp_pure_forall : BiPureForall siPropI.
 Proof. exact: @pure_forall_2. Qed.
 
 Global Instance siProp_later_contractive : BiLaterContractive siPropI.
-Proof. apply later_contractive. Qed.
+Proof. exact: @later_contractive. Qed.
 
 Lemma siProp_internal_eq_mixin : BiInternalEqMixin siPropI (@siProp_internal_eq).
 Proof.
-- 
GitLab