1 files changed, 23 insertions, 8 deletions
diff --git a/src/Data.hs b/src/Data.hs
index e7b3148..e86aaa6 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -11,6 +11,8 @@
 module Data (module Data, (:~:)(Refl)) where
 
 import Data.Functor.Product
+import Data.GADT.Compare
+import Data.GADT.Show
 import Data.Some
 import Data.Type.Equality
 import Unsafe.Coerce (unsafeCoerce)
@@ -73,10 +75,15 @@ data SNat n where
   SS :: SNat n -> SNat (S n)
 deriving instance Show (SNat n)
 
-instance TestEquality SNat where
-  testEquality SZ SZ = Just Refl
-  testEquality (SS n) (SS n') | Just Refl <- testEquality n n' = Just Refl
-  testEquality _ _ = Nothing
+instance GCompare SNat where
+  gcompare SZ SZ = GEQ
+  gcompare SZ _ = GLT
+  gcompare _ SZ = GGT
+  gcompare (SS n) (SS n') = gorderingLift1 (gcompare n n')
+
+instance TestEquality SNat where testEquality = geq
+instance GEq SNat where geq = defaultGeq
+instance GShow SNat where gshowsPrec = defaultGshowsPrec
 
 fromSNat :: SNat n -> Int
 fromSNat SZ = 0
@@ -90,10 +97,6 @@ reSNat :: Nat -> Some SNat
 reSNat Z = Some SZ
 reSNat (S n) | Some n' <- reSNat n = Some (SS n')
 
-fromNat :: Nat -> Int
-fromNat Z = 0
-fromNat (S m) = succ (fromNat m)
-
 class KnownNat n where knownNat :: SNat n
 instance KnownNat Z where knownNat = SZ
 instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
@@ -155,6 +158,18 @@ vecInit (x :< xs@(_ :< _)) = x :< vecInit xs
 unsafeCoerceRefl :: a :~: b
 unsafeCoerceRefl = unsafeCoerce Refl
 
+gorderingLift1 :: GOrdering a a' -> GOrdering (f a) (f a')
+gorderingLift1 GLT = GLT
+gorderingLift1 GGT = GGT
+gorderingLift1 GEQ = GEQ
+
+gorderingLift2 :: GOrdering a a' -> GOrdering b b' -> GOrdering (f a b) (f a' b')
+gorderingLift2 GLT _ = GLT
+gorderingLift2 GGT _ = GGT
+gorderingLift2 GEQ GLT = GLT
+gorderingLift2 GEQ GGT = GGT
+gorderingLift2 GEQ GEQ = GEQ
+
 data Bag t = BNone | BOne t | BTwo !(Bag t) !(Bag t) | BMany [Bag t] | BList [t]
   deriving (Show, Functor, Foldable, Traversable)