Univs: fix bug #5180

In the kernel's generic conversion, backtrack on UniverseInconsistency
for the unfolding heuristic (single backtracking point in reduction).
This exception can be raised in the univ_compare structure to produce
better error messages when the generic conversion function is called
from higher level code in reductionops.ml, which itself is called during
unification in evarconv.ml.
Inside the kernel, the infer and check variants of conversion never
raise UniverseInconsistency though, so this does not change the behavior
of the kernel.

4 files changed, 73 insertions, 3 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6c664f7918..1ae89347ad 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (try
 	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
 	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-       with NotConvertible ->
+       with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9812c45f7b..8a2b2469d6 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,7 +36,7 @@ type 'a extended_conversion_function =
 type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = 
-  { (* Might raise NotConvertible *)
+  { (* Might raise NotConvertible or UnivInconsistency *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> 
 		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -56,9 +56,12 @@ constructors. *)
 val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
+(** These two never raise UnivInconsistency, inferred_universes
+    just gathers the constraints. *)
 val checked_universes : UGraph.t universe_compare
 val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
+(** These two functions can only raise NotConvertible *)
 val conv : constr extended_conversion_function
 
 val conv_leq : types extended_conversion_function
@@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> types infer_conversion_function
 
+(** Depending on the universe state functions, this might raise
+  [UniverseInconsistency] in addition to [NotConvertible] (for better error
+  messages). *)
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 332d4e0b26..297f0a1a8e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1262,7 +1262,7 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   match pb with
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
-    
+
 let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
   with Evd.UniversesDiffer
diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v
new file mode 100644
index 0000000000..261092ee6d
--- /dev/null
+++ b/test-suite/bugs/closed/5180.v
@@ -0,0 +1,64 @@
+Universes a b c ω ω'.
+Definition Typeω := Type@{ω}.
+Definition Type2 : Typeω := Type@{c}.
+Definition Type1 : Type2 := Type@{b}.
+Definition Type0 : Type1 := Type@{a}.
+
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Definition Typei' (n : nat)
+  := match n return Type@{ω'} with
+     | 0 => Type0
+     | 1 => Type1
+     | 2 => Type2
+     | _ => Typeω
+     end.
+Definition TypeOfTypei' {n} (x : Typei' n) : Type@{ω'}
+  := match n return Typei' n -> Type@{ω'} with
+     | 0 | 1 | 2 | _ => fun x => x
+     end x.
+Definition Typei (n : nat) : Typei' (S n)
+  := match n return Typei' (S n) with
+     | 0 => Type0
+     | 1 => Type1
+     | _ => Type2
+     end.
+Definition TypeOfTypei {n} (x : TypeOfTypei' (Typei n)) : Type@{ω'}
+  := match n return TypeOfTypei' (Typei n) -> Type@{ω'} with
+     | 0 | 1 | _ => fun x => x
+     end x.
+Check Typei 0 : Typei 1.
+Check Typei 1 : Typei 2.
+
+Definition lift' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => (x : Type)
+     end.
+Definition lift'' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => x
+     end. (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+Check (fun x : TypeOfTypei' (Typei 0) => TypeOfTypei' (Typei 1)).
+
+Definition lift''' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)).
+  refine match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))  with
+         | 0 | 1 | 2 | _ => fun x => _
+         end.
+  exact x.
+  Undo.
+  (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+  all:compute in *.
+  all:exact x.
\ No newline at end of file