decrease priority for rtc_reflexive instance

We give this instance a lower-than-usual priority because when it is applied to Reflexive ?, it leads to a new evar being created for R. Unfortunately, we cannot set Hint Mode for Reflexive in a way that just rules out Reflexive ? [1], but we can at least stop TC search from using this instance. This helps performance because it gives TC search less freedom in the remainder of the search. It doesn't seem like backtracking is happening here.

Also see the discussion below https://gitlab.mpi-sws.org/FP/iris-coq/commit/8e8c722870b36c23032d9bc10019e40e6eb6be62. I think this is useful even if we decide to roll back the IntoVal change as there may be other places where rtc_reflexive inadvertently gets chosen.

[1] That would break https://gitlab.mpi-sws.org/FP/iris-coq/blob/38ba379fae88865ed3a06ba44bf22938b6524610/theories/algebra/list.v#L213

changed the description

added 1 commit

• 9c9d14b0 - decrease priority for rtc_reflexive instance

Compare with previous version

I did some more research and reported Coq bug #7916, and updated the comment in the code.

This makes the following test pass, which I am going to add to Iris:

(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs. *)
Lemma test_setoid_rewrite :
  exists R, @Reflexive Prop R /\ R = iff.
Proof.
  eexists. split.
  - apply _.
  - reflexivity.
Qed.

Thanks for looking into this. The current workaround seems fine to me, so feel free to merge.

This makes the following test pass, which I am going to add to Iris:

In an ideal world (with Hint Mode ! ! for `Reflexive), this should fail. Please put a reference to the Coq bug and this MR.

In an ideal world (with Hint Mode ! ! for `Reflexive), this should fail. Please put a reference to the Coq bug and this MR.

Sure, will do.

merged

mentioned in commit 0eb9a89b

This makes the following test pass, which I am going to add to Iris:

Ideally, shouldn't we add this as a test to std++?

I realize we don't have anything for tests currently. How difficult would it be to copy the testing infrastructure from Iris?

How difficult would it be to copy the testing infrastructure from Iris?

Not at all.

However, we should also test in Iris in case we declare more instances there.

mentioned in merge request !39 (merged)