Compensating 6fd763431 on postponing subtyping evar-evar problems.

Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.

4 files changed, 39 insertions, 8 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 307edcc89..9f1b118fb 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -121,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
 let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
-let add_conv_oriented_pb (pbty,env,t1,t2) evd =
+let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
-  | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
-  | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
-  | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
+  | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
+  | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
+  | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
 
 (*------------------------------------*
  * Restricting existing evars         *
@@ -1111,13 +1111,13 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
     with CannotProject (evd,ev2) ->
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
     try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let pbty = if force then None else pbty in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9313e2232..4e38bd4e6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -779,7 +779,9 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb ?(tail=false) pb d =
+  if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+  else {d with conv_pbs = pb::d.conv_pbs}
 
 let evar_source evk d = (find d evk).evar_source
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cf6ba07c6..48704f75b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -397,7 +397,7 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb :  evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
new file mode 100644
index 000000000..2c87a908f
--- /dev/null
+++ b/test-suite/complexity/bug4076.v
@@ -0,0 +1,29 @@
+(* Check behavior of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i : nat), P i -> P i.
+Parameter P : nat -> Type.
+
+Definition g (n : nat) (a0 : P n) : P n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  a17.