From 3359d749cc36bffb28b1845c2a85a16dc7d17c87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Na=C3=AFm=20Favier?= <n@monade.li>
Date: Sat, 4 Jan 2025 04:24:14 +0100
Subject: [PATCH] =?UTF-8?q?chore:=20make=20`Dec-=E2=86=92`=20incoherent?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It overlaps with `Dec-Fin-∀`.
---
 src/Data/Dec/Base.lagda.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md
index e4bf2476b..4aa0a1fb9 100644
--- a/src/Data/Dec/Base.lagda.md
+++ b/src/Data/Dec/Base.lagda.md
@@ -153,6 +153,7 @@ instance
   Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes λ _ → q
   Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ no ¬q ⦄ = no λ pq → ¬q (pq p)
   Dec-→ {Q = _} ⦃ no ¬p ⦄ ⦃ q ⦄ = yes λ p → absurd (¬p p)
+  {-# INCOHERENT Dec-→ #-}
 
   Dec-⊤ : Dec ⊤
   Dec-⊤ = yes tt