feat: Allow primitive projections with postponed eta (no sort poly)

[TDiazT]

This PR relaxes the constraints on defining records with primitive projections, namely for Type and Prop, by postponing the check to conversion. Namely, it introduces a new argument has_eta to decide whether to check or reject during conversion. This is a prelude to #21416.

• Records defined in Type/Prop with fields only in SProp can be defined and have NoEta, thus fail conversion.
• Records defined at some sort s with fields only in SProp can be defined and have MaybeEta, but currently fail during conversion.
• Records defined at some sort s with fields in other sorts are allowed and have MaybeEta.

Associated RFC : rocq-prover/rfcs#111.

Examples

Test cases added in success/record_postponed_eta.v

Set Primitive Projections.

Record RTypeToSProp (A : SProp) : Type := { f1 : A }.

(* Conversion when record is in Type and field in SProp fails correctly *)
Goal forall (A:SProp) (r2 : RTypeToSProp A), eq r2 {| f1 := r2.(f1 A) |}.
Proof. intros A r2. Fail reflexivity. Abort.
(* Unable to unify "{| f1 := f1 _ r2 |}" with "r2" *)
    
Record RPropToSProp (A : SProp) : Prop := {  f2 : A }.

(* Conversion when record is in Prop and field in SProp fails correctly *)
Goal forall (A:SProp) (r2 : RPropToSProp A), eq r2 {| f2 := r2.(f2 A) |}.
Proof. intros A r2. Fail reflexivity. Abort.
(* Unable to unify "{| f2 := f2 _ r2 |}" with "r2". *)

Set Universe Polymorphism.

Record RSToSProp@{s;u|s -> SProp} (A : SProp) : Type@{s;u} := {  f3 : A }.

Inductive eq@{s s'; u} (A : Type@{s;u}) (a : A) : A -> Prop :=  eq_refl : eq A a a.

(* Conversion when record is in Type and field in SProp fails correctly *)
Goal forall (A:SProp) (r2 : RSToSProp@{Type;0} A), eq r2 {| f3 := r2.(f3 A) |}.
Proof. intros A r2. Fail reflexivity. Abort.
(* Unable to unify "{| f3 := f3 _ r2 |}" with "r2". *)

Main API Changes

• declarations.mli : PrimRecord is now defined with a record, including a new argument of type has_eta.

Overlays

• Adapt to rocq-prover/rocq#21438 (PrimRecord record type + has_eta) MetaRocq/metarocq#1230
• Adapt to rocq-prover/rocq#21438 (Check for existing relevant field) rocq-community/rocq-lean-import#55

---

• Added / updated test-suite.

• Added changelog.

• Added / updated documentation.

  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[yannl35133]

@coqbot run full ci

[ppedrot]

The year is 2026 and I discover a new OCaml syntax. Since when is that pattern allowed without parentheses?

[ppedrot]

Some messages need a few tweaks, for instance:

Set Primitive Projections.

Record T (A : SProp) : Type := {
  p : A
}.

About T.

gives

[...]
T has primitive projections with eta conversion.
[...]

[ppedrot]

Rather than removing the example, I think you should keep it and add an About command to witness the correct message here.

[ppedrot]

@coqbot run full ci

[ppedrot]

@coqbot run full ci

[ppedrot]

Why is the CI broken now?

[TDiazT]

Why is the CI broken now?

Ah, wrong url for my metarocq repo...

The lean one I don't know yet.

[SkySkimmer]

Full CI from 2 weeks ago had the same lean importer error https://gitlab.inria.fr/coq/coq/-/jobs/6619036
The lean importer declares as primitive record any inductive in Type with 0 indices 1 constructor.
I guess the inductive mentioned in the error got turned into fakerecord and now is a primitive record without eta. Then the generated eliminator must now be non dependent which causes the error.
We could try adding a "exists relevant field" check at https://github.com/rocq-community/rocq-lean-import/blob/166733bac6841a04d92cce0226748560bf77433c/src/lean.ml#L1309 (kinda dual to the "all fields irrelevant" check in the _ :: _, true case below).

[SkySkimmer]

Suggested change

	overlay metarocq https://github.com/TDiazT/metarocq primitive-postponed-eta 21438
	overlay metarocq https://github.com/TDiazT/metacoq primitive-postponed-eta 21438

or rename your repo (renaming your repo will prevent such errors in the future)

[TDiazT]

Full CI from 2 weeks ago had the same lean importer error https://gitlab.inria.fr/coq/coq/-/jobs/6619036 The lean importer declares as primitive record any inductive in Type with 0 indices 1 constructor. I guess the inductive mentioned in the error got turned into fakerecord and now is a primitive record without eta. Then the generated eliminator must now be non dependent which causes the error. We could try adding a "exists relevant field" check at https://github.com/rocq-community/rocq-lean-import/blob/166733bac6841a04d92cce0226748560bf77433c/src/lean.ml#L1309 (kinda dual to the "all fields irrelevant" check in the _ :: _, true case below).

Yep, that seems to work. I am not really understanding what it is that this piece of code is doing though (in the importer).
If the inductive is in Type and has at least one relevant field, then we are turning it into a record with primitive projections (returning Some, etc?), if not then we are turning it into a fake record (and thus recovering the previous behavior)? Is that it?

[ppedrot]

@coqbot run full ci

[SkySkimmer]

If the inductive is in Type and has at least one relevant field, then we are turning it into a record with primitive projections (returning Some, etc?), if not then we are turning it into a fake record (and thus recovering the previous behavior)? Is that it?

If not then it's a regular inductive, not fakerecord.
This code is trying to emulate lean 4's behaviour where all inductives with 1 constructor and no indices have definitional eta.
In rocq definitional eta needs the inductive to be declared as a primitive record and not be recursive etc, and primitive records without definitional eta don't have dependent elimination, so we try to declare as many primitive records with eta as possible and to avoid declaring primitive records without eta.

[ppedrot]

@coqbot merge now

[coqbot-app]

@ppedrot: Please take care of the following overlays:

• 21438-TDiazT-primitive-postponed-eta.sh