Fixing bug #2454: inversion predicate strategy for inferring the type

of "match" is not general enough; if there is a non dependent type
constraint, we also try w/o inversion predicate in the return clause.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13727 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 27 insertions, 21 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 848befbeca..f92471ce03 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -520,7 +520,7 @@ val noccur_between : int -> int -> constr -> bool
 
 (** Checking function for terms containing existential- or
    meta-variables.  The function [noccur_with_meta] does not consider
-   meta-variables applied to some terms (intented to be its local
+   meta-variables applied to some terms (intended to be its local
    context) (for existential variables, it is necessarily the case) *)
 val noccur_with_meta : int -> int -> constr -> bool
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f749efdc78..c61edbc55e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1601,7 +1601,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
-let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
+let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
   let arsign = extract_arity_signature env tomatchs sign in
   let names = List.rev (List.map (List.map pi1) arsign) in
   let preds =
@@ -1614,32 +1614,31 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
         let pred1 =
           prepare_predicate_from_arsign_tycon loc tomatchs sign arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
-	let sigma2,pred2 = build_inversion_problem loc env !evdref tomatchs t in
-	[!evdref, KnownDep, pred1; sigma2, DepUnknown, pred2]
-    | None, Some (None, t) ->
-	(* Only one strategy: we build an "inversion" predicate *)
-	let sigma,pred = build_inversion_problem loc env !evdref tomatchs t in
-	[sigma, DepUnknown, pred]
-    | None,  _ ->
-	(* No type constaints: we use two strategies *)
-	let t = mkExistential env ~src:(loc, CasesType) evdref in
-	(* First strategy: we build an inversion problem *)
-	let sigma1,pred1 = build_inversion_problem loc env !evdref tomatchs t in
+	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
+	[sigma, KnownDep, pred1; sigma2, DepUnknown, pred2]
+    | None, _ ->
+	(* No dependent type constraint, or no constraints at all: *)
+	(* we use two strategies *)
+        let sigma,t = match tycon with
+	| Some (None, t) -> sigma,t
+	| _ -> new_evar sigma env ~src:(loc, CasesType) (new_Type ()) 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 names) t in
-	[sigma1, DepUnknown, pred1; !evdref, KnownNotDep, pred2]
+	[sigma1, DepUnknown, pred1; sigma, KnownNotDep, pred2]
     (* Some type annotation *)
     | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
       let env = List.fold_right push_rels arsign env in
+      let evdref = ref sigma in
       let predcclj = typing_fun (mk_tycon (new_Type ())) env evdref rtntyp in
-      Option.iter (fun tycon ->
+      let sigma = Option.cata (fun tycon ->
           let tycon = lift_tycon_type (List.length arsign) tycon in
-	  evdref :=
-            Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
-        tycon;
-      let predccl = (j_nf_evar !evdref predcclj).uj_val in
-      [!evdref, KnownDep, predccl]
+          Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
+        !evdref tycon in
+      let predccl = (j_nf_evar sigma predcclj).uj_val in
+      [sigma, KnownDep, predccl]
   in
   List.map
     (fun (sigma,dep,pred) ->
@@ -1663,7 +1662,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
   let sign = List.map snd tomatchl in
-  let preds = prepare_predicate loc typing_fun evdref env tomatchs sign tycon predopt in
+  let preds = prepare_predicate loc typing_fun !evdref env tomatchs sign tycon predopt in
 
   let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 2972184338..af6e2cd336 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -506,3 +506,10 @@ Definition test (s:step E E) :=
     | Step nil _ (cons E nil) _ Plus l l' => true
     | _ => false
   end.
+
+(* Testing regression of bug 2454 ("get" used not be type-checkable when
+   defined with its type constraint) *)
+
+Inductive K : nat -> Type := KC : forall (p q:nat), K p.
+
+Definition get : K O -> nat := fun x => match x with KC p q => q end.