Workaround until this is fixed: instead of using the {{...}} syntax, define f by hand:

f : {@0 x : A} {{_ : R x}} → A
f {{r}} = R.f r

Note that the parameters are erased in the type of the record constructor, but not in the record module's telescope (#4786 (comment)).

Yeah, now I actually wish it were possible to mark the module parameters of the record module as erased, but without marking the arguments to the record type as erased.

Actually, would that be a reasonable thing to do? We are already changing the visibility of the record parameters to be hidden; why not also change the quantity to @0 at the same time?

A workaround, if you really want to have a module with the same name as the record type:

module _ where

module Record where

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

open Record public hiding (module R)

module R {@0 A : Set₂} (r : R A) where

  x : A
  x = Record.R.x r

r₁ : R Set₁
r₁ = record { x = Set }

r₂ : R Set₁
r₂ .Record.R.x = Set

Actually, would that be a reasonable thing to do? We are already changing the visibility of the record parameters to be hidden; why not also change the quantity to @0 at the same time?

It is not necessarily the case that all code in a record module can be type-checked when the parameters are erased.

A workaround, if you really want to have a module with the same name as the record type:
[...]

Yes that works, unfortunately I also do care about being able to use the actual unqualified name of the field in copatterns.

It is not necessarily the case that all code in a record module can be type-checked when the parameters are erased.

That is something we could check. (At the cost of throwing error messages about erasure at users who did not use erasure in their code.)

That is something we could check.

Are you suggesting that we should see if the code type-checks with @0, and only change the telescope if it does? I would prefer if the user had to declare their intention more explicitly. One could imagine using some kind of keyword in the record type's header, but what if you want to mark only some parameters as erased in the record module? I suggest that we first get some experience with this kind of code, and then work out a design once we know what we want to do. I have at least one example in which one can't make all parameters erased.

Yeah no I agree completely that we should not decide on whether or not it checks, what I meant was that we might just always mark parameters of the record module as erased. But this doesn't seem possible since you have an example that would be broken by this change. So perhaps a specific keyword to toggle on erasure of record parameters would be the best solution.

Independently of whether we decide to add such a keyword, I still consider the behaviour of the original example I posted here a bug that should be fixed regardless.

I've made a separate issue for erasure of module parameters from definitions inside the record module: #5770

Side-note: see here for a remark on what "instance-opening" really is.

I've added the --erase-record-parameters flag in #5770 and I'm happy with it, so I am not planning to do more about this issue.