WIP: DecideEq

dec/src/Data/Type/Dec.hs

@@ -1,8 +1,12 @@
+{-# LANGUAGE GADTs         #-}
+{-# LANGUAGE PolyKinds     #-}
+{-# LANGUAGE TypeOperators #-}
 module Data.Type.Dec (
     -- * Types
     Neg,
     Dec (..),
     Decidable (..),
+    DecideEq (..),
     -- * Neg combinators
     toNegNeg,
     tripleNeg,
@@ -15,6 +19,7 @@ module Data.Type.Dec (
     decToBool,
     ) where
 
+import Data.Type.Equality ((:~:) (..))
 import Data.Void          (Void)
 
 -- | Intuitionistic negation.
@@ -36,6 +41,15 @@ data Dec a
 class Decidable a where
     decide :: Dec a
 
+-- | Decidable equality.
+--
+-- @since 0.0.4
+class DecideEq s where
+    decideEq :: s a -> s b -> Dec (a :~: b)
+
+instance DecideEq ((:~:) c) where
+    decideEq Refl Refl = Yes Refl
+
 -------------------------------------------------------------------------------
 -- Neg combinators
 -------------------------------------------------------------------------------

fin/src/Data/Fin.hs

@@ -1,11 +1,11 @@
 {-# LANGUAGE DataKinds            #-}
 {-# LANGUAGE DeriveDataTypeable   #-}
-{-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
 {-# LANGUAGE StandaloneDeriving   #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE EmptyCase            #-}
 -- | Finite numbers.
 --
 -- This module is designed to be imported as

fin/src/Data/Type/Nat.hs

@@ -190,6 +190,15 @@ discreteNat = getDiscreteNat $ induction (DiscreteNat start) (\p -> DiscreteNat
 
 newtype DiscreteNat n = DiscreteNat { getDiscreteNat :: forall m. SNatI m => Dec (n :~: m) }
 
+-- |
+--
+-- @since 0.1.1
+instance DecideEq SNat where
+    decideEq SZ SZ = Yes Refl
+    decideEq SS SS = discreteNat
+    decideEq SS SZ = No $ \p -> case p of {}
+    decideEq SZ SS = No $ \p -> case p of {}
+
 instance TestEquality SNat where
     testEquality SZ SZ = Just Refl
     testEquality SZ SS = Nothing