From c200c2b41e88dd7d4a1b9e90e0c35a7ed047309c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 30 May 2016 23:52:58 +0200
Subject: Univs: Fix bug #4726

When using Record and an explicit sort constraint, the
universe was wrongly made flexible and minimized.
---
 test-suite/bugs/closed/4726.v | 19 +++++++++++++++++++
 toplevel/record.ml            | 13 +++++++++----
 2 files changed, 28 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/4726.v

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/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
-- 
cgit v1.2.3