Something in std++ enables implicit generalization of instances

The following script fails, as I would expect because k is not bound:

Class Even (n: nat) := even : exists m, 2 * m = n.

Global Instance even_even: Even (2*k).

However, the following script works:

From stdpp Require Export prelude.

Class Even (n: nat) := even : exists m, 2 * m = n.

Global Instance even_even: Even (2*k).

The culprit is the following block of options:

Global Generalizable All Variables.
Global Set Asymmetric Patterns.
Global Unset Transparent Obligations.

Even if std++ wants to use these internally, I think we should be careful inflicting them on our users. I certainly think that "Generalizable All Variables" is a misfeature; e.g. it led to completely bogus error messages when PersistentP got renamed to Persistent.

I am not so sure about the others, as I don't know what they do. But am rather sour about ssreflect inflicting its bullet choice on us (lucky enough, the in-Coq version no longer does this), and now I have to discover that std++ does the same. :( At the very least, there should be comments explaining why changing this option for all users is the right thing to do.

It seems that Generalizable All Variables both enables generalization in `{...} and in Instance. We use the former a lot. I am not sure how I think about that one, but I am not very happy about it for instances.

Also see https://github.com/coq/coq/issues/6030

Thanks for creating an issue for Global Generalizable All Variables. What you write is correct: we only want arguments in `{...} to be implicitly generalized, the other effect is bogus.

As for:

Global Set Asymmetric Patterns.

I think we should get rid of that. They changed the behavior of pattern variables in 8.6 → 8.7, and this enables the old behavior. I just enabled it because I did not want to port anything yet. I don't have time now, but I would welcome a MR that disables this option and adjusts the code accordingly.

There was little trouble removing Set Asymmetric Patterns, at least for Iris.

Also, are you sure this was 8.6 -> 8.7 and not 8.5 -> 8.6? CI says the new behaviors works just fine on 8.6.

There was little trouble removing Set Asymmetric Patterns, at least for Iris.

That's good. Can you try in std++ too, and push these changes?

Also, are you sure this was 8.6 -> 8.7 and not 8.5 -> 8.6? CI says the new behaviors works just fine on 8.6.

That may be.

There was little trouble removing Set Asymmetric Patterns, at least for Iris.

That's good. Can you try in std++ too, and push these changes?

I noticed you already did. Most of these changes are for the better. I made two minor tweaks.

As for Global Unset Transparent Obligations: We always use Program to solve logical side-conditions. As such, they should be made Opaque, because otherwise we end up with performance problems.

Note that in most cases we use Next Obligation. (* ... *) Qed., for which this option does not matter. However, sometimes we use things like Solve Obligations with naive_solver (* ... *), and then the obligations should surely be opaque.

Also note that we make more changes to Program, like Obligation Tactic := idtac.. The default is some ad-hoc tactic that performs some arbitrary simplifications.

Added some documentation about the Program-related options in 0d0be97b.

I added a section about this to the README and also commented on Unset Transparent Obligations.

Should we leave this open to track the undesired generalized Instance on our side, or leave that on the Coq side only?

Should we leave this open to track the undesired generalized Instance on our side, or leave that on the Coq side only?

Sounds like a good idea.

Talking about options; I would like to enable the following option too:

Global Set Refine Instance Mode.

Right now, when you write something like:

Instance foo : Foo x := bar _.

Then Coq would try to solve the _ by type class resolution, and if it fails to succeed, it opens a goal.

The latter is extremely error prone: it happened to me many times that because of a change, an Instance out of the suddens opened a goal. Usually what happens then is that when closing a section or ending the file, Coq starts complaining that some goals have not been proved.

The option Set Refine Instance Mode makes sure that Instance fails immediately, which is the sensible behavior.

Any thoughts?

PS1: I wanted to do this a long time ago, but then I could not because of Coq bug #4580. This bug has been fixed for a long time now, though.

PS2: Enabling this option requires zero changes to both std++ and Iris.

I don't mind that change, but I do mind effects on the global state of Coq. I think we should solve https://gitlab.mpi-sws.org/FP/iris-coq/issues/66 before adding even more such effects.