    {-# LANGUAGE TemplateHaskell, PolyKinds, DataKinds, TypeFamilies,
                 TypeOperators, GADTs, ScopedTypeVariables, UndecidableInstances,
                 DefaultSignatures, FlexibleContexts, InstanceSigs, NoStarIsType,
                 TypeApplications
      #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Prelude.Num
    -- Copyright   :  (C) 2014 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Defines and exports promoted and singleton versions of definitions from
    -- GHC.Num.
    --
    -- Be warned that some of the associated type families in the 'PNum' class
    -- (@(+)@, @(-)@, and @(*)@) clash with their counterparts for 'Nat' in the
    -- "GHC.TypeLits" module.
    ----------------------------------------------------------------------------

    module Data.Singletons.Prelude.Num (
      PNum(..), SNum(..), Subtract, sSubtract,

      -- ** Defunctionalization symbols
      type (+@#@$), type (+@#@$$), type (+@#@$$$),
      type (-@#@$), type (-@#@$$), type (-@#@$$$),
      type (*@#@$), type (*@#@$$), type (*@#@$$$),
      NegateSym0, NegateSym1,
      AbsSym0, AbsSym1,
      SignumSym0, SignumSym1,
      FromIntegerSym0, FromIntegerSym1,
      SubtractSym0, SubtractSym1, SubtractSym2
      ) where

    import Data.Ord (Down(..))
    import Data.Singletons.Single
    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Ord
    import Data.Singletons.TypeLits.Internal
    import Data.Singletons.Decide
    import qualified GHC.TypeNats as TN
    import GHC.TypeNats (SomeNat(..), someNatVal)
    import Unsafe.Coerce

    $(singletonsOnly [d|
      -- Basic numeric class.
      --
      -- Minimal complete definition: all except 'negate' or @(-)@
      class  Num a  where
          (+), (-), (*)       :: a -> a -> a
          infixl 6 +
          infixl 6 -
          infixl 7 *
          -- Unary negation.
          negate              :: a -> a
          -- Absolute value.
          abs                 :: a -> a
          -- Sign of a number.
          -- The functions 'abs' and 'signum' should satisfy the law:
          --
          -- > abs x * signum x == x
          --
          -- For real numbers, the 'signum' is either @-1@ (negative), @0@ (zero)
          -- or @1@ (positive).
          signum              :: a -> a
          -- Conversion from a 'Nat'.
          fromInteger         :: Nat -> a

          x - y               = x + negate y

          negate x            = 0 - x

      -- deriving newtype instance Num a => Num (Down a)
      instance Num a => Num (Down a) where
          Down a + Down b = Down (a + b)
          Down a - Down b = Down (a - b)
          Down a * Down b = Down (a * b)
          negate (Down a) = Down (negate a)
          abs    (Down a) = Down (abs a)
          signum (Down a) = Down (signum a)
          fromInteger n   = Down (fromInteger n)
      |])

    -- Workaround for #326
    infixl 6 +
    infixl 6 -
    infixl 7 *

    -- PNum instance
    type family SignumNat (a :: Nat) :: Nat where
      SignumNat 0 = 0
      SignumNat x = 1

    instance PNum Nat where
      type a + b = a TN.+ b
      type a - b = a TN.- b
      type a * b = a TN.* b
      type Negate (a :: Nat) = Error "Cannot negate a natural number"
      type Abs (a :: Nat) = a
      type Signum a = SignumNat a
      type FromInteger a = a

    -- SNum instance
    instance SNum Nat where
      sa :: Sing t
    sa %+ :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t)
    %+ sb :: Sing t
    sb =
        let a :: Demote Nat
    a = Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    sa
            b :: Demote Nat
    b = Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    sb
            ex :: SomeNat
    ex = Natural -> SomeNat
    someNatVal (Natural
    Demote Nat
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + Natural
    Demote Nat
    b)
        in
        case SomeNat
    ex of
          SomeNat (Proxy n
    _ :: Proxy ab) -> SNat n -> SNat (t + t)
    forall a b. a -> b
    unsafeCoerce (Sing n
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: Sing ab)

      sa :: Sing t
    sa %- :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t)
    %- sb :: Sing t
    sb =
        let a :: Demote Nat
    a = Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    sa
            b :: Demote Nat
    b = Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    sb
            ex :: SomeNat
    ex = Natural -> SomeNat
    someNatVal (Natural
    Demote Nat
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    - Natural
    Demote Nat
    b)
        in
        case SomeNat
    ex of
          SomeNat (Proxy n
    _ :: Proxy ab) -> SNat n -> SNat (t - t)
    forall a b. a -> b
    unsafeCoerce (Sing n
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: Sing ab)

      sa :: Sing t
    sa %* :: Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t)
    %* sb :: Sing t
    sb =
        let a :: Demote Nat
    a = Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    sa
            b :: Demote Nat
    b = Sing t -> Demote Nat
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing t
    sb
            ex :: SomeNat
    ex = Natural -> SomeNat
    someNatVal (Natural
    Demote Nat
    a Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    * Natural
    Demote Nat
    b)
        in
        case SomeNat
    ex of
          SomeNat (Proxy n
    _ :: Proxy ab) -> SNat n -> SNat (t * t)
    forall a b. a -> b
    unsafeCoerce (Sing n
    forall (n :: Nat). KnownNat n => SNat n
    SNat :: Sing ab)

      sNegate :: Sing t -> Sing (Apply NegateSym0 t)
    sNegate _ = [Char] -> SNat (Error "Cannot negate a natural number")
    forall a. HasCallStack => [Char] -> a
    error "Cannot call sNegate on a natural number singleton."

      sAbs :: Sing t -> Sing (Apply AbsSym0 t)
    sAbs x :: Sing t
    x = Sing t
    Sing (Apply AbsSym0 t)
    x

      sSignum :: Sing t -> Sing (Apply SignumSym0 t)
    sSignum sx :: Sing t
    sx =
        case Sing t
    sx Sing t -> Sing 0 -> Decision (t :~: 0)
    forall k (a :: k) (b :: k).
    SDecide k =>
    Sing a -> Sing b -> Decision (a :~: b)
    %~ (Sing 0
    forall k (a :: k). SingI a => Sing a
    sing :: Sing 0) of
          Proved Refl -> Sing 0
    forall k (a :: k). SingI a => Sing a
    sing :: Sing 0
          Disproved _ -> SNat 1 -> SNat (SignumNat t)
    forall a b. a -> b
    unsafeCoerce (Sing 1
    forall k (a :: k). SingI a => Sing a
    sing :: Sing 1)

      sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t)
    sFromInteger x :: Sing t
    x = Sing t
    Sing (Apply FromIntegerSym0 t)
    x

    $(singletonsOnly [d|
      subtract :: Num a => a -> a -> a
      subtract x y = y - x
      |])