Fixed bug #2135 (second-order unification was raising cryptic message)

- made the example work (a call to whd_meta was missing)
- replaced the internal error messages of w_unify_to_subterm_list into
  user-understandable messages
- incidentally fixed the meaning of whd_meta (which now takes an evd)
  and meta_name (which now does what it means and do not treat differently
  the instantiated metas)

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

6 files changed, 27 insertions, 11 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ed18f5e97..cf788f36d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -694,10 +694,7 @@ let meta_reassign mv (v,pb) evd =
 
 (* If the meta is defined then forget its name *)
 let meta_name evd mv =
-  try
-    let (na,def) = clb_name (Metamap.find mv evd.metas) in
-    if def then Anonymous else na
-  with Not_found -> Anonymous
+  try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
 
 let meta_with_name evd id =
   let na = Name id in
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 5b829e5bf..e92ab3206 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -32,6 +32,8 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
   | CannotFindWellTypedAbstraction of constr * constr list
+  | AbstractionOverMeta of name * name
+  | NonLinearUnification of name * constr
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -174,6 +176,14 @@ let error_cannot_coerce env sigma (m,n) =
 let error_cannot_find_well_typed_abstraction env sigma p l =
   raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (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_ise sigma env,AbstractionOverMeta (m,n)))
+
+let error_non_linear_unification env sigma hdmeta t =
+  let m = Evd.meta_name sigma hdmeta in
+  raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t)))
+
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e6e01fc44..f55e70bef 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -31,6 +31,8 @@ type pretype_error =
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
   | CannotFindWellTypedAbstraction of constr * constr list
+  | AbstractionOverMeta of name * name
+  | NonLinearUnification of name * constr
   (** Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -101,6 +103,12 @@ 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_abstraction_over_meta : env -> Evd.evar_map ->
+  metavariable -> metavariable -> 'b
+
+val error_non_linear_unification : env -> Evd.evar_map ->
+  metavariable -> constr -> 'b
+
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type_loc :
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dae668243..bb0ce44ea 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -635,8 +635,8 @@ let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_l
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta metasubst c = match kind_of_term c with
-  | Meta p -> (try List.assoc p metasubst with Not_found -> c)
+let whd_meta sigma c = match kind_of_term c with
+  | Meta p -> (try meta_value sigma p with Not_found -> c)
   | _ -> c
 
 (* Try to replace all metas. Does not replace metas in the metas' values
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index f3bfa1e5f..4518c693d 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -206,7 +206,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env ->  evar_map -> constr
 
 (** {6 Special-Purpose Reduction Functions } *)
 
-val whd_meta : (metavariable * constr) list -> constr -> constr
+val whd_meta : evar_map -> constr -> constr
 val plain_instance : (metavariable * constr) list -> constr -> constr
 val instance :evar_map -> (metavariable * constr) list -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b1b925f78..01109d8af 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -880,12 +880,13 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
   else
     res
 
-let w_unify_to_subterm_list env flags allow_K oplist t evd =
+let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
   List.fold_right
     (fun op (evd,l) ->
+      let op = whd_meta evd op in
       if isMeta op then
 	if allow_K then (evd,op::l)
-	else error "Unify_to_subterm_list"
+	else error_abstraction_over_meta env evd hdmeta (destMeta op)
       else if occur_meta_or_existential op then
         let (evd',cl) =
           try
@@ -895,7 +896,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
         in
 	  if not allow_K && (* ensure we found a different instance *)
 	    List.exists (fun op -> eq_constr op cl) l
-	  then error "Unify_to_subterm_list"
+	  then error_non_linear_unification env evd hdmeta cl
 	  else (evd',cl::l)
       else if allow_K or dependent op t then
 	(evd,op::l)
@@ -909,7 +910,7 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   (* Remove delta when looking for a subterm *)
   let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
   let (evd',cllist) =
-    w_unify_to_subterm_list env flags allow_K oplist typ evd in
+    w_unify_to_subterm_list env flags allow_K p oplist typ evd in
   let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env evd' typp typ cllist in
   w_merge env false flags (evd',[p,pred,(ConvUpToEta 0,TypeProcessed)],[])