- Fix in kernel conversion not folding the universe constraints

correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.

2 files changed, 39 insertions, 66 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8773f4f34..a820e337e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -221,47 +221,23 @@ type conv_pb =
 let is_cumul = function CUMUL -> true | CONV -> false
 let is_pos = function Pos -> true | Null -> false
 
-(* let sort_cmp env pb s0 s1 cuniv = *)
-(*   match (s0,s1) with *)
-(*     | (Prop c1, Prop c2) when is_cumul pb -> *)
-(*       begin match c1, c2 with *)
-(*       | Null, _ | _, Pos -> cuniv (\* Prop <= Set *\) *)
-(*       | _ -> raise NotConvertible *)
-(*       end *)
-(*     | (Prop c1, Prop c2) -> *)
-(*         if c1 == c2 then cuniv else raise NotConvertible *)
-(*     | (Prop c1, Type u) when is_cumul pb -> *)
-(*       enforce_leq (if is_pos c1 then Universe.type0 else Universe.type0m) u cuniv *)
-(*     | (Type u, Prop c) when is_cumul pb -> *)
-(*       enforce_leq u (if is_pos c then Universe.type0 else Universe.type0m) cuniv *)
-(*     | (Type u1, Type u2) -> *)
-(* 	(match pb with *)
-(*            | CONV -> Univ.enforce_eq u1 u2 cuniv *)
-(* 	   | CUMUL -> enforce_leq u1 u2 cuniv) *)
-(*     | (_, _) -> raise NotConvertible *)
-
-(* let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty *)
-(* let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty   *)
-
 let check_eq (univs, cstrs as cuniv) u u' = 
   match cstrs with
   | None -> if check_eq univs u u' then cuniv else raise NotConvertible
   | Some cstrs -> 
     univs, Some (Univ.enforce_eq u u' cstrs)
-    (* let cstr = Univ.enforce_eq u u' Univ.Constraint.empty in *)
-    (* try let univs' = Univ.enforce_constraint cstr univs in *)
-    (* 	  univs', Some (Univ.enforce_eq u u' cstrs) *)
-    (* with UniverseInconsistency _ -> raise NotConvertible *)
 
-let check_leq (univs, cstrs as cuniv) u u' = 
+let check_leq ?(record=false) (univs, cstrs as cuniv) u u' = 
   match cstrs with
   | None -> if check_leq univs u u' then cuniv else raise NotConvertible
   | Some cstrs -> 
-    univs, Some (Univ.enforce_leq u u' cstrs)
-    (* let cstr = Univ.enforce_leq u u' Univ.Constraint.empty in *)
-    (*   try let univs' = Univ.enforce_constraint cstr univs in *)
-    (* 	    univs', Some (Univ.enforce_leq u u' cstrs) *)
-    (*   with UniverseInconsistency _ -> raise NotConvertible *)
+    let cstrs' = Univ.enforce_leq u u' cstrs in
+    let cstrs' = if record then 
+	Univ.Constraint.add (Option.get (Univ.Universe.level u),Univ.Le,
+			     Option.get (Univ.Universe.level u')) cstrs' 
+      else cstrs' 
+    in
+      univs, Some cstrs'
 
 let sort_cmp_universes pb s0 s1 univs =
   match (s0,s1) with
@@ -274,23 +250,14 @@ let sort_cmp_universes pb s0 s1 univs =
     | (Prop c1, Type u) ->
       let u0 = univ_of_sort s0 in
 	(match pb with
-	| CUMUL -> check_leq univs u0 u
+	| CUMUL -> check_leq ~record:true univs u0 u
 	| CONV -> check_eq univs u0 u)
-    | (Type u, Prop c) -> 
-      let u1 = univ_of_sort s1 in
-	(match pb with
-	| CUMUL -> check_leq univs u u1
-	| CONV -> check_eq univs u u1)
+    | (Type u, Prop c) -> raise NotConvertible
     | (Type u1, Type u2) -> 
 	(match pb with
 	| CUMUL -> check_leq univs u1 u2
 	| CONV -> check_eq univs u1 u2)
 
-(* let sort_cmp _ _ _ cuniv = cuniv *)
-
-(* let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint *)
-(* let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint *)
-
 let rec no_arg_available = function
   | [] -> true
   | Zupdate _ :: stk -> no_arg_available stk
@@ -594,7 +561,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
 and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
-    (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
+    (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
     (eq_ind)
     lft1 stk1 lft2 stk2 cuniv
 
@@ -665,7 +632,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
     if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 
     else Constr.eq_constr_univs_infer univs t1 t2
   in
-    if b && Univ.check_constraints cstrs univs then cstrs
+    if b && (try ignore(Univ.merge_constraints cstrs univs); true with _ -> false) then 
+      cstrs
     else 
       let (u, cstrs) = 
 	clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8a48eb5db..7ab0aa93c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1341,7 +1341,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 arc.rank >= max_rank
+      if Level.is_small arc.univ || arc.rank >= max_rank
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
@@ -1394,27 +1394,13 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v (p:explanation) =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforce_univ_leq : Level.t -> Level.t -> unit *)
-(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
-let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
-  if is_leq g arcu arcv then g
-  else match fast_compare g arcv arcu with
-    | FastLT -> 
-      (match compare g arcv arcu with
-      | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p))
-      | _ -> anomaly (Pp.str "Univ.fast_compare"))
-    | FastLE  -> merge g arcv arcu
-    | FastNLE -> fst (setleq g arcu arcv)
-    | FastEQ -> anomaly (Pp.str "Univ.compare")
-
 (* enforc_univ_eq : Level.t -> Level.t -> unit *)
 (* enforc_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
   let g,arcv = safe_repr g v in
-  match fast_compare g arcu arcv with
+    match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT ->
       (match compare g arcu arcv with
@@ -1431,11 +1417,27 @@ let enforce_univ_eq u v g =
       | FastNLE -> merge_disc g arcu arcv
       | FastEQ -> anomaly (Pp.str "Univ.compare"))
 
+(* enforce_univ_leq : Level.t -> Level.t -> unit *)
+(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
+let enforce_univ_leq u v g =
+  let g,arcu = safe_repr g u in
+  let g,arcv = safe_repr g v in
+  if is_leq g arcu arcv then g
+  else
+    match fast_compare g arcv arcu with
+    | FastLT -> 
+      (match compare g arcv arcu with
+      | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p))
+      | _ -> anomaly (Pp.str "Univ.fast_compare"))
+    | FastLE  -> merge g arcv arcu
+    | FastNLE -> fst (setleq g arcu arcv)
+    | FastEQ -> anomaly (Pp.str "Univ.compare")
+
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
   let g,arcu = safe_repr g u in
   let g,arcv = safe_repr g v in
-  match fast_compare g arcu arcv with
+    match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
     | FastEQ -> 
@@ -1452,7 +1454,10 @@ let enforce_univ_lt u v g =
 	| _ -> anomaly (Pp.str "Univ.fast_compare"))
 	  
 let empty_universes = LMap.empty
-let initial_universes = enforce_univ_leq Level.prop Level.set LMap.empty
+
+(* Prop = Set is forbidden here. *)
+let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty
+
 let is_initial_universes g = LMap.equal (==) g initial_universes
 
 (* Constraints and sets of constraints. *)    
@@ -2176,7 +2181,7 @@ let normalize_universes g =
         univ = v;
         lt = LSet.elements lt;
         le = LSet.elements le;
-	rank = rank
+	rank = rank;
       }
   in
   LMap.mapi canonicalize g
@@ -2321,7 +2326,7 @@ let sort_universes orig =
   let fold i accu u =
     if 0 < i then
       let pred = types.(i - 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; } in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0} in
       LMap.add u (Canonical arc) accu
     else accu
   in