stdpp breaks setoid rewriting

The setoid rewriting mechanism uses a bunch of typeclass machinery to infer Proper instances for the contexts being rewritten in, and it uses flip to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes flip typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In base.v, we have:

Typeclasses Transparent id compose flip const.

This nullifies the effect of the very first non-comment non-import line of Classes/Init.v in the Coq stdlib:

Typeclasses Opaque id const flip compose arrow impl iff not all.

Here's a minimal demonstration of the problems this causes:

From Coq Require Import ssreflect ssrfun ssrbool.

Require Import Morphisms.
Require Import PeanoNat.

Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.

Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
  move=> n m o H1 H2.
    by setoid_rewrite <- H1 in H2 at 1.
Qed.

Require Import stdpp.base.

Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
  move=> n m o H1 H2.
  Fail setoid_rewrite <- H1 in H2 at 1.
Abort.

Section FlippedInstance.
  (* Thus seemingly necessitating: *)
  Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
  Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.

  Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
  Proof.
    move=> n m o H1 H2.
      by setoid_rewrite <- H1 in H2 at 1.
  Qed.
End FlippedInstance.

(* But alternatively: *)

Typeclasses Opaque flip.

Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
  move=> n m o H1 H2.
    by setoid_rewrite <- H1 in H2 at 1.
Qed.

changed the description

Thanks for the report.

In Iris, we always add explicit Proper instances for flip because the automatic infrastructure for these instances is not very reliable, if I recall correctly.

That said, I do agree that it's not great that we override the Coq stdlib's defaults here. Adapting std++ to not override these defaults is easy (see below for a patch), but it breaks Iris (and probably many reverse-dependencies of Iris) in non-trivial ways. In Iris Proof Mode, all unification is done via type classes, so there it's really annoying if these operations were TC opaque.

So, I see the following options:

1. Mark this as WONTFIX, but document why we override the defaults by making id compose flip const TC transparent.
2. Accept the patch below, but make id compose flip const TC transparent in Iris.

@jung @jjourdan Any opinions?

diff --git a/theories/base.v b/theories/base.v
index b76f16a..07ec9b0 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -529,7 +529,6 @@ Arguments id _ _ / : assert.
 Arguments compose _ _ _ _ _ _ / : assert.
 Arguments flip _ _ _ _ _ _ / : assert.
 Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
diff --git a/theories/list.v b/theories/list.v
index 1203a5d..e0ad21a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3166,11 +3166,11 @@ Section find.
   Qed.
 
   Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) :
-    list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
+    list_find P (f <$> l) = prod_map id f <$> list_find (λ x, P (f x)) l.
   Proof.
     induction l as [|x l IH]; [done|]; csimpl. (* csimpl re-folds fmap *)
     case_decide; [done|].
-    rewrite IH. by destruct (list_find (P ∘ f) l).
+    rewrite IH. by destruct (list_find _ l).
   Qed.
 
   Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
diff --git a/theories/pretty.v b/theories/pretty.v
index 296cccb..04e8b31 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -70,5 +70,4 @@ Instance pretty_Z : Pretty Z := λ x,
   end%string.
 Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
 Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty.
-Proof. apply _. Qed.
-
+Proof. intros ???. by apply (inj N.of_nat), (inj (pretty (A:=N))). Qed.

If the infrastructure is unreliable for you, it may be because of this exact issue :)

I don't have extensive experience with it myself, so I may be wrong, but—how much of you saying so is informed by projects that are working under this breakage?

Also, would another alternative be to just define separate versions of flip, etc, in stdpp? There's enough core stuff that uses definitions like those that fiddling with their evaluation and transparency behavior seems pretty questionable in general—is there a good reason to not just make your own overrides? I suppose it would create a ton of work to migrate every usage...

I can find some attempts in the history, but a problem is that 9d7640c0 doesn't have many details; if I had to track it down, I might have to rebuild that commit and the iris ecosystem to find out the problem. (But I haven't git blamed this back till the beginning right now).

However that is just a revert of a commit from the day before, b81aa3aa.

Sure, and that has even fewer details...

In Iris, we always add explicit Proper instances for flip because the automatic infrastructure for these instances is not very reliable, if I recall correctly.

Maybe that is caused by std++ messing with the flags of flip, though...

but it breaks Iris (and probably many reverse-dependencies of Iris) in non-trivial ways. In Iris Proof Mode, all unification is done via type classes, so there it's really annoying if these operations were TC opaque.

Could you give an example for the kind of unification that fails now, in particular one involving flip?

I do agree, however, that making id opaque is really strange. This should be the posterchild of a NOP, but through opacity it is not.

This sounds like a really good argument to make IPM use a separate hint DB from normal TC search. Or maybe we can just use two DBs and both of their opacity hints? However, I have no idea how multiple DBs with different opacity hints interact.