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

4 files changed, 34 insertions, 16 deletions

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