Inconsistency using malicious plugin in 8.19.0

[SkySkimmer]

plugin code (omitting the DECLARE PLUGIN etc):

{
open Names
open UState
open Constr
open Context

let hack () =
  let q0 = Sorts.QVar.make_var 0 and q1 = Sorts.QVar.make_var 1 in
  let u = UVars.Instance.of_array ([|QVar q1;QVar q0|],[||]) in
  let univs = Polymorphic_entry (UVars.UContext.make ([|Anonymous;Anonymous|],[||]) (u, Univ.Constraints.empty)) in
  let univs = univs, UnivNames.empty_binders in
  let nA = make_annot (Name (Id.of_string "A")) Relevant in
  let na = make_annot (Name (Id.of_string "a")) (RelevanceVar q0) in
  let s = mkSort (Sorts.qsort q0 Univ.Universe.type0) in
  let body = mkLambda (nA, s,
                       mkLambda (na, mkRel 1, mkRel 1))
  in
  let ty = mkProd (nA, s, mkProd (na, mkRel 1, mkRel 2)) in
  let e = Declare.definition_entry ~opaque:true ~types:ty ~univs body in
  let _ : GlobRef.t = Declare.declare_entry ~name:(Id.of_string "hack")
      ~kind:(IsProof Lemma) ~impargs:[] ~uctx:UState.empty e
  in
  ()
}

VERNAC COMMAND EXTEND Hack CLASSIFIED AS SIDEFF
| [ "Hack" ] -> { Hack.hack() }
END

Hack defines opaque hack@{s' s|} : forall A : Type@{s|Set}, A -> A but due to #18594 the kernel thinks its relevance is s'.

Exploit coq code (omitting Declare ML Module):

Hack.

Definition hack' := hack@{SProp Type|}.

Set Primitive Projections.
Record R (n:nat) := mk { x : nat; proof : n = x }.

Definition x0 := mk 0 0 eq_refl.
Definition x1 := mk 1 1 eq_refl.

Definition bad : (hack' _ x0).(x _) = (hack' _ x1).(x _) := eq_refl.

Lemma bad' : False.
Proof.
  apply (O_S 0).
  transitivity (hack' _ x0).(x _); [|transitivity (hack' _ x1).(x _)].
  - apply proof.
  - exact bad.
  - symmetry;apply proof.
Qed.

The resulting vo is accepted by coqchk due to #18625

[SkySkimmer]

Fixed by #18596