Record forgets implicitness information

[meygerjos]

When Record converts to Variant, it drops the data about which arguments are implicit.

> Variant example {n : nat} (e : n=n) :=
 | a : nat -> example e.
> Check a.  
a
     : forall e : ?n = ?n, nat -> example e
where
?n : [ |- nat]
> Record example2 {n : nat} (e : n=n) := a2 { r: nat }.
> Check a2.
a2
     : forall (n : nat) (e : n = n), nat -> example2 e

Coq Version

The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 9 2021 11:34:01 with OCaml 4.07.1

[ejgallego]

This seems indeed due to implicits for the record declaration not being preserved for the constructor.