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

10 files changed, 52 insertions, 26 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index aeeefbfa4..21f86233a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -233,12 +233,6 @@ let type_of_constructors ind (mib,mip) =
 
 (************************************************************************)
 
-let error_elim_expln kp ki =
-  match kp,ki with
-  | (InType | InSet), InProp -> NonInformativeToInformative
-  | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
-  | _ -> WrongArity
-
 (* Type of case predicates *)
 
 let local_rels ctxt =
@@ -290,7 +284,7 @@ exception LocalArity of (sorts_family * sorts_family * arity_error) option
 let check_allowed_sort ksort specif =
   if not (List.exists ((=) ksort) (elim_sorts specif)) then
     let s = inductive_sort_family (snd specif) in
-    raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
+    raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
 
 let is_correct_arity env c pj ind specif params =
   let arsign,_ = get_instantiated_arity specif params in
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 0f849e11a..8f129999b 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -109,4 +109,9 @@ let error_ill_formed_rec_body env why lna i fixenv vdefj =
 let error_ill_typed_rec_body env i lna vdefj vargs =
   raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
+let error_elim_explain kp ki =
+  match kp,ki with
+  | (InType | InSet), InProp -> NonInformativeToInformative
+  | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
+  | _ -> WrongArity
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 2bf96f322..7c61e1057 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -97,3 +97,4 @@ val error_ill_formed_rec_body :
 val error_ill_typed_rec_body  :
   env -> int -> name array -> unsafe_judgment array -> types array -> 'a
 
+val error_elim_explain : sorts_family -> sorts_family -> arity_error
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 121d7dcc1..b104db026 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 69ee8d029..7762d18f6 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 834c27969..e8acd67ca 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 1a90b23f2..3ffc587ef 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 b40605f22..85abe2569 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 1e75d375d..e2fd6a9d8 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
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 5ac6ce82b..c65cf3036 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *.
 change 3 at 1 with (1+2) in H, H|-.
 change 3 in |- * at 1.
  *)
+
+(* Test that pretyping checks allowed elimination sorts *)
+
+Goal True.
+Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
+Fail change True with
+        match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
+Abort.