A more informative message when the elimination predicate for

destruct, rewrite, etc. is not well-typed.

Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.

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

7 files changed, 24 insertions, 18 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c2ded73ad1..be5eb5dbdd 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -651,6 +651,8 @@ let set_solve_evars f = solve_evars := f
  * proposition from Dan Grayson]
  *)
 
+exception TypingFailed of evar_map
+
 let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   try
   let args = Array.to_list args in
@@ -702,10 +704,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
 
   (* We instantiate the evars of which the value is forced by typing *)
   let evd,rhs =
-    try !solve_evars env_evar evd rhs
+    let evdref = ref evd in
+    try let c = !solve_evars env_evar evdref rhs in !evdref,c
     with e when Pretype_errors.precatchable_exception e ->
       (* Could not revert all subterms *)
-      raise Exit in
+      raise (TypingFailed !evdref) in
 
   let rec abstract_free_holes evd = function
   | (id,idty,c,_,evsref,_,_)::l ->
@@ -736,7 +739,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       Evd.define evk rhs evd in
 
   abstract_free_holes evd subst, true
-  with Exit -> evd, false
+  with TypingFailed evd -> Evd.define evk rhs evd, false
 
 let second_order_matching_with_args ts env evd ev l t =
 (*
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index d3f8b451a4..5a329f5f4a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -44,7 +44,7 @@ val check_conv_record : constr * types stack -> constr * types stack ->
     (constr stack * types stack) * constr *
     (int * constr)
 
-val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
+val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
 
 val second_order_matching : transparent_state -> env -> evar_map -> 
   existential -> occurrences option list -> constr -> evar_map * bool
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ec808de0ff..f5870a8c0b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -39,7 +39,7 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
-  | CannotFindWellTypedAbstraction of constr * constr list
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
   | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
   | NonLinearUnification of Name.t * constr
@@ -162,8 +162,8 @@ let error_cannot_unify_local env sigma (m,n,sn) =
 let error_cannot_coerce env sigma (m,n) =
   raise (PretypeError (env, sigma,CannotUnify (m,n,None)))
 
-let error_cannot_find_well_typed_abstraction env sigma p l =
-  raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
+let error_cannot_find_well_typed_abstraction env sigma p l e =
+  raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l,e)))
 
 let error_wrong_abstraction_type env sigma na a p l =
   raise (PretypeError (env, sigma,WrongAbstractionType (na,a,p,l)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 36ae6c13fc..ee79651316 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -13,6 +13,7 @@ open Sign
 open Environ
 open Glob_term
 open Inductiveops
+open Type_errors
 
 (** {6 The type of errors raised by the pretyper } *)
 
@@ -41,7 +42,7 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
-  | CannotFindWellTypedAbstraction of constr * constr list
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
   | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
   | NonLinearUnification of Name.t * constr
@@ -49,7 +50,7 @@ type pretype_error =
   | VarNotFound of Id.t
   | UnexpectedType of constr * constr
   | NotProduct of constr
-  | TypingError of Type_errors.type_error
+  | TypingError of type_error
 
 exception PretypeError of env * Evd.evar_map * pretype_error
 
@@ -105,7 +106,7 @@ val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
-      constr -> constr list -> 'b
+      constr -> constr list -> (env * type_error) option -> 'b
 
 val error_wrong_abstraction_type :  env -> Evd.evar_map ->
       Name.t -> constr -> types -> types -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5ae04488fd..7cf7e58890 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -287,10 +287,9 @@ let e_type_of env evd c =
   (* side-effect on evdref *)
   !evdref, Termops.refresh_universes j.uj_type
 
-let solve_evars env evd c =
-  let evdref = ref evd in
+let solve_evars env evdref c =
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  !evdref, nf_evar !evdref c
+  nf_evar !evdref c
 
 let _ = Evarconv.set_solve_evars solve_evars
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 88dc895e6f..084bdbc4f1 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -30,7 +30,7 @@ val check   : env -> evar_map -> constr -> types -> unit
 val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
-val solve_evars : env -> evar_map -> constr -> evar_map * constr
+val solve_evars : env -> evar_map ref -> constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4c0f12d3c7..8b89bd438d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -69,8 +69,11 @@ let abstract_list_all env evd typ c l =
   let p = abstract_scheme env c l_with_all_occs ctxt in
   let typp =
     try Typing.type_of env evd p
-    with UserError _ | Type_errors.TypeError _ ->
-      error_cannot_find_well_typed_abstraction env evd p l in
+    with
+    | UserError _ ->
+        error_cannot_find_well_typed_abstraction env evd p l None
+    | Type_errors.TypeError (env',x) ->
+        error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
   (p,typp)
 
 let set_occurrences_of_last_arg args =
@@ -83,8 +86,8 @@ let abstract_list_all_with_dependencies env evd typ c l =
   let evd,b =
     Evarconv.second_order_matching empty_transparent_state
       env evd ev' argoccs c in
-  if b then nf_evar evd (existential_value evd (destEvar ev))
-  else error "Cannot find a well-typed abstraction."
+  let p = nf_evar evd (existential_value evd (destEvar ev)) in
+  if b then p else error_cannot_find_well_typed_abstraction env evd p l None
 
 (**)