From de50c9765c5236040702ff9f4ee10282d8a871de Mon Sep 17 00:00:00 2001
From: olafklinke <84761329+olafklinke@users.noreply.github.com>
Date: Thu, 23 Mar 2023 11:52:10 +0100
Subject: [PATCH 1/2] add Decidable instances for ->, Neg and Either

add instances
`Decidable a => Decidable (Neg a)`
`(Decidable a, Decidable b) => Decidable (a -> b)`
`(Decidable a, Decidable b) => Decidable (Either a b)`
---
 src/Data/Type/Dec.hs | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/Data/Type/Dec.hs b/src/Data/Type/Dec.hs
index a527524..764096f 100644
--- a/src/Data/Type/Dec.hs
+++ b/src/Data/Type/Dec.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
 module Data.Type.Dec (
     -- * Types
     Neg,
@@ -70,6 +71,26 @@ instance (Decidable a, Decidable b) => Decidable (a, b) where
             No ny -> No (\c -> ny (snd c))
             Yes y -> Yes (x, y)
 
+-- | Implications are decidable
+instance forall a b. (Decidable a, Decidable b) => Decidable (a -> b) where
+    decide = case (decide :: Dec a, decide :: Dec b) of
+        (No no, _    ) -> Yes (absurd.no)
+        (Yes a, No no) -> No (\f -> no (f a))
+        (Yes _, Yes b) -> Yes (const b)
+
+-- | Disjunctions are decidable
+instance forall a b. (Decidable a, Decidable b) => Decidable (Either a b) where
+    decide = case (decide :: Dec a, decide :: Dec b) of
+        (No a, No b) -> No (either a b)
+        (Yes a, _  ) -> Yes (Left a)
+        (No _,Yes b) -> Yes (Right b)
+
+-- | Negations are decidable
+instance forall a. Decidable a => Decidable (a -> Void) where
+    decide = case decide :: Dec a of
+        Yes a -> No (\neg -> neg a)
+        No no -> Yes no
+
 -------------------------------------------------------------------------------
 -- Neg combinators
 -------------------------------------------------------------------------------

From 048f569552f6c1c472273587a66fef9ce1364396 Mon Sep 17 00:00:00 2001
From: olafklinke <84761329+olafklinke@users.noreply.github.com>
Date: Thu, 23 Mar 2023 15:01:43 +0100
Subject: [PATCH 2/2] remove Decidable for negation

Decidability for `Neg a` is subsumed by decidability of implication. Avoid overlapping instances.
---
 src/Data/Type/Dec.hs | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/Data/Type/Dec.hs b/src/Data/Type/Dec.hs
index 764096f..bb123c8 100644
--- a/src/Data/Type/Dec.hs
+++ b/src/Data/Type/Dec.hs
@@ -71,7 +71,8 @@ instance (Decidable a, Decidable b) => Decidable (a, b) where
             No ny -> No (\c -> ny (snd c))
             Yes y -> Yes (x, y)
 
--- | Implications are decidable
+-- | Implications are decidable.
+-- Note: This subsumes @(a -> Void)@ so negations are decidable.
 instance forall a b. (Decidable a, Decidable b) => Decidable (a -> b) where
     decide = case (decide :: Dec a, decide :: Dec b) of
         (No no, _    ) -> Yes (absurd.no)
@@ -85,12 +86,6 @@ instance forall a b. (Decidable a, Decidable b) => Decidable (Either a b) where
         (Yes a, _  ) -> Yes (Left a)
         (No _,Yes b) -> Yes (Right b)
 
--- | Negations are decidable
-instance forall a. Decidable a => Decidable (a -> Void) where
-    decide = case decide :: Dec a of
-        Yes a -> No (\neg -> neg a)
-        No no -> Yes no
-
 -------------------------------------------------------------------------------
 -- Neg combinators
 -------------------------------------------------------------------------------