Minimize Prop <= i to i := Set

Fix part of #8196, fix #12414
Replaces #9343

5 files changed, 32 insertions, 3 deletions

diff --git a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst
new file mode 100644
index 0000000000..6c442ca1aa
--- /dev/null
+++ b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst
@@ -0,0 +1,5 @@
+- **Changed:** Heuristics for universe minimization to :g:`Set`: also
+  use constraints ``Prop <= i`` (`#10331
+  <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with
+  help from Maxime Dénès and Matthieu Sozeau, fixes `#12414
+  <https://github.com/coq/coq/issues/12414>`_).
diff --git a/engine/uState.ml b/engine/uState.ml
index 2cb88c7fff..9557111cfd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -675,7 +675,7 @@ let subst_univs_context_with_def def usubst (ctx, cst) =
   (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
 
 let is_trivial_leq (l,d,r) =
-  Level.is_prop l && (d == Le || (d == Lt && Level.is_set r))
+  Level.is_prop l && (d == Le || d == Lt) && Level.is_set r
 
 (* Prop < i <-> Set+1 <= i <-> Set < i *)
 let translate_cstr (l,d,r as cstr) =
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index c5854e27f3..4ed6e97526 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -292,17 +292,23 @@ let is_bound l lbound = match lbound with
 | UGraph.Bound.Prop -> Level.is_prop l
 | UGraph.Bound.Set -> Level.is_set l
 
+(* if [is_minimal u] then constraints [u <= v] may be dropped and get
+   used only for set_minimization. *)
+let is_minimal ~lbound u =
+  Level.is_sprop u || Level.is_prop u || is_bound u lbound
+
 (* TODO check is_small/sprop *)
 let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && is_minimal ~lbound l) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
     else Constraint.empty
   in
+  let smallles = Constraint.map (fun (_,_,r) -> Level.set, Le, r) smallles in
   let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
diff --git a/test-suite/bugs/closed/bug_12414.v b/test-suite/bugs/closed/bug_12414.v
new file mode 100644
index 0000000000..50b4b86eff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12414.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Inductive list {T} : Type := | cons (t : T) : list -> list. (* who needs nil anyway? *)
+Arguments list : clear implicits.
+
+Fixpoint map {A B} (f: A -> B) (l : list A) : list B :=
+  let '(cons t l) := l in cons (f t) (map f l).
+About map@{_ _}.
+(* Two universes, as expected. *)
+
+Definition map_Set@{} {A B : Set} := @map A B.
+
+Definition map_Prop@{} {A B : Prop} := @map A B.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9ab8ace39e..0796b507a1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -457,5 +457,10 @@ Module ObligationRegression.
   (** Test for a regression encountered when fixing obligations for
       stronger restriction of universe context. *)
   Require Import CMorphisms.
-  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _ _}.
+  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _}.
 End ObligationRegression.
+
+Axiom poly@{i} : forall(A : Type@{i}) (a : A), unit.
+
+Definition nonpoly := @poly True Logic.I.
+Definition check := nonpoly@{}.