- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some

cases of Type (* Prop *) <= Set.
- Do check types of metavariables at the end of apply's unification,
if it failed at the beginning (otherwise universe constraints can be incomplete).

4 files changed, 39 insertions, 35 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a820e337ef..5024675bff 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -167,12 +167,6 @@ let convert_universes (univs,cstrs as cuniv) u u' =
     | None -> raise NotConvertible
     | Some cstrs -> 
       (univs, Some (Univ.enforce_eq_instances u u' cstrs)))
-
-      (* try  *)
-      (* 	let cstr = Univ.enforce_eq_instances u u' Univ.Constraint.empty in *)
-      (* 	let univs' = Univ.enforce_constraint cstr univs in *)
-      (* 	  (univs', Some (Univ.enforce_eq_instances u u' cstrs)) *)
-      (* with UniverseInconsistency _ -> raise NotConvertible) *)
       
 let conv_table_key k1 k2 cuniv =
   match k1, k2 with
@@ -632,8 +626,7 @@ 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 && (try ignore(Univ.merge_constraints cstrs univs); true with _ -> false) then 
-      cstrs
+    if b 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 7ab0aa93c1..8984938d36 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1198,9 +1198,9 @@ let fast_compare g arcu arcv =
 
 let is_leq g arcu arcv =
   arcu == arcv ||
- (match fast_compare_neq false g arcu arcv with
- | FastNLE -> false
- | (FastEQ|FastLE|FastLT) -> true)
+    (match fast_compare_neq false g arcu arcv with
+    | FastNLE -> false
+    | (FastEQ|FastLE|FastLT) -> true)
     
 let is_lt g arcu arcv =
   if arcu == arcv then false
@@ -1241,7 +1241,7 @@ let check_smaller g strict u v =
     let proparc = prop_arc g in
       arcu == proparc ||
 	((arcv != proparc && arcu == set_arc g) ||
-	     is_leq g arcu arcv)
+	    is_leq g arcu arcv)
 
 (** Then, checks on universes *)
 
@@ -1345,17 +1345,17 @@ let merge g arcu arcv =
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
-    match between g arcu arcv with
+      match between g arcu arcv with
       | [] -> anomaly (str "Univ.between")
       | arc::rest ->
         let (max_rank, old_max_rank, best_arc, rest) =
           List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
-        if max_rank > old_max_rank then best_arc, g, rest
-        else begin
-          (* one redirected node also has max_rank *)
-          let arcu = {best_arc with rank = max_rank + 1} in
-          arcu, enter_arc arcu g, rest
-        end 
+          if max_rank > old_max_rank then best_arc, g, rest
+          else begin
+              (* one redirected node also has max_rank *)
+            let arcu = {best_arc with rank = max_rank + 1} in
+	      arcu, enter_arc arcu g, rest
+          end 
   in
   let redirect (g,w,w') arcv =
     let g' = enter_equiv_arc arcv.univ arcu.univ g in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 940a54128c..f5d1aa9f4c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -371,7 +371,7 @@ let process_universe_constraints univs vars alg templ cstrs =
 		  later. *)
 	      if Univ.is_small_univ l then 
 		match Univ.Universe.level r with
-		| Some r when Univ.LMap.mem r !vars -> 
+		| Some r ->
 		  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
 		| _ -> local
 	      else local
@@ -380,10 +380,10 @@ let process_universe_constraints univs vars alg templ cstrs =
 	      | None -> error ("Algebraic universe on the right")
 	      | Some rl ->
 		if Univ.Level.is_small rl then
-		  (if Univ.LSet.for_all (fun l -> 
-		    Univ.Level.is_small l || Univ.LMap.mem l !vars) 
+		  (if Univ.LSet.for_all (fun l ->
+		    Univ.Level.is_small l || Univ.LMap.mem l !vars)
 		      (Univ.Universe.levels l) then
-		      Univ.enforce_leq l r local
+		      Univ.enforce_eq l r local
 		   else raise (Univ.UniverseInconsistency (Univ.Le, l, r, [])))
 		else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then
 		  unify_universes fo l Univ.UEq r local
@@ -408,8 +408,9 @@ let process_universe_constraints univs vars alg templ cstrs =
 		  instantiate_variable r' l vars
 		else if not (Univ.check_eq univs l r) then
 		  (* Two rigid/global levels, none of them being local,
-		     one of them being Prop/Set, disallow *)
-		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
+		     one of them being Prop, disallow *)
+		  if Univ.Level.equal l' Univ.Level.prop || 
+		    Univ.Level.equal r' Univ.Level.prop then
 		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, []))
 		  else
 		    if fo then 
@@ -1128,14 +1129,13 @@ let set_leq_sort evd s1 s2 =
   match is_eq_sort s1 s2 with
   | None -> evd
   | Some (u1, u2) ->
-      match s1, s2 with
-      | Prop c, Prop c' -> 
-	  if c == Null && c' == Pos then evd
-	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
-      | Type _, Prop _ ->
-	raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))
-      | _, _ -> 
-        add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
+    if Univ.is_type0_univ u2 then
+      if Univ.is_small_univ u1 then evd
+      else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))
+    else if Univ.is_type0m_univ u2 then 
+      raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))
+    else 
+      add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
 	    
 let check_eq evd s s' =
   Univ.check_eq evd.universes.uctx_universes s s'
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1b2afd19a5..2b3e943559 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1057,8 +1057,19 @@ let w_merge env with_types flags (evd,metas,evars) =
     then Evd.define sp c evd'''
     else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in
 
-  (* merge constraints *)
-  w_merge_rec evd (order_metas metas) (List.rev evars) []
+  let check_types evd = 
+    let metas = Evd.meta_list evd in
+    let eqns = List.fold_left (fun acc (mv, b) ->
+      match b with
+      | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc
+      | _ -> acc) [] metas
+    in w_merge_rec evd [] [] eqns
+  in
+  let res =  (* merge constraints *)
+    w_merge_rec evd (order_metas metas) (List.rev evars) []
+  in
+    if with_types then check_types res
+    else res
 
 let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
   let metas,evd = retract_coercible_metas evd in