{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE Safe                 #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Binary natural numbers. @DataKinds@ stuff.
module Data.Type.Bin (
    -- * Singleton
    SBin (..), SBinP (..),
    sbinToBin, BP.sbinpToBinP,
    sbinToNatural, BP.sbinpToNatural,
    -- * Implicit
    SBinI (..), SBinPI (..),
    withSBin, BP.withSBinP,
    reify,
    reflect,
    reflectToNum,
    -- * Type equality
    eqBin,
    EqBin,
    -- * Induction
    induction,
    -- * Arithmetic
    -- ** Successor
    Succ, Succ', Succ'',
    withSucc,
    -- ** Predecessor
    Pred,
    -- ** Addition
    Plus,
    -- ** Extras
    Mult2, Mult2Plus1,
    -- * Conversions
    -- ** To GHC Nat
    ToGHC, FromGHC,
    -- ** To fin Nat
    ToNat, FromNat,
    -- * Aliases
    Bin0, Bin1, Bin2, Bin3, Bin4, Bin5, Bin6, Bin7, Bin8, Bin9,
    ) where

import Control.DeepSeq   (NFData (..))
import Data.Bin          (Bin (..), BinP (..))
import Data.Boring       (Boring (..))
import Data.EqP          (EqP (..))
import Data.GADT.Compare (GEq (..), defaultEq)
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
import qualified GHC.TypeLits   as GHC

import TrustworthyCompat

-- $setup
-- >>> :set -XDataKinds -XExplicitNamespaces -XTypeOperators
-- >>> import Data.Bin
-- >>> 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

-------------------------------------------------------------------------------
-- Singletons
-------------------------------------------------------------------------------

-- | Singleton of 'Bin'.
data SBin (b :: Bin) where
    SBZ :: SBin 'BZ
    SBP :: SBinPI b => SBin ('BP b)
  deriving (Typeable)

deriving instance Show (SBin b)

-------------------------------------------------------------------------------
-- Implicits
-------------------------------------------------------------------------------

-- | Let constraint solver construct 'SBin'.
class                SBinI (b :: Bin) where sbin :: SBin b
instance             SBinI 'BZ        where sbin :: SBin 'BZ
sbin = SBin 'BZ
SBZ
instance SBinPI b => SBinI ('BP b )   where sbin :: SBin ('BP b)
sbin = SBin ('BP b)
forall (b :: BinP). SBinPI b => SBin ('BP b)
SBP

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Construct 'SBinI' dictionary from 'SBin'.
withSBin :: SBin b -> (SBinI b => r) -> r
withSBin :: forall (b :: Bin) r. SBin b -> (SBinI b => r) -> r
withSBin SBin b
SBZ SBinI b => r
k = r
SBinI b => r
k
withSBin SBin b
SBP SBinI b => r
k = r
SBinI b => r
k

-- | Reify 'Bin'
--
-- >>> reify bin3 reflect
-- 3
--
reify :: forall r. Bin -> (forall b. SBinI b => Proxy b -> r) -> r
reify :: forall r.
Bin -> (forall (b :: Bin). SBinI b => Proxy @Bin b -> r) -> r
reify Bin
BZ     forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k = Proxy @Bin 'BZ -> r
forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k (Proxy @Bin 'BZ
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy 'BZ)
reify (BP BinP
b) forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k = BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
forall r.
BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
BP.reify BinP
b (\(Proxy @BinP b
_ :: Proxy b) -> Proxy @Bin ('BP b) -> r
forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k (Proxy @Bin ('BP b)
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy ('BP b)))

-- | Reflect type-level 'Bin' to the term level.
reflect :: forall b proxy. SBinI b => proxy b -> Bin
reflect :: forall (b :: Bin) (proxy :: Bin -> *). SBinI b => proxy b -> Bin
reflect proxy b
p = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> Bin
BZ
    SBin b
SBP -> BinP -> Bin
BP (proxy ('BP b) -> BinP
forall (bn :: BinP). SBinPI bn => proxy ('BP bn) -> BinP
aux proxy b
proxy ('BP b)
p)
  where
    aux :: forall bn. SBinPI bn => proxy ('BP bn) -> BinP
    aux :: forall (bn :: BinP). SBinPI bn => proxy ('BP bn) -> BinP
aux proxy ('BP bn)
_ = Proxy @BinP bn -> BinP
forall (b :: BinP) (proxy :: BinP -> *).
SBinPI b =>
proxy b -> BinP
BP.reflect (Proxy @BinP bn
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy bn)

-- | Reflect type-level 'Bin' to the term level 'Num'.
reflectToNum :: forall b proxy a. (SBinI b, Num a) => proxy b -> a
reflectToNum :: forall (b :: Bin) (proxy :: Bin -> *) a.
(SBinI b, Num a) =>
proxy b -> a
reflectToNum proxy b
p = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> a
0
    SBin b
SBP -> proxy ('BP b) -> a
forall (bn :: BinP). SBinPI bn => proxy ('BP bn) -> a
aux proxy b
proxy ('BP b)
p
  where
    aux :: forall bn. SBinPI bn => proxy ('BP bn) -> a
    aux :: forall (bn :: BinP). SBinPI bn => proxy ('BP bn) -> a
aux proxy ('BP bn)
_ = Proxy @BinP bn -> a
forall (b :: BinP) (proxy :: BinP -> *) a.
(SBinPI b, Num a) =>
proxy b -> a
BP.reflectToNum (Proxy @BinP bn
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy bn)

-- | Convert 'SBin' to 'Bin'.
sbinToBin :: forall n. SBin n -> Bin
sbinToBin :: forall (n :: Bin). SBin n -> Bin
sbinToBin SBin n
SBZ   = Bin
BZ
sbinToBin s :: SBin n
s@SBin n
SBP = SBin ('BP b) -> Bin
forall (m :: BinP). SBinPI m => SBin ('BP m) -> Bin
aux SBin n
SBin ('BP b)
s where
    aux :: forall m. SBinPI m => SBin ('BP m) -> Bin
    aux :: forall (m :: BinP). SBinPI m => SBin ('BP m) -> Bin
aux SBin ('BP m)
_ = BinP -> Bin
BP (SBinP m -> BinP
forall (n :: BinP). SBinP n -> BinP
BP.sbinpToBinP (SBinP m
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP m))

-- | Convert 'SBin' to 'Natural'.
--
-- >>> sbinToNatural (sbin :: SBin Bin9)
-- 9
--
sbinToNatural :: forall n. SBin n -> Natural
sbinToNatural :: forall (n :: Bin). SBin n -> Natural
sbinToNatural SBin n
SBZ = Natural
0
sbinToNatural s :: SBin n
s@SBin n
SBP = SBin ('BP b) -> Natural
forall (m :: BinP). SBinPI m => SBin ('BP m) -> Natural
aux SBin n
SBin ('BP b)
s where
    aux :: forall m. SBinPI m => SBin ('BP m) -> Natural
    aux :: forall (m :: BinP). SBinPI m => SBin ('BP m) -> Natural
aux SBin ('BP m)
_ = SBinP m -> Natural
forall (n :: BinP). SBinP n -> Natural
BP.sbinpToNatural (SBinP m
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP m)

-------------------------------------------------------------------------------
-- Equality
-------------------------------------------------------------------------------

eqBin :: forall a b. (SBinI a, SBinI b) => Maybe (a :~: b)
eqBin :: forall (a :: Bin) (b :: Bin).
(SBinI a, SBinI b) =>
Maybe ((:~:) @Bin a b)
eqBin = case (SBin a
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin a, SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b) of
    (SBin a
SBZ, SBin b
SBZ) -> (:~:) @Bin a b -> Maybe ((:~:) @Bin a b)
forall a. a -> Maybe a
Just (:~:) @Bin a a
(:~:) @Bin a b
forall {k} (a :: k). (:~:) @k a a
Refl
    (SBin a
SBP, SBin b
SBP) -> Maybe ((:~:) @Bin a b)
Maybe ((:~:) @Bin ('BP b) ('BP b))
forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @Bin ('BP n) ('BP m))
recur where
      recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('BP n :~: 'BP m)
      recur :: forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @Bin ('BP n) ('BP m))
recur = do
          (:~:) @BinP n m
Refl <- Maybe ((:~:) @BinP n m)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
BP.eqBinP :: Maybe (n :~: m)
          (:~:) @Bin ('BP n) ('BP m) -> Maybe ((:~:) @Bin ('BP n) ('BP m))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Bin ('BP n) ('BP n)
(:~:) @Bin ('BP n) ('BP m)
forall {k} (a :: k). (:~:) @k a a
Refl

    (SBin a, SBin b)
_          -> Maybe ((:~:) @Bin a b)
forall a. Maybe a
Nothing

instance TestEquality SBin where
    testEquality :: forall (a :: Bin) (b :: Bin).
SBin a -> SBin b -> Maybe ((:~:) @Bin a b)
testEquality SBin a
SBZ SBin b
SBZ = (:~:) @Bin a b -> Maybe ((:~:) @Bin a b)
forall a. a -> Maybe a
Just (:~:) @Bin a a
(:~:) @Bin a b
forall {k} (a :: k). (:~:) @k a a
Refl
    testEquality SBin a
SBP SBin b
SBP = Maybe ((:~:) @Bin a b)
Maybe ((:~:) @Bin ('BP b) ('BP b))
forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @Bin ('BP n) ('BP m))
recur where
        recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('BP n :~: 'BP m)
        recur :: forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @Bin ('BP n) ('BP m))
recur = do
            (:~:) @BinP n m
Refl <- Maybe ((:~:) @BinP n m)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
BP.eqBinP :: Maybe (n :~: m)
            (:~:) @Bin ('BP n) ('BP m) -> Maybe ((:~:) @Bin ('BP n) ('BP m))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Bin ('BP n) ('BP n)
(:~:) @Bin ('BP n) ('BP m)
forall {k} (a :: k). (:~:) @k a a
Refl
    testEquality SBin a
_   SBin b
_   = Maybe ((:~:) @Bin a b)
forall a. Maybe a
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

-------------------------------------------------------------------------------
-- Induction
-------------------------------------------------------------------------------

-- | Induction on 'Bin'.
induction
    :: forall b f. SBinI b
    => f 'BZ                                                     -- ^ \(P(0)\)
    -> f ('BP 'BE)                                               -- ^ \(P(1)\)
    -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb)))  -- ^ \(\forall b. P(b) \to P(2b)\)
    -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb)))  -- ^ \(\forall b. P(b) \to P(2b + 1)\)
    -> f b
induction :: forall (b :: Bin) (f :: Bin -> *).
SBinI b =>
f 'BZ
-> f ('BP 'BE)
-> (forall (bb :: BinP).
    SBinPI bb =>
    f ('BP bb) -> f ('BP ('B0 bb)))
-> (forall (bb :: BinP).
    SBinPI bb =>
    f ('BP bb) -> f ('BP ('B1 bb)))
-> f b
induction f 'BZ
z f ('BP 'BE)
e forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb))
o forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb))
i = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> f b
f 'BZ
z
    SBin b
SBP -> f b
f ('BP b)
forall (bb :: BinP). SBinPI bb => f ('BP bb)
go
  where
    go :: forall bb. SBinPI bb => f ('BP bb)
    go :: forall (bb :: BinP). SBinPI bb => f ('BP bb)
go = case SBinP bb
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP bb of
        SBinP bb
SBE -> f ('BP bb)
f ('BP 'BE)
e
        SBinP bb
SB0 -> f ('BP b1) -> f ('BP ('B0 b1))
forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb))
o f ('BP b1)
forall (bb :: BinP). SBinPI bb => f ('BP bb)
go
        SBinP bb
SB1 -> f ('BP b1) -> f ('BP ('B1 b1))
forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb))
i f ('BP b1)
forall (bb :: BinP). SBinPI bb => f ('BP bb)
go

-------------------------------------------------------------------------------
-- Conversion to GHC Nat
-------------------------------------------------------------------------------

-- | Convert to GHC 'GHC.Nat'.
--
-- >>> :kind! ToGHC Bin5
-- ToGHC Bin5 :: GHC.Nat...
-- = 5
--
type family ToGHC (b :: Bin) :: GHC.Nat where
    ToGHC 'BZ     = 0
    ToGHC ('BP n) = BP.ToGHC n

-- | Convert from GHC 'GHC.Nat'.
--
-- >>> :kind! FromGHC 7
-- FromGHC 7 :: Bin
-- = 'BP ('B1 ('B1 'BE))
--
type family FromGHC (n :: GHC.Nat) :: Bin where
    FromGHC n = FromGHC' (GhcDivMod2 n)

type family FromGHC' (p :: (GHC.Nat, Bool)) :: Bin where
    FromGHC' '(0, 'False) = 'BZ
    FromGHC' '(0, 'True)  = 'BP 'BE
    FromGHC' '(n, 'False) = Mult2 (FromGHC n)
    FromGHC' '(n, 'True)  = 'BP (Mult2Plus1 (FromGHC n))

-- | >>> :kind! GhcDivMod2 13
-- GhcDivMod2 13 :: (GHC.Nat, Bool)
-- = '(6, 'True)
--
type family GhcDivMod2 (n :: GHC.Nat) :: (GHC.Nat, Bool) where
    GhcDivMod2 0 = '(0, 'False)
    GhcDivMod2 1 = '(0, 'True)
    GhcDivMod2 n = GhcDivMod2' (GhcDivMod2 (n GHC.- 2))

type family GhcDivMod2' (p :: (GHC.Nat, Bool)) :: (GHC.Nat, Bool) where
    GhcDivMod2' '(n, b) = '(1 GHC.+ n, b)

-------------------------------------------------------------------------------
-- Conversion to Nat
-------------------------------------------------------------------------------

-- | Convert to @fin@ 'Nat'.
--
-- >>> :kind! ToNat Bin5
-- ToNat Bin5 :: Nat
-- = 'S ('S ('S ('S ('S 'Z))))
--
type family ToNat (b :: Bin) :: Nat where
    ToNat 'BZ     = 'Z
    ToNat ('BP n) = BP.ToNat n

-- | Convert from @fin@ 'Nat'.
--
-- >>> :kind! FromNat N.Nat5
-- FromNat N.Nat5 :: Bin
-- = 'BP ('B1 ('B0 'BE))
--
type family FromNat (n :: Nat) :: Bin where
    FromNat n = FromNat' (N.DivMod2 n)

type family FromNat' (p :: (Nat, Bool)) :: Bin where
    FromNat' '( 'Z, 'False) = 'BZ
    FromNat' '( 'Z, 'True)  = 'BP 'BE
    FromNat' '( n,  'False) = Mult2 (FromNat n)
    FromNat' '( n,  'True)  = 'BP (Mult2Plus1 (FromNat n))

-------------------------------------------------------------------------------
-- Extras
-------------------------------------------------------------------------------

-- | Multiply by two.
--
-- >>> :kind! Mult2 Bin0 == Bin0
-- Mult2 Bin0 == Bin0 :: Bool
-- = 'True
--
-- >>> :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)

-- | Multiply by two and add one.
--
-- >>> :kind! Mult2Plus1 Bin0
-- Mult2Plus1 Bin0 :: BinP
-- = 'BE
--
-- >>> :kind! Mult2Plus1 Bin4 == BinP9
-- Mult2Plus1 Bin4 == BinP9 :: Bool
-- = 'True
--
type family Mult2Plus1 (b :: Bin) :: BinP where
    Mult2Plus1 'BZ     = 'BE
    Mult2Plus1 ('BP n) = ('B1 n)

-------------------------------------------------------------------------------
-- Arithmetic: Succ
-------------------------------------------------------------------------------

-- | Successor type family.
--
-- >>> :kind! Succ Bin5
-- Succ Bin5 :: Bin
-- = 'BP ('B0 ('B1 'BE))
--
-- @
-- `Succ`   :: 'Bin' -> 'Bin'
-- `Succ'`  :: 'Bin' -> 'BinP'
-- `Succ''` :: 'BinP' -> 'Bin'
-- @
type Succ b = 'BP (Succ' b)

type family Succ' (b :: Bin) :: BinP where
    Succ' 'BZ     = 'BE
    Succ' ('BP b) = BP.Succ b

type Succ'' b = 'BP (BP.Succ b)

withSucc :: forall b r. SBinI b => Proxy b -> (SBinPI (Succ' b) => r) -> r
withSucc :: forall (b :: Bin) r.
SBinI b =>
Proxy @Bin b -> (SBinPI (Succ' b) => r) -> r
withSucc Proxy @Bin b
p SBinPI (Succ' b) => r
k = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> r
SBinPI (Succ' b) => r
k
    SBin b
SBP -> Proxy @Bin ('BP b) -> (SBinPI (Succ b) => r) -> r
forall (b :: BinP) r.
SBinPI b =>
Proxy @Bin ('BP b) -> (SBinPI (Succ b) => r) -> r
withSucc' Proxy @Bin b
Proxy @Bin ('BP b)
p r
SBinPI (Succ b) => r
SBinPI (Succ' b) => r
k

withSucc' :: forall b r. SBinPI b => Proxy ('BP b) -> (SBinPI (BP.Succ b) => r) -> r
withSucc' :: forall (b :: BinP) r.
SBinPI b =>
Proxy @Bin ('BP b) -> (SBinPI (Succ b) => r) -> r
withSucc' Proxy @Bin ('BP b)
_ SBinPI (Succ b) => r
k = Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
BP.withSucc (Proxy @BinP b
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy b) r
SBinPI (Succ b) => r
k

-------------------------------------------------------------------------------
-- Predecessor
-------------------------------------------------------------------------------

-- | Predecessor type family..
--
-- >>> :kind! Pred BP.BinP1
-- Pred BP.BinP1 :: Bin
-- = 'BZ
--
-- >>> :kind! Pred BP.BinP5 == Bin4
-- Pred BP.BinP5 == Bin4 :: Bool
-- = 'True
--
-- >>> :kind! Pred BP.BinP8 == Bin7
-- Pred BP.BinP8 == Bin7 :: Bool
-- = 'True
--
-- >>> :kind! Pred BP.BinP6 == Bin5
-- Pred BP.BinP6 == Bin5 :: Bool
-- = 'True
--
type family Pred (b :: BinP) :: Bin where
    Pred 'BE     = 'BZ
    Pred ('B1 n) = 'BP ('B0 n)
    Pred ('B0 n) = 'BP (Pred' n)

type family Pred' (b :: BinP) :: BinP where
    Pred' 'BE     = 'BE
    Pred' ('B1 m) = 'B1 ('B0 m)
    Pred' ('B0 m) = 'B1 (Pred' m)

-------------------------------------------------------------------------------
-- Arithmetic: Plus
-------------------------------------------------------------------------------

-- | Addition.
--
-- >>> :kind! Plus Bin3 Bin3 == Bin6
-- Plus Bin3 Bin3 == Bin6 :: Bool
-- = 'True
--
-- >>> :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 b
boring = SBin b
forall (b :: Bin). SBinI b => SBin b
sbin

-------------------------------------------------------------------------------
-- some
-------------------------------------------------------------------------------

-- | @since 0.1.3
instance Eq (SBin a) where
    SBin a
_ == :: SBin a -> SBin a -> Bool
== SBin a
_ = Bool
True

-- | @since 0.1.3
instance Ord (SBin a) where
    compare :: SBin a -> SBin a -> Ordering
compare SBin a
_ SBin a
_ = Ordering
EQ

-- | @since 0.1.3
instance EqP SBin where eqp :: forall (a :: Bin) (b :: Bin). SBin a -> SBin b -> Bool
eqp = SBin a -> SBin b -> Bool
forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq @k f =>
f a -> f b -> Bool
defaultEq

-- | @since 0.1.2
instance GShow SBin where
    gshowsPrec :: forall (b :: Bin). Int -> SBin b -> ShowS
gshowsPrec = Int -> SBin a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

-- | @since 0.1.2
instance NFData (SBin n) where
    rnf :: SBin n -> ()
rnf SBin n
SBZ = ()
    rnf SBin n
SBP = ()

-- | @since 0.1.2
instance GNFData SBin where
    grnf :: forall (n :: Bin). SBin n -> ()
grnf = SBin a -> ()
forall a. NFData a => a -> ()
rnf

-- | @since 0.1.2
instance GEq SBin where
    geq :: forall (a :: Bin) (b :: Bin).
SBin a -> SBin b -> Maybe ((:~:) @Bin a b)
geq = SBin a -> SBin b -> Maybe ((:~:) @Bin a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality @k f =>
f a -> f b -> Maybe ((:~:) @k a b)
forall (a :: Bin) (b :: Bin).
SBin a -> SBin b -> Maybe ((:~:) @Bin a b)
testEquality

-------------------------------------------------------------------------------
--- Aliases of Bin
-------------------------------------------------------------------------------

type Bin0 = 'BZ
type Bin1 = 'BP BP.BinP1
type Bin2 = 'BP BP.BinP2
type Bin3 = 'BP BP.BinP3
type Bin4 = 'BP BP.BinP4
type Bin5 = 'BP BP.BinP5
type Bin6 = 'BP BP.BinP6
type Bin7 = 'BP BP.BinP7
type Bin8 = 'BP BP.BinP8
type Bin9 = 'BP BP.BinP9