Merge PR coq#17810: Warn when minimizing inductive to set even though…

… minim to set is off

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

engine/univMinim.mli

@@ -39,3 +39,5 @@ val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t ->
   Level.Set.t (* univ variables that can be substituted by algebraics *) ->
   extra ->
   (universe_opt_subst * Level.Set.t) in_universe_context_set
+
+val get_set_minimization : unit -> bool

vernac/comInductive.ml

@@ -528,15 +528,33 @@ let variance_of_entry ~cumulative ~variances uctx =
       assert (lvs <= lus);
       Some (Array.append variances (Array.make (lus - lvs) None))
 
+let warn_bad_set_minimization =
+  CWarnings.create ~name:"bad-set-minimization" ~category:Deprecation.Version.v8_18
+    Pp.(fun () -> strbrk "This inductive will be minimized to Set even though Universe Minimization ToSet is unset. This will change in a future version.")
+
+let warn_bad_set_minimization ?loc () =
+  if UnivMinim.get_set_minimization () then ()
+  else warn_bad_set_minimization ?loc ()
+
 let interp_mutual_inductive_constr ~sigma ~template ~udecl ~variances ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
   (* Compute renewed arities *)
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (on_snd (List.map nf)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
-  let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
-  let sigma = Evd.minimize_universes sigma in
+  let sigma', arities = inductive_levels env_ar_params sigma arities constructors in
+  let sigma =
+    let sigma' = Evd.minimize_universes sigma' in
+    let () = List.iter (fun ty ->
+        let _, s = Reduction.dest_arity env_ar_params ty in
+        let s = EConstr.ESorts.make s in
+        if EConstr.ESorts.is_set sigma' s && not (EConstr.ESorts.is_set sigma s)
+        then warn_bad_set_minimization ())
+        arities
+    in
+    sigma'
+  in
   let nf = Evarutil.nf_evars_universes sigma in
   let arities = List.map nf arities in
   let constructors = List.map (on_snd (List.map nf)) constructors in
@@ -857,5 +875,5 @@ module Internal =
 struct
 
 let compute_constructor_level = compute_constructor_level
-
+let warn_bad_set_minimization = warn_bad_set_minimization
 end

vernac/comInductive.mli

@@ -125,4 +125,5 @@ val variance_of_entry
 module Internal :
 sig
   val compute_constructor_level : Environ.env -> Evd.evar_map -> EConstr.rel_context -> Sorts.t
+  val warn_bad_set_minimization : ?loc:Loc.t  -> unit -> unit
 end

vernac/record.ml

@@ -225,8 +225,9 @@ let typecheck_params_and_fields def poly udecl ps (records : DataI.t list) : tc_
         if Sorts.is_small univ &&
            Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma esort) then
            (* We can assume that the level in aritysort is not constrained
-               and clear it, if it is flexible *)
-          Evd.set_eq_sort env_ar sigma EConstr.ESorts.set esort, (univ, EConstr.mkSort (EConstr.ESorts.make univ))
+               and clear it, if it is flexible *) begin
+          ComInductive.Internal.warn_bad_set_minimization ();
+          Evd.set_eq_sort env_ar sigma EConstr.ESorts.set esort, (univ, EConstr.mkSort (EConstr.ESorts.make univ)) end
         else sigma, (univ, typ)
   in
   let (sigma, typs) = List.fold_left2_map fold sigma typs data in