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, 21 insertions, 0 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 9661b3bfa..f746def5c 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
    hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
 
 Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
+
+
+Module TemplateProp.
+
+  (** Check lowering of a template universe polymorphic inductive to Prop *)
+  
+  Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Check Foo True : Prop.
+
+End TemplateProp.
+
+Module PolyNoLowerProp.
+
+  (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *)
+  
+  Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Fail Check Foo True : Prop.
+
+End PolyNoLowerProp.