Fix #8364: making univ algebraic when already equal to another.

When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.

NB: The bug called make_flexible_variable on Top.15 and
~~~
   {Top.15 Top.14} |= Top.11 < Top.6
                      Top.14 < Top.5
                      Top.11 = Top.15

  ALGEBRAIC UNIVERSES:{Top.17 Top.16}
  UNDEFINED UNIVERSES:Top.17 := Top.14+1
                      Top.16 := Top.14+1
  WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].

4 files changed, 63 insertions, 19 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 5b0671c06e..6aecc368e6 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -577,25 +577,33 @@ let add_global_univ uctx u =
                                      uctx_universes = univs }
 
 let make_flexible_variable ctx ~algebraic u =
-  let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
-  let uvars' = Univ.LMap.add u None uvars in
-  let avars' = 
-    if algebraic then
-      let uu = Univ.Universe.make u in
-      let substu_not_alg u' v =
-        Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
-      in
-      let has_upper_constraint () =
-        Univ.Constraint.exists
-          (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u)
-          (Univ.ContextSet.constraints cstrs)
-      in
-        if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ())
-        then Univ.LSet.add u avars else avars 
-    else avars 
-  in
-  {ctx with uctx_univ_variables = uvars'; 
-      uctx_univ_algebraic = avars'}
+  let open Univ in
+  let {uctx_local = cstrs; uctx_univ_variables = uvars;
+       uctx_univ_algebraic = avars; uctx_universes=g; } = ctx in
+  assert (try LMap.find u uvars == None with Not_found -> true);
+  match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with
+  | Some v ->
+    let uvars' = LMap.add u (Some (Universe.make v)) uvars in
+    { ctx with uctx_univ_variables = uvars'; }
+  | None ->
+    let uvars' = LMap.add u None uvars in
+    let avars' =
+      if algebraic then
+        let uu = Universe.make u in
+        let substu_not_alg u' v =
+          Option.cata (fun vu -> Universe.equal uu vu && not (LSet.mem u' avars)) false v
+        in
+        let has_upper_constraint () =
+          Constraint.exists
+            (fun (l,d,r) -> d == Lt && Level.equal l u)
+            (ContextSet.constraints cstrs)
+        in
+        if not (LMap.exists substu_not_alg uvars || has_upper_constraint ())
+        then LSet.add u avars else avars
+      else avars
+    in
+    {ctx with uctx_univ_variables = uvars';
+              uctx_univ_algebraic = avars'}
 
 let make_nonalgebraic_variable ctx u =
   { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic }
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index fe07a1c90e..afdc8f1511 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -868,6 +868,21 @@ let constraints_for ~kept g =
 
 let domain g = LMap.domain g.entries
 
+let choose p g u =
+  let exception Found of Level.t in
+  let ru = (repr g u).univ in
+  if p ru then Some ru
+  else
+    try LMap.iter (fun v -> function
+        | Canonical _ -> () (* we already tried [p ru] *)
+        | Equiv v' ->
+          let rv = (repr g v').univ in
+          if rv == ru && p v then raise (Found v)
+          (* NB: we could also try [p v'] but it will come up in the
+             rest of the iteration regardless. *)
+      ) g.entries; None
+    with Found v -> Some v
+
 (** [sort_universes g] builds a totally ordered universe graph.  The
     output graph should imply the input graph (and the implication
     will be strict most of the time), but is not necessarily minimal.
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index a389b35993..4dbfac5c73 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -73,6 +73,10 @@ val sort_universes : t -> t
    of the universes into equivalence classes. *)
 val constraints_of_universes : t -> Constraint.t * LSet.t list
 
+val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+(** [choose p g u] picks a universe verifying [p] and equal
+   to [u] in [g]. *)
+
 (** [constraints_for ~kept g] returns the constraints about the
    universes [kept] in [g] up to transitivity.
 
diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v
new file mode 100644
index 0000000000..10f955b41f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8364.v
@@ -0,0 +1,17 @@
+Unset Primitive Projections.
+
+Record Box (A:Type) := box { unbox : A }.
+Arguments box {_} _. Arguments unbox {_} _.
+
+Definition map {A B} (f:A -> B) x :=
+  match x with box x => box (f x) end.
+
+Definition tuple (l : Box Type) : Type :=
+  match l with
+  | box x => x
+  end.
+
+Fail Inductive stack : Type -> Type :=
+| Stack T foos :
+  tuple (map stack foos) ->
+  stack T.