Universes: enforce Set <= i for all Type occurrences.

10 files changed, 128 insertions, 74 deletions

diff --git a/Makefile.build b/Makefile.build
index 30b93a0e8..0455a247b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -69,7 +69,7 @@ TIMED=          # non-empty will activate a default time command
 
 TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
                 # e.g. "'time -p'"
-
+CAMLFLAGS:=${CAMLFLAGS} -w -3
 # NB: if you want to collect compilation timings of .v and import them
 # in a spreadsheet, I suggest something like:
 #   make TIMED=1 2> timings.csv
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8c89abe94..9c065101a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -286,7 +286,10 @@ let typecheck_inductive env mie =
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
 	  type_in_type env || (check_leq (universes env') infu defu &&
-	    not (is_type0m_univ defu && not is_unit))
+				not (is_type0m_univ defu && not is_unit)
+				  (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *)
+
+			     )
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 336cdb653..040e9bc27 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -270,8 +270,10 @@ module Level = struct
   let is_small x = 
     match data x with
     | Level _ -> false
-    | _ -> true
-
+    | Var _ -> false
+    | Prop -> true
+    | Set -> true
+ 
   let is_prop x =
     match data x with
     | Prop -> true
@@ -670,7 +672,7 @@ let arc_is_lt arc = match arc.status with
 | Unset | SetLe -> false
 | SetLt -> true
 
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset}
+let terminal ?(predicative=false) u = {univ=u; lt=[]; le=[]; rank=0; predicative; status = Unset}
 
 module UMap :
 sig
@@ -720,6 +722,16 @@ let enter_arc ca g =
 
 (* Every Level.t has a unique canonical arc representative *)
 
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+  {(terminal u) with lt=[v]}
+    
+let empty_universes =
+  let g = enter_arc (terminal ~predicative:true Level.set) UMap.empty in
+  let g = enter_arc (terminal_lt Level.prop Level.set) g in
+    g
+
 (* repr : universes -> Level.t -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 
@@ -733,6 +745,22 @@ let rec repr g u =
     | Equiv v -> repr g v
     | Canonical arc -> arc
 
+let get_prop_arc g = repr g Level.prop
+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. *)
 
@@ -745,6 +773,8 @@ let safe_repr g u =
   try g, safe_repr_rec g u
   with Not_found ->
     let can = terminal u in
+    let setarc = get_set_arc g in
+    let g = enter_arc {setarc with le=u::setarc.le} g in
     enter_arc can g, can
 
 (* reprleq : canonical_arc -> canonical_arc list *)
@@ -789,7 +819,6 @@ let between g arcu arcv =
   in
   let good,_,_ = explore ([arcv],[],false) arcu in
     good
-
 (* We assume  compare(u,v) = LE with v canonical (see compare below).
    In this case List.hd(between g u v) = repr u
    Otherwise, between g u v = []
@@ -900,8 +929,9 @@ let get_explanation strict g arcu arcv =
         in
         find [] arc.lt
   in
+  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
   try
-    let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
+    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
     (** Reset all the touched arcs. *)
     let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
     List.rev c
@@ -972,7 +1002,6 @@ let fast_compare_neq strict g arcu arcv =
     else process_le c to_revert (arc :: lt_todo) le_todo lt le
 
   in
-
   try
     let (to_revert, c) = cmp FastNLE [] [] [arcu] in
     (** Reset all the touched arcs. *)
@@ -1021,10 +1050,6 @@ let check_equal g u v =
 
 let check_eq_level g u v = u == v || check_equal g u v
 
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-let get_prop_arc g = snd (safe_repr g Level.prop)
-
 let check_smaller g strict u v =
   let g, arcu = safe_repr g u in
   let g, arcv = safe_repr g v in
@@ -1120,7 +1145,7 @@ 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 Level.is_small arc.univ || arc.rank >= max_rank
+      if 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
@@ -1150,7 +1175,7 @@ let merge g arcu arcv =
 (* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g arc1 arc2 =
-  let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
   let arcu, g = 
     if not (Int.equal arc1.rank arc2.rank) then arcu, g
     else
@@ -1173,8 +1198,8 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v (p:explanation option) =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforc_univ_eq : Level.t -> Level.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
   let g,arcu = safe_repr g u in
@@ -1225,18 +1250,10 @@ let enforce_univ_lt u v g =
         let p = get_explanation false g arcv arcu  in
         error_inconsistency Lt u v p
 
-let empty_universes = UMap.empty
-
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes = empty_universes
 
 let is_initial_universes g = UMap.equal (==) g initial_universes
-
-let add_universe vlev g = 
-  let v = terminal vlev in
-  let proparc = get_prop_arc g in
-    enter_arc {proparc with le=vlev::proparc.le}
-      (enter_arc v g)
       
 (* Constraints and sets of constraints. *)    
 
@@ -1370,10 +1387,12 @@ let check_univ_leq u v =
 
 let enforce_leq u v c =
   let open Universe.Huniv in
+  let rec aux acc v =
   match v with
-  | Cons (v, _, Nil) ->
-    fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+  | Cons (v, _, l) ->
+    aux (fold (fun u -> constraint_add_leq u v) u c) l
+  | Nil -> acc
+  in aux c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7aaf2ffe6..76453cbb0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,11 @@ sig
 
   val is_small : t -> bool
   (** Is the universe set or prop? *)
-
+		       
+  val is_prop : t -> bool
+  val is_set : t -> bool
+  (** Is it specifically Prop or Set *)
+		       
   val compare : t -> t -> int
   (** Comparison function *)
 
@@ -159,8 +163,8 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop. *)
-val add_universe : universe_level -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= Prop or Set. *)
+val add_universe : universe_level -> predicative:bool -> universes -> universes
 
 (** {6 Constraints. } *)
 
diff --git a/library/universes.ml b/library/universes.ml
index 1c8a5ad77..c67371e3b 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -182,10 +182,13 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_leq univs u1 u2 then true
-	else
-	  (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
-	   true)
+	  if Univ.check_leq univs u1 u2 then
+	    ((if Univ.is_small_univ u1 then
+		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
+	     true)
+	  else
+	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
+	     true)
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -820,10 +823,18 @@ let minimize_univ_variables ctx us algs left right cstrs =
       if v == None then fst (aux acc u)
       else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs)
       us (ctx, us, algs, lbounds, cstrs)
-      
+
 let normalize_context_set ctx us algs = 
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   let uf = UF.create () in
+  (** 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)
+	else (smallles, Constraint.add cstr noneqs))
+    csts (Constraint.empty, Constraint.empty)
+  in
   let csts = 
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
@@ -831,11 +842,15 @@ let normalize_context_set ctx us algs =
       Univ.constraints_of_universes g
   in
   let noneqs =
-    Constraint.fold (fun (l,d,r) noneqs ->
-      if d == Eq then (UF.union l r uf; noneqs) 
-      else Constraint.add (l,d,r) noneqs)
-    csts Constraint.empty
+    Constraint.fold (fun (l,d,r as cstr) noneqs ->
+      if d == Eq then (UF.union l r uf; noneqs)
+      else (* We ignore the trivial Prop/Set <= i constraints. *)
+	if d == Le && Univ.Level.is_small l then
+	  noneqs
+	else Constraint.add cstr noneqs)
+      csts Constraint.empty
   in
+  let noneqs = Constraint.union noneqs smallles in
   let partition = UF.partition uf in
   let flex x = LMap.mem x us in
   let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> 
@@ -941,12 +956,12 @@ let simplify_universe_context (univs,csts) =
   let csts' = subst_univs_level_constraints subst csts' in
     (univs', csts'), subst
 
-let is_small_leq (l,d,r) =
-  Level.is_small l && d == Univ.Le
+let is_trivial_leq (l,d,r) =
+  Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))
 
 (* Prop < i <-> Set+1 <= i <-> Set < i *)
 let translate_cstr (l,d,r as cstr) =
-  if Level.equal Level.prop l && d == Univ.Lt then
+  if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then
     (Level.set, d, r)
   else cstr
 
@@ -954,7 +969,7 @@ let refresh_constraints univs (ctx, cstrs) =
   let cstrs', univs' = 
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
-      if Univ.check_constraint univs c && not (is_small_leq c) then acc
+      if is_trivial_leq c then acc
       else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 632611291..fe5f12dd8 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -453,7 +453,7 @@ let add_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes }
+      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
 
 (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -1058,36 +1058,49 @@ let with_context_set rigid d (a, ctx) =
 let add_uctx_names s l (names, names_rev) =
     (UNameMap.add s l names, Univ.LMap.add l s names_rev)
 
-let uctx_new_univ_variable rigid name
+let uctx_new_univ_variable rigid name predicative
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.add_universe u ctx in
-  let uctx' = 
+  let uctx', pred =
     match rigid with
-    | UnivRigid -> uctx
+    | UnivRigid -> uctx, true
     | UnivFlexible b -> 
       let uvars' = Univ.LMap.add u None uvars in
 	if b then {uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.add u avars}
-	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
+	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
+	else {uctx with uctx_univ_variables = uvars'}, false
+  in
+  (* let ctx' = *)
+  (*   if pred then *)
+  (*     Univ.ContextSet.add_constraints *)
+  (* 	(Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *)
+  (*   else ctx' *)
+  (* in *)
   let names = 
     match name with
     | Some n -> add_uctx_names n u uctx.uctx_names
     | None -> uctx.uctx_names
   in
+  let initial =
+    Univ.add_universe u pred uctx.uctx_initial_universes
+  in						     
+  let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-      uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
-
-let new_univ_level_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+		uctx_universes = Univ.add_universe u pred uctx.uctx_universes;
+		uctx_initial_universes = initial}
+  in uctx', u
+						     
+let new_univ_level_variable ?name ?(predicative=true) rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+let new_univ_variable ?name ?(predicative=true) rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?name rigid d =
-  let (d', u) = new_univ_variable rigid ?name d in
+let new_sort_variable ?name ?(predicative=true) rigid d =
+  let (d', u) = new_univ_variable rigid ?name ~predicative d in
     (d', Type u)
 
 let make_flexible_variable evd b u =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 94d9d5f66..c2ccc6d21 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -505,9 +505,9 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 048faa916..9d3952e64 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -267,10 +267,9 @@ Section GenericInstances.
   Qed.
 
   (** The complement of a crelation conserves its proper elements. *)
-  
   Program Definition complement_proper
           `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-    Proper (RA ==> RA ==> iff) (complement R) := _.
+    Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
   
   Next Obligation.
   Proof.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 50f853f0e..375495c88 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -370,7 +370,7 @@ Module EqNotations.
 End EqNotations.
 
 Import EqNotations.
-
+Set Printing Universes.
 Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
 Proof.
 intros.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index e2e5d8704..d397eed61 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -467,16 +467,17 @@ let inductive_levels env evdref poly arities inds =
 	    Evd.set_leq_sort env evd (Prop Pos) du
 	  else evd
 	in
-	  (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *)
-	  let duu = Sorts.univ_of_sort du in
-	  let evd =
-	    if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
-	      if is_flexible_sort evd duu then
-		Evd.set_eq_sort env evd (Prop Null) du
-	      else evd
-	    else Evd.set_eq_sort env evd (Type cu) du
-	  in
-	    (evd, arity :: arities))
+	let duu = Sorts.univ_of_sort du in
+	let evd =
+	  if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
+	    if is_flexible_sort evd duu then
+	      if Evd.check_leq evd Univ.type0_univ duu then
+	      	evd
+	      else Evd.set_eq_sort env evd (Prop Null) du
+	    else evd
+	  else Evd.set_eq_sort env evd (Type cu) du
+	in
+	  (evd, arity :: arities))
     (!evdref,[]) (Array.to_list levels') destarities sizes
   in evdref := evd; List.rev arities