Option to erase record parameters in record module without erasing them as arguments to the type

[jespercockx]

As noted in #5769, it would be useful to have an option (either a global flag or a record keyword) to mark the parameters of a record module as being erased (as in having a @0 annotation) without marking the arguments to the record type itself as erased.

This would mean for example that the following code should be accepted:

postulate A : Set
postulate a : A

record R (x : A) : Set where
  y : A
  y = a

f : (@0 x : A) → R x → A
f x r = R.y {x} r

... and the following code should be rejected:

postulate A : Set

record R (x : A) : Set where
  y : A
  y = x

For some motivation for why I think we need this feature, see agda/agda2hs#88

[nad]

As I wrote elsewhere I think we should wait a bit until we have more practice writing code like this. We can already express what you want to express, except that you might not be able to use certain names.

I saw that there is a bug in agda2hs that you want to fix. Perhaps it makes sense to change Agda in order to fix this bug, but I don't think we should rush things.

Currently record modules are strange: the parameters are not erased in the telescope of a record module, but when you open the module you get projections with erased parameters (#4786 (comment)). The design would arguably be cleaner if we always erased the parameters, but that would break existing code. I suggest that we run some experiments, and see how much code breaks in practice. If most code is still accepted, then we could perhaps go with the clean design.

[jespercockx]

The problem with "waiting until we have a bit more practice" is that this issue is currently preventing me from experimenting further with using @0: it is currently impossible to mark record module parameters as erased, which means all functions that use a function defined in a record parameters can also not have erased arguments, which renders the whole exercise pointless.

Technically I can work around the problem, however it requires me to:

1. Not use open C {{...}} syntax and instead redefine the projections by hand outside of the record.
2. Use qualified names for the field names whenever I'm defining an element of the record type (since the unqualified names are just functions because of 1.).
3. Not define any functions inside the record module, but instead define them outside so the parameters can be marked with @0.

I can do these things myself, but they make it extremely annoying to add @0 annotations to existing code. Also, it is simply too much to ask users of Agda2Hs to adhere to these restrictions. So in practice the effect will be that we get not more but less experience with @0.

I am not opposed to running some experiments to see what would happen if we always erased parameters (i.e. turn on the --erase-record-parameters flag from #5771 by default). By far the easiest way to run these experiments would be to first push the flag but leave it off by default so everyone can experiment with it. Then if we decide at some point that it is the right behavior we can change the default to it being turned on. This does not break anyone's code and gives us time to evaluate so I do not see why this would be "rushing things".

[nad]

If agda2hs relies on the use of this option, not only in the implementation of agda2hs, but also in the Agda code, isn't there a risk that we will have to support it to ensure backwards compatibility? I'm fine with adding the option temporarily, use it for testing, and then evaluate it before we release the next version of Agda.

(By the way, I suspect that lots of code in the standard library will fail with this option turned on.)

[jespercockx]

I could create a separate branch of Agda2Hs for testing out this new flag, but keep the main version as it is until and unless we decide to keep the behaviour of --erase-record-parameters in Agda (either as an option or as the default behaviour). I cannot promise that no people will start using this version and decide they like it better than the current one and will thus demand this flag to stay in Agda. Is this satisfactory to you?

[jespercockx]

Regarding the standard library: It is the kind of change that only works when you consistently annotate arguments with @0 across your codebase, so I understand that the standard library will not just check with this option enabled.

[nad]

Is this satisfactory to you?

Sure.

Regarding the standard library: It is the kind of change that only works when you consistently annotate arguments with @0 across your codebase, so I understand that the standard library will not just check with this option enabled.

If you use --without-K, then you cannot even mark all "types" with @0. The following code is rejected (#4784, #5448):

{-# OPTIONS --without-K #-}

module _ where

open import Agda.Builtin.Equality

module Fails {@0 A : Set} {@0 P : A → Set} where

  subst : {x y : A} → x ≡ y → P x → P y
  subst refl p = p

Agda.Primitive.Cubical.primTransp (λ i → P (x i)) φ
(subst refl
 (Agda.Primitive.Cubical.primTransp (λ i → P x₁) φ
  x₂)) is not usable at the required modality
when checking the definition of subst