Allow projections to be declared as classes.

[mattam82]

Kind: feature

This fixes an arbitrary limitation of typeclasses, which didn't allow primitive projections
to be declared as class heads. They can usefully be used as proxys. In our use case:

Class UR A B := {
  ur : A -> B -> Type 
}.

We want to declare ur as a type class head, as in all instances of UR, ur is itself defined by a type-class. We can use a hint to unfold the ur projection when applied to a particular UR instance to simplify the goal to a new typeclass constraint. This allows a kind of dependent type-class resolution.

As long as users did not try to do Existing Class ur for some primitive projection ur, which had no effect previously, this should be backwards compatible.

Fix #12975, fix #8994.

• Added / updated test-suite
• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified).

[SkySkimmer]

@mattam82 is this PR dead?

[mattam82]

It's been forgotten, I'll try to bring it back to life

[ppedrot]

@mattam82 ping. I believe this is quite high priority actually.

[mattam82]

@ppedrot I’m on holidays next week, so if you want to pick it up you’re welcome. Otherwise thanks for the reminder !

[mattam82]

Rebased now, let's see.

[mattam82]

@ppedrot this is ready now.

[ppedrot]

This is adding a new dependency to the legacy constant binding mechanism. I know we're a bit in a hurry w.r.t. the release, but instead of doing that we should have a type of global references including projections. I can validate the PR as is, but if you have time, could you do that the right way from the start?

[mattam82]

Hmm, I don't really have time right now, but indeed that should happen next. Note that we already had code using Projection.constant here, so it's not really worse than before.

[ppedrot]

@mattam82 can you squash the last commit? It's useless to keep it.

[mattam82]

Sure. I rebased on #14392 to see where CI gets now.

[ppedrot]

Erm, I would gladly have merged this PR without the additional comments as soon as the original CI would have finished... This needs to be merged before the branch, so you'll have to rebase again to remove the commits once your experiment is finished.

[mattam82]

That's fine. I'm not sure this is the end just yet.

[coqbot-app]

Hey, I have detected that there were CI failures at commit 2a691de without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 92f3b90 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-coq_tools.

[coqbot-app]

Hey, I have detected that there were CI failures at commit 2a691de without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 92f3b90 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-coq_tools.

[ppedrot]

Why is coqbot repeating the very same thing twice?

[JasonGross]

It'll report again every time the overall pipeline status check is finished. If a job fails and then someone restarts the job, when it finishes the second time, this will trigger a second comment. Perhaps that's what happened? (The coq-tools issue is on my side, I'll fix it shortly, sorry.)

[mattam82]

What is coq-tools ?

[mattam82]

Yes, I did retrigger it.

[mattam82]

Do you mean that the failure of the ci-coq_tools job is your fault?

[JasonGross]

Do you mean that the failure of the ci-coq_tools job is your fault?

Yes, I pushed what I thought was an innocuous commit working around an intermittent issue with the native compiler, not realizing that it would change the output log, and I didn't enforce the discipline of running the test-suite before pushing. This broke about half of the output tests, which I'm now fixing; it should be fixed within 10 minutes, and sorry about this.

[mattam82]

That's good news, both PRs should go green by tonight then!

[JasonGross]

coq-tools should be fixed now, I've restarted it

[coqbot-app]

Hey, I have detected that there were CI failures at commit 2a691de without any failure in the test-suite.
I checked that the corresponding jobs for the base commit 92f3b90 succeeded. You can ask me to try to extract a minimal test case from this so that it can be added to the test-suite.
If you tag me saying @coqbot ci minimize, I will minimize the following target: ci-coq_tools.

[ppedrot]

... still failing it seems.

[JasonGross]

Yeah, I forgot that -native-compiler ondemand is required to work around native compiler issues on old versions of coq but produces warnings on new versions of Coq. Hopefully now fixed

[ppedrot]

@mattam82 in order not to lose time I have rebased and slightly tweaked the commit message, I'll merge when the CI finishes.

[mattam82]

@ppedrot thanks a whole bunch!