What does the ! do? I can write `{!Foo}, but the documentation does not even mention that possibility.
Which effect does `{Foo} have with Generalizable No Variables? Is it just an anonymous binder, or is there some other effect? This is interesting because while anonymous binders with {_: Foo} are disallowed for section variables, `{Foo} is allowed.
Can you give an example of what this means? What’s a case where the behavior is different with and without the bang, and what’s the behavior in each case? (I can’t make sense of “prevents the intern code from inserting the declared implicits”, despite being familiar with Coq.)
Generalizable No Variables shouldn’t affect `{Foo} as it contains no generalizable ones, but they are coming from implicits I do believe [I didn’t check]. I would change if you use `{Foo n} I think.
@ejgallegoone of your answers has broken code blocks, which (since we are talking about backtics here) means I don’t really know what you mean. FWIW, you can have a backtic in an inline code-block by surrounding it with double-packtics:
`` `{Foo} ``
will render as `{Foo}
(Don’t forget the space between the “opening backtics” and the first “content backtic”.)
It would also help if you could add some comments to your examples to explain what they are showing, all I see is code that does “stuff”.
Generalizable No Variables.
Class M (n : nat).
Definition equiv1 `{M} : Type. Admitted.
Why does this even work? An implicit argument is missing and generalization is turned off! This makes no sense.
Also, seems like it treats the argument of M as implicit, even though it is not implicit? I made some experiments:
Generalizable All Variables.
Class FALSE := mkFalse : False.
Definition def1 (H:False): Type := nat.
Definition def2 {H:False}: Type := nat.
Definition def3 (H:FALSE): Type := nat.
Definition def4 {H:FALSE}: Type := nat.
Class tc_def1 (H:False) := mkDef1 : Type.
Class tc_def2 {H:False} := mkDef2 : Type.
Class tc_def3 (H:FALSE) := mkDef3 : Type.
Class tc_def4 {H:FALSE} := mkDef4 : Type.
Section test.
Fail Context `{def1 _}. (* _ does not get generalized *)
Fail Context `{def2}. (* implicit _ does not get generalized *)
Fail Context `{def3 _}. (* _ of TC type does not get generalized *)
Fail Context `{def4}. (* implicit _ does not get generalized *)
Fail Context `{tc_def1 _}. (* _ in TC type does not get generalized *)
Context `{tc_def2}. (* implicit _ in TC type DOES get generalized *) End test. Section test.
Context `{tc_def3}. (* WTF, the argument became implicit?!? *) End test. Section test.
Context `{tc_def4}. (* implicit _ of TC type in TC type DOES get generalized *)
End test.
(* And now with !. Nothing gets generalized. *)
Section test.
Fail Context `{!def1 _}.
Fail Context `{!def2}.
Fail Context `{!def3 _}.
Fail Context `{!def4}.
Fail Context `{!tc_def1 _}.
Fail Context `{!tc_def2}.
Fail Context `{!tc_def3 _}.
Fail Context `{!tc_def4}.
End test.
So somehow it matters whether the outer type is a typeclass or not. With implicit arguments, @foo _ and foo does not behave the same. And some arguments get treated as implicit even though they are not. (In lambda-rust, we also had a case where an argument got treated a sexplicit even though it is not, but I have not been able to minimize that.)
But of course, even with a !, some things do get generalized. So I have no idea what you mean by “prevents the intern code from inserting the declared implicits”. I’m afraid your examples don’t answer the question what that means.
It seems like Generalize affects variables that appear in the original argument. When variables don’t appear it is ! that controls if the rest of the arguments are filled. I am not very familiar with the design of this part of the system so I cannot comment [other that we’d be happy to improve the current situation]
I am sorry I confused you with the “implicits” quote, as you can see it makes little effect. When arguments are missing they are filled as if they were implicits, that’s all. Generalization by filling missing arguments only happens for things registered Class, this should be in the manual right?
Indeed that’s essential. The head symbol should have class status.
Sorry I didn’t phrase this properly, but indeed I think my examples are clear. If M is a class, with parameters a b, without ! they’ll be inserted as implicits, with !M, they will be not.
This is explained in our ITP paper with Nicolas Oury. AFAIR, the idea was to give only a subset of the arguments and generalize the rest, when encoding inheritance of classes by parametrization, probably not the best idea in retrospect.
Maybe it’s already obvious to all, but when the discussion ends, can the participants make sure that a bug or PR is opened as a follow-up, to either ensure that this functionality is documented, or altered and documented, or deprecated to be eventually removed?
@Zimmi48 I absolutely agree. And ideally someone who actually knows the code can make an authoritative statement about what the (intended) behavior is, instead of me trying to reverse-engineer that from a bunch of examples.
If we are talking functionality, IMO the behavior with ! should be the default (which to my understanding is to only generalize things that have been explicitly named), and then maybe there is some way to opt-in to other stuff being generalized (implicit parameters of classes, it seems). But it’s probably too late for that, and now I have to be super careful in every code review that every single use of generalization also uses a !…
Actually, uh, things are even more “interesting” than I thought… in my example, nothing changes when you remove Generalizable All Variables! This compiles:
Class FALSE := mkFalse : False.
Class tc_def1 (H:False) := mkDef1 : Type.
Class tc_def2 {H:False} := mkDef2 : Type.
Class tc_def3 (H:FALSE) := mkDef3 : Type.
Class tc_def4 {H:FALSE} := mkDef4 : Type.
Section test.
Fail Context `{tc_def1 _}. (* _ in TC type does not get generalized *)
Context `{tc_def2}. (* implicit _ in TC type DOES get generalized *) End test. Section test.
Context `{tc_def3}. (* WTF, the argument became implicit?!? *) End test. Section test.
Context `{tc_def4}. (* implicit _ of TC type in TC type DOES get generalized *)
End test.
So, generalizing implicit parameters of typeclasses is default behavior and has nothing to do with Generalizable All Variables. Uh. That’s… somewhat unsettling.^^
I mean, it does make sense – how would that depend on the variable names whitelisted with Generalizable All Variables anyway. But it seems like a dangerous default, to aggressively generalize so much. Is there an option to disable this behavior?
Thanks! I assume the [ C t1 t2 ] syntax from the paper corresponds to `{C t1 t2}?
To add to the list of weird things about `{Foo} with typeclasses without !:
Class tc_def2 {H:False} (n:nat) := mkDef2 : Type.
Generalizable All Variables.
Section test.
Context `{tc_def2 n}.
End test.
Can you guess the type of n?
Answer
The type of n is False. It also adds an n0: nat. It seems to entirely ignore which arguments are implicit, just fill up the first arguments with the given parameters, and then generalize the rest.
Here’s some more tests:
Class FALSE := mkFalse : False.
Class tc_def1 (H:False) := mkDef1 : Type.
Class tc_def2 {H:False} := mkDef2 : Type.
Class tc_def3 (H:FALSE) := mkDef3 : Type.
Class tc_def4 {H:FALSE} := mkDef4 : Type.
Generalizable All Variables.
Section test.
Context `{tc_def1 X}. (* as expected *) End test. Section test.
Context `{tc_def2 X}. (* implicit argument became explicit?? *) End test. Section test.
Fail Context `{tc_def3 X}. (* explicit argument became implicit?!? *) End test. Section test.
Fail Context `{tc_def4 X}. (* as expected *)
End test.
I conclude that when using `{Foo} with typeclasses without !, the implicit status of arguments is entirely ignored. Arguments are always passed explicitly, and then the remaining arguments are generalized. Except that somehow if the last argument is a typeclass, you are not allowed to give it explicitly? This makes no sense… in fact I’d argue ignoring whether an argument is implicit is just a bug.
And I found one more hidden cave full of unexplored gems: turns out you can add ! to an Instance declaration. I have not yet figured out entirely what it does, and don’t have time to minimize right now, but I will leave you with this (taken from Iris):
Generalizable No Variables.
Instance own_cmra_sep_homomorphism {ÎŁ A} `{inG ÎŁ (A:ucmraT)} Îł :
!WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
fails, saying
Error: Unbound and ungeneralizable variable Îł
while of course γ got bound explicitly…
And this
Generalizable All Variables.
Instance own_cmra_sep_homomorphism {ÎŁ A} `{inG ÎŁ (A:ucmraT)} :
!WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
So, to come back to what @Zimmi48 said, yes please someone document this, but I feel this needs to be done by someone who can actually read the code for this. Doing a phenomenological study of Coq will only get us that far – whoever implemented this was clearly more creative than me, because the hypotheses I come up with for explaining what happens tend to be shattered quickly.
An interesting point came up on Gitter: When checking whether a `{Foo A B} is a typeclass (and hence has implicit arguments generalized), it seems Coq does not look through notation.
When generalizing a binder whose type is a typeclass, its own class arguments are omitted from the syntax and are generalized using automatic names, without instance search. Other arguments are also generalized unless provided. This produces a fully general statement.
Thanks a lot, that answers most of my questions.
@SkySkimmer Is it correct that when not using !, the implicit status of arguments (when the type is a typeclass) is ignored? That was the result of my experiments. Would be great to see that either called out as a bug, or described in the documentation.
