diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,12 @@
 # Version history for bin
 
+## 0.1.2
+
+- Add `boring` instances
+- Add `EqBinP` and `EqBin` type families
+- Add `NFData` instances
+- Add `GEq`, `GNFData`, `GShow` (from `some` package) instances for `SBin` and `SBinP`.
+
 ## 0.1.1
 
 - Explicitly mark all modules as Safe or Trustworthy.
diff --git a/bin.cabal b/bin.cabal
--- a/bin.cabal
+++ b/bin.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.2
 name:               bin
-version:            0.1.1
+version:            0.1.2
 synopsis:           Bin: binary natural numbers.
 category:           Data, Dependent Types, Singletons, Math
 description:
@@ -43,6 +43,7 @@
    || ==8.8.4
    || ==8.10.4
    || ==9.0.1
+   || ==9.2.1
 
 source-repository head
   type:     git
@@ -64,17 +65,19 @@
 
   other-modules:    TrustworthyCompat
   build-depends:
-    , base        >=4.7     && <4.16
+    , base        >=4.7     && <4.17
+    , boring      ^>=0.2
     , dec         ^>=0.0.3
     , deepseq     >=1.3.0.2 && <1.5
     , fin         ^>=0.2
-    , hashable    >=1.2.7.0 && <1.4
+    , hashable    >=1.2.7.0 && <1.5
     , QuickCheck  ^>=2.14.2
+    , some        ^>=1.0.3
 
   if !impl(ghc >=7.10)
     build-depends: nats ^>=1.1.2
 
-  if impl(ghc >= 9.0)
+  if impl(ghc >=9.0)
     -- these flags may abort compilation with GHC-8.10
     -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295
     ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode
diff --git a/src/Data/Bin/Pos.hs b/src/Data/Bin/Pos.hs
--- a/src/Data/Bin/Pos.hs
+++ b/src/Data/Bin/Pos.hs
@@ -32,12 +32,14 @@
        (Bounded (..), Eq, Int, Integer, Ord (..), Show (..), ShowS, String,
        fmap, fromIntegral, map, showParen, showString, ($), (.))
 
+import Control.DeepSeq (NFData (..))
 import Data.Bin        (Bin (..), BinP (..))
 import Data.BinP.PosP  (PosP (..))
 import Data.Typeable   (Typeable)
 import Numeric.Natural (Natural)
 
 import qualified Data.BinP.PosP  as PP
+import qualified Data.Boring     as Boring
 import qualified Data.Type.Bin   as B
 import qualified Data.Type.BinP  as BP
 import qualified Test.QuickCheck as QC
@@ -79,6 +81,10 @@
     minBound = Pos minBound
     maxBound = Pos maxBound
 
+-- | @since 0.1.2
+instance NFData (Pos b) where
+    rnf (Pos p) = rnf p
+
 -------------------------------------------------------------------------------
 -- QuickCheck
 -------------------------------------------------------------------------------
@@ -185,6 +191,18 @@
 --
 weakenRight1 :: SBinPI b => Pos ('BP b) -> Pos (Succ'' b)
 weakenRight1 (Pos b) = Pos (PP.weakenRight1 b)
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance b ~ 'BP 'BE => Boring.Boring (Pos b) where
+    boring = boring
+
+-- | @since 0.1.2
+instance b ~ 'BZ => Boring.Absurd (Pos b) where
+    absurd = absurd
 
 -------------------------------------------------------------------------------
 -- Universe
diff --git a/src/Data/BinP/PosP.hs b/src/Data/BinP/PosP.hs
--- a/src/Data/BinP/PosP.hs
+++ b/src/Data/BinP/PosP.hs
@@ -35,6 +35,7 @@
        Ordering (..), Show (..), ShowS, String, either, fmap, fromIntegral, map,
        showParen, showString, ($), (*), (+), (++), (.))
 
+import Control.DeepSeq (NFData (..))
 import Data.Bin        (BinP (..))
 import Data.Nat        (Nat (..))
 import Data.Proxy      (Proxy (..))
@@ -43,6 +44,7 @@
 import Numeric.Natural (Natural)
 
 import qualified Data.Bin        as B
+import qualified Data.Boring     as Boring
 import qualified Data.Type.Bin   as B
 import qualified Data.Type.BinP  as BP
 import qualified Data.Type.Nat   as N
@@ -107,6 +109,17 @@
         SB0 -> There0 maxBound
         SB1 -> There1 maxBound
 
+-- | @since 0.1.2
+instance NFData (PosP b) where
+    rnf (PosP p) = rnf p
+
+-- | @since 0.1.2
+instance NFData (PosP' n b) where
+    rnf (AtEnd w)  = rnf w
+    rnf (Here w)   = rnf w
+    rnf (There1 p) = rnf p
+    rnf (There0 p) = rnf p
+
 -------------------------------------------------------------------------------
 -- QuickCheck
 -------------------------------------------------------------------------------
@@ -277,6 +290,14 @@
     B.SBE -> map AtEnd W.universe
     B.SB0 -> map There0 universe'
     B.SB1 -> map Here W.universe ++ map There1 universe'
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance b ~ 'BE => Boring.Boring (PosP b) where
+    boring = boring
 
 -------------------------------------------------------------------------------
 -- Helpers
diff --git a/src/Data/Type/Bin.hs b/src/Data/Type/Bin.hs
--- a/src/Data/Type/Bin.hs
+++ b/src/Data/Type/Bin.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE KindSignatures       #-}
 {-# LANGUAGE RankNTypes           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -28,6 +29,7 @@
     reflectToNum,
     -- * Type equality
     eqBin,
+    EqBin,
     -- * Induction
     induction,
     -- * Arithmetic
@@ -49,12 +51,17 @@
     Bin0, Bin1, Bin2, Bin3, Bin4, Bin5, Bin6, Bin7, Bin8, Bin9,
     ) where
 
-import Data.Bin        (Bin (..), BinP (..))
-import Data.Nat        (Nat (..))
-import Data.Proxy      (Proxy (..))
-import Data.Type.BinP  (SBinP (..), SBinPI (..))
-import Data.Typeable   (Typeable)
-import Numeric.Natural (Natural)
+import Control.DeepSeq   (NFData (..))
+import Data.Bin          (Bin (..), BinP (..))
+import Data.Boring       (Boring (..))
+import Data.GADT.Compare (GEq (..))
+import Data.GADT.DeepSeq (GNFData (..))
+import Data.GADT.Show    (GShow (..))
+import Data.Nat          (Nat (..))
+import Data.Proxy        (Proxy (..))
+import Data.Type.BinP    (SBinP (..), SBinPI (..))
+import Data.Typeable     (Typeable)
+import Numeric.Natural   (Natural)
 
 import qualified Data.Type.BinP as BP
 import qualified Data.Type.Nat  as N
@@ -63,10 +70,11 @@
 import TrustworthyCompat
 
 -- $setup
--- >>> :set -XDataKinds
+-- >>> :set -XDataKinds -XExplicitNamespaces -XTypeOperators
 -- >>> import Data.Bin
--- >>> import Data.Type.BinP (BinP2, BinP3)
+-- >>> import Data.Type.BinP (BinP2, BinP3, BinP9)
 -- >>> import Data.Nat (Nat (..))
+-- >>> import Data.Type.Equality (type (==))
 -- >>> import qualified Data.Type.BinP as BP
 -- >>> import qualified Data.Type.Nat as N
 -- >>> import qualified GHC.TypeLits as GHC
@@ -81,6 +89,8 @@
     SBP :: SBinPI b => SBin ('BP b)
   deriving (Typeable)
 
+deriving instance Show (SBin b)
+
 -------------------------------------------------------------------------------
 -- Implicits
 -------------------------------------------------------------------------------
@@ -168,6 +178,16 @@
             return Refl
     testEquality _   _   = Nothing
 
+-- | @since 0.1.2
+type family EqBin (n :: Bin) (m :: Bin) where
+    EqBin 'BZ     'BZ     = 'True
+    EqBin ('BP n) ('BP m) = BP.EqBinP n m
+    EqBin n       m       = 'False
+
+#if !MIN_VERSION_base(4,11,0)
+type instance n == m = EqBin n m
+#endif
+
 -------------------------------------------------------------------------------
 -- Induction
 -------------------------------------------------------------------------------
@@ -197,7 +217,7 @@
 -- | Convert to GHC 'GHC.Nat'.
 --
 -- >>> :kind! ToGHC Bin5
--- ToGHC Bin5 :: GHC.Nat
+-- ToGHC Bin5 :: GHC.Nat...
 -- = 5
 --
 type family ToGHC (b :: Bin) :: GHC.Nat where
@@ -266,13 +286,14 @@
 
 -- | Multiply by two.
 --
--- >>> :kind! Mult2 Bin0
--- Mult2 Bin0 :: Bin
--- = 'BZ
+-- >>> :kind! Mult2 Bin0 == Bin0
+-- Mult2 Bin0 == Bin0 :: Bool
+-- = 'True
 --
--- >>> :kind! Mult2 Bin7
--- Mult2 Bin7 :: Bin
--- = 'BP ('B0 ('B1 BinP3))
+-- >>> :kind! Mult2 Bin3 == Bin6
+-- Mult2 Bin3 == Bin6 :: Bool
+-- = 'True
+--
 type family Mult2 (b :: Bin) :: Bin where
     Mult2 'BZ     = 'BZ
     Mult2 ('BP n) = 'BP ('B0 n)
@@ -283,9 +304,10 @@
 -- Mult2Plus1 Bin0 :: BinP
 -- = 'BE
 --
--- >>> :kind! Mult2Plus1 Bin5
--- Mult2Plus1 Bin5 :: BinP
--- = 'B1 ('B1 BinP2)
+-- >>> :kind! Mult2Plus1 Bin4 == BinP9
+-- Mult2Plus1 Bin4 == BinP9 :: Bool
+-- = 'True
+--
 type family Mult2Plus1 (b :: Bin) :: BinP where
     Mult2Plus1 'BZ     = 'BE
     Mult2Plus1 ('BP n) = ('B1 n)
@@ -331,17 +353,17 @@
 -- Pred BP.BinP1 :: Bin
 -- = 'BZ
 --
--- >>> :kind! Pred BP.BinP5
--- Pred BP.BinP5 :: Bin
--- = 'BP ('B0 ('B0 BP.BinP1))
+-- >>> :kind! Pred BP.BinP5 == Bin4
+-- Pred BP.BinP5 == Bin4 :: Bool
+-- = 'True
 --
--- >>> :kind! Pred BP.BinP8
--- Pred BP.BinP8 :: Bin
--- = 'BP ('B1 ('B1 'BE))
+-- >>> :kind! Pred BP.BinP8 == Bin7
+-- Pred BP.BinP8 == Bin7 :: Bool
+-- = 'True
 --
--- >>> :kind! Pred BP.BinP6
--- Pred BP.BinP6 :: Bin
--- = 'BP ('B1 ('B0 'BE))
+-- >>> :kind! Pred BP.BinP6 == Bin5
+-- Pred BP.BinP6 == Bin5 :: Bool
+-- = 'True
 --
 type family Pred (b :: BinP) :: Bin where
     Pred 'BE     = 'BZ
@@ -359,18 +381,47 @@
 
 -- | Addition.
 --
--- >>> :kind! Plus Bin7 Bin7
--- Plus Bin7 Bin7 :: Bin
--- = 'BP ('B0 ('B1 ('B1 'BE)))
+-- >>> :kind! Plus Bin3 Bin3 == Bin6
+-- Plus Bin3 Bin3 == Bin6 :: Bool
+-- = 'True
 --
--- >>> :kind! Mult2 Bin7
--- Mult2 Bin7 :: Bin
--- = 'BP ('B0 ('B1 BinP3))
+-- >>> :kind! Mult2 Bin3 == Bin6
+-- Mult2 Bin3 == Bin6 :: Bool
+-- = 'True
 --
 type family Plus (a :: Bin) (b :: Bin) :: Bin where
     Plus 'BZ     b       = b
     Plus a       'BZ     = a
     Plus ('BP a) ('BP b) = 'BP (BP.Plus a b)
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance SBinI b => Boring (SBin b) where
+    boring = sbin
+
+-------------------------------------------------------------------------------
+-- some
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance GShow SBin where
+    gshowsPrec = showsPrec
+
+-- | @since 0.1.2
+instance NFData (SBin n) where
+    rnf SBZ = ()
+    rnf SBP = ()
+
+-- | @since 0.1.2
+instance GNFData SBin where
+    grnf = rnf
+
+-- | @since 0.1.2
+instance GEq SBin where
+    geq = testEquality
 
 -------------------------------------------------------------------------------
 --- Aliases of Bin
diff --git a/src/Data/Type/BinP.hs b/src/Data/Type/BinP.hs
--- a/src/Data/Type/BinP.hs
+++ b/src/Data/Type/BinP.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE KindSignatures       #-}
 {-# LANGUAGE RankNTypes           #-}
 {-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -28,6 +29,7 @@
     reflectToNum,
     -- * Type equality
     eqBinP,
+    EqBinP,
     -- * Induction
     induction,
     -- * Arithmetic
@@ -45,11 +47,16 @@
     BinP1, BinP2, BinP3, BinP4, BinP5, BinP6, BinP7, BinP8, BinP9,
     ) where
 
-import Data.BinP       (BinP (..))
-import Data.Nat        (Nat (..))
-import Data.Proxy      (Proxy (..))
-import Data.Typeable   (Typeable)
-import Numeric.Natural (Natural)
+import Control.DeepSeq   (NFData (..))
+import Data.BinP         (BinP (..))
+import Data.Boring       (Boring (..))
+import Data.GADT.Compare (GEq (..))
+import Data.GADT.DeepSeq (GNFData (..))
+import Data.GADT.Show    (GShow (..))
+import Data.Nat          (Nat (..))
+import Data.Proxy        (Proxy (..))
+import Data.Typeable     (Typeable)
+import Numeric.Natural   (Natural)
 
 import qualified Data.Type.Nat as N
 import qualified GHC.TypeLits  as GHC
@@ -71,15 +78,17 @@
     SB1 :: SBinPI b => SBinP ('B1 b)
   deriving (Typeable)
 
+deriving instance Show (SBinP b)
+
 -------------------------------------------------------------------------------
 -- Implicits
 -------------------------------------------------------------------------------
 
 -- | Let constraint solver construct 'SBinP'.
 class                SBinPI (b :: BinP) where sbinp :: SBinP b
-instance             SBinPI 'BE          where sbinp = SBE
-instance SBinPI b => SBinPI ('B0 b)      where sbinp = SB0
-instance SBinPI b => SBinPI ('B1 b)      where sbinp = SB1
+instance             SBinPI 'BE         where sbinp = SBE
+instance SBinPI b => SBinPI ('B0 b)     where sbinp = SB0
+instance SBinPI b => SBinPI ('B1 b)     where sbinp = SB1
 
 -------------------------------------------------------------------------------
 -- Conversions
@@ -146,6 +155,17 @@
 
     testEquality _ _ = Nothing
 
+-- | @since 0.1.2
+type family EqBinP (n :: BinP) (m :: BinP) where
+    EqBinP 'BE 'BE         = 'True
+    EqBinP ('B0 n) ('B0 m) = EqBinP n m
+    EqBinP ('B1 n) ('B1 m) = EqBinP n m
+    EqBinP n       m       = 'False
+
+#if !MIN_VERSION_base(4,11,0)
+type instance n == m = EqBinP n m
+#endif
+
 -------------------------------------------------------------------------------
 -- Convert to GHC Nat
 -------------------------------------------------------------------------------
@@ -249,6 +269,36 @@
         SBE -> e
         SB0 -> o go
         SB1 -> i go
+
+-------------------------------------------------------------------------------
+-- Boring
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance SBinPI b => Boring (SBinP b) where
+    boring = sbinp
+
+-------------------------------------------------------------------------------
+-- some
+-------------------------------------------------------------------------------
+
+-- | @since 0.1.2
+instance GShow SBinP where
+    gshowsPrec = showsPrec
+
+-- | @since 0.1.2
+instance NFData (SBinP n) where
+    rnf SBE = ()
+    rnf SB0 = ()
+    rnf SB1 = ()
+
+-- | @since 0.1.2
+instance GNFData SBinP where
+    grnf = rnf
+
+-- | @since 0.1.2
+instance GEq SBinP where
+    geq = testEquality
 
 -------------------------------------------------------------------------------
 -- Aliases of BinP
diff --git a/src/TrustworthyCompat.hs b/src/TrustworthyCompat.hs
--- a/src/TrustworthyCompat.hs
+++ b/src/TrustworthyCompat.hs
@@ -1,9 +1,11 @@
-{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE Trustworthy        #-}
 module TrustworthyCompat (
     (:~:) (..),
     TestEquality (..),
     coerce,
+    type (==),
 ) where
 
 import Data.Coerce        (coerce)
-import Data.Type.Equality (TestEquality (..), (:~:) (..))
+import Data.Type.Equality (TestEquality (..), type (==), (:~:) (..))