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.