Improving error message when abtraction over goal (abstract_list_all

used when applying schemes - induction, rewrite, ...) is well-typed
but not of the right type.

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

4 files changed, 20 insertions, 7 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d91273037d..0cd5743cdb 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -28,6 +28,7 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
   | CannotFindWellTypedAbstraction of constr * constr list
+  | WrongAbstractionType of name * constr * types * types
   | AbstractionOverMeta of name * name
   | NonLinearUnification of name * constr
   (* Pretyping *)
@@ -154,6 +155,9 @@ let error_cannot_coerce env sigma (m,n) =
 let error_cannot_find_well_typed_abstraction env sigma p l =
   raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
 
+let error_wrong_abstraction_type env sigma na a p l =
+  raise (PretypeError (env, sigma,WrongAbstractionType (na,a,p,l)))
+
 let error_abstraction_over_meta env sigma hdmeta metaarg =
   let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
   raise (PretypeError (env, sigma,AbstractionOverMeta (m,n)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index ef4d2cc689..e2e66e80fd 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -30,6 +30,7 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
   | CannotFindWellTypedAbstraction of constr * constr list
+  | WrongAbstractionType of name * constr * types * types
   | AbstractionOverMeta of name * name
   | NonLinearUnification of name * constr
   (** Pretyping *)
@@ -106,6 +107,9 @@ val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
       constr -> constr list -> 'b
 
+val error_wrong_abstraction_type :  env -> Evd.evar_map ->
+      name -> constr -> types -> types -> 'b
+
 val error_abstraction_over_meta : env -> Evd.evar_map ->
   metavariable -> metavariable -> 'b
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 886c4a3aa1..e25a880f80 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -60,15 +60,17 @@ let abstract_scheme env c l lname_typ =
     (List.rev l)
     lname_typ
 
+(* Precondition: resulting abstraction is expected to be of type [typ] *)
+
 let abstract_list_all env evd typ c l =
   let ctxt,_ = splay_prod_n env evd (List.length l) typ in
   let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in
-  try
-    if is_conv_leq env evd (Typing.type_of env evd p) typ then p
-    else error "abstract_list_all"
-  with UserError _ | Type_errors.TypeError _ ->
-    error_cannot_find_well_typed_abstraction env evd p l
+  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
+  (p,typp)
 
 let set_occurrences_of_last_arg args =
   Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
@@ -1176,7 +1178,10 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
   let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
-  let pred = abstract_list_all env evd' typp typ cllist in
+  let pred,predtyp = abstract_list_all env evd' typp typ cllist in
+  if not (is_conv_leq env evd predtyp typp) then
+    error_wrong_abstraction_type env evd
+      (Evd.meta_name evd p) pred typp predtyp;
   w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[])
 
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e3fd46afea..df87283f99 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -58,7 +58,7 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
    abstracts the terms in l over c to get a term of type t 
    (exported for inv.ml) *)
 val abstract_list_all :
-  env -> evar_map -> constr -> constr -> constr list -> constr
+  env -> evar_map -> constr -> constr -> constr list -> constr * types
 
 
 (* For tracing *)