It happens that the type inference algorithm (pretyping) did not check

that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,

Incidentally removed in pretyping an ill-placed coercion.

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

6 files changed, 37 insertions, 19 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 121d7dcc1b..b104db0267 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -947,7 +947,7 @@ let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
   snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs)
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
-  let pred= abstract_predicate env !evdref indf current dep tms p in
+  let pred = abstract_predicate env !evdref indf current dep tms p in
   (pred, whd_betaiota !evdref
            (applist (pred, realargs@[current])))
 
@@ -1169,7 +1169,9 @@ and match_current pb tomatch =
 	    find_predicate pb.caseloc pb.env pb.evdref
 	      pb.pred current indt (names,dep) pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
-	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
+	  let pred = nf_betaiota !(pb.evdref) pred in
+	  let case = mkCase (ci,pred,current,brvals) in
+	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 69ee8d0290..7762d18f65 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -559,10 +559,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
 		     let v =
-		       let mis,_ = dest_ind_family indf in
-		       let ci = make_case_info env mis LetStyle in
-			 mkCase (ci, p, cj.uj_val,[|f|]) in
-		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+		       let ind,_ = dest_ind_family indf in
+		       let ci = make_case_info env ind LetStyle in
+		       Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		       mkCase (ci, p, cj.uj_val,[|f|]) in
+		     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
 
 		 | None ->
 		     let tycon = lift_tycon cs.cs_nargs tycon in
@@ -578,9 +579,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
-		       let mis,_ = dest_ind_family indf in
-		       let ci = make_case_info env mis LetStyle in
-			 mkCase (ci, p, cj.uj_val,[|f|])
+		       let ind,_ = dest_ind_family indf in
+		       let ci = make_case_info env ind LetStyle in
+		       Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		       mkCase (ci, p, cj.uj_val,[|f|])
 		     in { uj_val = v; uj_type = ccl })
 
     | GIf (loc,c,(na,po),b1,b2) ->
@@ -611,10 +613,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		let ccl = nf_evar !evdref pj.utj_val in
 		let pred = it_mkLambda_or_LetIn ccl psign in
 		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
-		let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
-								     uj_type = typ} tycon
-		in
-		  jtyp.uj_val, jtyp.uj_type
+	        pred, typ
 	    | None ->
 		let p = match tycon with
 		  | Some (None, ty) -> ty
@@ -644,9 +643,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  let b1 = f cstrs.(0) b1 in
 	  let b2 = f cstrs.(1) b2 in
 	  let v =
-	    let mis,_ = dest_ind_family indf in
-	    let ci = make_case_info env mis IfStyle in
-	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+	    let ind,_ = dest_ind_family indf in
+	    let ci = make_case_info env ind IfStyle in
+	    let pred = nf_evar !evdref pred in
+	    Typing.check_allowed_sort env !evdref ind cj.uj_val pred;
+	    mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 834c27969e..e8acd67caf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -770,7 +770,7 @@ let splay_arity env sigma c =
     | Sort s -> l,s
     | _ -> invalid_arg "splay_arity"
 
-let sort_of_arity env c = snd (splay_arity env Evd.empty c)
+let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
   let rec decrec env m ln c = if m = 0 then (ln,c) else
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1a90b23f21..3ffc587ef8 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -152,7 +152,7 @@ val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 val splay_prod : env ->  evar_map -> constr -> (name * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (name * constr) list * constr
 val splay_arity : env ->  evar_map -> constr -> (name * constr) list * sorts
-val sort_of_arity : env -> constr -> sorts
+val sort_of_arity : env -> evar_map -> constr -> sorts
 val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
 val splay_prod_assum :
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b40605f228..85abe2569b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -68,6 +68,16 @@ let e_judge_of_case env evdref ci pj cj lfj =
   { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
     uj_type = rslty }
 
+let check_allowed_sort env sigma ind c p =
+  let pj = Retyping.get_judgment_of env sigma p in
+  let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
+  let specif = Global.lookup_inductive ind in
+  let sorts = elim_sorts specif in
+  if not (List.exists ((=) ksort) sorts) then
+    let s = inductive_sort_family (snd specif) in
+    error_elim_arity env ind sorts c pj
+      (Some(ksort,s,error_elim_explain ksort s))
+
 let e_judge_of_cast env evdref cj k tj =
   let expected_type = tj.utj_val in
   if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
@@ -218,4 +228,3 @@ let solve_evars env evd c =
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
   nf_evar !evdref c
-  
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1e75d375d9..e2fd6a9d84 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 open Environ
 open Evd
@@ -27,3 +28,8 @@ val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
 val solve_evars : env -> evar_map -> constr -> constr
+
+(** Raise an error message if incorrect elimination for this inductive *)
+(** (first constr is term to match, second is return predicate) *)
+val check_allowed_sort : env -> evar_map -> inductive -> constr -> constr ->
+  unit