Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given.

This no-inversion and maximal abstraction over dependencies in (rel)
variables heuristic was used only when a type constraint was given.

By doing so, we ensure that all three strategies "inversion with
dependencies as evars", "no-inversion and maximal abstraction over
dependencies in (rel) variables", "no-inversion and no abstraction
over dependencies" are tried in all situations where a return clause
has to be inferred.

See penultimate commit for discussion.

2 files changed, 23 insertions, 14 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 951c36290c..f167e65b96 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2008,10 +2008,17 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
                       !!env sigma t
   in
   let preds =
-    match pred, tycon with
+    match pred with
     (* No return clause *)
-    | None, Some t ->
-        let sigma,t = refresh_tycon sigma t in
+    | None ->
+        let sigma,t =
+          match tycon with
+          | Some t -> refresh_tycon sigma t
+          | None ->
+             (* No type constraint: we first create a generic evar type constraint *)
+             let src = (loc, Evar_kinds.CasesType false) in
+             let sigma, (t, _) = new_type_evar !!env sigma univ_flexible_alg ~src in
+             sigma, t in
         (* First strategy: we build an "inversion" predicate, also replacing the *)
         (* dependencies with existential variables *)
         let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
@@ -2030,18 +2037,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
              [sigma1, pred1, arsign; sigma2, pred2, arsign; sigma, pred3, arsign]
          | _ ->
              [sigma1, pred1, arsign; sigma, pred3, arsign])
-    | None, None ->
-        (* No type constraint: we use two strategies *)
-        (* we first create a generic evar type constraint *)
-        let src = (loc, Evar_kinds.CasesType false) in
-        let sigma, (t, _) = new_type_evar !!env sigma univ_flexible_alg ~src in
-        (* First strategy: we build an "inversion" predicate *)
-        let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-        (* Second strategy: we use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten arsign)) t in
-        [sigma1, pred1, arsign; sigma, pred2, arsign]
     (* Some type annotation *)
-    | Some rtntyp, _ ->
+    | Some rtntyp ->
       (* We extract the signature of the arity *)
       let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index e388acdcb0..8fad41cd8f 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -101,3 +101,15 @@ Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
         | F  => f y H1
         | G _ => f y H2
         end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.