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, 8 insertions, 3 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aa24733d9..27c1dd031 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1934,14 +1934,19 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  *)
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
+  let refresh_tycon sigma t =
+    refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
+		      env sigma t
+  in
   let preds =
     match pred, tycon with
     (* No return clause *)
     | None, Some t when not (noccur_with_meta 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
-	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let p1 =
+       (* First strategy: we abstract the tycon wrt to the dependencies *)
+         let sigma, t = refresh_tycon sigma t in
+         let p1 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
@@ -1952,7 +1957,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
         let sigma,t = match tycon with
-	| Some t -> sigma,t
+	| Some t -> refresh_tycon sigma t
 	| None -> 
           let sigma = Sigma.Unsafe.of_evar_map sigma in
           let Sigma ((t, _), sigma, _) =