    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE InstanceSigs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# OPTIONS_GHC -Wno-orphans #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Prelude.Const
    -- Copyright   :  (C) 2018 Ryan Scott
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Exports the promoted and singled versions of the 'Const' data type.
    --
    -----------------------------------------------------------------------------

    module Data.Singletons.Prelude.Const (
      -- * The 'Const' singleton
      Sing, SConst(..), GetConst,

      -- * Defunctionalization symbols
      ConstSym0, ConstSym1,
      GetConstSym0, GetConstSym1
      ) where

    import Control.Applicative
    import Data.Kind (Type)
    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Base
      hiding ( Const, ConstSym0, ConstSym1
             , Foldr, FoldrSym0, sFoldr )
    import Data.Singletons.Prelude.Enum
    import Data.Singletons.Prelude.Eq
    import Data.Singletons.Prelude.Foldable
    import Data.Singletons.Prelude.Instances hiding (FoldlSym0, sFoldl)
    import Data.Singletons.Prelude.Monad.Internal
    import Data.Singletons.Prelude.Monoid
    import Data.Singletons.Prelude.Num
    import Data.Singletons.Prelude.Ord
    import Data.Singletons.Prelude.Semigroup.Internal
    import Data.Singletons.Prelude.Show
    import Data.Singletons.Promote
    import Data.Singletons.Single

    {-
    Const's argument `b` is poly-kinded, and as a result, we have a choice as to
    what Sing instance to give it. We could use either

    1. data instance Sing :: forall (k :: Type) (a :: Type) (b :: k).    Const a b -> Type
    2. data instance Sing :: forall             (a :: Type) (b :: Type). Const a b -> Type

    Option (1) is the more permissive one, so we opt for that. However, singletons'
    TH machinery does not jive with this option, since the SingKind instance it
    tries to generate:

      instance (SingKind a, SingKind b) => SingKind (Const a b) where
        type Demote (Const a b) = Const (Demote a) (Demote b)

    Assumes that `b` is of kind Type. Until we get a more reliable story for
    poly-kinded Sing instances (see #150), we simply write the Sing instance by
    hand.
    -}
    data SConst :: forall (k :: Type) (a :: Type) (b :: k). Const a b -> Type where
      SConst :: { SConst ('Const a) -> Sing a
    sGetConst :: Sing a } -> SConst ('Const a)
    type instance Sing = SConst
    instance SingKind a => SingKind (Const a b) where
      type Demote (Const a b) = Const (Demote a) b
      fromSing :: Sing a -> Demote (Const a b)
    fromSing (SConst sa) = Demote a -> Const (Demote a) b
    forall k a (b :: k). a -> Const a b
    Const (Sing a -> Demote a
    forall k (a :: k). SingKind k => Sing a -> Demote k
    fromSing Sing a
    sa)
      toSing :: Demote (Const a b) -> SomeSing (Const a b)
    toSing (Const a) = Demote a
    -> (forall (a :: a). Sing a -> SomeSing (Const a b))
    -> SomeSing (Const a b)
    forall k r.
    SingKind k =>
    Demote k -> (forall (a :: k). Sing a -> r) -> r
    withSomeSing Demote a
    a ((forall (a :: a). Sing a -> SomeSing (Const a b))
     -> SomeSing (Const a b))
    -> (forall (a :: a). Sing a -> SomeSing (Const a b))
    -> SomeSing (Const a b)
    forall a b. (a -> b) -> a -> b
    $ SConst ('Const a) -> SomeSing (Const a b)
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing (SConst ('Const a) -> SomeSing (Const a b))
    -> (Sing a -> SConst ('Const a)) -> Sing a -> SomeSing (Const a b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Sing a -> SConst ('Const a)
    forall a k (b :: k) (a :: a). Sing a -> SConst ('Const a)
    SConst
    instance SingI a => SingI ('Const a) where
      sing :: Sing ('Const a)
    sing = Sing a -> SConst ('Const a)
    forall a k (b :: k) (a :: a). Sing a -> SConst ('Const a)
    SConst Sing a
    forall k (a :: k). SingI a => Sing a
    sing

    $(genDefunSymbols [''Const])
    instance SingI ConstSym0 where
      sing :: Sing ConstSym0
    sing = SingFunction1 ConstSym0 -> Sing ConstSym0
    forall k1 k (f :: k1 ~> k). SingFunction1 f -> Sing f
    singFun1 SingFunction1 ConstSym0
    forall a k (b :: k) (a :: a). Sing a -> SConst ('Const a)
    SConst

    $(singletons [d|
      type family GetConst (x :: Const a b) :: a where
        GetConst ('Const x) = x
      |])

    $(singletonsOnly [d|
      deriving instance Bounded a => Bounded (Const a b)
      deriving instance Eq      a => Eq      (Const a b)
      deriving instance Ord     a => Ord     (Const a b)

      -- deriving instance Enum a => Enum (Const a b)
      instance Enum a => Enum (Const a b) where
        succ (Const x)     = Const (succ x)
        pred (Const x)     = Const (pred x)
        toEnum i           = Const (toEnum i)
        fromEnum (Const x) = fromEnum x
        enumFromTo (Const x) (Const y) = map Const (enumFromTo x y)
        enumFromThenTo (Const x) (Const y) (Const z) =
            map Const (enumFromThenTo x y z)

      -- deriving instance Monoid a => Monoid (Const a b)
      instance Monoid a => Monoid (Const a b) where
        mempty = Const mempty

      -- deriving instance Num a => Num (Const a b)
      instance Num a => Num (Const a b) where
        Const x + Const y = Const (x + y)
        Const x - Const y = Const (x - y)
        Const x * Const y = Const (x * y)
        negate (Const x)  = Const (negate x)
        abs    (Const x)  = Const (abs    x)
        signum (Const x)  = Const (signum x)
        fromInteger n     = Const (fromInteger n)

      -- deriving instance Semigroup a => Semigroup (Const a b)
      instance Semigroup a => Semigroup (Const a b) where
        Const x <> Const y = Const (x <> y)

      -- -| This instance would be equivalent to the derived instances of the
      -- 'Const' newtype if the 'runConst' field were removed
      instance Show a => Show (Const a b) where
          showsPrec d (Const x) = showParen (d > 10) $
                                  showString "Const " . showsPrec 11 x

      deriving instance Functor (Const m)
      deriving instance Foldable (Const m)

      instance Monoid m => Applicative (Const m) where
          pure _ = Const mempty
          liftA2 _ (Const x) (Const y) = Const (x `mappend` y)
          Const x <*> Const y = Const (x `mappend` y)
      |])