Trying a no-inversion no-dependency heuristic for match return clause.

The no-inversion no-dependency heuristic was used only in the absence
of type constraint. We may now use it also in the presence of a type
constraint.

See previous commit for discussion.

1 files changed, 22 insertions, 19 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9d461d1aa..464dc18b9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1932,32 +1932,35 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
     (* No return clause *)
-    | None, Some t when not (noccur_with_meta 0 max_int t) ->
-	(* If the tycon is not closed w.r.t real variables, we try *)
-        (* two different strategies *)
-	(* First strategy: we build an "inversion" predicate *)
+    | None, Some t ->
+        (* 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
 	(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+        (* Third strategy: we take the type constraint as it is; of course we could *)
+        (* need something inbetween, abstracting some but not all of the dependencies *)
+        (* the "inversion" strategy deals with that but unification may not be *)
+        (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
+        (* work (yet) when a constructor has a type not precise enough for the inversion *)
+        (* see log message for details *)
+        let pred3 = lift (List.length (List.flatten arsign)) t in
 	(match p2 with
-	 | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2]
-	 | None -> [sigma1, pred1])
-    | None, _ ->
-	(* No dependent type constraint, or no constraints at all: *)
-	(* we use two strategies *)
-        let sigma,t = match tycon with
-	| Some t -> sigma,t
-	| None -> 
-          let sigma = Sigma.Unsafe.of_evar_map sigma in
-          let Sigma ((t, _), sigma, _) =
-	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
-          let sigma = Sigma.to_evar_map sigma in
-	    sigma, t
-	in
+	 | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
+             [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 or tycon as a non dependent pred *)
+	(* 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 *)