Univs: entirely disallow instantiation of polymorphic constants with

Prop levels.

As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.

8 files changed, 102 insertions, 80 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index dc0a4b43c..2b3a2bdb1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1707,7 +1707,9 @@ struct
     else if Array.length y = 0 then x 
     else Array.append x y
 
-  let of_array a = a
+  let of_array a =
+    assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+    a
 
   let to_array a = a
 
@@ -1715,7 +1717,7 @@ struct
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else t'
+      if t' == t then t else of_array t'
 
   let levels x = LSet.of_array x
 
diff --git a/library/declare.ml b/library/declare.ml
index 5968fbf38..994a6557a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -431,7 +431,7 @@ let cache_universes (p, l) =
 		     Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
   in
-    Global.push_context_set false ctx;
+    Global.push_context_set p ctx;
     if p then Lib.add_section_context ctx;
     Universes.set_global_universe_names glob'
 
diff --git a/library/universes.ml b/library/universes.ml
index 1b6f7a9d5..a8e9478e1 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
 	      if d == Univ.Le then
 		enforce_leq inst (Universe.make r) cstrs
-	      else 
+	      else
 		try let lev = Option.get (Universe.level inst) in
 		      Constraint.add (lev, d, r) cstrs
 		with Option.IsNone -> failwith "")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dd4fcf198..faba5c756 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -394,18 +394,22 @@ let pretype_global loc rigid env evd gr us =
     match us with
     | None -> evd, None
     | Some l -> 
-      let _, ctx = Universes.unsafe_constr_of_global gr in
-      let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
-      let len = Array.length arr in
-	if len != List.length l then
-	  user_err_loc (loc, "pretype", 
-			str "Universe instance should have length " ++ int len)
-	else
-	  let evd, l' = List.fold_left (fun (evd, univs) l -> 
+       let _, ctx = Universes.unsafe_constr_of_global gr in
+       let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
+       let len = Array.length arr in
+       if len != List.length l then
+	 user_err_loc (loc, "pretype", 
+		       str "Universe instance should have length " ++ int len)
+       else
+	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
 	    let evd, l = interp_universe_level_name evd l in
 	      (evd, l :: univs)) (evd, []) l
-      in 
-	evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+	 in
+	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
+	   user_err_loc (loc, "pretype",
+		 str "Universe instances cannot contain Prop, polymorphic" ++
+		   str " universe instances must be greater or equal to Set.");
+	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
   in
     Evd.fresh_global ~rigid ?names:instance env evd gr
 
@@ -440,13 +444,15 @@ let pretype_sort evdref = function
 
 let new_type_evar env evdref loc =
   let e, s = 
-    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
+    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
+      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
   in e
 
 let get_projection env cst =
   let cb = lookup_constant cst env in
     match cb.Declarations.const_proj with
-    | Some {Declarations.proj_ind = mind; proj_npars = n; proj_arg = m; proj_type = ty} -> 
+    | Some {Declarations.proj_ind = mind; proj_npars = n;
+	    proj_arg = m; proj_type = ty} -> 
       (cst,mind,n,m,ty)
     | None -> raise Not_found
 
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b8..43c9b5129 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) :=
   let foo (A : Type@{j}) := A in foo B.
 
 Fail Check @setlt@{j Prop}.
-Check @setlt@{Prop j}.
-Check @setle@{Prop j}.
-
 Fail Definition foo := @setle@{j Prop}.
-Definition foo := @setle@{Prop j}.
+Check setlt@{Set i}.
+Check setlt@{Set j}.
\ No newline at end of file
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index fdedbf672..b13671cec 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -269,16 +269,6 @@ Section GenericInstances.
   Unset Strict Universe Declaration.
   
   (** The complement of a crelation conserves its proper elements. *)
-  Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
-          `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-    Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
-  
-  Next Obligation.
-  Proof.
-    unfold complement.
-    pose (mR x y X x0 y0 X0).
-    intuition.
-  Qed.
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
   Program Definition flip_proper
@@ -521,8 +511,8 @@ Ltac proper_reflexive :=
 Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
 Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
 
-Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
-  : typeclass_instances.
+(* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper  *)
+(*   : typeclass_instances. *)
 Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
   : typeclass_instances.
 Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 6f736e45f..cdc3e0461 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -658,4 +658,3 @@ Proof.
     exists x; intro; exact Hx.
     exists x0; exact Hnot.
 Qed.
-
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index ede51f57f..4e582934a 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -344,53 +344,6 @@ End Paradox.
 
 End NoRetractToImpredicativeUniverse.
 
-(** * Prop is not a retract *)
-
-(** The existence in the pure Calculus of Constructions of a retract
-    from [Prop] into a small type of [Prop] is inconsistent. This is a
-    special case of the previous result. *)
-
-Module NoRetractFromSmallPropositionToProp.
-
-Section Paradox.
-
-(** ** Retract of [Prop] in a small type *)
-
-(** The retract is axiomatized using logical equivalence as the
-    equality on propositions. *)
-
-Variable bool : Prop.
-Variable p2b : Prop -> bool.
-Variable b2p : bool -> Prop.
-Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
-Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
-
-(** ** Paradox *)
-
-Theorem paradox : forall B:Prop, B.
-Proof.
-  intros B.
-  pose proof
-      (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
-  refine (P _ _ _ _ _ _ _ _ _ _);clear P.
-  + exact bool.
-  + exact (fun x => forall P:Prop, (x->P)->P).
-  + cbn. exact (fun _ x P k => k x).
-  + cbn. intros F P x.
-    apply P.
-    intros f.
-    exact (f x).
-  + cbn. easy.
-  + exact b2p.
-  + exact p2b.
-  + exact p2p2.
-  + exact p2p1.
-Qed.
-
-End Paradox.
-
-End NoRetractFromSmallPropositionToProp.
-
 (** * Modal fragments of [Prop] are not retracts *)
 
 (** In presence of a a monadic modality on [Prop], we can define a
@@ -534,6 +487,80 @@ End Paradox.
 
 End NoRetractToNegativeProp.
 
+(** * Prop is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+    from [Prop] into a small type of [Prop] is inconsistent. This is a
+    special case of the previous result. *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+(** ** The universe of propositions. *)
+
+Definition NProp := { P:Prop | P -> P}.
+Definition El : NProp -> Prop := @proj1_sig _ _.
+
+Section MParadox.
+
+(** ** Retract of [Prop] in a small type, using the identity modality. *)
+
+Variable bool : NProp.
+Variable p2b : NProp -> El bool.
+Variable b2p : El bool -> NProp.
+Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem mparadox : forall B:NProp, El B.
+Proof.
+  intros B.
+  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  + exact (fun P => P).
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + exact bool.
+  + exact p2b.
+  + exact b2p.
+  + auto.
+  + auto.
+  + exact B.
+  + exact h.
+Qed.
+
+End MParadox.
+
+Section Paradox.
+
+(** ** Retract of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+    equality on propositions. *)
+Variable bool : Prop.
+Variable p2b : Prop -> bool.
+Variable b2p : bool -> Prop.
+Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
+Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:Prop, B.
+Proof.
+  intros B.
+  refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+                   (exist _ B (fun x => x))).
+  + intros p. red. red. exact (p2b (El p)).
+  + cbn. intros b. red. exists (b2p b). exact (fun x => x).
+  + cbn. intros [A H]. cbn. apply p2p1.
+  + cbn. intros [A H]. cbn. apply p2p2.
+Qed.
+
+End Paradox.
+
+End NoRetractFromSmallPropositionToProp.
+
+
 (** * Large universes are no retracts of [Prop]. *)
 
 (** The existence in the Calculus of Constructions with universes of a