From 9b7fa3bb0fd0fbd45413f91d599ba6ee95db9b88 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Apr 2023 10:31:06 +0200
Subject: [PATCH] Make projections of BI operational type classes `Typeclasses
 Opaque`.

This avoids weird unification, where `@bupd ? ? ?` is unified with `@plainly ? ? ?`.

`embed` was already opaque, but `bupd`/`fupd`/`plainly`/`internal_eq` were not.
---
 iris/base_logic/lib/later_credits.v | 2 +-
 iris/bi/internal_eq.v               | 2 ++
 iris/bi/plainly.v                   | 2 ++
 iris/bi/updates.v                   | 2 ++
 4 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 5f27454f6..c7624ac10 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -266,7 +266,7 @@ Module le_upd.
        with the basic updates. *)
     Local Lemma bi_bupd_mixin_le_upd : BiBUpdMixin (iPropI Σ) le_upd.
     Proof.
-      split.
+      split; rewrite /bupd.
       - apply _.
       - apply le_upd_intro.
       - apply le_upd_mono.
diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index c5020d48e..1e7b3526a 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -16,6 +16,8 @@ Class InternalEq (PROP : Type) :=
 Global Arguments internal_eq {_ _ _} _ _ : simpl never.
 Global Hint Mode InternalEq ! : typeclass_instances.
 Global Instance: Params (@internal_eq) 3 := {}.
+Typeclasses Opaque internal_eq.
+
 Infix "≡" := internal_eq : bi_scope.
 Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.
 
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 93d1e86b8..a8a50b3d6 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -15,6 +15,8 @@ Class Plainly (PROP : Type) := plainly : PROP → PROP.
 Global Arguments plainly {PROP}%type_scope {_} _%I.
 Global Hint Mode Plainly ! : typeclass_instances.
 Global Instance: Params (@plainly) 2 := {}.
+Typeclasses Opaque plainly.
+
 Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 359a8dc9e..8c6a60621 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -17,6 +17,7 @@ Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Global Instance : Params (@bupd) 2 := {}.
 Global Hint Mode BUpd ! : typeclass_instances.
 Global Arguments bupd {_}%type_scope {_} _%bi_scope.
+Typeclasses Opaque bupd.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
 Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
@@ -26,6 +27,7 @@ Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Global Instance: Params (@fupd) 4 := {}.
 Global Hint Mode FUpd ! : typeclass_instances.
 Global Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
+Typeclasses Opaque fupd.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
 Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.
-- 
GitLab