diff --git a/theories/countable.v b/theories/countable.v
index 535d94b2dd6b56b008f8aecd220f2d67aa6f0484..5573876a28e047e09fe82abc79e2190543df2b41 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -3,6 +3,11 @@ From stdpp Require Export list numbers list_numbers fin.
 From stdpp Require Import options.
 Local Open Scope positive.
 
+(* Note that [Countable A] gives rise to [EqDecision A] by checking equality of
+the results of [encode]. This instance of [EqDecision A] is very inefficient, so
+the native decider is typically preferred for actual computation. To avoid
+overlapping instances, we include [EqDecision A] explicitly as a parameter of
+[Countable A]. *)
 Class Countable A `{EqDecision A} := {
   encode : A → positive;
   decode : positive → option A;