Make the universe of primitive arrays irrelevant

Fix #13354

This change is very specific to array, but should not be a significant
obstacle to generalization of the feature to eg axioms if we want to later.

7 files changed, 57 insertions, 26 deletions

diff --git a/doc/changelog/01-kernel/13356-primarray-cumul.rst b/doc/changelog/01-kernel/13356-primarray-cumul.rst
new file mode 100644
index 0000000000..978ca325bf
--- /dev/null
+++ b/doc/changelog/01-kernel/13356-primarray-cumul.rst
@@ -0,0 +1,5 @@
+- **Changed:** Primitive arrays are now irrelevant in their single
+  polymorphic universe (same as a polymorphic cumulative list
+  inductive would be) (`#13356
+  <https://github.com/coq/coq/pull/13356>`_, fixes `#13354
+  <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert).
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0c84dee572..c29de27efb 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -452,6 +452,9 @@ let eq_universes env sigma cstrs cv_pb refargs l l' =
     let open GlobRef in
     let open UnivProblem in
     match refargs with
+    | Some (ConstRef c, 1) when Environ.is_array_type env c ->
+      cstrs := compare_cumulative_instances cv_pb true [|Univ.Variance.Irrelevant|] l l' !cstrs;
+      true
     | None | Some (ConstRef _, _) ->
       cstrs := enforce_eq_instances_univs true l l' !cstrs; true
     | Some (VarRef _, _) -> assert false (* variables don't have instances *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 914c951eb6..716b098995 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -569,6 +569,11 @@ let is_primitive env c =
   | Declarations.Primitive _ -> true
   | _ -> false
 
+let is_array_type env c =
+  match env.retroknowledge.Retroknowledge.retro_array with
+  | None -> false
+  | Some c' -> Constant.CanOrd.equal c c'
+
 let polymorphic_constant cst env =
   Declareops.constant_is_polymorphic (lookup_constant cst env)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 60696184ef..344906897b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -250,6 +250,8 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 val is_primitive : env -> Constant.t -> bool
 
+val is_array_type : env -> Constant.t -> bool
+
 (** {6 Primitive projections} *)
 
 (** Checks that the number of parameters is correct. *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c891b885c4..cf40263f61 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -280,11 +280,12 @@ let convert_constructors ctor nargs u1 u2 (s, check) =
   convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
     ctor nargs u1 u2 s, check
 
-let conv_table_key infos k1 k2 cuniv =
+let conv_table_key infos ~nargs k1 k2 cuniv =
   if k1 == k2 then cuniv else
   match k1, k2 with
   | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' ->
     if Univ.Instance.equal u u' then cuniv
+    else if Int.equal nargs 1 && is_array_type (info_env infos) cst then cuniv
     else
       let flex = evaluable_constant cst (info_env infos)
         && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
@@ -304,6 +305,11 @@ let unfold_ref_with_args infos tab fl v =
     Some (a, (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v)))
   | Undef _ | OpaqueDef _ | Primitive _ -> None
 
+let same_args_size sk1 sk2 =
+  let n = CClosure.stack_args_size sk1 in
+  if Int.equal n (CClosure.stack_args_size sk2) then n
+  else raise NotConvertible
+
 type conv_tab = {
   cnv_inf : clos_infos;
   lft_tab : clos_tab;
@@ -408,7 +414,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
       (try
-         let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
+         let nargs = same_args_size v1 v2 in
+         let cuniv = conv_table_key infos.cnv_inf ~nargs fl1 fl2 cuniv in
          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible | Univ.UniverseInconsistency _ ->
         let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in
@@ -577,17 +584,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
-          let nargs = CClosure.stack_args_size v1 in
-          if not (Int.equal nargs (CClosure.stack_args_size v2))
-          then raise NotConvertible
-          else
-            match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
-            | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-            | exception MustExpand ->
-              let env = info_env infos.cnv_inf in
-              let hd1 = eta_expand_ind env pind1 in
-              let hd2 = eta_expand_ind env pind2 in
-              eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
+          let nargs = same_args_size v1 v2 in
+          match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
+          | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          | exception MustExpand ->
+            let env = info_env infos.cnv_inf in
+            let hd1 = eta_expand_ind env pind1 in
+            let hd2 = eta_expand_ind env pind2 in
+            eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
@@ -597,17 +601,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
-          let nargs = CClosure.stack_args_size v1 in
-          if not (Int.equal nargs (CClosure.stack_args_size v2))
-          then raise NotConvertible
-          else
-            match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
-            | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-            | exception MustExpand ->
-              let env = info_env infos.cnv_inf in
-              let hd1 = eta_expand_constructor env pctor1 in
-              let hd2 = eta_expand_constructor env pctor2 in
-              eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
+          let nargs = same_args_size v1 v2 in
+          match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
+          | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          | exception MustExpand ->
+            let env = info_env infos.cnv_inf in
+            let hd1 = eta_expand_constructor env pctor1 in
+            let hd2 = eta_expand_constructor env pctor2 in
+            eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
       else raise NotConvertible
 
     (* Eta expansion of records *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 90af143a2d..ca16c52026 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -567,8 +567,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     let compare_heads evd =
       match EConstr.kind evd term, EConstr.kind evd term' with
       | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
-        let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
-        check_strict evd u u'
+        if Int.equal (Stack.args_size sk) 1 && Environ.is_array_type env c
+        then
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          compare_cumulative_instances evd [|Univ.Variance.Irrelevant|] u u'
+        else
+          let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
+          check_strict evd u u'
       | Const _, Const _ -> UnifFailure (evd, NotSameHead)
       | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
         if EInstance.is_empty u && EInstance.is_empty u' then Success evd
diff --git a/test-suite/bugs/closed/bug_13354.v b/test-suite/bugs/closed/bug_13354.v
new file mode 100644
index 0000000000..fbda10a9d2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13354.v
@@ -0,0 +1,10 @@
+
+Primitive array := #array_type.
+
+Definition testArray : array nat := [| 1; 2; 4 | 0 : nat |].
+
+Definition on_array {A:Type} (x:array A) : Prop := True.
+
+Check on_array testArray.
+
+Check @on_array nat testArray.