diff --git a/stdpp/decidable.v b/stdpp/decidable.v
index 39ccc1b42e9d941955a04ccd9a76edd78cd98b6d..cd6118d3eeedd105207fe1d00b9820a5bcdbce0b 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.
 
diff --git a/tests/decidable.ref b/tests/decidable.ref
new file mode 100644
index 0000000000000000000000000000000000000000..5f8d2cc7e8ee4103dad7aa3768a21d11cf206d2a
--- /dev/null
+++ b/tests/decidable.ref
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+No applicable tactic.
diff --git a/tests/decidable.v b/tests/decidable.v
new file mode 100644
index 0000000000000000000000000000000000000000..e192d1822fc838f52b343775b28e77b396c5555d
--- /dev/null
+++ b/tests/decidable.v
@@ -0,0 +1,11 @@
+From stdpp Require Import list.
+
+(** Test that Coq does not infer [x ∈ xs] as [False] by eagerly using
+[False_dec] on a goal with unresolved type class instances. *)
+Example issue_165 (x : nat) :
+  ¬ ∃ xs : list nat, (guard (x ∈ xs); Some x) ≠ None.
+Proof.
+  intros [xs Hxs]. case_option_guard; [|done].
+  Fail done. (* Would succeed if the instance backing [x ∈ xs] is infered as
+  [False]. *)
+Abort.