From 36c1ed8e7c66844acd0880cd1ff94bd31e38780c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Feb 2018 14:50:56 +0100
Subject: [PATCH] Add a `NoBackTrack` type class.
`NoBackTrack P` requires `P` but will never backtrack on it
once a result for `P` has been found.
---
theories/base.v | 16 ++++++++++++++++
1 file changed, 16 insertions(+)
diff --git a/theories/base.v b/theories/base.v
index 5cd1bd9b..811d46b3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -46,6 +46,22 @@ End seal.
Arguments unseal {_ _} _ : assert.
Arguments seal_eq {_ _} _ : assert.
+(** * Non-backtracking type classes *)
+(** The type class [NoBackTrack P] can be used to establish [P] without ever
+backtracking on the instance of [P] that has been found. Backtracking may
+normally happen when [P] contains evars that could be instanciated in different
+ways depending on which instance is picked, and type class search somewhere else
+depends on this evar.
+
+The proper way of handling this would be by setting Coq's option
+`Typeclasses Unique Instances`. However, this option seems to be broken, see Coq
+issue #6714.
+
+See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
+of this type class. *)
+Class NoBackTrack (P : Prop) := { no_backtrack : P }.
+Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
+
(** * Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
--
GitLab