[ssr] avoid HO unif when doing truncation analysis

Eliminators can be:
- dependent: ... -> forall x (y : I x), P x y
- truncated: ... -> forall x (y : I x), P x
- funind like: ..-> forall x, P t
The user may provide a term t in `elim: t`
- t may be the last argument
- t may be the last "pattern" (standing for the last
argument of P)

We use unification to see if t (and its type) fits
in one of these cases (and/or to infer t).

This patch refuses to use unification in the HO case
eg `?T a = t` since the result is too often a false
positive.

2 files changed, 70 insertions, 23 deletions

diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a0b1d784f1..8a2f18c850 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -253,31 +253,49 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   (* Here we try to understand if the main pattern/term the user gave is
    * the first pattern to be matched (i.e. if elimty ends in P t1 .. tn,
    * weather tn is the t the user wrote in 'elim: t' *)
-  let c_is_head_p, gl = match cty with
+  let c_is_head_p, gl =
+    match cty with
     | None -> true, gl  (* The user wrote elim: _ *)
     | Some (c, c_ty, _) ->
-    let res = 
-      (* we try to see if c unifies with the last arg of elim *)
-      if elim_is_dep then None else
-      let arg = List.assoc (n_elim_args - 1) elim_args in
-      let gl, arg_ty = pfe_type_of gl arg in
-      match saturate_until gl c c_ty (fun c c_ty gl ->
-        pf_unify_HO (pf_unify_HO gl c_ty arg_ty) arg c) with
-      | Some (c, _, _, gl) -> Some (false, gl)
-      | None -> None in
-    match res with
-    | Some x -> x
-    | None ->
-      (* we try to see if c unifies with the last inferred pattern *)
-      let inf_arg = List.hd inf_deps_r in
-      let gl, inf_arg_ty = pfe_type_of gl inf_arg in
-      match saturate_until gl c c_ty (fun _ c_ty gl ->
-              pf_unify_HO gl c_ty inf_arg_ty) with
-      | Some (c, _, _,gl) -> true, gl
-      | None ->
-        errorstrm Pp.(str"Unable to apply the eliminator to the term"++
-          spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++
-          pr_econstr_env env (project gl) inf_arg_ty) in
+      let rec first = function
+        | [] ->
+          errorstrm Pp.(str"Unable to apply the eliminator to the term"++
+            spc()++pr_econstr_env env (project gl) c++spc())
+        | x :: rest ->
+          match x () with
+          | None -> first rest
+          | Some (b,gl) -> b, gl
+      in
+      (* Unify two terms if their heads are not applied unif variables, eg
+       * not (?P x). The idea is to rule out cases where the problem is too
+       * vague to drive the current heuristics. *)
+      let pf_unify_HO_rigid gl a b =
+        let is_applied_evar x = match EConstr.kind (project gl) x with
+          | App(x,_) -> EConstr.isEvar (project gl) x
+          | _ -> false in
+        if is_applied_evar a || is_applied_evar b then
+          raise Evarconv.(UnableToUnify(project gl,
+                   Pretype_errors.ProblemBeyondCapabilities))
+        else pf_unify_HO gl a b in
+      let try_c_last_arg () =
+        (* we try to see if c unifies with the last arg of elim *)
+        if elim_is_dep then None else
+        let arg = List.assoc (n_elim_args - 1) elim_args in
+        let gl, arg_ty = pfe_type_of gl arg in
+        match saturate_until gl c c_ty (fun c c_ty gl ->
+          pf_unify_HO (pf_unify_HO_rigid gl c_ty arg_ty) arg c) with
+        | Some (c, _, _, gl) -> Some (false, gl)
+        | None -> None in
+      let try_c_last_pattern () =
+        (* we try to see if c unifies with the last inferred pattern *)
+        if inf_deps_r = [] then None else
+        let inf_arg = List.hd inf_deps_r in
+        let gl, inf_arg_ty = pfe_type_of gl inf_arg in
+        match saturate_until gl c c_ty (fun _ c_ty gl ->
+                pf_unify_HO_rigid gl c_ty inf_arg_ty) with
+        | Some (c, _, _,gl) -> Some(true, gl)
+        | None -> None in
+      first [try_c_last_arg;try_c_last_pattern] in
   ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pfe_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
diff --git a/test-suite/ssr/elim_noquant.v b/test-suite/ssr/elim_noquant.v
new file mode 100644
index 0000000000..e6662203e9
--- /dev/null
+++ b/test-suite/ssr/elim_noquant.v
@@ -0,0 +1,29 @@
+Require Import ssreflect.
+
+
+Axiom app : forall T, list T -> list T -> list T.
+Arguments app {_}.
+Infix "++" := app.
+
+Lemma test (aT rT : Type)
+           (pmap : (aT -> option rT) -> list aT -> list rT)
+           (perm_eq : list rT -> list rT -> Prop)
+           (f : aT -> option rT)
+           (g : rT -> aT)
+           (s t : list aT)
+           (E : forall T : list aT -> Type,
+               (forall s1 s2 s3 : list aT,
+                  T (s1 ++ s2 ++ s3) -> T (s2 ++ s1 ++ s3)) ->
+                 T s -> T t) :
+        perm_eq (pmap f s) (pmap f t).
+Proof.
+elim/E: (t).
+Admitted.
+
+
+Lemma test2 (a b : nat) : a = b -> b = 1.
+Proof.
+elim.
+match goal with |- a = 1 => idtac end.
+Admitted.
+