    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.TypeLits.Internal
    -- Copyright   :  (C) 2014 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines and exports singletons useful for the Nat and Symbol kinds.
    -- This exports the internal, unsafe constructors. Use Data.Singletons.TypeLits
    -- for a safe interface.
    --
    ----------------------------------------------------------------------------

    {-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, FlexibleInstances,
                 UndecidableInstances, ScopedTypeVariables, RankNTypes,
                 GADTs, FlexibleContexts, TypeOperators, ConstraintKinds,
                 TemplateHaskell, TypeApplications #-}
    {-# OPTIONS_GHC -Wno-orphans #-}

    module Data.Singletons.TypeLits.Internal (
      Sing,

      Nat, Symbol,
      SNat(..), SSymbol(..), withKnownNat, withKnownSymbol,
      Error, sError,
      ErrorWithoutStackTrace, sErrorWithoutStackTrace,
      Undefined, sUndefined,
      KnownNat, TN.natVal, KnownSymbol, symbolVal,
      type (^), (%^),
      type (<=?), (%<=?),

      -- * Defunctionalization symbols
      ErrorSym0, ErrorSym1,
      ErrorWithoutStackTraceSym0, ErrorWithoutStackTraceSym1,
      UndefinedSym0,
      type (^@#@$),  type (^@#@$$),  type (^@#@$$$),
      type (<=?@#@$),  type (<=?@#@$$),  type (<=?@#@$$$)
      ) where

    import Data.Singletons.Promote
    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Eq
    import Data.Singletons.Prelude.Ord as O
    import Data.Singletons.Decide
    import Data.Singletons.Prelude.Bool
    import GHC.Stack (HasCallStack)
    import GHC.TypeLits as TL
    import qualified GHC.TypeNats as TN
    import Numeric.Natural (Natural)
    import Unsafe.Coerce

    import qualified Data.Text as T
    import Data.Text ( Text )

    ----------------------------------------------------------------------
    ---- TypeLits singletons ---------------------------------------------
    ----------------------------------------------------------------------

    data SNat (n :: Nat) = KnownNat n => SNat
    type instance Sing = SNat

    instance KnownNat n => SingI n where
      sing :: Sing n
    sing = Sing n
    forall (n :: Nat). KnownNat n => SNat n
    SNat

    instance SingKind Nat where
      type Demote Nat = Natural
      fromSing :: Sing a -> Demote Nat
    fromSing (SNat :: Sing n) = Proxy a -> Natural
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Natural
    TN.natVal (Proxy a
    forall k (t :: k). Proxy t
    Proxy :: Proxy n)
      toSing :: Demote Nat -> SomeSing Nat
    toSing n :: Demote Nat
    n = case Natural -> SomeNat
    TN.someNatVal Natural
    Demote Nat
    n of
                   SomeNat (Proxy n
    _ :: Proxy n) -> Sing n -> SomeSing Nat
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing n
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: Sing n)

    data SSymbol (n :: Symbol) = KnownSymbol n => SSym
    type instance Sing = SSymbol

    instance KnownSymbol n => SingI n where
      sing :: Sing n
    sing = Sing n
    forall (n :: Symbol). KnownSymbol n => SSymbol n
    SSym

    instance SingKind Symbol where
      type Demote Symbol = Text
      fromSing :: Sing a -> Demote Symbol
    fromSing (SSym :: Sing n) = String -> Text
    T.pack (Proxy a -> String
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> String
    symbolVal (Proxy a
    forall k (t :: k). Proxy t
    Proxy :: Proxy n))
      toSing :: Demote Symbol -> SomeSing Symbol
    toSing s :: Demote Symbol
    s = case String -> SomeSymbol
    someSymbolVal (Text -> String
    T.unpack Demote Symbol
    Text
    s) of
                   SomeSymbol (Proxy n
    _ :: Proxy n) -> Sing n -> SomeSing Symbol
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (Sing n
    forall (n :: Symbol). KnownSymbol n => SSymbol n
    SSym :: Sing n)

    -- SDecide instances:
    instance SDecide Nat where
      (SNat :: Sing n) %~ :: Sing a -> Sing b -> Decision (a :~: b)
    %~ (SNat :: Sing m)
        | Just r :: a :~: b
    r <- Proxy a -> Proxy b -> Maybe (a :~: b)
    forall (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    Proxy a -> Proxy b -> Maybe (a :~: b)
    TN.sameNat (Proxy a
    forall k (t :: k). Proxy t
    Proxy :: Proxy n) (Proxy b
    forall k (t :: k). Proxy t
    Proxy :: Proxy m)
        = (a :~: b) -> Decision (a :~: b)
    forall a. a -> Decision a
    Proved a :~: b
    r
        | Bool
    otherwise
        = Refuted (a :~: b) -> Decision (a :~: b)
    forall a. Refuted a -> Decision a
    Disproved (\_ -> String -> Void
    forall a. HasCallStack => String -> a
    error String
    errStr)
        where errStr :: String
    errStr = "Broken Nat singletons"

    instance SDecide Symbol where
      (SSym :: Sing n) %~ :: Sing a -> Sing b -> Decision (a :~: b)
    %~ (SSym :: Sing m)
        | Just r :: a :~: b
    r <- Proxy a -> Proxy b -> Maybe (a :~: b)
    forall (a :: Symbol) (b :: Symbol).
    (KnownSymbol a, KnownSymbol b) =>
    Proxy a -> Proxy b -> Maybe (a :~: b)
    sameSymbol (Proxy a
    forall k (t :: k). Proxy t
    Proxy :: Proxy n) (Proxy b
    forall k (t :: k). Proxy t
    Proxy :: Proxy m)
        = (a :~: b) -> Decision (a :~: b)
    forall a. a -> Decision a
    Proved a :~: b
    r
        | Bool
    otherwise
        = Refuted (a :~: b) -> Decision (a :~: b)
    forall a. Refuted a -> Decision a
    Disproved (\_ -> String -> Void
    forall a. HasCallStack => String -> a
    error String
    errStr)
        where errStr :: String
    errStr = "Broken Symbol singletons"

    -- PEq instances
    instance PEq Nat
    instance PEq Symbol

    -- need SEq instances for TypeLits kinds
    instance SEq Nat where
      (SNat :: Sing n) %== :: Sing a -> Sing b -> Sing (a == b)
    %== (SNat :: Sing m)
        = case Proxy a -> Proxy b -> Maybe (a :~: b)
    forall (a :: Nat) (b :: Nat).
    (KnownNat a, KnownNat b) =>
    Proxy a -> Proxy b -> Maybe (a :~: b)
    sameNat (Proxy a
    forall k (t :: k). Proxy t
    Proxy :: Proxy n) (Proxy b
    forall k (t :: k). Proxy t
    Proxy :: Proxy m) of
            Just Refl -> Sing (a == b)
    SBool 'True
    STrue
            Nothing   -> SBool 'False -> SBool (DefaultEq a b)
    forall a b. a -> b
    unsafeCoerce SBool 'False
    SFalse

    instance SEq Symbol where
      (SSym :: Sing n) %== :: Sing a -> Sing b -> Sing (a == b)
    %== (SSym :: Sing m)
        = case Proxy a -> Proxy b -> Maybe (a :~: b)
    forall (a :: Symbol) (b :: Symbol).
    (KnownSymbol a, KnownSymbol b) =>
    Proxy a -> Proxy b -> Maybe (a :~: b)
    sameSymbol (Proxy a
    forall k (t :: k). Proxy t
    Proxy :: Proxy n) (Proxy b
    forall k (t :: k). Proxy t
    Proxy :: Proxy m) of
            Just Refl -> Sing (a == b)
    SBool 'True
    STrue
            Nothing   -> SBool 'False -> SBool (DefaultEq a b)
    forall a b. a -> b
    unsafeCoerce SBool 'False
    SFalse

    -- POrd instances
    instance POrd Nat where
      type (a :: Nat) `Compare` (b :: Nat) = a `TN.CmpNat` b

    instance POrd Symbol where
      type (a :: Symbol) `Compare` (b :: Symbol) = a `TL.CmpSymbol` b

    -- SOrd instances
    instance SOrd Nat where
      a :: Sing t
    a sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
    `sCompare` b :: Sing t
    b = case Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    a Natural -> Natural -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    b of
                         LT -> SOrdering 'LT -> SOrdering (CmpNat t t)
    forall a b. a -> b
    unsafeCoerce SOrdering 'LT
    SLT
                         EQ -> SOrdering 'EQ -> SOrdering (CmpNat t t)
    forall a b. a -> b
    unsafeCoerce SOrdering 'EQ
    SEQ
                         GT -> SOrdering 'GT -> SOrdering (CmpNat t t)
    forall a b. a -> b
    unsafeCoerce SOrdering 'GT
    SGT

    instance SOrd Symbol where
      a :: Sing t
    a sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)
    `sCompare` b :: Sing t
    b = case Sing t -> Demote Symbol
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    a Text -> Text -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` Sing t -> Demote Symbol
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    b of
                         LT -> SOrdering 'LT -> SOrdering (CmpSymbol t t)
    forall a b. a -> b
    unsafeCoerce SOrdering 'LT
    SLT
                         EQ -> SOrdering 'EQ -> SOrdering (CmpSymbol t t)
    forall a b. a -> b
    unsafeCoerce SOrdering 'EQ
    SEQ
                         GT -> SOrdering 'GT -> SOrdering (CmpSymbol t t)
    forall a b. a -> b
    unsafeCoerce SOrdering 'GT
    SGT

    -- Convenience functions

    -- | Given a singleton for @Nat@, call something requiring a
    -- @KnownNat@ instance.
    withKnownNat :: Sing n -> (KnownNat n => r) -> r
    withKnownNat :: Sing n -> (KnownNat n => r) -> r
    withKnownNat SNat f :: KnownNat n => r
    f = r
    KnownNat n => r
    f

    -- | Given a singleton for @Symbol@, call something requiring
    -- a @KnownSymbol@ instance.
    withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
    withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
    withKnownSymbol SSym f :: KnownSymbol n => r
    f = r
    KnownSymbol n => r
    f

    -- | The promotion of 'error'. This version is more poly-kinded for
    -- easier use.
    type family Error (str :: k0) :: k where {}
    $(genDefunSymbols [''Error])
    instance SingI (ErrorSym0 :: Symbol ~> a) where
      sing :: Sing ErrorSym0
    sing = SingFunction1 ErrorSym0 -> Sing ErrorSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 SingFunction1 ErrorSym0
    forall (str :: Symbol) a. HasCallStack => Sing str -> a
    sError

    -- | The singleton for 'error'
    sError :: HasCallStack => Sing (str :: Symbol) -> a
    sError :: Sing str -> a
    sError sstr :: Sing str
    sstr = String -> a
    forall a. HasCallStack => String -> a
    error (Text -> String
    T.unpack (Sing str -> Demote Symbol
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing str
    sstr))

    -- | The promotion of 'errorWithoutStackTrace'. This version is more
    -- poly-kinded for easier use.
    type family ErrorWithoutStackTrace (str :: k0) :: k where {}
    $(genDefunSymbols [''ErrorWithoutStackTrace])
    instance SingI (ErrorWithoutStackTraceSym0 :: Symbol ~> a) where
      sing :: Sing ErrorWithoutStackTraceSym0
    sing = SingFunction1 ErrorWithoutStackTraceSym0
    -> Sing ErrorWithoutStackTraceSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 SingFunction1 ErrorWithoutStackTraceSym0
    forall (str :: Symbol) a. Sing str -> a
    sErrorWithoutStackTrace

    -- | The singleton for 'errorWithoutStackTrace'.
    sErrorWithoutStackTrace :: Sing (str :: Symbol) -> a
    sErrorWithoutStackTrace :: Sing str -> a
    sErrorWithoutStackTrace sstr :: Sing str
    sstr = String -> a
    forall a. String -> a
    errorWithoutStackTrace (Text -> String
    T.unpack (Sing str -> Demote Symbol
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing str
    sstr))

    -- | The promotion of 'undefined'.
    type family Undefined :: k where {}
    $(genDefunSymbols [''Undefined])

    -- | The singleton for 'undefined'.
    sUndefined :: HasCallStack => a
    sUndefined :: a
    sUndefined = a
    forall a. HasCallStack => a
    undefined

    -- | The singleton analogue of '(TN.^)' for 'Nat's.
    (%^) :: Sing a -> Sing b -> Sing (a ^ b)
    sa :: Sing a
    sa %^ :: Sing a -> Sing b -> Sing (a ^ b)
    %^ sb :: Sing b
    sb =
      let a :: Demote Nat
    a = Sing a -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing a
    sa
          b :: Demote Nat
    b = Sing b -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing b
    sb
          ex :: SomeNat
    ex = Natural -> SomeNat
    TN.someNatVal (Natural
    Demote Nat
    a Natural -> Natural -> Natural
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Natural
    Demote Nat
    b)
      in
      case SomeNat
    ex of
        SomeNat (Proxy n
    _ :: Proxy ab) -> SNat n -> SNat (a ^ b)
    forall a b. a -> b
    unsafeCoerce (Sing n
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: Sing ab)
    infixr 8 %^

    -- Defunctionalization symbols for type-level (^)
    $(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 :: Nat) (b :: Nat). 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 :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a ^ b)
    %^)

    -- | The singleton analogue of 'TN.<=?'
    --
    -- Note that, because of historical reasons in GHC's 'TN.Nat' API, 'TN.<=?'
    -- is incompatible (unification-wise) with 'O.<=' and the 'PEq', 'SEq',
    -- 'POrd', and 'SOrd' instances for 'Nat'.  @(a '<=?' b) ~ 'True@ does not
    -- imply anything about @a 'O.<=' b@ or any other 'PEq' / 'POrd'
    -- relationships.
    --
    -- (Be aware that 'O.<=' in the paragraph above refers to 'O.<=' from the
    -- 'POrd' typeclass, exported from "Data.Singletons.Prelude.Ord", and /not/
    -- the 'TN.<=' from "GHC.TypeNats".  The latter is simply a type alias for
    -- @(a 'TN.<=?' b) ~ 'True@.)
    --
    -- This is provided here for the sake of completeness and for compatibility
    -- with libraries with APIs built around '<=?'.  New code should use
    -- 'CmpNat', exposed through this library through the 'POrd' and 'SOrd'
    -- instances for 'Nat'.
    (%<=?) :: Sing a -> Sing b -> Sing (a <=? b)
    sa :: Sing a
    sa %<=? :: Sing a -> Sing b -> Sing (a <=? b)
    %<=? sb :: Sing b
    sb = SBool (Case_6989586621679389926 a b (CmpNat a b))
    -> SBool (a <=? b)
    forall a b. a -> b
    unsafeCoerce (Sing a
    sa Sing a -> Sing b -> Sing (Apply (Apply (<=@#@$) a) b)
    forall a (t :: a) (t :: a).
    SOrd a =>
    Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t)
    %<= Sing b
    sb)
    infix 4 %<=?

    -- Defunctionalization symbols for (<=?)
    $(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 :: Nat) (b :: Nat). 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 :: Nat) (b :: Nat). Sing a -> Sing b -> Sing (a <=? b)
    %<=?)