Fix in the unification algorithm using evars: unify types of evar

instances and the corresponding evar's type if it contains existentials
to avoid dangling evars. No noticeable performance impact (at least on the
stdlib). Subsumes (and fixes) the (broken) fix in unification.ml that was
previously patched by M. Puech.
Improve error messages related to existential variables and type
classes.


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

5 files changed, 33 insertions, 13 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5491607153..aed50c4687 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -891,6 +891,12 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
  * context "hyps" and not referring to itself.
  *)
 
+and occur_existential evm c =
+  let rec occrec c = match kind_of_term c with
+    | Evar (e, _) -> if not (is_defined evm e) then raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
+
 and evar_define env (evk,_ as ev) rhs evd =
   try
     let (evd',body) = invert_definition env evd ev rhs in
@@ -1045,12 +1051,22 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
 	    then solve_evar_evar evar_define env evd ev1 ev2
 	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
       | _ ->
-	  evar_define env ev1 t2 evd in
+	  let evd = evar_define env ev1 t2 evd in
+	  let evm = evars_of evd in
+	  let evi = Evd.find evm evk1 in
+	    if occur_existential evm evi.evar_concl then
+	      let evenv = evar_env evi in
+	      let evc = nf_isevar evd evi.evar_concl in
+	      let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in
+	      let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
+		fst (conv_algo evenv evd Reduction.CUMUL ty evc)
+	    else evd
+    in
     let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
-    List.fold_left
-      (fun (evd,b as p) (pbty,env,t1,t2) ->
-	if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
-      pbs
+      List.fold_left
+	(fun (evd,b as p) (pbty,env,t1,t2) ->
+	  if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
+	pbs
   with e when precatchable_exception e ->
     (evd,false)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index aa6cc297b3..99252ce653 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -473,6 +473,13 @@ let occur_existential c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
+let occur_meta_or_existential c = 
+  let rec occrec c = match kind_of_term c with
+    | Evar _ -> raise Occur
+    | Meta _ -> raise Occur
+    | _ -> iter_constr occrec c
+  in try occrec c; false with Occur -> true
+
 let occur_const s c = 
   let rec occur_rec c = match kind_of_term c with
     | Const sp when sp=s -> raise Occur
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 92c0a78d48..f5f1a459f4 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -93,6 +93,7 @@ val strip_head_cast : constr -> constr
 exception Occur
 val occur_meta : types -> bool
 val occur_existential : types -> bool
+val occur_meta_or_existential : types -> bool
 val occur_const : constant -> types -> bool
 val occur_evar : existential_key -> types -> bool
 val occur_in_global : env -> identifier -> constr -> unit
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c437d9eab2..1f1bdb4ffc 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -30,7 +30,7 @@ type typeclass = {
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. 
      The boolean indicates if the typeclass argument is a direct superclass and the global reference
-     gives a direct link to the class itselft. *)
+     gives a direct link to the class itself. *)
   cl_context : (global_reference * bool) option list * rel_context; 
 
   (* Context of definitions and properties on defs, will not be shared *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a2671b5d11..9444d91372 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -521,12 +521,8 @@ let w_merge env with_types flags (metas,evars) evd =
 	      let evd' = mimick_evar evd flags f (Array.length cl) evn in
 	      w_merge_rec evd' metas evars eqns
           | _ ->
-	      let evi = Evd.find (evars_of evd) evn in
-	      let env' = push_rels_assum (List.map (fun (_,t) -> Anonymous,t) evars') env in
-	      let rty = Retyping.get_type_of_with_meta env' (evars_of evd) (metas_of evd) rhs' in
-	      let evd', rhs'' = w_coerce_to_type env' evd rhs' rty evi.evar_concl in
-	      let evd'' = solve_simple_evar_eqn env' evd' ev rhs'' in
-		w_merge_rec evd'' metas evars' eqns
+	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
+		metas evars' eqns
 	end
     | [] -> 
 
@@ -694,7 +690,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
       if isMeta op then
 	if allow_K then (evd,op::l)
 	else error "Match_subterm"
-      else if occur_meta op then
+      else if occur_meta_or_existential op then
         let (evd',cl) =
           try 
 	    (* This is up to delta for subterms w/o metas ... *)