Refine 9cc95f5, unification of Let-In's, bug #3929

We unify types of let-ins in FO heuristic before their bodies, using
cumulativity in either direction. This maintains the invariant that we
are comparing terms in related types throughout unification.
Also adapt test-suite file for bug #3929.

2 files changed, 61 insertions, 3 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e5fc5a188d..912fd198b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -590,9 +590,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match kind_of_term term1, kind_of_term term2 with
         | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
-        let f1 i =
+        let f1 i = (* FO *)
           ise_and i
-	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
+            [(fun i -> ise_try i
+               [(fun i -> evar_conv_x ts env i CUMUL t1 t2);
+                (fun i -> evar_conv_x ts env i CUMUL t2 t1)]);
+             (fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v
index 4031dcc45e..955581ef26 100644
--- a/test-suite/bugs/closed/3929.v
+++ b/test-suite/bugs/closed/3929.v
@@ -1,5 +1,36 @@
+Universes i j.
+Set Printing Universes.
+Set Printing All.
+Polymorphic Definition lt@{x y} : Type@{y} := Type@{x}.
 Goal True.
-evar (T:Type).
+evar (T:Type@{i}).
+set (Z := nat : Type@{j}). simpl in Z.
+let Tv:=eval cbv [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+(** This enforces i <= j *)
+Fail pose (lt@{i j}).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+exact I. 
+Defined.
+
+Goal True.
+evar (T:nat).
+pose (Z:=0).
+let Tv:=eval cbv [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+Abort.
+
+Goal True.
+evar (T:Set).
 pose (Z:=nat).
 let Tv:=eval cbv [T] in T in
 pose (x:=Tv).
@@ -10,3 +41,27 @@ let Tv:=eval cbv [T] in T in
 constr_eq Zv Tv.
 Abort.
 
+Goal forall (A:Type)(a:A), True.
+intros A a.
+evar (T:A).
+pose (Z:=a).
+let Tv:=eval cbv delta [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+Abort.
+
+Goal True.
+evar (T:Type).
+pose (Z:=nat).
+let Tv:=eval cbv [T] in T in
+pose (x:=Tv).
+revert x.
+refine (_ : let x:=Z in True).
+let Zv:=eval cbv [Z] in Z in
+let Tv:=eval cbv [T] in T in
+constr_eq Zv Tv.
+Abort.