Replace record directive "eta-equality" by "no-eta-equality;pattern"

[andreasabel]

Replace record directive eta-equality by no-eta-equality; pattern.

Future Agda might not allow unguarded record types with eta-equality in safe mode anymore.
So we switch eta off here, but make the constructor a pattern so that it can still be matched on.

Re: agda/agda#7470

[andreasabel]

These two commits passed CI when based onto master.
Now I rebased them onto merge-v2.1.1 so I can use them with Agda master (2.8.0).

[andreasabel]

Unfortunately, CI does not run anymore since the merge base is not master anymore.

I will have to change it back to master once #2473 has landed:

• Merge v2.1.1 into master #2473

[andreasabel]

I reset experimental to current master and rebased this PR onto experimental. So we are back in the main stream now.

[MatthewDaggitt]

Great, thank you!

[MatthewDaggitt]

As this is a breaking change, is it possible to wait until we know for sure that Agda will also make the breaking change?

[andreasabel]

As this is a breaking change, is it possible to wait until we know for sure that Agda will also make the breaking change?

Yes, let's wait until the Agda side is settled.

Commit 91e2c01 seems benign as probably the affected module is used mostly internally in the ring solver tactic.

Commit 8caaeae is more invasive and might have larger repercussions on the user of the Record structure. A pretext is here:

• Regression related to recursive records agda#840

[jamesmckinna]

Re: being a breaking change, the common case I worry most about will be the ability, currently exploited systematically, to never mention, either as a pattern on the LHS, nor as a term on the RHS, of definitions, the value tt : ⊤ of the unit type...
... but I suppose, at least IIUC, that pattern will ensure that the LHS uses will be OK under this change, while no-eta will have a lot of trivial-but-annoying knock-on consequences on the RHS? Is this analysis/'understanding' broadly correct?

[jamesmckinna]

Further to my comment above: does the change mean (morally) that (inductive) records are now a parameter-only specialisation of (the now-more-general?) one-constructor data declarations (which have pattern, as it were, automatically, for their single constructor, and moreover no eta-expansion/contraction allowed)? or will some instances of eta still be permitted?
(Apologies if I haven't understood the internals of all this, but I remember at AIM in Delft being recommended to use records mutually with inductive data for a certain representation, without being entirely clear about the pragmatics/trade-offs involved, and these now seem to be changing?)