Refining PR#924 (insensitivity of projection heuristics to alphabet).

We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.

We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).

2 files changed, 49 insertions, 4 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 7f81d1aa3..258385abc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -842,12 +842,22 @@ 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 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 List.index Id.equal id sign < List.index Id.equal id' sign then x else y)
+         if is_preferred_projection_over sign x y then x else y)
     l y
   | _ -> assert false
 
@@ -1439,8 +1449,11 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         | [] -> raise Not_found
         | [id,p] -> (mkVar id, p)
         | _ ->
-            let (id,p) = find_most_recent_projection evi sols in
-            if choose then (mkVar id, p) else raise (NotUniqueInType sols)
+            if choose then
+              let (id,p) = choose_projection evi sols in
+              (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
diff --git a/test-suite/bugs/closed/6070.v b/test-suite/bugs/closed/6070.v
new file mode 100644
index 000000000..49b16f625
--- /dev/null
+++ b/test-suite/bugs/closed/6070.v
@@ -0,0 +1,32 @@
+(* A slight shortening of bug 6078 *)
+
+(* This bug exposed a different behavior of unshelve_unifiable
+   depending on which projection is found in the unification
+   heuristics *)
+
+Axiom flat_type : Type.
+Axiom interp_flat_type : flat_type -> Type.
+Inductive type := Arrow (_ _ : flat_type).
+Definition interp_type (t : type)
+  := interp_flat_type (match t with Arrow s d => s end)
+     -> interp_flat_type (match t with Arrow s d => d end).
+Axiom Expr : type -> Type.
+Axiom Interp : forall {t : type}, Expr t -> interp_type t.
+Axiom Wf : forall {t}, Expr t -> Prop.
+Axiom a : forall f, interp_flat_type f.
+
+Definition packaged_expr_functionP A :=
+  (fun F : Expr A -> Expr A
+   => forall e' v, Interp (F e') v = a (let (_,f) := A in f)).
+Goal forall (f f0 : flat_type)
+            (e : forall _ : Expr (@Arrow f f0),
+                Expr (@Arrow f f0)),
+    @packaged_expr_functionP (@Arrow f f0) e.
+  intros.
+  refine (fun (e0 : Expr (Arrow f f0))
+   => (fun zHwf':True =>
+   (fun v : interp_flat_type f =>
+      ?[G] : ?[U] = ?[V] :> interp_flat_type ?[v])) ?[H]);
+   [ | ].
+   (* Was: Error: Tactic failure: Incorrect number of goals (expected 3 tactics). *)
+Abort.