Substitute terms for evars-as-goals as soon as they are solved in

typeclass resolution. Fixes a bug reported by Eelis van der Weegen.


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

2 files changed, 81 insertions, 8 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4a2964a6fc..558ee34d69 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -226,7 +226,8 @@ type validation = evar_map -> proof_tree list -> proof_tree
 
 let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
 
-type autoinfo = { hints : Auto.hint_db; only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds }
+type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
+		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds }
 type autogoal = goal * autoinfo
 type 'ans fk = unit -> 'ans
 type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -272,7 +273,7 @@ let intro_tac : atac =
 	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) 
 	    (true,false,false) info.only_classes None (List.hd (evar_context g')) in
 	  let ldb = Hint_db.add_list hint info.hints in
-	    (g', { info with hints = ldb; auto_last_tac = str"intro" })) gls
+	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = str"intro" })) gls
       in {it = gls'; sigma = s})
 
 let normevars_tac : atac = 
@@ -280,7 +281,7 @@ let normevars_tac : atac =
     (fun {it = gls; sigma = s} info ->
       let gls' =
 	List.map (fun g' ->
-	  (g', { info with auto_last_tac = str"NORMEVAR" })) gls
+	  (g', { info with is_evar = None; auto_last_tac = str"NORMEVAR" })) gls
       in {it = gls'; sigma = s})
 
 
@@ -335,6 +336,7 @@ let hints_tac hints =
 	  let gls' = list_map_i (fun j g -> 
 	    let info = 
 	      { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+		is_evar = None;
 		hints = 
 		  if b && g.evar_hyps <> gl.evar_hyps 
 		  then make_autogoal_hints info.only_classes
@@ -351,7 +353,17 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
     | (gl,info) :: gls ->
 	second.skft (fun ({it=gls';sigma=s'},v') fk' ->
 	  let fk'' = if gls' = [] && Evarutil.is_ground_term s gl.evar_concl then
-	    (if !typeclasses_debug then msgnl (str"no backtrack on" ++ pr_ev s gl); fk) else fk' in
+	    (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' in
+	  let s' = 
+	    if gls' = [] then
+	      match info.is_evar with
+	      | Some ev -> 
+		  let prf = v' s' [] in
+		  let term, _ = Refiner.extract_open_proof s' prf in
+		    Evd.define ev term s'
+	      | None -> s'
+	    else s'
+	  in
 	    aux s' ((gls',v')::acc) fk'' gls) fk {it = (gl,info); sigma = s}
     | [] -> Some (List.rev acc, s, fk)
   in fun ({it = gls; sigma = s},v) fk ->
@@ -385,13 +397,14 @@ let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res
 let rec fix (t : 'a tac) : 'a tac =
   then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
 
-let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) g =
+let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) ev g =
   let hints = make_autogoal_hints only_classes ~st g in
-    (g.it, { hints = hints ; only_classes = only_classes; auto_depth = []; auto_last_tac = mt() })
+    (g.it, { hints = hints ; is_evar = ev; 
+	     only_classes = only_classes; auto_depth = []; auto_last_tac = mt() })
       
 let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' =
   { it = list_map_i (fun i g -> 
-    let (gl, auto) = make_autogoal ~only_classes ~st {it = snd g; sigma = evm'} in
+    let (gl, auto) = make_autogoal ~only_classes ~st (Some (fst g)) {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
 
 let get_result r = 
@@ -414,7 +427,7 @@ let eauto_tac hints =
   fix (or_tac intro_tac (then_tac normevars_tac (hints_tac hints)))
   
 let eauto ?(only_classes=true) ?st hints g =
-  let gl = { it = make_autogoal ~only_classes ?st g; sigma = project g } in
+  let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in
     match run_tac (eauto_tac hints) gl with
     | None -> raise Not_found
     | Some ({it = goals; sigma = s}, valid) ->
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
new file mode 100644
index 0000000000..55351a472c
--- /dev/null
+++ b/test-suite/success/Typeclasses.v
@@ -0,0 +1,60 @@
+Generalizable All Variables.
+
+Module mon.
+
+Reserved Notation "'return' t" (at level 0).
+Reserved Notation "x >>= y" (at level 65, left associativity).
+
+
+
+Record Monad {m : Type -> Type} := {
+  unit : Π {α}, α -> m α where "'return' t" := (unit t) ;
+  bind : Π {α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ;
+  bind_unit_left : Π {α β} (a : α) (f : α -> m β), return a >>= f = f a }.
+
+Print Visibility.
+Print unit.
+Implicit Arguments unit [[m] [m0] [α]].
+Implicit Arguments Monad [].
+Notation "'return' t" := (unit t).
+
+(* Test correct handling of existentials and defined fields. *)
+
+Class A `(e: T) := { a := True }.
+Class B `(e_: T) := { e := e_; sg_ass :> A e }.
+
+Goal forall `{B T}, a.
+  intros. exact I.
+Defined.
+
+Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }.
+
+Goal forall `{B' T}, a.
+  intros. exact I.
+Defined.
+
+End mon.
+
+(* Correct treatment of dependent goals *) 
+
+(* First some preliminaries: *)
+
+Section sec.
+  Context {N: Type}.
+  Class C (f: N->N) := {}.
+  Class E := { e: N -> N }.
+  Context
+    (g: N -> N) `(E) `(C e)
+    `(forall (f: N -> N), C f -> C (fun x => f x))
+    (U: forall f: N -> N, C f -> False).
+
+(* Now consider the following: *)
+
+  Let foo := U (fun x => e x).
+  Check foo _.
+
+(* This type checks fine, so far so good. But now
+ let's try to get rid of the intermediate constant foo.
+ Surely we can just expand it inline, right? Wrong!: *)
+ Check U (fun x => e x) _.
+End sec.
\ No newline at end of file