From 011e9bbb8e2b1338da89e0443e5252e56c6714bd Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 23 May 2021 23:58:05 +0200
Subject: [PATCH] Change the tactic for resolving typeclass instances from
 canonical structures.

Example include Equiv, Dist, Op, Core, Valid, ValidN and Unit.

The previous hints used eapply. The new hint now use refine. These two
tactic use a different unification algorithm, which result in
different behavior with respect to canonical structures.

The refine tactic is followed by shelving all the remaining goals,
which correspond actually to existential variables.

In particular, in RustHornBelt, the version using apply is unable to
find the canonical structure of heterogeneous lists.
---
 CHANGELOG.md        |  4 ++++
 iris/algebra/cmra.v | 14 ++++++++------
 iris/algebra/ofe.v  |  5 +++--
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3322b97f5..923b66e6f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,10 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Demote the Camera structure on `list` to `iris_staging` since its composition
   is not very well-behaved.
 * Extend `gmap_view` with lemmas for "big" operations on maps.
+* Typeclasses instances triggering a canonical structure search such as `Equiv`,
+  `Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern`
+  based on `refine` instead of `apply`, in order to use Coq's newer unification
+  algorithm.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 43a8a068c..7824e3ac8 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -93,10 +93,11 @@ Global Arguments cmra_validN : simpl never.
 Global Arguments cmra_ofe_mixin : simpl never.
 Global Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmra.
-Global Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
-Global Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
-Global Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
-Global Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
+(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
+Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
+Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
+Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
+Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
 Coercion cmra_ofeO (A : cmra) : ofe := Ofe A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeO.
 
@@ -215,7 +216,8 @@ Global Arguments ucmra_ofe_mixin : simpl never.
 Global Arguments ucmra_cmra_mixin : simpl never.
 Global Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmra.
-Global Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
+(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
+Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
 Coercion ucmra_ofeO (A : ucmra) : ofe := Ofe A (ucmra_ofe_mixin A).
 Canonical Structure ucmra_ofeO.
 Coercion ucmra_cmraR (A : ucmra) : cmra :=
@@ -1543,7 +1545,7 @@ Section option_prod.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
 End option_prod.
 
-Lemma option_fmap_mono {A B : cmra} (f : A → B) ma mb :
+Lemma option_fmap_mono {A B : cmra} (f : A → B) (ma mb : option A) :
   Proper ((≡) ==> (≡)) f →
   (∀ a b, a ≼ b → f a ≼ f b) →
   ma ≼ mb → f <$> ma ≼ f <$> mb.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 68c57a3f3..65dab9152 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -56,8 +56,9 @@ Structure ofe := Ofe {
 }.
 Global Arguments Ofe _ {_ _} _.
 Add Printing Constructor ofe.
-Global Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
-Global Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+(* FIXME(Coq #6294) : we need the new unification algorithm here. *)
+Global Hint Extern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.
+Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
 Global Arguments ofe_car : simpl never.
 Global Arguments ofe_equiv : simpl never.
 Global Arguments ofe_dist : simpl never.
-- 
GitLab