Fix bug #4627: records with no declared arity can be template polymorphic.

As if we were adding : Type. Consistent with inductives with no
declared arity.

2 files changed, 52 insertions, 3 deletions

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 200d1a9387..c5ae7e8913 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -114,13 +114,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 (Name id,None,fullarity) env0) in