# Documentation of \`{!Foo}?

**URL:** <https://discourse.rocq-prover.org/t/documentation-of-foo/129>\
**Category:** Using Rocq\
**Created:** [February 22, 2019, 2:41pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129 "2019-02-22T14:41:54Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 22, 2019, 2:41pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/1 "2019-02-22T14:41:54Z")

</div>

I am looking for more documentation on the behavior of ``{Foo}`. I found [https://coq.inria.fr/refman/language/gallina-extensions.html#index-1](https://coq.inria.fr/refman/language/gallina-extensions.html#index-1) but that is rather incomplete. The following questions remain open:

- 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.

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [February 23, 2019, 12:25am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/2 "2019-02-23T00:25:16Z")

</div>

Looking at the code, the bang will set the flag on the generalized constructor:

```auto
  | Generalized of binding_kind * binding_kind * bool
      (** Inner binding, outer bindings, typeclass-specific flag
	 for implicit generalization of superclasses *)

```

when this is set, it prevents the intern code from inserting the declared implicits, it seems.

---

<div class="post-metadata">

**Author:** ![JasonGross](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jasongross/32/32_2.png) [@JasonGross](https://discourse.rocq-prover.org/u/JasonGross)\
**Post date:** [February 23, 2019, 12:27am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/3 "2019-02-23T00:27:25Z")

</div>

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.)

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [February 23, 2019, 12:40am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/4 "2019-02-23T00:40:31Z")

</div>

This is an example @JasonGross, why this is useful I have no idea:

```auto
Class M (n : nat).
Definition equiv1 `{M} : Type. Admitted.
Fail Definition equiv2 `{!M} : Type.
Generalizable Variables n.
Definition equiv3 `{!M n} : Type. Admitted.

```

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [February 23, 2019, 12:48am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/5 "2019-02-23T00:48:12Z")

</div>

> [@RalfJ](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [February 23, 2019, 12:49am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/6 "2019-02-23T00:49:25Z")

</div>

That is to say:

```auto
Generalizable No Variables.
Class M (n : nat).
Definition equiv1 `{M} : Type. Admitted.
Fail Definition equiv2 `{M n} : Type. Admitted.

```

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 23, 2019, 8:49am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/7 "2019-02-23T08:49:43Z")

</div>

@ejgallego [one of your answers](https://discourse.rocq-prover.org/t/documentation-of-foo/129/4) 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:

```auto
`` `{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”.

* * *

```auto
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:

```auto
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 s_explicit_ 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.

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [February 23, 2019, 12:19pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/8 "2019-02-23T12:19:32Z")

</div>

> [@RalfJ](#):
>
> Why does this even work? An implicit argument is missing and generalization is turned _off_ ! This makes no sense.

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?

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [February 23, 2019, 12:22pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/9 "2019-02-23T12:22:24Z")

</div>

> [@RalfJ](#):
>
> So somehow it matters whether the _outer type_ is a typeclass or not.

Indeed that’s essential. The head symbol should have class status.

> [@RalfJ](#):
>
> I’m afraid your examples don’t answer the question what that means.

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.

---

<div class="post-metadata">

**Author:** ![mattam82](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mattam82/32/11_2.png) [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Post date:** [February 26, 2019, 8:49pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/10 "2019-02-26T20:49:43Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 27, 2019, 9:47am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/11 "2019-02-27T09:47:08Z")

</div>

@mattam82 got a link to that paper?

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [February 27, 2019, 10:52am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/12 "2019-02-27T10:52:43Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 27, 2019, 11:13am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/13 "2019-02-27T11:13:44Z")

</div>

@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 `!`…

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 27, 2019, 11:18am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/14 "2019-02-27T11:18:50Z")

</div>

Actually, uh, things are even more “interesting” than I thought… in my example, nothing changes when you remove `Generalizable All Variables`! This compiles:

```auto
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?

---

<div class="post-metadata">

**Author:** ![mattam82](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mattam82/32/11_2.png) [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Post date:** [February 27, 2019, 11:43am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/15 "2019-02-27T11:43:40Z")

</div>

Here it is: [https://www.irif.fr/~sozeau/research/publications/First-Class\_Type\_Classes.pdf](https://www.irif.fr/~sozeau/research/publications/First-Class_Type_Classes.pdf)

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 27, 2019, 1:30pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/16 "2019-02-27T13:30:29Z")

</div>

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 `!`:

```auto
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:

```auto
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.

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [February 27, 2019, 1:35pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/17 "2019-02-27T13:35:48Z")

</div>

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):

```auto
Generalizable No Variables.
Instance own_cmra_sep_homomorphism {Σ A} `{inG Σ (A:ucmraT)} γ :
  !WeakMonoidHomomorphism op uPred_sep (≡) (own γ).

```

fails, saying

```auto
Error: Unbound and ungeneralizable variable γ

```

while of course `γ` got bound explicitly…

And this

```auto
Generalizable All Variables.
Instance own_cmra_sep_homomorphism {Σ A} `{inG Σ (A:ucmraT)} :
  !WeakMonoidHomomorphism op uPred_sep (≡) (own γ).

```

fails saying

```auto
Error: Mismatched contexts while declaring instance: 
 Expected: (M1 M2 : ofeT) (o1 : M1 → M1 → M1) (o2 : M2 → M2 → M2) (H : Monoid o1) 
  (H0 : Monoid o2) (R : relation M2) (f : M1 → M2)
 Found: op uPred_sep (≡) (own γ)

```

Hu?

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.

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [March 13, 2019, 9:07am UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/18 "2019-03-13T09:07:00Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [May 23, 2019, 12:55pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/19 "2019-05-23T12:55:36Z")

</div>

@SkySkimmer has now improved the documentation (here: [https://coq.github.io/doc/master/refman/language/gallina-extensions.html#implicit-generalization](https://coq.github.io/doc/master/refman/language/gallina-extensions.html#implicit-generalization)) and removed one very peculiar use of this `!` syntax ([https://github.com/coq/coq/pull/10185](https://github.com/coq/coq/pull/10185)). Thanks @ejgallego for reminding me of this discussion.

---

<div class="post-metadata">

**Author:** ![RalfJ](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ralfj/32/59_2.png) [@RalfJ](https://discourse.rocq-prover.org/u/RalfJ)\
**Post date:** [May 24, 2019, 5:28pm UTC](https://discourse.rocq-prover.org/t/documentation-of-foo/129/20 "2019-05-24T17:28:23Z")

</div>

> 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.

[Next page](https://discourse.rocq-prover.org/t/documentation-of-foo/129.md?page=2)