Jesper Cockx

This is not a regression, so it can wait until the next release.

I think ideally we should also have a user-facing front page that is not the user manual or the github page. It doesn't have to contain a lot of information,...

Agreed, I had already forgotten we had activated it.

According to https://github.com/agda/agda/pull/6123#issuecomment-1472151296, this should only be merged AFTER #6537

This is currently unreviewable due to the large number of commits. Also, the test suite seems to be failing.

Confluence checking is very synactic by necessity, so it is not necessarily expected to be invariant under beta- or eta-equality. However, the error message here is certainly strange.

The problem is that with `λ where` you don't necessarily get a simple list of all the fields: there can be other patterns or copatterns, and this can be different...

I do not have a test case but either way it does not seem like a good idea to merge this now, so I'm moving it to `later`.

I don't think there's any faulty behavior here, marking a field as an instance just turns the projection function into an instance, which is consistent with how any other function...

For completeness, here is how I would write the code with an instance field (rather than an instance projection): ```agda postulate P : Set record Q : Set where field...