3 files changed, 95 insertions, 2 deletions

diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
index 58668d03..6f37de65 100644
--- a/test-suite/typeclasses/NewSetoid.v
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (* Certified Haskell Prelude.
  * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
 Require Import Coq.Program.Program.
diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v
new file mode 100644
index 00000000..fff740ed
--- /dev/null
+++ b/test-suite/typeclasses/backtrack.v
@@ -0,0 +1,84 @@
+(* Set Typeclasses Unique Instances *)
+(** This lets typeclass search assume that instance heads are unique,
+    so if one matches no other need to be tried,
+    avoiding backtracking (even in unique solutions mode) 
+    This is on a class-by-class basis.
+ *)
+
+(* Non unique *)
+Class B.
+Class A.
+Set Typeclasses Unique Instances.
+(* Unique *)
+Class D.
+Class C (A : Type) := c : A.
+
+Hint Mode C +.
+Fail Definition test := c.
+
+Unset Typeclasses Unique Instances.
+Instance : B -> D -> C nat := fun _ _ => 0.
+Instance : A -> D -> C nat := fun _ _ => 0.
+Instance : B -> C bool := fun _ => true.
+
+Instance : forall A, C A -> C (option A) := fun A _ => None.
+
+Set Typeclasses Debug.
+
+Set Typeclasses Unique Solutions.
+(** This forces typeclass resolution to fail if at least two solutions 
+   exist to a given set of constraints. This is a global setting.
+   For constraints involving assumed unique instances, it will not fail
+   if two such instances could apply, however it will fail if two different
+   instances of a unique class could apply.
+ *)
+Fail Definition foo (d d' : D) (b b' : B) (a' a'' : A) := c : nat.
+Definition foo (d d' : D) (b b' : B) (a' : A) := c : nat.
+
+Fail Definition foo' (b b' : B) := _ : B.
+Unset Typeclasses Unique Solutions.
+Definition foo' (b b' : B) := _ : B.
+
+Set Typeclasses Unique Solutions.
+Definition foo'' (d d' : D) := _ : D.
+
+(** Cut backtracking *)
+Module BacktrackGreenCut.
+  Unset Typeclasses Unique Solutions.
+  Class C (A : Type) := c : A.
+
+  Class D (A : Type) : Type := { c_of_d :> C A }.
+  
+  Instance D1 : D unit.
+  Admitted.
+  
+  Instance D2 : D unit.
+  Admitted.
+
+  (** Two instances of D unit, but when searching for [C unit], no 
+      backtracking on the second instance should be needed except
+      in dependent cases. Check by adding an unresolvable constraint.
+   *)
+
+  Variable f : D unit -> C bool -> True.
+  Fail Definition foo := f _ _. 
+  
+  Fail Definition foo' := let y := _ : D unit in let x := _ : C bool in f _ x. 
+  
+  Unset Typeclasses Strict Resolution.
+  Class Transitive (A : Type) := { trans : True }.
+  Class PreOrder (A : Type) := { preorder_trans :> Transitive A }.
+  Class PartialOrder (A : Type) := { partialorder_trans :> Transitive A }.
+  Class PartialOrder' (A : Type) := { partialorder_trans' :> Transitive A }.
+  
+  Instance: PreOrder nat. Admitted.
+  Instance: PartialOrder nat. Admitted.
+  
+  Class NoInst (A : Type) := {}.
+    
+  Variable foo : forall `{ T : Transitive nat } `{ NoInst (let x:=@trans _ T in nat) }, nat.
+  
+  Fail Definition bar := foo.
+
+
+End BacktrackGreenCut.
diff --git a/test-suite/typeclasses/deftwice.v b/test-suite/typeclasses/deftwice.v
new file mode 100644
index 00000000..439782c9
--- /dev/null
+++ b/test-suite/typeclasses/deftwice.v
@@ -0,0 +1,9 @@
+Class C (A : Type) := c : A -> Type.
+
+Record Inhab (A : Type) := { witness : A }. 
+
+Instance inhab_C : C Type := Inhab.
+
+Variable full : forall A (X : C A), forall x : A, c x.
+
+Definition truc {A : Type} : Inhab A := (full _ _ _).
\ No newline at end of file