Univs: fix bug #4443.

Do not substitute rigid variables during minimization, keeping
their equality constraints instead.

2 files changed, 43 insertions, 6 deletions

diff --git a/library/universes.ml b/library/universes.ml
index a8e9478e13..3eae612c8c 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -205,7 +205,7 @@ let leq_constr_univs_infer univs m n =
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	  if Univ.check_leq univs u1 u2 then
-	    ((if Univ.is_small_univ u1 then
+	    ((if Univ.is_type0_univ u1 then
 		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
 	     true)
 	  else
@@ -904,22 +904,28 @@ let normalize_context_set ctx us algs =
   let noneqs = Constraint.union noneqs smallles in
   let partition = UF.partition uf in
   let flex x = LMap.mem x us in
-  let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> 
+  let ctx, subst, us, eqs = List.fold_left (fun (ctx, subst, us, cstrs) s -> 
     let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in
     (* Add equalities for globals which can't be merged anymore. *)
     let cstrs = LSet.fold (fun g cst -> 
       Constraint.add (canon, Univ.Eq, g) cst) global
       cstrs 
     in
+    (* Also add equalities for rigid variables *)
+    let cstrs = LSet.fold (fun g cst -> 
+      Constraint.add (canon, Univ.Eq, g) cst) rigid
+      cstrs
+    in
     let subst = LSet.fold (fun f -> LMap.add f canon) rigid subst in
-    let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in 
-      (LSet.diff (LSet.diff ctx rigid) flexible, subst, cstrs))
-    (ctx, LMap.empty, Constraint.empty) partition
+    let subst = LSet.fold (fun f -> LMap.add f canon) flexible subst in
+    let canonu = Some (Universe.make canon) in
+    let us = LSet.fold (fun f -> LMap.add f canonu) flexible us in
+      (LSet.diff ctx flexible, subst, us, cstrs))
+    (ctx, LMap.empty, us, Constraint.empty) partition
   in
   (* Noneqs is now in canonical form w.r.t. equality constraints, 
      and contains only inequality constraints. *)
   let noneqs = subst_univs_level_constraints subst noneqs in
-  let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in
   (* Compute the left and right set of flexible variables, constraints
      mentionning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr = 
diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v
new file mode 100644
index 0000000000..66dfa0e685
--- /dev/null
+++ b/test-suite/bugs/closed/4443.v
@@ -0,0 +1,31 @@
+Set Universe Polymorphism.
+
+Record TYPE@{i} := cType {
+  type : Type@{i};
+}.
+
+Definition PROD@{i j k}
+  (A : Type@{i})
+  (B : A -> Type@{j})
+  : TYPE@{k}.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+Local Unset Strict Universe Declaration.
+Definition PRODinj
+  (A : Type@{i})
+  (B : A -> Type)
+  : TYPE.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+  Monomorphic Universe i j.
+  Monomorphic Constraint j < i.
+Set Printing Universes.
+Check PROD@{i i i}.
+Check PRODinj@{i j}.
+Fail Check PRODinj@{j i}.
\ No newline at end of file