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

3 files changed, 32 insertions, 25 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, _) =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ba566f374..ee4148de6 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
 
 val prepare_predicate :            Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
            (Term.types * tomatch_type) list ->
            Context.Rel.t list ->
            Constr.constr option ->
-           'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+           glob_constr option ->
+           (Evd.evar_map * Names.name list * Term.constr) list
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f0aa9b564..02e10d7fc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,33 +42,34 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-let refresh_level evd s =
-  match Evd.is_sort_variable evd s with
-  | None -> true
-  | Some l -> not (Evd.is_flexible_level evd l)
-
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 		      pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh status dir t = 
-    match kind_of_term t with
-    | Sort (Type u as s) when
-      (match Univ.universe_level u with
-      | None -> true
-      | Some l -> not onlyalg && refresh_level evd s) ->
+  let refresh_sort status dir s =
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
       if dir then set_leq_sort env !evdref s' s
       else set_leq_sort env !evdref s s'
     in
-      modified := true; evdref := evd; mkSort s'
+    modified := true; evdref := evd; mkSort s'
+  in
+  let rec refresh onlyalg status dir t = 
+    match kind_of_term t with
+    | Sort (Type u as s) ->
+       (match Univ.universe_level u with
+	| None -> refresh_sort status dir s
+	| Some l ->
+	   (match Evd.universe_rigidity evd l with
+	    | UnivRigid -> if not onlyalg then refresh_sort status dir s else t
+	    | UnivFlexible alg ->
+	       if onlyalg && alg then
+	         (evdref := Evd.make_flexible_variable !evdref false l; t)
+	       else t))
     | Sort (Prop Pos as s) when refreshset && not dir ->
-       let s' = evd_comb0 (new_sort_variable status) evdref in
-       let evd = set_leq_sort env !evdref s s' in
-       modified := true; evdref := evd; mkSort s'
+       refresh_sort status dir s
     | Prod (na,u,v) -> 
-      mkProd (na,u,refresh status dir v)
+      mkProd (na, u, refresh onlyalg status dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
@@ -81,7 +82,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
       Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
-      let ty' = refresh univ_flexible true evi.evar_concl in
+      let ty' = refresh onlyalg univ_flexible true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
@@ -101,9 +102,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   in
   let t' = 
     if isArity t then
-      (match pbty with
-      | None -> t
-      | Some dir -> refresh status dir t)
+      match pbty with
+      | None -> refresh true univ_flexible false t
+      | Some dir -> refresh onlyalg status dir t
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t