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

This refines even further c24bcae (PR #924) and 6304c84:
- c24bcae fixed the order in the heuristic
- 6304c84 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.

pretyping/evarsolve.ml

@@ -599,34 +599,38 @@ 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
               | Construct cstr ->
                   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 = Id.Map.find idc revmap in
+                let sub = try Int.Map.find ic all with Not_found -> [] 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 +797,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 +816,15 @@ 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
+  List.rev_append subst1 (List.rev subst2)
 
 (* [filter_solution] checks if one and only one possible projection exists
  * among a set of solutions to a projection problem *)
@@ -842,25 +847,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
@@ -1444,12 +1430,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

test-suite/bugs/closed/2670.v

@@ -15,6 +15,14 @@ Proof.
   refine (match e return _ with refl_equal => _ end).
   reflexivity.
   Undo 2.
+  (** Check unsensitivity to alphabetic order *)
+  refine (match e as a in _ = b return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
+  (** Check unsensitivity 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.