    {-# LANGUAGE DataKinds           #-}
    {-# LANGUAGE EmptyCase           #-}
    {-# LANGUAGE FlexibleContexts    #-}
    {-# LANGUAGE GADTs               #-}
    {-# LANGUAGE PolyKinds           #-}
    {-# LANGUAGE RankNTypes          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeOperators       #-}
    {-# OPTIONS_GHC -Wno-redundant-constraints #-}
    -- | Additions to "Data.Type.Bool".
    module Data.Singletons.Bool (
        SBool(..),
        SBoolI(..),
        fromSBool,
        withSomeSBool,
        reflectBool,
        reifyBool,
        -- * Data.Type.Dec
        -- | 'discreteBool' is available with @base >= 4.7@ (GHC-7.8)
        discreteBool,
        -- * Data.Type.Bool and .Equality
        -- | These are only defined with @base >= 4.7@
        sboolAnd, sboolOr, sboolNot,
        eqToRefl, eqCast, sboolEqRefl,
        trivialRefl,
        ) where

    import Control.DeepSeq    (NFData (..))
    import Data.Boring        (Boring (..))
    import Data.GADT.Compare  (GCompare (..), GEq (..), GOrdering (..))
    import Data.GADT.DeepSeq  (GNFData (..))
    import Data.GADT.Show     (GRead (..), GShow (..))
    import Data.Proxy         (Proxy (..))
    import Data.Type.Bool
    import Data.Type.Dec      (Dec (..))
    import Data.Type.Equality
    import Unsafe.Coerce      (unsafeCoerce)

    import Data.EqP  (EqP (..))
    import Data.OrdP (OrdP (..))

    import qualified Data.Some.Church as Church

    -- $setup
    -- >>> :set -XDataKinds -XTypeOperators
    -- >>> import Data.Proxy (Proxy (..))
    -- >>> import Data.Type.Dec
    -- >>> import Data.Some
    -- >>> import Data.GADT.Compare
    -- >>> import Data.GADT.Show
    -- >>> import Data.Type.Equality

    data SBool (b :: Bool) where
        STrue  :: SBool 'True
        SFalse :: SBool 'False

    class    SBoolI (b :: Bool) where sbool :: SBool b
    instance SBoolI 'True       where sbool :: SBool 'True
    sbool = SBool 'True
    STrue
    instance SBoolI 'False      where sbool :: SBool 'False
    sbool = SBool 'False
    SFalse

    -- | @since 0.1.5
    instance Show (SBool b) where
        showsPrec :: Int -> SBool b -> ShowS
    showsPrec Int
    _ SBool b
    STrue  = String -> ShowS
    showString String
    "STrue"
        showsPrec Int
    _ SBool b
    SFalse = String -> ShowS
    showString String
    "SFalse"

    -- | @since 0.1.5
    instance Eq (SBool b) where
        SBool b
    _ == :: SBool b -> SBool b -> Bool
    == SBool b
    _ = Bool
    True

    -- | @since 0.1.5
    instance Ord (SBool b) where
        compare :: SBool b -> SBool b -> Ordering
    compare SBool b
    _ SBool b
    _ = Ordering
    EQ

    -- | @since 0.1.6
    instance NFData (SBool b) where
        rnf :: SBool b -> ()
    rnf SBool b
    STrue  = ()
        rnf SBool b
    SFalse = ()

    -------------------------------------------------------------------------------
    -- conversion to and from explicit SBool values
    -------------------------------------------------------------------------------

    -- | Convert an 'SBool' to the corresponding 'Bool'.
    --
    -- @since 0.1.4
    fromSBool :: SBool b -> Bool
    fromSBool :: forall (b :: Bool). SBool b -> Bool
    fromSBool SBool b
    STrue  = Bool
    True
    fromSBool SBool b
    SFalse = Bool
    False

    -- | Convert a normal 'Bool' to an 'SBool', passing it into a continuation.
    --
    -- >>> withSomeSBool True fromSBool
    -- True
    --
    -- @since 0.1.4
    withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r
    withSomeSBool :: forall r. Bool -> (forall (b :: Bool). SBool b -> r) -> r
    withSomeSBool Bool
    True  forall (b :: Bool). SBool b -> r
    f = SBool 'True -> r
    forall (b :: Bool). SBool b -> r
    f SBool 'True
    STrue
    withSomeSBool Bool
    False forall (b :: Bool). SBool b -> r
    f = SBool 'False -> r
    forall (b :: Bool). SBool b -> r
    f SBool 'False
    SFalse

    -------------------------------------------------------------------------------
    -- reify & reflect
    -------------------------------------------------------------------------------

    -- | Reify 'Bool' to type-level.
    --
    -- >>> reifyBool True reflectBool
    -- True
    --
    reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r
    reifyBool :: forall r.
    Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r
    reifyBool Bool
    True  forall (b :: Bool). SBoolI b => Proxy b -> r
    f = Proxy 'True -> r
    forall (b :: Bool). SBoolI b => Proxy b -> r
    f (Proxy 'True
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy 'True)
    reifyBool Bool
    False forall (b :: Bool). SBoolI b => Proxy b -> r
    f = Proxy 'False -> r
    forall (b :: Bool). SBoolI b => Proxy b -> r
    f (Proxy 'False
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy 'False)

    -- | Reflect to term-level.
    --
    -- >>> reflectBool (Proxy :: Proxy 'True)
    -- True
    reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool
    reflectBool :: forall (b :: Bool) (proxy :: Bool -> *).
    SBoolI b =>
    proxy b -> Bool
    reflectBool proxy b
    _ = SBool b -> Bool
    forall (b :: Bool). SBool b -> Bool
    fromSBool (SBool b
    forall (b :: Bool). SBoolI b => SBool b
    sbool :: SBool b)

    -------------------------------------------------------------------------------
    -- Boring
    -------------------------------------------------------------------------------

    -- | @since 0.1.6
    instance SBoolI b => Boring (SBool b) where
        boring :: SBool b
    boring = SBool b
    forall (b :: Bool). SBoolI b => SBool b
    sbool

    -------------------------------------------------------------------------------
    -- Data.GADT (some)
    -------------------------------------------------------------------------------

    -- |
    --
    -- >>> geq STrue STrue
    -- Just Refl
    --
    -- >>> geq STrue SFalse
    -- Nothing
    --
    -- @since 0.1.6
    instance GEq SBool where
        geq :: forall (a :: Bool) (b :: Bool).
    SBool a -> SBool b -> Maybe (a :~: b)
    geq SBool a
    STrue  SBool b
    STrue  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
        geq SBool a
    SFalse SBool b
    SFalse = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
        geq SBool a
    _      SBool b
    _      = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    -- |
    --
    -- @since 0.1.6
    instance GCompare SBool where
        gcompare :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> GOrdering a b
    gcompare SBool a
    SFalse SBool b
    SFalse = GOrdering a a
    GOrdering a b
    forall {k} (a :: k). GOrdering a a
    GEQ
        gcompare SBool a
    SFalse SBool b
    STrue  = GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
        gcompare SBool a
    STrue  SBool b
    SFalse = GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT
        gcompare SBool a
    STrue  SBool b
    STrue  = GOrdering a a
    GOrdering a b
    forall {k} (a :: k). GOrdering a a
    GEQ

    -- | @since 0.1.6
    instance GNFData SBool where
        grnf :: forall (b :: Bool). SBool b -> ()
    grnf SBool a
    STrue  = ()
        grnf SBool a
    SFalse = ()

    -- |
    --
    -- >>> showsPrec 0 STrue ""
    -- "STrue"
    --
    -- @since 0.1.6
    instance GShow SBool where
        gshowsPrec :: forall (b :: Bool). Int -> SBool b -> ShowS
    gshowsPrec = Int -> SBool a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec

    -- |
    --
    -- >>> readsPrec 0 "Some STrue" :: [(Some SBool, String)]
    -- [(Some STrue,"")]
    --
    -- >>> readsPrec 0 "Some SFalse" :: [(Some SBool, String)]
    -- [(Some SFalse,"")]
    --
    -- >>> readsPrec 0 "Some Else" :: [(Some SBool, String)]
    -- []
    --
    -- @since 0.1.6
    instance GRead SBool where
        greadsPrec :: Int -> GReadS SBool
    greadsPrec Int
    _ String
    s =
            [ (SBool 'True -> Some SBool
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    Church.mkSome SBool 'True
    STrue, String
    t)
            | (String
    "STrue", String
    t) <- ReadS String
    lex String
    s
            ]
            [(Some SBool, String)]
    -> [(Some SBool, String)] -> [(Some SBool, String)]
    forall a. [a] -> [a] -> [a]
    ++
            [ (SBool 'False -> Some SBool
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    Church.mkSome SBool 'False
    SFalse, String
    t)
            | (String
    "SFalse", String
    t) <- ReadS String
    lex String
    s
            ]

    -- | @since 0.1.7
    instance EqP SBool where
        eqp :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Bool
    eqp SBool a
    STrue  SBool b
    STrue  = Bool
    True
        eqp SBool a
    SFalse SBool b
    SFalse = Bool
    True
        eqp SBool a
    _      SBool b
    _      = Bool
    False

    -- | @since 0.1.7
    instance OrdP SBool where
        comparep :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Ordering
    comparep SBool a
    STrue  SBool b
    STrue  = Ordering
    EQ
        comparep SBool a
    SFalse SBool b
    SFalse = Ordering
    EQ
        comparep SBool a
    STrue  SBool b
    SFalse = Ordering
    GT
        comparep SBool a
    SFalse SBool b
    STrue  = Ordering
    LT

    -------------------------------------------------------------------------------
    -- Discrete
    -------------------------------------------------------------------------------

    -- | Decidable equality.
    --
    -- >>> decShow (discreteBool :: Dec ('True :~: 'True))
    -- "Yes Refl"
    --
    -- @since 0.1.5
    discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b)
    discreteBool :: forall (a :: Bool) (b :: Bool).
    (SBoolI a, SBoolI b) =>
    Dec (a :~: b)
    discreteBool = case (SBool a
    forall (b :: Bool). SBoolI b => SBool b
    sbool :: SBool a, SBool b
    forall (b :: Bool). SBoolI b => SBool b
    sbool :: SBool b) of
        (SBool a
    STrue,  SBool b
    STrue)  -> (a :~: b) -> Dec (a :~: b)
    forall a. a -> Dec a
    Yes a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
        (SBool a
    STrue,  SBool b
    SFalse) -> Neg (a :~: b) -> Dec (a :~: b)
    forall a. Neg a -> Dec a
    No (Neg (a :~: b) -> Dec (a :~: b)) -> Neg (a :~: b) -> Dec (a :~: b)
    forall a b. (a -> b) -> a -> b
    $ \a :~: b
    p  -> case a :~: b
    p of {}
        (SBool a
    SFalse, SBool b
    STrue)  -> Neg (a :~: b) -> Dec (a :~: b)
    forall a. Neg a -> Dec a
    No (Neg (a :~: b) -> Dec (a :~: b)) -> Neg (a :~: b) -> Dec (a :~: b)
    forall a b. (a -> b) -> a -> b
    $ \a :~: b
    p  -> case a :~: b
    p of {}
        (SBool a
    SFalse, SBool b
    SFalse) -> (a :~: b) -> Dec (a :~: b)
    forall a. a -> Dec a
    Yes a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl

    -------------------------------------------------------------------------------
    -- Witnesses
    -------------------------------------------------------------------------------

    -- | >>> sboolAnd STrue SFalse
    -- SFalse
    sboolAnd :: SBool a -> SBool b -> SBool (a && b)
    sboolAnd :: forall (a :: Bool) (b :: Bool).
    SBool a -> SBool b -> SBool (a && b)
    sboolAnd SBool a
    SFalse SBool b
    _ = SBool 'False
    SBool (a && b)
    SFalse
    sboolAnd SBool a
    STrue  SBool b
    b = SBool b
    SBool (a && b)
    b

    sboolOr :: SBool a -> SBool b -> SBool (a || b)
    sboolOr :: forall (a :: Bool) (b :: Bool).
    SBool a -> SBool b -> SBool (a || b)
    sboolOr SBool a
    STrue  SBool b
    _ = SBool 'True
    SBool (a || b)
    STrue
    sboolOr SBool a
    SFalse SBool b
    b = SBool b
    SBool (a || b)
    b

    sboolNot :: SBool a -> SBool (Not a)
    sboolNot :: forall (a :: Bool). SBool a -> SBool (Not a)
    sboolNot SBool a
    STrue  = SBool 'False
    SBool (Not a)
    SFalse
    sboolNot SBool a
    SFalse = SBool 'True
    SBool (Not a)
    STrue

    -- | @since 0.1.1.0
    eqToRefl :: (a == b) ~ 'True => a :~: b
    eqToRefl :: forall {k} (a :: k) (b :: k). ((a == b) ~ 'True) => a :~: b
    eqToRefl = (() :~: ()) -> a :~: b
    forall a b. a -> b
    unsafeCoerce () :~: ()
    trivialRefl

    -- | @since 0.1.1.0
    eqCast :: (a == b) ~ 'True => a -> b
    eqCast :: forall a b. ((a == b) ~ 'True) => a -> b
    eqCast = a -> b
    forall a b. a -> b
    unsafeCoerce

    -- | @since 0.1.1.0
    trivialRefl :: () :~: ()
    trivialRefl :: () :~: ()
    trivialRefl = () :~: ()
    forall {k} (a :: k). a :~: a
    Refl

    -- | Useful combination of 'sbool' and 'eqToRefl'
    --
    -- @since 0.1.2.0
    sboolEqRefl :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
    sboolEqRefl :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
    sboolEqRefl = case SBool (a == b)
    forall (b :: Bool). SBoolI b => SBool b
    sbool :: SBool (a == b) of
        SBool (a == b)
    STrue  -> (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: b
    forall {k} (a :: k) (b :: k). ((a == b) ~ 'True) => a :~: b
    eqToRefl
        SBool (a == b)
    SFalse -> Maybe (a :~: b)
    forall a. Maybe a
    Nothing