Forcing i > Set for global universes (incomplete)

8 files changed, 61 insertions, 39 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 109e3830c..c433c0789 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -181,26 +181,41 @@ let fold_named_context_reverse f ~init env =
 
 (* Universe constraints *)
 
-let add_constraints c env =
-  if Univ.Constraint.is_empty c then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+				     
+let add_constraints c env =
+  if Univ.Constraint.is_empty c then env
+  else map_universes (Univ.merge_constraints c) env
 
 let check_constraints c env =
   Univ.check_constraints c env.env_stratification.env_universes
 
-let set_engagement c env = (* Unsafe *)
-  { env with env_stratification =
-    { env.env_stratification with env_engagement = c } }
-
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+  let g = Array.fold_left (fun g v -> Univ.add_universe v strict g)
+			  g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+  in
+    Univ.merge_constraints (Univ.UContext.constraints ctx) g
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+  let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g)
+			 (Univ.ContextSet.levels ctx) g
+  in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = c } }
 
 (* Global constants *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4ad0327fc..9f6ea522a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env
 
 (** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83e566041..e89b6ef8f 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -100,11 +100,11 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
+	      
 let infer_declaration env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context uctx env in
+      let env = push_context ~strict:(not poly) uctx env in
       let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,7 +115,7 @@ let infer_declaration env kn dcl =
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:true c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -135,7 +135,7 @@ let infer_declaration env kn dcl =
 	c.const_entry_inline_code, c.const_entry_secctx
 
   | DefinitionEntry c ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:(not c.const_entry_polymorphic) c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 040e9bc27..b61b441d2 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -750,17 +750,6 @@ let get_set_arc g = repr g Level.set
 let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
-let add_universe vlev ~predicative g = 
-  let v = terminal ~predicative vlev in
-  let arc =
-    let arc =
-      if predicative then get_set_arc g else get_prop_arc g
-    in
-      { arc with le=vlev::arc.le}
-  in
-  let g = enter_arc arc g in
-    enter_arc v g
-
 (* [safe_repr] also search for the canonical representative, but
    if the graph doesn't contain the searched universe, we add it. *)
 
@@ -777,6 +766,18 @@ let safe_repr g u =
     let g = enter_arc {setarc with le=u::setarc.le} g in
     enter_arc can g, can
 
+let add_universe vlev strict g = 
+  let v = terminal ~predicative:true vlev in
+  let arc =
+    let arc = get_set_arc g in
+      if strict then
+	{ arc with lt=vlev::arc.lt}
+      else 
+	{ arc with le=vlev::arc.le}
+  in
+  let g = enter_arc arc g in
+    enter_arc v g
+
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
 let reprleq g arcu =
@@ -1145,7 +1146,8 @@ let merge g arcu arcv =
   (* we find the arc with the biggest rank, and we redirect all others to it *)
   let arcu, g, v =
     let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if arc.rank >= max_rank && not (Level.is_small best_arc.univ)
+      if Level.is_small arc.univ ||
+	   (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 76453cbb0..fe7fc1ab9 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,8 +163,8 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop or Set. *)
-val add_universe : universe_level -> predicative:bool -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set. *)
+val add_universe : universe_level -> bool -> universes -> universes
 
 (** {6 Constraints. } *)
 
diff --git a/library/universes.ml b/library/universes.ml
index c67371e3b..0544585dc 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -830,8 +830,13 @@ let normalize_context_set ctx us algs =
   (** Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
     Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
-	if d == Le && Univ.Level.is_small l then
-	  (Constraint.add cstr smallles, noneqs)
+        if d == Le then
+	  if Univ.Level.is_small l then
+	    (Constraint.add cstr smallles, noneqs)
+	  else if Level.is_small r then
+	    raise (Univ.UniverseInconsistency
+		     (Le,Universe.make l,Universe.make r,None))
+	  else (smallles, Constraint.add cstr noneqs)
 	else (smallles, Constraint.add cstr noneqs))
     csts (Constraint.empty, Constraint.empty)
   in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9f2d28438..a25479d48 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1083,11 +1083,11 @@ let uctx_new_univ_variable rigid name predicative
     | None -> uctx.uctx_names
   in
   let initial =
-    Univ.add_universe u true uctx.uctx_initial_universes
+    Univ.add_universe u false uctx.uctx_initial_universes
   in						     
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-		uctx_universes = Univ.add_universe u true uctx.uctx_universes;
+		uctx_universes = Univ.add_universe u false uctx.uctx_universes;
 		uctx_initial_universes = initial}
   in uctx', u
 						     
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index 980431576..6e97ed2af 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -117,7 +117,7 @@ intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact a
 Defined.
 
 Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X }  : iseqclass R A -> ishinh ( carrier A ) .
-intros X R A; exact ( fun is : iseqclass R A =>  projT1' _ is ).
+intros X R A. exact (fun is : iseqclass R A => projT1' _ is ).
 Defined.
 
 Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) .
@@ -141,7 +141,7 @@ Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f.
   admit.
 Defined.
 
-Definition setquot { X : UU } ( R : hrel X ) : Type.
+Definition setquot { X : UU } ( R : hrel X ) : Set.
 intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ).
 Defined.
 Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R.
@@ -157,7 +157,7 @@ Definition setquotinset { X : UU } ( R : hrel X ) : hSet.
 intros; exact ( hSetpair (setquot R) admit) .
 Defined.
 
-Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ).
+Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot@{i j k l m n p Set q r} RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ).
 intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _  ( projT2' _ cd ) ) ) ).
 Defined.