Merge PR #13305: Only lower inductives to Prop if the type is syntactically an arity.

Reviewed-by: ppedrot

1 files changed, 14 insertions, 8 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 597e55a39e..8cb077ca21 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -271,9 +271,8 @@ let inductive_levels env evd arities inds =
     if Sorts.is_prop a || Sorts.is_sprop a then None
     else Some (univ_of_sort a)) destarities
   in
-  let cstrs_levels, min_levels, sizes =
-    CList.split3
-      (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
+  let cstrs_levels, sizes =
+    CList.split (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
         let len = List.length tys in
         let minlev = Sorts.univ_of_sort du in
         let minlev =
@@ -283,13 +282,15 @@ let inductive_levels env evd arities inds =
         in
         let minlev =
           (* Indices contribute. *)
-          if indices_matter env && List.length ctx > 0 then (
+          if indices_matter env then begin
             let ilev = sign_level env evd ctx in
-              Univ.sup ilev minlev)
+            Univ.sup ilev minlev
+          end
           else minlev
         in
         let clev = extract_level env evd minlev tys in
-          (clev, minlev, len)) inds destarities)
+        (clev, len))
+        inds destarities)
   in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
@@ -326,8 +327,13 @@ let inductive_levels env evd arities inds =
         let duu = Sorts.univ_of_sort du in
         let template_prop, evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
-            if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              true, Evd.set_eq_sort env evd Sorts.prop du
+            if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu)
+            then if Term.isArity arity
+            (* If not a syntactic arity, the universe may be used in a
+               polymorphic instance and so cannot be lowered to Prop.
+               See #13300. *)
+              then true, Evd.set_eq_sort env evd Sorts.prop du
+              else false, Evd.set_eq_sort env evd Sorts.set du
             else false, evd
           else false, Evd.set_eq_sort env evd (sort_of_univ cu) du
         in