Merge PR #7257: Fixing yet a source of dependency on alphabetic order in unification.

8 files changed, 83 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/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
new file mode 100644
index 0000000000..019cb8054d
--- /dev/null
+++ b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then
+    cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification
+    cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto
+fi
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.