Fix UGraph.check_eq!

Universes are kept in normal form w.r.t. equality but not the <=
relation, so the previous check worked almost always but was actually
too strict! In cases like (max(Set,u) = u) when u is declared >= Set it
was failing to find an equality. Applying the KISS principle:
u = v <-> u <= v /\ v <= u.

Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of
a colon in a typing judgment), this was not the case when an algebraic
universe instantiated an evar that appeared in the term. We force their
universe variable status to change in refresh_universes to avoid this.

Fix ind sort inference: Use syntactic universe equality for inductive
sort inference instead of check_leq (which now correctly takes
constraints into account) and simplify code

1 files changed, 7 insertions, 14 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index e2712615b..4884d0deb 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -638,19 +638,6 @@ let check_smaller g strict u v =
 
 type 'a check_function = universes -> 'a -> 'a -> bool
 
-let check_equal_expr g x y =
-  x == y || (let (u, n) = x and (v, m) = y in 
-               Int.equal n m && check_equal g u v)
-
-let check_eq_univs g l1 l2 =
-  let f x1 x2 = check_equal_expr g x1 x2 in
-  let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in
-    Universe.for_all (fun x1 -> exists x1 l2) l1
-    && Universe.for_all (fun x2 -> exists x2 l1) l2
-
-let check_eq g u v =
-  Universe.equal u v || check_eq_univs g u v
-
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -669,7 +656,13 @@ let real_check_leq g u v =
 let check_leq g u v =
   Universe.equal u v ||
     is_type0m_univ u ||
-    check_eq_univs g u v || real_check_leq g u v
+    real_check_leq g u v
+
+let check_eq_univs g l1 l2 =
+  real_check_leq g l1 l2 && real_check_leq g l2 l1
+
+let check_eq g u v =
+  Universe.equal u v || check_eq_univs g u v
 
 (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *)