Fixing yet a source of dependency on alphabetic order in unification.

This refines even further c24bcae8 (PR #924) and 6304c843:
- c24bcae8 fixed the order in the heuristic
- 6304c843 improved the order by preferring projections

There remained a dependency in the alphabetic order in selecting
unification candidates. The current commit fixes it.

We radically change the representation of the substitution to invert
by using a map indexed on the rank in the signature rather than on the
name of the variable.

More could be done to use numbers further, e.g. for representing
aliases.

Note that this has consequences on the test-suite (in
output/Notations.v) as some problems now infer a dependent return
clause.

7 files changed, 79 insertions, 52 deletions

diff --git a/CHANGES b/CHANGES
index ff242fe285..46266a1bd0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,12 @@ Focusing
   e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
   As usual, unfocus with `}` once the sub-goal is fully solved.
 
+Specification language
+
+- A fix to unification (which was sensitive to the ascii name of
+  variables) may occasionally change type inference in incompatible
+  ways, especially regarding the inference of the return clause of "match".
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7baa755ab5..81e8bd06f5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1726,7 +1726,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
           (named_context !!extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
-      let candidates = u :: List.map mkRel vl in
+      let candidates = List.rev (u :: List.map mkRel vl) in
       let ev = evd_comb1 (Evarutil.new_evar !!extenv ~src ~filter ~candidates) evdref ty in
       lift k ev
   in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 984fa92c0e..6c52dacaa9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1317,6 +1317,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
       let rec aux = function
       | [] -> user_err Pp.(str "Unsolvable existential variables.")
       | a::l ->
+          (* In case of variables, most recent ones come first *)
           try
             let conv_algo = evar_conv_x ts in
             let evd = check_evar_instance evd evk a conv_algo in
@@ -1327,9 +1328,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
           with
           | IllTypedInstance _ -> aux l
           | e when Pretype_errors.precatchable_exception e -> aux l in
-      (* List.rev is there to favor most dependent solutions *)
-      (* and favor progress when used with the refine tactics *)
-      let evd = aux (List.rev l) in
+      (* Expected invariant: most dependent solutions come first *)
+      (* so as to favor progress when used with the refine tactics *)
+      let evd = aux l in
       solve_unconstrained_evars_with_candidates ts evd
 
 let solve_unconstrained_impossible_cases env evd =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3f5d186d4e..2dd3721980 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -599,11 +599,12 @@ let solve_pattern_eqn env sigma l c =
 let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
   let evar_aliases = compute_var_aliases sign sigma in
-  let (_,full_subst,cstr_subst) =
-    List.fold_right
-      (fun decl (args,all,cstrs) ->
+  let (_,full_subst,cstr_subst,_) =
+    List.fold_right_i
+      (fun i decl (args,all,cstrs,revmap) ->
         match decl,args with
         | LocalAssum (id,c), a::rest ->
+            let revmap = Id.Map.add id i revmap in
             let cstrs =
               let a',args = decompose_app_vect sigma a in
               match EConstr.kind sigma a' with
@@ -611,22 +612,26 @@ let make_projectable_subst aliases sigma evi args =
                   let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in
                   Constrmap.add (fst cstr) ((args,id)::l) cstrs
               | _ -> cstrs in
-            (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)
+            let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in
+            (rest,all,cstrs,revmap)
         | LocalDef (id,c,_), a::rest ->
+            let revmap = Id.Map.add id i revmap in
             (match EConstr.kind sigma c with
             | Var id' ->
                 let idc = normalize_alias_var sigma evar_aliases id' in
-                let sub = try Id.Map.find idc all with Not_found -> [] in
+                let ic, sub =
+                  try let ic = Id.Map.find idc revmap in ic, Int.Map.find ic all
+                  with Not_found -> i, [] (* e.g. [idc] is a filtered variable: treat [id] as an assumption *) in
                 if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then
-                  (rest,all,cstrs)
+                  (rest,all,cstrs,revmap)
                 else
-                  (rest,
-                   Id.Map.add idc ((a,normalize_alias_opt sigma aliases a,id)::sub) all,
-                   cstrs)
+                  let all = Int.Map.add ic ((a,normalize_alias_opt sigma aliases a,id)::sub) all in
+                  (rest,all,cstrs,revmap)
             | _ ->
-                (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs))
-        | _ -> anomaly (Pp.str "Instance does not match its signature."))
-      sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
+                let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in
+                (rest,all,cstrs,revmap))
+        | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0
+      sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in
   (full_subst,cstr_subst)
 
 (*------------------------------------*
@@ -793,11 +798,11 @@ let rec assoc_up_to_alias sigma aliases y yc = function
 
 let rec find_projectable_vars with_evars aliases sigma y subst =
   let yc = normalize_alias sigma aliases y in
-  let is_projectable idc idcl subst' =
+  let is_projectable idc idcl (subst1,subst2 as subst') =
     (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
     try
       let id = assoc_up_to_alias sigma aliases y yc idcl in
-      (id,ProjectVar)::subst'
+      (id,ProjectVar)::subst1,subst2
     with Not_found ->
     (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
     (* projectable on [y] *)
@@ -812,14 +817,18 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
             let subst,_ = make_projectable_subst aliases sigma evi argsv in
             let l = find_projectable_vars with_evars aliases sigma y subst in
             match l with
-            | [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst'
+            | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2)
             | _ -> subst'
           end
         | [] -> subst'
         | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.")
       else
         subst' in
-  Id.Map.fold is_projectable subst []
+  let subst1,subst2 = Int.Map.fold is_projectable subst ([],[]) in
+  (* We return the substitution with ProjectVar first (from most
+     recent to oldest var), followed by ProjectEvar (from most recent
+     to oldest var too) *)
+  subst1 @ subst2
 
 (* [filter_solution] checks if one and only one possible projection exists
  * among a set of solutions to a projection problem *)
@@ -842,25 +851,6 @@ let rec find_solution_type evarenv = function
   | (id,ProjectEvar _)::l -> find_solution_type evarenv l
   | [] -> assert false
 
-let is_preferred_projection_over sign (id,p) (id',p') =
-  (* We give priority to projection of variables over instantiation of
-     an evar considering that the latter is a stronger decision which
-     may even procude an incorrect (ill-typed) solution *)
-  match p, p' with
-  | ProjectEvar _, ProjectVar -> false
-  | ProjectVar, ProjectEvar _ -> true
-  | _, _ ->
-     List.index Id.equal id sign < List.index Id.equal id' sign
-
-let choose_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 is_preferred_projection_over sign x y 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
@@ -1447,12 +1437,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)
-        | _ ->
-            if choose then
-              let (id,p) = choose_projection evi sols in
-              (mkVar id, p)
-            else
-              raise (NotUniqueInType sols)
+        | (id,p)::_ ->
+            if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
       let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
@@ -1556,7 +1542,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
                 let t =
                   map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
                     imitate envk t in
-                t::l
+                (* Less dependent solutions come last *)
+                l@[t]
               with e when CErrors.noncritical e -> l in
             (match candidates with
             | [x] -> x
diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v
index c401420e94..791889b24b 100644
--- a/test-suite/bugs/closed/2670.v
+++ b/test-suite/bugs/closed/2670.v
@@ -15,6 +15,14 @@ Proof.
   refine (match e return _ with refl_equal => _ end).
   reflexivity.
   Undo 2.
+  (** Check insensitivity to alphabetic order *)
+  refine (match e as a in _ = b return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
+  (** Check insensitivity to alphabetic order *)
+  refine (match e as z in _ = y return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
   (* Next line similarly has a dependent and a non dependent solution *)
   refine (match e with refl_equal => _ end).
   reflexivity.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b60b1ee863..94b86fc222 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -125,13 +125,15 @@ s
      : nat
 fun _ : nat => 9
      : nat -> nat
-fun (x : nat) (p : x = x) => match p with
-                             | ONE => ONE
-                             end = p
+fun (x : nat) (p : x = x) =>
+match p in (_ = n) return (n = n) with
+| ONE => ONE
+end = p
      : forall x : nat, x = x -> Prop
-fun (x : nat) (p : x = x) => match p with
-                             | 1 => 1
-                             end = p
+fun (x : nat) (p : x = x) =>
+match p in (_ = n) return (n = n) with
+| 1 => 1
+end = p
      : forall x : nat, x = x -> Prop
 bar  0
      : nat
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index b287b5facf..e1df9ba84a 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -559,3 +559,26 @@ split.
 - (* clear b:True *) match goal with H:_ |- _ => clear H end.
   (* use a:0=0 *) match goal with H:_ |- _ => exact H end.
 Qed.
+
+(* Test choice of most dependent solution *)
+Goal forall n, n = 0 -> exists p, p = n /\ p = 0.
+intros. eexists ?[p]. split. rewrite H.
+reflexivity. (* Compatibility tells [?p:=n] rather than [?p:=0] *)
+exact H. (* this checks that the goal is [n=0], not [0=0] *)
+Qed.
+
+(* Check insensitivity to alphabetic order of names*)
+(* In both cases, the last name is conventionally chosen *)
+(* Before 8.9, the name coming first in alphabetic order *)
+(* was chosen. *)
+Goal forall m n, m = n -> n = 0 -> exists p, p = n /\ p = 0.
+intros. eexists ?[p]. split. rewrite H.
+reflexivity.
+exact H0.
+Qed.
+
+Goal forall n m, n = m -> m = 0 -> exists p, p = m /\ p = 0.
+intros. eexists ?[p]. split. rewrite H.
+reflexivity.
+exact H0.
+Qed.