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

1 files changed, 21 insertions, 5 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)