Fix handling of only_classes at toplevel

6 files changed, 234 insertions, 84 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 063bfbe6d..d9780dcc8 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -348,11 +348,12 @@ let constr_flags = {
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
-let refine_tac ist simple c =
+let refine_tac ist simple with_classes c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let flags = constr_flags in
+    let flags =
+      { constr_flags with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
@@ -364,11 +365,23 @@ let refine_tac ist simple c =
   end }
 
 TACTIC EXTEND refine
-| [ "refine" uconstr(c) ] -> [ refine_tac ist false c ]
+| [ "refine" uconstr(c) ] ->
+   [ refine_tac ist false true c ]
 END
 
 TACTIC EXTEND simple_refine
-| [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ]
+| [ "simple" "refine" uconstr(c) ] ->
+   [ refine_tac ist true true c ]
+END
+
+TACTIC EXTEND notcs_refine
+| [ "notypeclasses" "refine" uconstr(c) ] ->
+   [ refine_tac ist false false c ]
+END
+
+TACTIC EXTEND notcs_simple_refine
+| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
+   [ refine_tac ist true false c ]
 END
 
 (**********************************************************************)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1a2f7ff2..103368e02 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -92,7 +92,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
-      optdepr  = false;
+      optdepr  = true;
       optname  = "do typeclass search modulo eta conversion";
       optkey   = ["Typeclasses";"Modulo";"Eta"];
       optread  = get_typeclasses_modulo_eta;
@@ -183,8 +183,8 @@ let set_typeclasses_depth =
 type search_strategy = Dfs | Bfs
 
 let set_typeclasses_strategy = function
-  | Dfs -> set_typeclasses_iterative_deepening true
-  | Bfs -> set_typeclasses_iterative_deepening false
+  | Dfs -> set_typeclasses_iterative_deepening false
+  | Bfs -> set_typeclasses_iterative_deepening true
 
 let pr_ev evs ev =
   Printer.pr_constr_env (Goal.V82.env evs ev) evs
@@ -302,7 +302,7 @@ let with_prods nprods poly (c, clenv) f =
           | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
           | Some (diff, clenv') -> f.enter gl (c, diff, clenv')
       with e when CErrors.noncritical e ->
-        Tacticals.New.tclFAIL 0 (CErrors.print e) end }
+        Tacticals.New.tclZEROMSG (CErrors.print e) end }
   else Proofview.Goal.nf_enter
          { enter = begin fun gl ->
                    if Int.equal nprods 0 then f.enter gl (c, None, clenv)
@@ -345,8 +345,8 @@ let pr_gls sigma gls =
 let shelve_dependencies gls =
   let open Proofview in
   tclEVARMAP >>= fun sigma ->
-  (if !typeclasses_debug > 1 then
-     Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls);
+  (if !typeclasses_debug > 1 && List.length gls > 0 then
+     Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
    shelve_goals gls)
 
 (** Hack to properly solve dependent evars that are typeclasses *)
@@ -1011,6 +1011,17 @@ module Search = struct
 	Evd.add sigma gl evi')
       sigma goals
 
+  let shelve_nonclass info =
+    Proofview.Goal.enter { enter = fun gl ->
+      let gl = Proofview.Goal.assume gl in
+      let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+      if is_class_type sigma (Proofview.Goal.concl gl) then
+        Proofview.tclUNIT ()
+      else (if !typeclasses_debug > 1 then
+              Feedback.msg_debug (pr_depth info.search_depth ++ str": shelving non-class subgoal " ++
+                                    pr_ev sigma (Proofview.Goal.goal gl));
+            Proofview.shelve) }
+
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
       depending on the dependencies of the goal and the unique/Prop
@@ -1121,7 +1132,7 @@ module Search = struct
                in the subgoals, turn them into subgoals now. *)
             let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in
             let shelved = List.map fst shelved and goals = List.map fst goals in
-            if !typeclasses_debug > 1 then
+            if !typeclasses_debug > 1 && not (List.is_empty goals) then
               Feedback.msg_debug
                 (str"Adding shelved subgoals to the search: " ++
                  prlist_with_sep spc (pr_ev sigma) goals ++
@@ -1137,12 +1148,18 @@ module Search = struct
         in res <*> tclEVARMAP >>= finish
       in
       if path_matches derivs [] then aux e tl
-      else ortac
-             (with_shelf tac >>= fun s ->
+      else
+        let filter =
+          if info.search_only_classes then shelve_nonclass info
+          else Proofview.tclUNIT ()
+        in
+        ortac
+             (with_shelf (tac <*> filter) >>= fun s ->
               let i = !idx in incr idx; result s i None)
-             (fun e' -> if CErrors.noncritical (fst e') then
-                       (pr_error e'; aux (merge_exceptions e e') tl)
-                     else iraise e')
+             (fun e' ->
+	      if CErrors.noncritical (fst e') then
+                (pr_error e'; aux (merge_exceptions e e') tl)
+              else (Printf.printf "raising again\n%!"; iraise e'))
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
@@ -1203,9 +1220,12 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
-    let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
-    search_tac hints depth 1 info
+    if only_classes && not (is_class_type sigma (Goal.concl gl)) then
+      Proofview.shelve
+    else
+      let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+      let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
+      search_tac hints depth 1 info
 
   let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
     let open Proofview in
@@ -1236,7 +1256,22 @@ module Search = struct
                                    | (e,ie) -> Proofview.tclZERO ~info:ie e)
     in aux 1
 
-  let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints =
+  let disallow_shelved tac =
+    let open Proofview in
+    with_shelf (tclONCE tac) >>= fun (shelved,result) ->
+    (if not (List.is_empty shelved) then
+       begin
+         Proofview.tclEVARMAP >>= fun sigma ->
+	 let gls = prlist_with_sep spc (pr_ev sigma) shelved in
+	 (if !typeclasses_debug > 0 then
+	  Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls));
+	 Tacticals.New.tclFAIL 1 (str"Proof search failed: " ++
+				  str"shelved goals remain: " ++ gls)
+       end
+     else tclUNIT result)
+
+  let eauto_tac ?(st=full_transparent_state) ?(unique=false) ~only_classes ~depth ~dep hints =
+    let open Proofview in
     let tac =
       let search = search_tac ~st only_classes dep hints in
       if get_typeclasses_iterative_deepening () then
@@ -1257,11 +1292,19 @@ module Search = struct
                                      else str" without reaching its limit"))
       | Proofview.MoreThanOneSuccess ->
          Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
-                                  str"more than one success found.")
+                                  str"more than one success found")
       | e -> Proofview.tclZERO ~info:ie e
-    in Proofview.tclOR tac error
+    in
+    let tac = Proofview.tclOR tac error in
+    let tac =
+      if unique then
+        Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
+      else tac
+    in
+    let tac = if only_classes then disallow_shelved tac else tac in
+    tac
 
-  let run_on_evars ?(unique=false) p evm tac =
+  let run_on_evars p evm tac =
     match evars_to_goals p evm with
     | None -> None (* This happens only because there's no evar having p *)
     | Some (goals, evm') ->
@@ -1275,11 +1318,6 @@ module Search = struct
        let _, pv = Proofview.init evm' [] in
        let pv = Proofview.unshelve goals pv in
        try
-         let tac =
-           if unique then
-             Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac
-           else tac
-         in
          let (), pv', (unsafe, shelved, gaveup), _ =
            Proofview.apply (Global.env ()) tac pv
          in
@@ -1298,16 +1336,15 @@ module Search = struct
          else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
-  let eauto depth only_classes unique dep st hints p evd =
-    let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep:(unique || dep) hints in
-    let res = run_on_evars ~unique p evd eauto_tac in
+  let evars_eauto depth only_classes unique dep st hints p evd =
+    let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+    let res = run_on_evars p evd eauto_tac in
     match res with
     | None -> evd
     | Some evd' -> evd'
-  (* TODO treat unique solutions *)
 
   let typeclasses_eauto ?depth unique st hints p evd =
-    eauto depth true unique false st hints p evd
+    evars_eauto depth true unique false st hints p evd
   (** Typeclasses eauto is an eauto which tries to resolve only
       goals of typeclass type, and assumes that the initially selected
       evars in evd are independent of the rest of the evars *)
@@ -1318,8 +1355,6 @@ module Search = struct
 end
 
 (** Binding to either V85 or Search implementations. *)
-let eauto depth ~only_classes ~st ~dep dbs =
-  Search.eauto_tac ~st ~only_classes ~depth ~dep dbs
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
                       ~depth dbs =
@@ -1336,7 +1371,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
       try V85.eauto85 depth ~only_classes ~st dbs gl
       with Not_found ->
 	Refiner.tclFAIL 0 (str"Proof search failed") gl)
-  else eauto depth ~only_classes ~st ~dep:true dbs
+  else Search.eauto_tac ~st ~only_classes ~depth ~dep:true dbs
 
 (** We compute dependencies via a union-find algorithm.
     Beware of the imperative effects on the partition structure,
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 565415a95..21c5d2172 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -40,6 +40,8 @@ module Search : sig
   val eauto_tac :
     ?st:Names.transparent_state ->
     (** The transparent_state used when working with local hypotheses  *)
+    ?unique:bool ->
+    (** Should we force a unique solution *)
     only_classes:bool ->
     (** Should non-class goals be shelved and resolved at the end *)
     depth:Int.t option ->
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index fcdfa0057..ff515038e 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -1,4 +1,3 @@
-Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
 Require Coq.Setoids.Setoid.
 Import Coq.Setoids.Setoid.
@@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops.
 Local Existing Instance ILFun_ILogic.
 Definition catOP (P Q: OPred) : OPred := admit.
 Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
-admit.
+apply admit.
 Defined.
 Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
 Class IsPointed (T : Type) := point : T.
@@ -69,8 +68,26 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     pose P;
     refine (P _ _)
   end; unfold Basics.flip.
-  2: solve [ apply reflexivity ].
-  Undo.
-  2: reflexivity. (* Toplevel input, characters 18-29:
-Error:
-Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
+  Focus 2.
+  Set Typeclasses Debug.
+  Set Typeclasses Legacy Resolution.
+  apply reflexivity.
+  (* Debug: 1.1: apply @IsPointed_catOP on
+(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
+Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
+Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
+Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
+Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
+Debug: Backtracking after apply @Equivalence_Reflexive
+Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
+Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
+Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
+*)
+  Undo. Unset Typeclasses Legacy Resolution.
+  Test Typeclasses Unique Solutions.
+  Test Typeclasses Unique Instances.
+  Show Existentials.
+  Set Typeclasses Debug Verbosity 2.
+  Set Printing All.
+  Fail apply reflexivity.
+  
\ No newline at end of file
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 651bbf7d2..4581a7ce4 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -5,12 +5,40 @@ Module onlyclasses.
   Hint Extern 0 Foo => exact foo : typeclass_instances.
   Goal Foo * Foo.
     split. shelve.
-    Fail typeclasses eauto.
+    Set Typeclasses Debug.
+    typeclasses eauto.
     typeclasses eauto with typeclass_instances.
     Unshelve. typeclasses eauto with typeclass_instances.
   Abort.
 End onlyclasses.
 
+Module shelve_non_class_subgoals.
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Class Bar := {}.
+  Instance bar1 (f:Foo) : Bar.
+
+  Typeclasses eauto := debug.
+  Set Typeclasses Debug Verbosity 2.
+  Goal Bar.
+    (* Solution has shelved subgoals *)
+    Fail typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+Module shelve_non_class_subgoals2.
+  Class Bar := {}.
+
+  Instance bar1 (t:Type) : Bar.
+  Hint Extern 0 => exact True : typeclass_instances.
+  Typeclasses eauto := debug.
+  Goal Bar.
+    Fail typeclasses eauto.
+    debug eauto with typeclass_instances.
+  Qed.  
+End shelve_non_class_subgoals2.
+
 Module bt.
 Require Import Equivalence.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 4db547f4e..9bcecfe1f 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -5,7 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Require Import List.
 
 Class A (A : Type).
   Instance an: A nat.
@@ -31,6 +30,8 @@ Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
+Existing Class and.
+
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
   eexists. eexists. typeclasses eauto.
@@ -46,7 +47,7 @@ Class C {T} `(a : A T) (t : T).
 Require Import Classes.Init.
 Hint Extern 0 { x : ?A & _ } =>
   unshelve class_apply @existT : typeclass_instances.
-
+Existing Class sigT.
 Set Typeclasses Debug.
 Instance can: C an 0.
 (* Backtrack on instance implementation *)
@@ -63,41 +64,6 @@ Proof.
 Defined.
   
 
-Parameter in_list : list (nat * nat) -> nat -> Prop.
-Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
-  ~ in_list l n.
-
-(* Hints Unfold not_in_list. *)
-
-Axiom
-  lem1 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
-
-Axiom
-  lem2 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
-
-Axiom
-  lem3 :
-    forall (l : list (nat * nat)) (n p q : nat),
-    not_in_list ((p, q) :: l) n -> not_in_list l n.
-
-Axiom
-  lem4 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
-
-Hint Resolve lem1 lem2 lem3 lem4: essai.
-
-Goal
-forall (l : list (nat * nat)) (n p q : nat),
-not_in_list ((p, q) :: l) n -> not_in_list l n.
-  intros.
-  eauto with essai.
-Qed.
-
 (* Example from Nicolas Magaud on coq-club - Jul 2000 *)
 
 Definition Nat : Set := nat.
@@ -126,6 +92,9 @@ Qed.
   Full backtracking on dependent subgoals.
  *)
 Require Import Coq.Classes.Init.
+
+Module NTabareau.
+
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
 Notation "x .1" := (projT1 x) (at level 3).
@@ -149,7 +118,8 @@ Hint Extern 5 (Bar ?D.1) =>
 Hint Extern 5 (Qux ?D.1) =>
     destruct D; simpl : typeclass_instances.
 
-Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances.
+Hint Extern 1 myType =>
+  unshelve refine (fooTobar _ _).1 : typeclass_instances.
 
 Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
 
@@ -158,8 +128,93 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance
 Unset Typeclasses Debug.
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Time typeclasses eauto 10.
+  Time typeclasses eauto 10 with typeclass_instances.
   Undo. Set Typeclasses Iterative Deepening.
-  Time typeclasses eauto.
+  Time typeclasses eauto with typeclass_instances.
 Defined.
 
+End NTabareau.
+
+Module NTabareauClasses.
+
+Set Typeclasses Dependency Order.
+Unset Typeclasses Iterative Deepening.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+Existing Class myType.
+
+Class Foo (a:myType) := {}.
+
+Class Bar (a:myType) := {}.
+
+Class Qux (a:myType) := {}.
+
+Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
+
+Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.
+
+Hint Extern 5 (Bar ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 5 (Qux ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } =>
+  unshelve notypeclasses refine (existT _ _ _) : typeclass_instances.
+
+Unset Typeclasses Debug.
+
+Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
+Proof.
+  Time typeclasses eauto 10 with typeclass_instances.
+  Undo. Set Typeclasses Iterative Deepening.
+  Time typeclasses eauto with typeclass_instances.
+Defined.
+
+End NTabareauClasses.
+
+
+Require Import List.
+
+Parameter in_list : list (nat * nat) -> nat -> Prop.
+Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
+  ~ in_list l n.
+
+(* Hints Unfold not_in_list. *)
+
+Axiom
+  lem1 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
+
+Axiom
+  lem2 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
+
+Axiom
+  lem3 :
+    forall (l : list (nat * nat)) (n p q : nat),
+    not_in_list ((p, q) :: l) n -> not_in_list l n.
+
+Axiom
+  lem4 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
+
+Hint Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal
+forall (l : list (nat * nat)) (n p q : nat),
+not_in_list ((p, q) :: l) n -> not_in_list l n.
+  intros.
+  eauto with essai.
+Qed.