When originally implementing erasure, I did not have the guts to make parameters erased. In particular, to not confront users with errors concerning erasure if they did not use erasure at all.
We might want to revisit the original decision now.

For projections there is a complication: some definition in the record module might use the parameters in a non-erased context. Perhaps we could fall back to the current behaviour if there is a non-trivial record module.

I don't see a conflict between making parameters erased for projections while leaving them non-erased for definitions in the record module.

The projections are defined in the record module, and the module's telescope is built using the parameters.

The projections are defined in the record module, and the module's telescope is built using the parameters.

Apparently you can build a record module in such a way that the parameters are not erased in the telescope, but when you open the module you get projections with erased parameters. With my attempted fix of this issue (16f1118) the following code is accepted:

record R (A : Set) : Set where
  field
    x : A

open R

_ : (@0 A : Set) → R A → A
_ = λ A → x {A = A}

_ : (@0 A : Set) → R A → A
_ = λ A → R.x {A = A}

However, the following code is rejected:

open module R′ (@0 A : Set) (r : R A) = R {A = A} r

I wonder if the code that generates composition operations for data and record types needs to be changed. @Saizan, can you take a look at this?

@wenkokke, do you discuss how parameters affect the types of constructors or projections in PLFA? If so this change might "break" the text. As an example, the statement that the constructor c of the data type D below is {A : Set} → D A is no longer correct after this change, because the type is {@0 A : Set} → D A.

data D (A : Set) : Set where
  c : D

Put erasure under a flag. (--erasure / --no-erasure).

@wenkokke, if this change is only active when --erasure is on, then it should not affect PLFA, so you can ignore my question.

The option --erasure should be infective. I wonder if one can still set things up so that (for instance) Agda.Builtin.Sigma._,_ can have erased parameter arguments.

One idea is to generate such arguments, but only print @0 if --erased is active. I wonder if anything would break if this approach is taken. If the only erased things are constructor arguments, what can go wrong? You can't include a parameter in a pattern, so I guess there won't be any erased variables or definitions. Consider the following code:

data D (@0 A : Set) : Set where
  c : D A

Is it possible to observe the difference between c : {@0 A : Set} → D A and c : {A : Set} → D A without using @0? The following code is accepted in the former case, but not the latter, but this code uses @0:

f : (@0 A : Set) → D A
f A = c {A = A}

Is there a risk that a meta-variable is created in an erased context, and thus cannot be used in a non-erased context? This could perhaps be addressed by ensuring that meta-variables are never created in an erased context when --erased is not active, but I wonder if that would create any new problems.

@nad the code for the composition operations still gets the parameter telescope from the datatype, so it's fine. The CubicalPrims test also passes, which confirms the generated code runs as expected.

Thanks.

If we take the approach that I speculate above, where @0 is inserted into the types of constructors and projections, but not printed, could the cubical composition operations be used to observe that the @0 annotations are present?

One option is to not have a --erasure option: the presence of --erasure should not rule out any models. The main disadvantage is perhaps that someone not familiar with erasure might see @0 in some type signature.

Consider the following code:

data D (A : Set) : Set where
  c : D A

record R (A : Set) : Set where
  constructor c
  field
    f : A

If you infer the type of c₁, then you get D _A_5, and for c₂ you get (f : _A_5) → R _A_5. However, for some reason the type inferred for R.f is {@0 A : Set} → R A → A. If you print the contents of the top-level module, then you get the following output:

Modules
  D
  R
Names
  D  : Set → Set
  R  : (A : Set) → Set
  c₁ : {@0 A : Set} → D A
  c₂ : {@0 A : Set} (f : A) → R A

For D and R you get the following results:

Modules
Names
  c₁ : {@0 A : Set} → D A

Modules
Names
  f : {@0 A : Set} → R A → A

@nad the code for the composition operations still gets the parameter telescope from the datatype, so it's fine. The CubicalPrims test also passes, which confirms the generated code runs as expected.

@Saizan, doesn't it make sense to erase the parameters also in the composition operations?

@nad it doesn't, why would it make sense? if you transport along (\ i -> List (ua e i)) I'd better be able to compute with that e. Even homogeneous composition needs them, as for e.g. \Sigma A B you'll need to transport along B composed with a filling.

I'm not familiar with the computation rules for the composition operations, that's why I asked you. If the parameters are (supposed to be) used for run-time computations, then it makes sense to not mark them as erased.

One option is to not have a --erasure option: the presence of --erasure should not rule out any models. The main disadvantage is perhaps that someone not familiar with erasure might see @0 in some type signature.

I suggest that we merge my implementation of this variant now, and see if anyone complains. Any objections?

There were no objections, so I merged my changes.