Merge PR #262: A cleaning step in using heuristics for inference of the return clause

4 files changed, 107 insertions, 67 deletions

diff --git a/CHANGES b/CHANGES
index b2f2987249..e16da2ab2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -83,7 +83,7 @@ Focusing
   e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
   As usual, unfocus with `}` once the sub-goal is fully solved.
 
-Specification language
+Specification language, type inference
 
 - A fix to unification (which was sensitive to the ascii name of
   variables) may occasionally change type inference in incompatible
@@ -94,6 +94,11 @@ Specification language
   induce an overhead if the cost of checking the conversion of the
   corresponding definitions is additionally high (PR #8215).
 
+- A few improvements in inference of the return clause of "match" can
+  exceptionally introduce incompatibilities (PR #262). This can be
+  solved by writing an explicit "return" clause, sometimes even simply
+  an explicit "return _" clause.
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 33ee579eca..37dd3708b3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1941,16 +1941,28 @@ let inh_conv_coerce_to_tycon ?loc env sigma j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
+let add_subst sigma c len (rel_subst,var_subst) =
+  match EConstr.kind sigma c with
+  | Rel n -> (n,len) :: rel_subst, var_subst
+  | Var id -> rel_subst, (id,len) :: var_subst
+  | _ -> assert false
+
+let dependent_rel_or_var sigma tm c =
+  match EConstr.kind sigma tm with
+  | Rel n -> not (noccurn sigma n c)
+  | Var id -> Termops.local_occur_var sigma id c
+  | _ -> assert false
+
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let subst, len =
+  let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match EConstr.kind sigma tm with
-          | Rel n when Int.equal signlen 1 && not (noccurn sigma n c)
+          | Rel _ | Var _ when Int.equal signlen 1 && dependent_rel_or_var sigma tm c
             (* The term to match is not of a dependent type itself *) ->
-	      ((n, len) :: subst, len - signlen)
-	  | Rel n when signlen > 1 (* The term is of a dependent type,
+              (add_subst sigma tm len subst, len - signlen)
+          | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1959,28 +1971,36 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match EConstr.kind sigma arg with
-                          | Rel n when not (noccurn sigma n c) ->
-			      ((n, len) :: subst, pred len)
+                          | Rel _ | Var _ when dependent_rel_or_var sigma arg c ->
+                              (add_subst sigma arg len subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-                      if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs
-		      then (n, len) :: subst else subst
+                      if dependent_rel_or_var sigma tm c && List.for_all (fun c -> isRel sigma c || isVar sigma c) realargs
+                      then add_subst sigma tm len subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign ([], nar)
+      (List.rev tomatchs) arsign (([],[]), nar)
   in
   let rec predicate lift c =
     match EConstr.kind sigma c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) subst in
+              let idx = Int.List.assoc (n - lift) rel_subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign. *)
+              (* A variable that is not matched, lift over the arsign *)
 	      mkRel (n + nar))
+      | Var id ->
+          (try
+              (* Make the predicate dependent on the matched variable *)
+              let idx = Id.List.assoc id var_subst in
+                mkRel (idx + lift)
+            with Not_found ->
+              (* A variable that is not matched *)
+              c)
       | _ ->
 	  EConstr.map_with_binders sigma succ predicate lift c
   in
@@ -1996,27 +2016,9 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * type and 1 assumption for each term not _syntactically_ in an
  * inductive type.
 
- * Each matched terms are independently considered dependent or not.
-
- * A type constraint but no annotation case: we try to specialize the
- * tycon to make the predicate if it is not closed.
+ * Each matched term is independently considered dependent or not.
  *)
 
-exception LocalOccur
-
-let noccur_with_meta sigma n m term =
-  let rec occur_rec n c = match EConstr.kind sigma c with
-    | Rel p -> if n<=p && p<n+m then raise LocalOccur
-    | App(f,cl) ->
-        (match EConstr.kind sigma f with
-           | Cast (c,_,_) when isMeta sigma c -> ()
-           | Meta _ -> ()
-           | _ -> EConstr.iter_with_binders sigma succ occur_rec n c)
-    | Evar (_, _) -> ()
-    | _ -> EConstr.iter_with_binders sigma succ occur_rec n c
-  in
-  try (occur_rec n term; true) with LocalOccur -> false
-
 let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
     (** If we put the typing constraint in the term, it has to be
@@ -2026,37 +2028,37 @@ 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 when not (noccur_with_meta sigma 0 max_int t) ->
-	(* If the tycon is not closed w.r.t real variables, we try *)
-        (* two different strategies *)
-       (* First strategy: we abstract the tycon wrt to the dependencies *)
-         let sigma, t = refresh_tycon sigma t in
-         let p1 =
+    | 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
+        (* 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
-	(* Second strategy: we build an "inversion" predicate *)
-	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	(match p1 with
-         | Some (sigma1,pred1,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign]
-         | None -> [sigma2, pred2, arsign])
-    | None, _ ->
-	(* No dependent type constraint, or no constraints at all: *)
-	(* we use two strategies *)
-        let sigma,t = match tycon with
-	| Some t -> refresh_tycon sigma t
-	| None -> 
-          let (sigma, (t, _)) =
-            new_type_evar !!env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
-	    sigma, t
-	in
-        (* First strategy: we build an "inversion" predicate *)
-	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-	(* Second strategy: we directly use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten arsign)) t in
-        [sigma1, pred1, arsign; sigma, pred2, arsign]
+        (* 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,arsign) when not (EConstr.eq_constr sigma pred2 pred3) ->
+             [sigma1, pred1, arsign; sigma2, pred2, arsign; sigma, pred3, arsign]
+         | _ ->
+             [sigma1, pred1, arsign; sigma, pred3, 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/output/Cases.out b/test-suite/output/Cases.out
index dfab400baa..cb835ab48d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -64,14 +64,9 @@ In environment
 texpDenote : forall t : type, texp t -> typeDenote t
 t : type
 e : texp t
-t1 : type
-t2 : type
-t0 : type
-b : tbinop t1 t2 t0
-e1 : texp t1
-e2 : texp t2
-The term "0" has type "nat" while it is expected to have type
- "typeDenote t0".
+n : nat
+The term "n" has type "nat" while it is expected to have type
+ "typeDenote ?t@{t1:=Nat}".
 fun '{{n, m, _}} => n + m
      : J -> nat
 fun '{{n, m, p}} => n + m + p
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a 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) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | 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.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.