From 92c79d918b1107a48914f7ccebbe71c555e792a3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Dec 2022 13:00:45 +0100
Subject: [PATCH] Use high cost for `Decision` instances for `True` and
 `False`.

---
 stdpp/decidable.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/stdpp/decidable.v b/stdpp/decidable.v
index 39ccc1b4..cd6118d3 100644
--- a/stdpp/decidable.v
+++ b/stdpp/decidable.v
@@ -87,8 +87,13 @@ Notation cast_if_not S := (if S then right _ else left _).
 
 (** * Instances of [Decision] *)
 (** Instances of [Decision] for operators of propositional logic. *)
-Global Instance True_dec: Decision True := left I.
-Global Instance False_dec: Decision False := right (False_rect False).
+(** The instances for [True] and [False] have a very high cost. If they are
+applied too eagerly, HO-unification could wrongfully instantiate TC instances
+with [λ .., True] or [λ .., False].
+See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/165 *)
+Global Instance True_dec: Decision True | 1000 := left I.
+Global Instance False_dec: Decision False | 1000 := right (False_rect False).
+
 Global Instance Is_true_dec b : Decision (Is_true b).
 Proof. destruct b; simpl; apply _. Defined.
 
-- 
GitLab