search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
585 stars 237 forks source link

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

Open andreasabel opened 2 months ago

andreasabel commented 2 months ago

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: https://github.com/agda/agda/pull/7470

andreasabel commented 2 months ago

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 commented 2 months ago

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:

andreasabel commented 2 months ago

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

MatthewDaggitt commented 2 months ago

Great, thank you!

MatthewDaggitt commented 2 months ago

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 commented 2 months ago

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 91e2c0130edc60a24b09ed1a69aa8fdebe7a106a seems benign as probably the affected module is used mostly internally in the ring solver tactic.

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

jamesmckinna commented 1 month ago

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?