Universe polymorphic record declaration fails in presence of a coercion

[ecranceMERCE]

Trying to add a Box record through Coq-Elpi fails if the field is a coercion. This issue is in the context of PR #400.

From elpi Require Import elpi.

Set Universe Polymorphism.

Elpi Command x.
Elpi Accumulate lp:{{
  gen :-
    coq.univ.new U,
    coq.univ.variable U I,
    RDecl =
      record "Box" (sort (typ {coq.univ.super U})) "MkBox" (
        field [coercion regular] "unbox" (sort (typ U)) (_\
      end-record)),
    coq.say "RDecl =" RDecl,
    @udecl! [I] tt [] tt => coq.env.add-indt RDecl _.
}}.
Elpi Typecheck.

Fail Elpi Query lp:{{ gen. }}.

Record Box@{i} : Type@{i+1} := MkBox { unbox :> Type@{i} }.

Changing coercion regular to coercion off works, but coercion reversible fails too.

cc @CohenCyril

[CohenCyril]

Cc @gares