Fixing one part of #5669 (unification heuristics sensitive to choice of names).

This surprising bug was caused by an Id.Set which was ordering
solutions to variable-projection problems in ascii order.

We fix it by re-considering the variables involved in the solutions
using the declaration order.

Note that in practice, this implies preferring a dependent solution
over a non-dependent one.

1 files changed, 11 insertions, 1 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9f48297613..d5c6f09760 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -847,6 +847,15 @@ let rec find_solution_type evarenv = function
   | (id,ProjectEvar _)::l -> find_solution_type evarenv l
   | [] -> assert false
 
+let find_most_recent_projection evi sols =
+  let sign = List.map get_id (evar_filtered_context evi) in
+  match sols with
+  | y::l ->
+     List.fold_right (fun (id,p as x) (id',_ as y) ->
+         if List.index Id.equal id sign < List.index Id.equal id' sign then x else y)
+    l y
+  | _ -> assert false
+
 (* In case the solution to a projection problem requires the instantiation of
  * subsidiary evars, [do_projection_effects] performs them; it
  * also try to instantiate the type of those subsidiary evars if their
@@ -1434,7 +1443,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
       let c, p = match sols with
         | [] -> raise Not_found
         | [id,p] -> (mkVar id, p)
-        | (id,p)::_::_ ->
+        | _ ->
+            let (id,p) = find_most_recent_projection evi sols in
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in