Merge branch 'bug4527' into trunk

10 files changed, 61 insertions, 27 deletions

diff --git a/CHANGES b/CHANGES
index 9ef048345c..4808dee794 100644
--- a/CHANGES
+++ b/CHANGES
@@ -80,6 +80,13 @@ Bugfixes
 - #4777: printing inefficiency with implicit arguments
 - #4752: CoqIDE crash on files not ended by ".v".
 - #4398: type_scope used consistently in "match goal".
+- #4527: when typechecking the statement of a lemma using universe polymorphic
+  definitions with explicit universe binders, check that the type can indeed be
+  typechecked using only those universes (after minimization of the other,
+  flexible universes), or raise an error (fixed scripts can be made forward
+  compatible).
+- #4726: treat user-provided sorts of universe polymorphic records as rigid
+  (i.e. non-minimizable).
 
 Changes from V8.5 to V8.5pl1
 ============================
diff --git a/engine/evd.ml b/engine/evd.ml
index b883db615e..1276c5994e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -252,6 +252,7 @@ let instantiate_evar_array info c args =
   | _ -> replace_vars inst c
 
 type evar_universe_context = UState.t
+
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
 let empty_evar_universe_context = UState.empty
diff --git a/engine/evd.mli b/engine/evd.mli
index df491c27b4..d6cf83525c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -511,6 +511,7 @@ val normalize_evar_universe_context : evar_universe_context ->
 val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
 val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
 val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 											   
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
@@ -568,8 +569,8 @@ val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_
 val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
-val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
-  Globnames.global_reference -> evar_map * constr
+val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
+  evar_map -> Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
   Conversion w.r.t. an evar map, not unifying universes. See 
diff --git a/engine/uState.ml b/engine/uState.ml
index 8aa9a61ab9..2fb64cd6e5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -49,7 +49,7 @@ let empty =
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
     uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes }
+    uctx_initial_universes = UGraph.initial_universes; }
 
 let make u =
     { empty with 
@@ -83,7 +83,7 @@ let union ctx ctx' =
           if local == ctx.uctx_local then ctx.uctx_universes
           else
             let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-              UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+            UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 let context_set ctx = ctx.uctx_local
 
@@ -263,13 +263,17 @@ let universe_context ?names ctx =
        if not (Univ.LSet.is_empty left) then
          let n = Univ.LSet.cardinal left in
          let loc =
-          let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in
-          try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost
+           try
+             let info =
+               Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in
+             Option.default Loc.ghost info.uloc
+           with Not_found -> Loc.ghost
          in
            user_err_loc (loc, "universe_context",
-                        (str(CString.plural n "Universe") ++ spc () ++
-                             Univ.LSet.pr (pr_uctx_level ctx) left ++
-                             spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound."))
+			(str(CString.plural n "Universe") ++ spc () ++
+			     Univ.LSet.pr (pr_uctx_level ctx) left ++
+			   spc () ++ str (CString.conjugate_verb_to_be n) ++
+                           str" unbound."))
       else
         let inst = Univ.Instance.of_array (Array.of_list newinst) in
         let ctx = Univ.UContext.make (inst,
@@ -329,7 +333,8 @@ let merge ?loc sideff rigid uctx ctx' =
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare uctx.uctx_universes in
   let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
-    { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial }
+  { uctx with uctx_names; uctx_local; uctx_universes;
+              uctx_initial_universes = initial }
 
 let merge_subst uctx s =
   { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
diff --git a/library/universes.ml b/library/universes.ml
index 75cbd5604b..21d960ea36 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -926,9 +926,7 @@ let normalize_context_set ctx us algs =
      mentionning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr = 
     Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
-      let lus = LMap.mem l us 
-      and rus = LMap.mem r us
-      in
+      let lus = LMap.mem l us and rus = LMap.mem r us in
       let ucstrsl' = 
 	if lus then add_list_map l (d, r) ucstrsl
 	else ucstrsl
@@ -1090,13 +1088,6 @@ let solve_constraints_system levels level_bounds level_min =
     for j=0 to nind-1 do
       if not (Int.equal i j) && Int.Set.mem j clos.(i) then
 	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
-	 (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *)
     done;
-    (* for j=0 to nind-1 do *)
-    (*   match levels.(j) with *)
-    (*   | Some u when not (Univ.Level.is_small u) -> *)
-    (* 	 v.(i) <- univ_level_rem u v.(i) level_min.(i) *)
-    (*   | _ -> () *)
-    (* done *)
   done;
   v
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 912fd198b6..729006dbb4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1225,9 +1225,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
 let solve_unconstrained_impossible_cases env evd =
   Evd.fold_undefined (fun evk ev_info evd' ->
     match ev_info.evar_source with
-    | _,Evar_kinds.ImpossibleCase -> 
+    | loc,Evar_kinds.ImpossibleCase ->
       let j, ctx = coq_unit_judge () in
-      let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd' ctx in
+      let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
       let ty = j_type j in
       let conv_algo = evar_conv_x full_transparent_state in
       let evd' = check_evar_instance evd' evk ty conv_algo in
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 50dceb8e6b..6b78ce72cc 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -465,6 +465,11 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+  let () =
+    match levels with
+    | None -> ()
+    | Some l -> ignore (Evd.universe_context evd ?names:l)
+  in
   let evd =
     if pi2 kind then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
diff --git a/test-suite/bugs/closed/4726.v b/test-suite/bugs/closed/4726.v
new file mode 100644
index 0000000000..0037b6fdea
--- /dev/null
+++ b/test-suite/bugs/closed/4726.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Definition le@{i j} : Type@{j} :=
+  (fun A : Type@{j} => A)
+  (unit : Type@{i}).  
+Definition eq@{i j} : Type@{j} := let x := le@{i j} in le@{j i}.
+
+Record Inj@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{j} :=
+  { inj : A }.
+
+Monomorphic Universe u1.
+Let ty1 : Type@{u1} := Set.
+Check Inj@{Set u1}.
+(* Would fail with univ inconsistency if the universe was minimized *)
+
+Record Inj'@{i j} (A : Type@{i}) (B : Type@{j}) : Type@{j} :=
+  { inj' : A; foo : Type@{j} := eq@{i j} }.
+Fail Check Inj'@{Set u1}. (* Do not drop constraint i = j *)
+Check Inj'@{Set Set}.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ffa2484eef..2875511d35 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1087,7 +1087,7 @@ let interp_recursive isfix fixl notations =
         | Some ls , Some us ->
 	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
 	     error "(co)-recursive definitions should all have the same universe binders";
-	   Some (ls @ us)) fixl None in
+	   Some us) fixl None in
   let ctx = Evd.make_evar_universe_context env all_universes in
   let evdref = ref (Evd.from_ctx ctx) in
   let fixctxs, fiximppairs, fixannots =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3151b13726..e9de6b5324 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -114,14 +114,19 @@ let typecheck_params_and_fields def id pl t ps nots fs =
   let t', template = match t with 
     | Some t -> 
        let env = push_rel_context newps env0 in
+       let poly =
+         match t with
+         | CSort (_, Misctypes.GType []) -> true | _ -> false in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_betadeltaiota env !evars s in
 	 (match kind_of_term sred with
 	 | Sort s' -> 
-	   (match Evd.is_sort_variable !evars s' with
-	   | Some l -> evars := Evd.make_flexible_variable !evars true l; 
-	     sred, true
-	   | None -> s, false)
+	    (if poly then
+               match Evd.is_sort_variable !evars s' with
+	       | Some l -> evars := Evd.make_flexible_variable !evars true l; 
+	                  sred, true
+	       | None -> s, false
+             else s, false)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None -> 
       let uvarkind = Evd.univ_flexible_alg in