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).

1 files changed, 32 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/6070.v b/test-suite/bugs/closed/6070.v
new file mode 100644
index 0000000000..49b16f6254
--- /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.