Rework typeclass resolution and control of backtracking.

Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).

1 files changed, 41 insertions, 0 deletions

diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v
new file mode 100644
index 000000000..d3e21898d
--- /dev/null
+++ b/test-suite/typeclasses/backtrack.v
@@ -0,0 +1,41 @@
+Set Typeclasses Strict Resolution.
+
+(* 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.
+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.
\ No newline at end of file