1 files changed, 185 insertions, 3 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 30a2a742..6b1f0315 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,117 @@
+Module onlyclasses.
+
+(* In 8.6 we still allow non-class subgoals *)
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Goal Foo * Foo.
+    split. shelve.
+    Set Typeclasses Debug.
+    typeclasses eauto.
+    Unshelve. typeclasses eauto.
+  Qed.
+
+  Module RJung.
+    Class Foo (x : nat).
+      
+      Instance foo x : x = 2 -> Foo x.
+      Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
+      Typeclasses eauto := debug.
+      Check (_ : Foo 2).
+
+
+      Fail Definition foo := (_ : 0 = 0).
+
+  End RJung.
+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 (of non typeclass type) *)
+    typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+Module RefineVsNoTceauto.
+
+  Class Foo (A : Type) := foo : A.
+  Instance: Foo nat := { foo := 0 }.
+  Instance: Foo nat := { foo := 42 }.
+  Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances.
+  Goal exists (f : Foo nat), @foo _ f = 0.
+  Proof.
+    unshelve (notypeclasses refine (ex_intro _ _ _)). 
+    Set Typeclasses Debug. Set Printing All.
+    all:once (typeclasses eauto).
+    Fail idtac. (* Check no subgoals are left *)
+    Undo 3.
+    (** In this case, the (_ = _) subgoal is not considered 
+        by typeclass resolution *)
+    refine (ex_intro _ _ _). Fail reflexivity.
+  Abort.
+
+End RefineVsNoTceauto.
+
+Module Leivantex2PR339.
+  (** Was a bug preventing to find hints associated with no pattern *)
+  Class Bar := {}.
+  Instance bar1 (t:Type) : Bar.
+  Hint Extern 0 => exact True : typeclass_instances.
+  Typeclasses eauto := debug.
+  Goal Bar.
+    Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto. (* Relies on resolution of a non-class subgoal *)
+    Undo 1.
+    typeclasses eauto with typeclass_instances.
+  Qed.
+End Leivantex2PR339.
+
+Module bt.
+Require Import Equivalence.
+
+Record Equ (A : Type) (R : A -> A -> Prop).
+Definition equiv {A} R (e : Equ A R) := R.
+Record Refl (A : Type) (R : A -> A -> Prop).
+Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo.
+
+Variable R : nat -> nat -> Prop.
+Lemma bas : Equ nat R.
+Admitted.
+Hint Resolve bas : foo.
+Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo.
+
+Goal exists R, @Refl nat R.
+  eexists.
+  Set Typeclasses Debug.
+  (* Fail solve [unshelve eauto with foo]. *)
+  Set Typeclasses Debug Verbosity 1.
+  Test Typeclasses Depth.
+  solve [typeclasses eauto with foo].
+Qed.
+
+Set Typeclasses Compatibility "8.5".
+Parameter f : nat -> Prop.
+Parameter g : nat -> nat -> Prop.
+Parameter h : nat -> nat -> nat -> Prop.
+Axiom a : forall x y, g x y -> f x -> f y.
+Axiom b : forall x (y : Empty_set), g (fst (x,y)) x.
+Axiom c : forall x y z, h x y z -> f x -> f y.
+Hint Resolve a b c : mybase.
+Goal forall x y z, h x y z -> f x -> f y.
+  intros.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
+  Unshelve.
+Abort.
+End bt.
 Generalizable All Variables.
 
 Module mon.
@@ -23,8 +137,15 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Goal forall `{B T}, a.
-  intros. exact I.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
+
+Goal forall `{B T}, Prop.
+  intros. apply a.
+Defined.
+
+Goal forall `{B T}, Prop.
+  intros. refine (@a _ _ _).
 Defined.
 
 Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }.
@@ -57,4 +178,65 @@ Section sec.
  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
+End sec.
+
+Module UniqueSolutions.
+  Set Typeclasses Unique Solutions.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := {}.
+    Instance eqb : Eq nat := {}.
+
+    Goal Eq nat.
+      try apply _.
+      Fail exactly_once typeclasses eauto.
+    Abort.
+End UniqueSolutions.
+
+
+Module UniqueInstances.
+  (** Optimize proof search on this class by never backtracking on (closed) goals
+      for it. *)
+  Set Typeclasses Unique Instances.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := _. constructor. Qed.
+    Instance eqb : Eq nat := {}.
+    Class Foo (A : Type) (e : Eq A) : Set.
+    Instance fooa : Foo _ eqa := {}.
+
+    Tactic Notation "refineu" open_constr(c) := unshelve refine c.
+
+    Set Typeclasses Debug.
+    Goal { e : Eq nat & Foo nat e }.
+      unshelve refineu (existT _ _ _).
+      all:simpl.
+      (** Does not backtrack on the (wrong) solution eqb *)
+      Fail all:typeclasses eauto.
+    Abort.
+End UniqueInstances.
+
+Module IterativeDeepening.
+
+  Class A.
+  Class B.
+  Class C.
+
+  Instance: B -> A | 0.
+  Instance: C -> A | 0.
+  Instance: C -> B -> A | 0.
+  Instance: A -> A | 0.
+  
+  Goal C -> A.
+    intros.
+    Set Typeclasses Debug.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    Fail typeclasses eauto 1.
+    typeclasses eauto 2.
+    Undo.
+    Unset Typeclasses Iterative Deepening.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    typeclasses eauto.
+  Qed.
+
+End IterativeDeepening.