Fixes incorrect handling of existing existentials variables in

 typeclass code.


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

11 files changed, 71 insertions, 37 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 3ebc3bb5c..67b3adede 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -157,8 +157,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   in
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
-  let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' sigma !isevars;
+  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 2118dfbdd..24066d860 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -73,7 +73,7 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (Evd.evars_of evd) evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 32aa3e413..808039de6 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -550,7 +550,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
 
-  let pretype_gen isevars env lvar kind c =
+  let pretype_gen_aux isevars env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -558,10 +558,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in
       isevars:=evd;
       nf_evar (evars_of !isevars) c'
 
+  let pretype_gen isevars env lvar kind c =
+    let c = pretype_gen_aux isevars env lvar kind c in
+      isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars;
+      nf_evar (evars_of !isevars) c
+
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -609,8 +613,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_tcc_evars evdref env kind c =
     pretype_gen evdref env ([],[]) kind c 
 
-  let understand_tcc sigma env ?expected_type:exptyp c =
-    let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+  let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
+    let ev, t = 
+      if resolve_classes then
+	ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c 
+      else
+	let isevars = ref (Evd.create_evar_defs sigma) in
+	let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in
+	  !isevars, c
+    in
       Evd.evars_of ev, t
 end
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1a5bd0c46..11d3b3710 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -98,7 +98,7 @@ sig
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
   
-  val understand_tcc :
+  val understand_tcc : ?resolve_classes:bool ->
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
 
   val understand_tcc_evars :
@@ -647,7 +647,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env (evars_of !evdref) tj.utj_val v
 
-  let pretype_gen evdref env lvar kind c =
+  let pretype_gen_aux evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -655,10 +655,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in
-      evdref := evd;
-      nf_evar (evars_of evd) c'
-
+      evdref := evd; c'
+	
+  let pretype_gen evdref env lvar kind c =
+    let c = pretype_gen_aux evdref env lvar kind c in
+      evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref;
+      nf_evar (evars_of !evdref) c
+	
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -669,7 +672,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in
     let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
@@ -689,7 +692,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c = pretype_gen evdref env lvar kind c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
       if fail_evar then 
-	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env (evars_of evd) evd in
+	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
 	let c = Evarutil.nf_isevar evd c in
 	  check_evars env Evd.empty evd c;
 	  evd, c
@@ -712,8 +715,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_tcc_evars evdref env kind c =
     pretype_gen evdref env ([],[]) kind c
 
-  let understand_tcc sigma env ?expected_type:exptyp c =
-    let evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+  let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
+    let evd, t =
+      if resolve_classes then
+	ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c 
+      else
+	let evdref = ref (Evd.create_evar_defs sigma) in
+	let c = pretype_gen_aux evdref env ([],[]) (OfType exptyp) c in
+	  !evdref, nf_isevar !evdref c
+    in
     Evd.evars_of evd, t
 end
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 64144f9a4..e7a8374b5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -40,7 +40,7 @@ sig
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
   
-  val understand_tcc :
+  val understand_tcc : ?resolve_classes:bool ->
     evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
     
   val understand_tcc_evars :
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ee385430c..4b078ff30 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -394,22 +394,29 @@ let dest_class_app c =
 let ((bool_in : bool -> Dyn.t),
     (bool_out : Dyn.t -> bool)) = Dyn.create "bool"
   
+let bool_false = bool_in false
+
 let is_resolvable evi =
   match evi.evar_extra with
       Some t -> if Dyn.tag t = "bool" then bool_out t else true
     | None -> true
 	
 let mark_unresolvable evi = 
-  { evi with evar_extra = Some (bool_in false) }
-
+  { evi with evar_extra = Some bool_false }
+    
+let mark_unresolvables sigma =
+  Evd.fold (fun ev evi evs ->
+    Evd.add evs ev (mark_unresolvable evi))
+    sigma Evd.empty
+    
 let has_typeclasses evd =
   Evd.fold (fun ev evi has -> has || 
     (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None 
 	&& is_resolvable evi))
     evd false
 
-let resolve_typeclasses ?(onlyargs=false) ?(fail=true) env sigma evd =
-  if not (has_typeclasses sigma) then evd
+let resolve_typeclasses ?(onlyargs=false) ?(fail=true) env evd =
+  if not (has_typeclasses (Evd.evars_of evd)) then evd
   else
     !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs fail
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e3c780402..b12a85869 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -77,8 +77,9 @@ val bool_out : Dyn.t -> bool
 
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
+val mark_unresolvables : evar_map -> evar_map
 
-val resolve_typeclasses : ?onlyargs:bool -> ?fail:bool -> env -> evar_map -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?fail:bool -> env -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
 val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 226cb3f01..855d388c4 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -28,8 +28,8 @@ let w_refine ev rawc evd =
   let e_info = Evd.find (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
-    try Pretyping.Default.understand_tcc (evars_of evd) env 
-      ~expected_type:e_info.evar_concl rawc 
+    try Pretyping.Default.understand_tcc ~resolve_classes:false
+      (evars_of evd) env ~expected_type:e_info.evar_concl rawc
     with _ -> error ("The term is not well-typed in the environment of " ^
 			string_of_existential ev)
   in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 38fd3ab63..192724b68 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -357,7 +357,10 @@ let full_eauto debug n lems gls =
   let db_list = List.map searchtable_map dbnames in
     e_search_auto debug n lems db_list gls
 
-let typeclasses_eauto debug n lems gls = 
+let nf_goal (gl, valid) =
+  { gl with sigma = Evarutil.nf_evars gl.sigma }, valid
+
+let typeclasses_eauto debug n lems gls =
   let dbnames = [typeclasses_db] in
   let db_list = List.map
     (fun x -> 
@@ -409,15 +412,17 @@ let resolve_one_typeclass env gl =
       let term = Evarutil.nf_evar (sig_sig gls') t in
 	if occur_existential term then raise Not_found else term
 
-let has_undefined p evd =
+let has_undefined p oevd evd =
   Evd.fold (fun ev evi has -> has ||
-    (evi.evar_body = Evar_empty && p ev evi))
+    (evi.evar_body = Evar_empty && p ev evi && 
+	(try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true)))
     (Evd.evars_of evd) false
     
 let resolve_all_evars debug m env p oevd =
+  let oevm = Evd.evars_of oevd in
   try
     let rec aux n evd =
-      if has_undefined p evd then
+      if has_undefined p oevm evd then
 	if n > 0 then
 	  let evd' = resolve_all_evars_once debug m env p evd in
 	    aux (pred n) evd'
@@ -792,7 +797,8 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
       | Some (env', (prf, hypinfo as x)) -> 
 	  let occ = succ occ in
 	    if is_occ occ then (	    
-	      evars := Evd.evar_merge !evars (Evd.evars_of (Evd.undefined_evars env'.evd));
+	      evars := Evd.evar_merge !evars 
+		(Evd.evars_of (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd)));
 	      match cstr with
 		  None -> Some x, occ
 		| Some _ ->
@@ -905,7 +911,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
     match eq with  
 	Some (p, (_, _, oldt, newt)) -> 
 	  (try 
-	      evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) ~fail:true !evars;
+	      evars := Typeclasses.resolve_typeclasses env ~fail:true !evars;
 	      let p = Evarutil.nf_isevar !evars p in
 	      let newt = Evarutil.nf_isevar !evars newt in
 	      let undef = Evd.undefined_evars !evars in
@@ -957,6 +963,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
 let cl_rewrite_clause c left2right occs clause gl =
   init_setoid ();
   let meta = Evarutil.new_meta() in
+  let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in
   let hypinfo = ref (decompose_setoid_eqhyp (pf_env gl) (project gl) c left2right) in
     cl_rewrite_clause_aux hypinfo meta occs clause gl
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 333a26f03..db5c54855 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -512,8 +512,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
   in
   let env' = push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
-  let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses env sigma !isevars;
+  isevars := resolve_typeclasses env !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let imps = 
@@ -569,10 +568,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	let term = Evarutil.nf_isevar !isevars term in
 	let evm = Evd.evars_of (undefined_evars !isevars) in
 	Evarutil.check_evars env Evd.empty !isevars termtype;
-	isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evm !isevars;
 	  if evm = Evd.empty then
 	    declare_instance_constant k pri global imps ?hook id term termtype
-	  else
+	  else begin
+	    isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	      Flags.silently (fun () ->
 		Command.start_proof id kind termtype 
@@ -584,6 +583,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
 	      id
+	  end
       end
 
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 11b849c4f..518ae25cf 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -844,8 +844,7 @@ let interp_recursive fixkind l boxed =
   let evd,_ = consider_remaining_unif_problems env_rec !evdref in
   let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
   let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
-  let evd = Typeclasses.resolve_typeclasses
-    ~onlyargs:false ~fail:true env (evars_of evd) evd in
+  let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
   List.iter (check_evars env_rec Evd.empty evd) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
   check_mutuality env kind (List.combine fixnames fixdefs);