    {-# LANGUAGE TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators,
                 GADTs, ScopedTypeVariables, DeriveDataTypeable, UndecidableInstances,
                 DataKinds, PolyKinds #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Prelude.Bool
    -- Copyright   :  (C) 2013-2014 Richard Eisenberg, Jan Stolarek
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines functions and datatypes relating to the singleton for 'Bool',
    -- including a singletons version of all the definitions in @Data.Bool@.
    --
    -- Because many of these definitions are produced by Template Haskell,
    -- it is not possible to create proper Haddock documentation. Please look
    -- up the corresponding operation in @Data.Bool@. Also, please excuse
    -- the apparent repeated variable names. This is due to an interaction
    -- between Template Haskell and Haddock.
    --
    ----------------------------------------------------------------------------

    module Data.Singletons.Prelude.Bool (
      -- * The 'Bool' singleton
      Sing, SBool(..),

      -- * Conditionals
      If, sIf,

      -- * Singletons from @Data.Bool@
      Not, sNot, type (&&), type (||), (%&&), (%||),

      -- | The following are derived from the function 'bool' in @Data.Bool@. The extra
      -- underscore is to avoid name clashes with the type 'Bool'.
      bool_, Bool_, sBool_, Otherwise, sOtherwise,

      -- * Defunctionalization symbols
      TrueSym0, FalseSym0,

      NotSym0, NotSym1,
      type (&&@#@$), type (&&@#@$$), type (&&@#@$$$),
      type (||@#@$), type (||@#@$$), type (||@#@$$$),
      Bool_Sym0, Bool_Sym1, Bool_Sym2, Bool_Sym3,
      OtherwiseSym0
      ) where

    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Instances
    import Data.Singletons.Promote
    import Data.Singletons.Single
    import Data.Type.Bool ( If, type (&&), type (||), Not )

    $(singletons [d|
      bool_ :: a -> a -> Bool -> a
      bool_ fls _tru False = fls
      bool_ _fls tru True  = tru
     |])

    $(singletonsOnly [d|
      otherwise               :: Bool
      otherwise               =  True
      |])

    -- | Conjunction of singletons
    (%&&) :: Sing a -> Sing b -> Sing (a && b)
    SFalse %&& :: Sing a -> Sing b -> Sing (a && b)
    %&& _ = Sing (a && b)
    SBool 'False
    SFalse
    STrue  %&& a :: Sing b
    a = Sing b
    Sing (a && b)
    a
    infixr 3 %&&
    $(genDefunSymbols [''(&&)])
    instance SingI (&&@#@$) where
      sing :: Sing (&&@#@$)
    sing = SingFunction2 (&&@#@$) -> Sing (&&@#@$)
    forall k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 (&&@#@$)
    forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
    (%&&)
    instance SingI x => SingI ((&&@#@$$) x) where
      sing :: Sing ((&&@#@$$) x)
    sing = SingFunction1 ((&&@#@$$) x) -> Sing ((&&@#@$$) x)
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 (SingI x => Sing x
    forall k (a :: k). SingI a => Sing a
    sing @x Sing x -> Sing t -> Sing (x && t)
    forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
    %&&)

    -- | Disjunction of singletons
    (%||) :: Sing a -> Sing b -> Sing (a || b)
    SFalse %|| :: Sing a -> Sing b -> Sing (a || b)
    %|| a :: Sing b
    a = Sing b
    Sing (a || b)
    a
    STrue  %|| _ = Sing (a || b)
    SBool 'True
    STrue
    infixr 2 %||
    $(genDefunSymbols [''(||)])
    instance SingI (||@#@$) where
      sing :: Sing (||@#@$)
    sing = SingFunction2 (||@#@$) -> Sing (||@#@$)
    forall k2 k3 k (f :: k2 ~> (k3 ~> k)). SingFunction2 f -> Sing f
    singFun2 SingFunction2 (||@#@$)
    forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b)
    (%||)
    instance SingI x => SingI ((||@#@$$) x) where
      sing :: Sing ((||@#@$$) x)
    sing = SingFunction1 ((||@#@$$) x) -> Sing ((||@#@$$) x)
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 (SingI x => Sing x
    forall k (a :: k). SingI a => Sing a
    sing @x Sing x -> Sing t -> Sing (x || t)
    forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b)
    %||)

    -- | Negation of a singleton
    sNot :: Sing a -> Sing (Not a)
    sNot :: Sing a -> Sing (Not a)
    sNot SFalse = Sing (Not a)
    SBool 'True
    STrue
    sNot STrue  = Sing (Not a)
    SBool 'False
    SFalse
    $(genDefunSymbols [''Not])
    instance SingI NotSym0 where
      sing :: Sing NotSym0
    sing = SingFunction1 NotSym0 -> Sing NotSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 SingFunction1 NotSym0
    forall (a :: Bool). Sing a -> Sing (Not a)
    sNot

    -- | Conditional over singletons
    sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
    sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
    sIf STrue b :: Sing b
    b _ = Sing b
    Sing (If a b c)
    b
    sIf SFalse _ c :: Sing c
    c = Sing c
    Sing (If a b c)
    c