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].

2 files changed, 19 insertions, 0 deletions

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.