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, 25 insertions, 15 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 464dc18b9..1b1f95883 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1930,9 +1930,19 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
-    match pred, tycon with
+    match pred with
     (* No return clause *)
-    | None, Some t ->
+    | None ->
+        let sigma,t =
+          match tycon with
+          | Some t -> sigma, t
+          | None ->
+             (* No type constraint: we first create a generic evar type constraint *)
+             let src = (loc, Evar_kinds.CasesType false) in
+             let sigma = Sigma.Unsafe.of_evar_map sigma in
+             let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
+             let sigma = Sigma.to_evar_map sigma 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
@@ -1951,20 +1961,8 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
              [sigma1, pred1; sigma2, pred2; sigma, pred3]
 	 | _ ->
              [sigma1, pred1; sigma, pred3])
-    | 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 = Sigma.Unsafe.of_evar_map sigma in
-        let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
-        let sigma = Sigma.to_evar_map sigma 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; sigma, pred2]
     (* Some type annotation *)
-    | Some rtntyp, _ ->
+    | Some rtntyp ->
       (* We extract the signature of the arity *)
       let envar = List.fold_right push_rel_context 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 e388acdcb..8fad41cd8 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.