Merge PR #12449: Minimize Prop <= i to i := Set

Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares

13 files changed, 96 insertions, 36 deletions

diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh
new file mode 100644
index 0000000000..fb5947d218
--- /dev/null
+++ b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then
+
+    mtac2_CI_REF=janno/coq-12449
+    mtac2_CI_GITURL=https://github.com/mtac2/mtac2
+
+fi
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/kernel/environ.ml b/kernel/environ.ml
index e497b7904a..dec9e1deb8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -274,6 +274,11 @@ let is_impredicative_sort env = function
 
 let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
 
+let is_impredicative_family env = function
+  | Sorts.InSProp | Sorts.InProp -> true
+  | Sorts.InSet -> is_impredicative_set env
+  | Sorts.InType -> false
+
 let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 47a118aa42..f443ba38e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -122,6 +122,7 @@ val indices_matter : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
+val is_impredicative_family : env -> Sorts.family -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index f33030d6a4..eaf8c65811 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -175,10 +175,7 @@ let define_evar_as_sort env evd (ev,args) =
   let evd' = Evd.define ev (mkSort s) evd in
   Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s
 
-(* Propagation of constraints through application and abstraction:
-   Given a type constraint on a functional term, returns the type
-   constraint on its domain and codomain. If the input constraint is
-   an evar instantiate it with the product of 2 new evars. *)
+(* Unify with unknown array *)
 
 let rec presplit env sigma c =
   let c = Reductionops.whd_all env sigma c in
@@ -189,25 +186,6 @@ let rec presplit env sigma c =
     presplit env sigma (mkApp (lam, args))
   | _ -> sigma, c
 
-let split_tycon ?loc env evd tycon =
-  match tycon with
-  | None -> evd,(make_annot Anonymous Relevant,None,None)
-  | Some c ->
-    let evd, c = presplit env evd c in
-    let evd, na, dom, rng = match EConstr.kind evd c with
-      | Prod (na,dom,rng) -> evd, na, dom, rng
-      | Evar ev ->
-        let (evd,prod) = define_evar_as_product env evd ev in
-        let (na,dom,rng) = destProd evd prod in
-        let anon = {na with binder_name = Anonymous} in
-        evd, anon, dom, rng
-      | _ ->
-        (* XXX no error to allow later coercion? Not sure if possible with funclass *)
-        error_not_product ?loc env evd c
-    in
-    evd, (na, mk_tycon dom, mk_tycon rng)
-
-
 let define_pure_evar_as_array env sigma evk =
   let evi = Evd.find_undefined sigma evk in
   let evenv = evar_env env evi in
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index e5c3f8baa1..5702e169c8 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
 open EConstr
 open Evd
 open Environ
@@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
   evar_map * existential
 
-val split_tycon :
-  ?loc:Loc.t -> env ->  evar_map -> type_constraint ->
-    evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint)
-
 val split_as_array : env -> evar_map -> type_constraint ->
   evar_map * type_constraint
 (** If the constraint can be made to look like [array A] return [A],
@@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t
 
 val pr_tycon : env -> evar_map -> type_constraint -> Pp.t
 
+(** Used for bidi heuristic when typing lambdas. Transforms an applied
+    evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *)
+val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b9825b6a92..7597661ca8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -925,7 +925,32 @@ struct
         let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in
         sigma, Some ty'
     in
-    let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in
+    let sigma,name',dom,rng =
+      match tycon' with
+      | None -> sigma,Anonymous, None, None
+      | Some ty ->
+        let sigma, ty = Evardefine.presplit !!env sigma ty in
+        match EConstr.kind sigma ty with
+        | Prod (na,dom,rng) ->
+          sigma, na.binder_name, Some dom, Some rng
+        | Evar ev ->
+          (* define_evar_as_product works badly when impredicativity
+             is possible but not known (#12623). OTOH if we know we
+             are impredicative (typically Prop) we want to keep the
+             information when typing the body. *)
+          let s = Retyping.get_sort_of !!env sigma ty in
+          if Environ.is_impredicative_sort !!env s
+             || Evd.check_leq sigma (Univ.Universe.type1) (Sorts.univ_of_sort s)
+          then
+            let sigma, prod = define_evar_as_product !!env sigma ev in
+            let na,dom,rng = destProd sigma prod in
+            sigma, na.binder_name, Some dom, Some rng
+          else
+            sigma, Anonymous, None, None
+        | _ ->
+          (* XXX no error to allow later coercion? Not sure if possible with funclass *)
+          error_not_product ?loc !!env sigma ty
+    in
     let dom_valcon = valcon_of_tycon dom in
     let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in
     let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in
@@ -934,7 +959,7 @@ struct
     let var',env' = push_rel ~hypnaming sigma var env in
     let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in
     let name = get_name var' in
-    let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in
+    let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
     discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
   let pretype_prod self (name, bk, c1, c2) =
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/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v
new file mode 100644
index 0000000000..9fdcb94e0c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12623.v
@@ -0,0 +1,18 @@
+Set Universe Polymorphism.
+
+Axiom M : Type -> Prop.
+Axiom raise : forall {T}, M T.
+
+Inductive goal : Type :=
+| AHyp : forall {A : Type}, goal.
+
+Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False).
+
+Class Seq (C : Type) :=
+  seq : C -> gtactic.
+Arguments seq {C _} _.
+
+Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise.
+
+Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise).
+Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise).
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v
index 0c236e12ad..00b9e9bd9d 100644
--- a/test-suite/bugs/closed/bug_5197.v
+++ b/test-suite/bugs/closed/bug_5197.v
@@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {|
   rel := fun _ A => (forall ω : Ω, A ω) -> Type;
                           |}.
 Set Printing Universes.
-Fail Definition Typeᵇ : El Typeᶠ :=
+Definition Typeᵇ : El Typeᶠ :=
   mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
 
-Definition Typeᵇ : El Typeᶠ :=
-  mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type).
+(* Definition Typeᵇ : El Typeᶠ := *)
+(*   mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *)
 
 (** Bidirectional typechecking helps here *)
 Require Import Program.Tactics.
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@{}.