Merge branch 'v8.5'

6 files changed, 68 insertions, 5 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f77e3312bb..489a8a729d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -143,6 +143,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
     try
       match kind_of_term t2 with
 	Prod (_,a,b) -> (* assert (l2=[]); *)
+	  let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
       	  if dependent (mkRel 1) b then raise Not_found
 	  else lookup_canonical_conversion (proji, Prod_cs),
 	    (Stack.append_app [|a;pop b|] Stack.empty)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 15e8022af0..a7b415552a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1555,8 +1555,9 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     | e when Errors.noncritical e -> raise (NotUnifiable None) in
   let merge_fun c1 c2 =
     match c1, c2 with
-    | Some (evd,c1,_) as x, Some (_,c2,_) ->
-      if is_conv env sigma c1 c2 then x else raise (NotUnifiable None)
+    | Some (evd,c1,x), Some (_,c2,_) ->
+      let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
+      if b then Some (evd, c1, x) else raise (NotUnifiable None)
     | Some _, None -> c1
     | None, Some _ -> c2
     | None, None -> None in
diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v
new file mode 100644
index 0000000000..405d09809c
--- /dev/null
+++ b/test-suite/bugs/4623.v
@@ -0,0 +1,5 @@
+Goal Type -> Type.
+set (T := Type).
+clearbody T.
+refine (@id _).
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v
new file mode 100644
index 0000000000..a737afcdab
--- /dev/null
+++ b/test-suite/bugs/4624.v
@@ -0,0 +1,7 @@
+Record foo := mkfoo { type : Type }.
+
+Canonical Structure fooA (T : Type) := mkfoo (T -> T).
+
+Definition id (t : foo) (x : type t) := x.
+
+Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v
new file mode 100644
index 0000000000..e1206bb37a
--- /dev/null
+++ b/test-suite/bugs/closed/4627.v
@@ -0,0 +1,49 @@
+Class sa (A:Type) := { }.
+
+Record predicate A (sa:sa A) :=
+  { pred_fun: A->Prop }.
+Record ABC : Type :=
+  { abc: Type }.
+Record T :=
+  { T_abc: ABC }.
+
+
+(*
+sa: forall _ : Type@{Top.179}, Prop
+predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)}
+T: Type@{Top.208+1}
+ABC: Type@{Top.208+1}
+abc: forall _ : ABC, Type@{Top.208}
+
+Top.205 <= Top.179   predicate <= sa.A
+Set < Top.208        Set < abc
+Set < Top.205        Set < predicate
+*)
+
+Definition foo : predicate T (Build_sa T) :=
+    {| pred_fun:= fun w => True |}.
+(* *)
+(* Top.208 < Top.205   <--- added by foo *)
+(* *)
+
+Check predicate nat (Build_sa nat).
+(*
+
+The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line.
+  -Jason Gross
+
+8.5          -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)}
+8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1}
+8.4pl4       -- predicate nat {| |}: Type (* max(Set, (Set)+1) *)
+*)
+
+(* This works in 8.4pl4 and SHOULD work in 8.5 *)
+Definition bar : ABC :=
+  {| abc:= predicate nat (Build_sa nat) |}.
+(*
+The term "predicate nat (Build_sa nat)" has type
+ "Type@{max(Set+1, Top.205)}"
+while it is expected to have type "Type@{Top.208}"
+(universe inconsistency: Cannot enforce Top.205 <=
+Top.208 because Top.208 < Top.205).
+*)
\ No newline at end of file
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ae0b885e47..db82c205cb 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -119,13 +119,13 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 	 (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 (* (not def) *) l; 
+	   | Some l -> evars := Evd.make_flexible_variable !evars true l; 
 	     sred, true
 	   | None -> s, false)
 	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
     | None -> 
-      let uvarkind = if (* not def *) true then Evd.univ_flexible_alg else Evd.univ_flexible in
-	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), false
+      let uvarkind = Evd.univ_flexible_alg in
+	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
   in
   let fullarity = it_mkProd_or_LetIn t' newps in
   let env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in