Quelques bricoles autour de l'unification:

- Un patch pour le bug de non vérification du typage de Stéphane L.
- Changement du fameux message "cannot solve a second-order matching problem"
  en espérant, à défaut de savoir résoudre plus souvent le problème, que
  le message est plus explicite.
- Divers changements cosmétiques.



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

6 files changed, 60 insertions, 22 deletions

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 71c6bb0dc3..605f2fcd03 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -112,7 +112,7 @@ val metavars_of : constr -> Metaset.t
 val mk_freelisted : constr -> constr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 
-(* Possible constraints over the instance of a metavariable:
+(* Status of an instance found by unification wrt to the meta it solves:
   - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
   - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
   - a term that can be eta-expanded n times while still being a solution
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cd32ac450a..06d1aa533b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -32,6 +32,7 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
+  | CannotFindWellTypedAbstraction of constr * constr list
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -166,6 +167,9 @@ let error_cannot_unify_local env sigma (m,n,sn) =
 let error_cannot_coerce env sigma (m,n) =
   raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
 
+let error_cannot_find_well_typed_abstraction env sigma p l =
+  raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+
 (*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 c6527f337e..a276b4ed51 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -34,6 +34,7 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * identifier option
+  | CannotFindWellTypedAbstraction of constr * constr list
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -101,6 +102,9 @@ val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
 
 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
+
 (*s Ml Case errors *)
 
 val error_cant_find_case_type_loc :
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 84f9330d3b..578afdb75c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -48,8 +48,8 @@ let abstract_list_all env evd typ c l =
   try 
     if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p
     else error "abstract_list_all"
-  with UserError _ ->
-    raise (PretypeError (env,CannotGeneralize typ))
+  with UserError _ | Type_errors.TypeError _ ->
+    error_cannot_find_well_typed_abstraction env (evars_of evd) p l
 
 (**)
 
@@ -142,7 +142,7 @@ let expand_constant env flags c =
   | Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env
   | _ -> None
 
-let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
+let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
   let nb = nb_rel env in
   let trivial_unify pb (metasubst,_) m n =
     match subst_defined_metas metasubst m with
@@ -243,11 +243,11 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
 	    is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
 	| None -> eq_constr m n)
     then 
-      (metas,[])
+      subst
     else 
-      unirec_rec env cv_pb conv_at_top (metas,[]) m n
+      unirec_rec env cv_pb conv_at_top subst m n
 
-let unify_0 = unify_0_with_initial_metas [] true
+let unify_0 = unify_0_with_initial_metas ([],[]) true
 
 let left = true
 let right = false
@@ -451,7 +451,7 @@ let solve_simple_evar_eqn env evd ev rhs =
    or in evars, possibly generating new unification problems; if [b]
    is true, unification of types of metas is required *)
 
-let w_merge env with_types flags metas evars evd =
+let w_merge env with_types flags (metas,evars) evd =
   let rec w_merge_rec evd metas evars eqns =
 
     (* Process evars *)
@@ -528,7 +528,7 @@ let w_merge env with_types flags metas evars evd =
 
 let w_unify_meta_types env ?(flags=default_unify_flags) evd =
   let metas,evd = retract_coercible_metas evd in
-  w_merge env true flags metas [] evd
+  w_merge env true flags (metas,[]) evd
 
 (* [w_unify env evd M N]
    performs a unification of M and N, generating a bunch of
@@ -540,12 +540,22 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    [clenv_typed_unify M N clenv] expects in addition that expected
    types of metavars are unifiable with the types of their instances    *)
 
+let check_types env evd subst m n =
+  if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
+    unify_0_with_initial_metas subst true env (evars_of evd) topconv 
+      default_unify_flags
+      (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
+      (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
+  else
+    subst
+
 let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
-  let (mc2,ec) = 
-    unify_0_with_initial_metas mc1 true env (evars_of evd') cv_pb flags m n
+  let subst1 = check_types env evd (mc1,[]) m n in
+  let subst2 =
+     unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n
   in 
-  w_merge env with_types flags mc2 ec evd'
+  w_merge env with_types flags subst2 evd'
 
 let w_unify_0 env = w_unify_core_0 env false
 let w_typed_unify env = w_unify_core_0 env true
@@ -653,7 +663,7 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
     w_unify_to_subterm_list env flags allow_K oplist typ evd in
   let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env evd' typp typ cllist in
-  w_unify_0 env topconv flags (mkMeta p) pred evd'
+  w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
 
 let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
   let c1, oplist1 = whd_stack ty1 in
@@ -673,7 +683,6 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
 	w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
     | _ -> error "w_unify2"
 
-
 (* The unique unification algorithm works like this: If the pattern is
    flexible, and the goal has a lambda-abstraction at the head, then
    we do a first-order unification.
@@ -707,9 +716,7 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 	    with ex when precatchable_exception ex -> 
 	      try 
 		w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	      with PretypeError (env,NoOccurrenceFound _) as e -> raise e
-		| ex when precatchable_exception ex -> 
-		    error "Cannot solve a second-order unification problem")
+	      with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
 	    
       (* Second order case *)
       | (Meta _, true, _, _ | _, _, Meta _, true) -> 
@@ -719,9 +726,8 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 	      | ex when precatchable_exception ex -> 
 		  try 
 		    w_typed_unify env cv_pb flags ty1 ty2 evd
-		  with ex when precatchable_exception ex -> 
-		    error "Cannot solve a second-order unification problem")
+		  with ex' when precatchable_exception ex' ->
+		    raise ex)
 	    
       (* General case: try first order *)
       | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
-
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 3b4e8af21f..e3fed09e7d 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -174,3 +174,15 @@ Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y.
 Theorem t : r true false.
 apply ax with (R := r).
 Qed.
+
+
+(* Check verification of type at unification (Submitted by Stéphane Lengrand)
+   (without verification, the first "apply" works which leads to wrongly
+   instantiate x by Prop) *)
+
+Theorem t: ~(forall x:Prop, ~x).
+unfold not.
+intro.
+eapply H.
+apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I).
+Defined.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4950f4064d..70450295be 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -403,7 +403,7 @@ let explain_cannot_unify_local env m n subn =
       psubn ++ str " contains local variables"
 
 let explain_refiner_cannot_generalize env ty =
-  str "Cannot find a well-typed generalisation of the goal with type : " ++
+  str "Cannot find a well-typed generalisation of the goal with type: " ++
   pr_lconstr_env env ty
 
 let explain_no_occurrence_found env c id =
@@ -419,6 +419,16 @@ let explain_cannot_unify_binding_type env m n =
   str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
   str "which should be unifiable with" ++ brk(1,1) ++ pn
 
+let explain_cannot_find_well_typed_abstraction env p l =
+  let la,lc = list_chop (List.length l - 1) l in
+  str "Abstracting over the " ++
+  str (plural (List.length l) "term") ++ spc () ++ 
+  hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++
+         (if la<>[] then str " and" ++ spc () else mt()) ++ 
+         pr_lconstr_env env (List.hd lc)) ++ spc () ++
+  str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ 
+  str "which is ill-typed"
+
 let explain_type_error env err =
   let env = make_all_name_different env in
   match err with
@@ -470,6 +480,8 @@ let explain_pretype_error env err =
   | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
   | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
+  | CannotFindWellTypedAbstraction (p,l) ->
+      explain_cannot_find_well_typed_abstraction env p l
 
       
 (* Typeclass errors *)
@@ -716,7 +728,7 @@ let explain_cannot_infer_predicate env typs =
   let env = make_all_name_different env in
   let pr_branch (cstr,typ) =
     let cstr,_ = decompose_app cstr in
-    str "For " ++ pr_lconstr_env env cstr ++ str " : " ++ pr_lconstr_env env typ
+    str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ
   in
   str "Unable to unify the types found in the branches:" ++
   spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))