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

6 files changed, 31 insertions, 9 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d91273037..0cd5743cd 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 ef4d2cc68..e2e66e80f 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 886c4a3aa..e25a880f8 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 e3fd46afe..df87283f9 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 *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d598a97e6..81c630884 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -102,8 +102,9 @@ let make_inv_predicate env sigma indf realargs id status concl =
               | None ->
 		let sort = get_sort_family_of env sigma concl in
 		let p = make_arity env true indf (new_sort_in_family sort) in
-		Unification.abstract_list_all env (Evd.create_evar_defs sigma)
-		  p concl (realargs@[mkVar id]) in
+		fst (Unification.abstract_list_all env
+                       (Evd.create_evar_defs sigma)
+		       p concl (realargs@[mkVar id])) in
 	  let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 53c4325e1..141acb3db 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -453,6 +453,13 @@ let explain_cannot_find_well_typed_abstraction env p l =
   str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
   str "which is ill-typed."
 
+let explain_wrong_abstraction_type env na abs expected result =
+  let ppname = match na with Anonymous -> mt() | Name id -> pr_id id ++ spc() in
+  str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++
+  pr_lconstr_env env expected ++ strbrk " with abstraction " ++
+  pr_lconstr_env env abs ++ strbrk " of incompatible type " ++ 
+  pr_lconstr_env env result ++ str "."
+
 let explain_abstraction_over_meta _ m n =
   strbrk "Too complex unification problem: cannot find a solution for both " ++
   pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
@@ -517,6 +524,7 @@ let explain_pretype_error env sigma err =
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
   | CannotFindWellTypedAbstraction (p,l) ->
       explain_cannot_find_well_typed_abstraction env p l
+  | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env n a t u
   | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
   | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
   | TypingError t -> explain_type_error env sigma t