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

[andreasabel]

trafficstars

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]

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:

• #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 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:

• agda/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?)

[andreasabel]

This PR was only addressing recursive records for which Agda cannot detect that they are guarded. The prime example for an unguarded record type would be this one:

record R : Set where
  inductive
  field r : R

Eta-expansion for R would go on forever, and Agda can see this, so it won't make this record eta-equality but rather no-eta-equality. There are cases where Agda's positivity checker can't ensure guardedness, these would be affected by the change in Agda (which is stalled now).

For completeness, here is an example of a guarded record type:

record M : Set where
  inductive
  field m : Maybe M

[MatthewDaggitt]

@andreasabel what is the status of this? Did this change make it into v2.8.0?

[andreasabel]

@andreasabel what is the status of this? Did this change make it into v2.8.0?

No, it didn't, so I didn't merge this PR into experimental. So I guess it should dropped from the milestone.