    {-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, TemplateHaskell, CPP #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.CustomStar
    -- Copyright   :  (C) 2013 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- This file implements 'singletonStar', which generates a datatype @Rep@ and associated
    -- singleton from a list of types. The promoted version of @Rep@ is kind @*@ and the
    -- Haskell types themselves. This is still very experimental, so expect unusual
    -- results!
    --
    ----------------------------------------------------------------------------

    module Data.Singletons.CustomStar (
      singletonStar,

      module Data.Singletons.Prelude.Eq,
      module Data.Singletons.Prelude.Bool,
      module Data.Singletons.TH
      ) where

    import Language.Haskell.TH
    import Data.Singletons.Util
    import Data.Singletons.Deriving.Infer
    import Data.Singletons.Deriving.Ord
    import Data.Singletons.Deriving.Show
    import Data.Singletons.Promote
    import Data.Singletons.Promote.Monad
    import Data.Singletons.Single.Monad
    import Data.Singletons.Single.Data
    import Data.Singletons.Single
    import Data.Singletons.Syntax
    import Data.Singletons.Names
    import Data.Singletons.TH
    import Control.Monad
    import Data.Maybe
    import Language.Haskell.TH.Desugar
    import Data.Singletons.Prelude.Eq
    import Data.Singletons.Prelude.Bool

    -- | Produce a representation and singleton for the collection of types given.
    --
    -- A datatype @Rep@ is created, with one constructor per type in the declared
    -- universe. When this type is promoted by the singletons library, the
    -- constructors become full types in @*@, not just promoted data constructors.
    --
    -- For example,
    --
    -- > $(singletonStar [''Nat, ''Bool, ''Maybe])
    --
    -- generates the following:
    --
    -- > data Rep = Nat | Bool | Maybe Rep deriving (Eq, Ord, Read, Show)
    --
    -- and its singleton. However, because @Rep@ is promoted to @*@, the singleton
    -- is perhaps slightly unexpected:
    --
    -- > data SRep (a :: *) where
    -- >   SNat :: Sing Nat
    -- >   SBool :: Sing Bool
    -- >   SMaybe :: Sing a -> Sing (Maybe a)
    -- > type instance Sing = SRep
    --
    -- The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
    -- @Bool@, and @Maybe@, not just promoted data constructors.
    --
    -- Please note that this function is /very/ experimental. Use at your own risk.
    singletonStar :: DsMonad q
                  => [Name]        -- ^ A list of Template Haskell @Name@s for types
                  -> q [Dec]
    singletonStar :: [Name] -> q [Dec]
    singletonStar names :: [Name]
    names = do
      [[DKind]]
    kinds <- (Name -> q [DKind]) -> [Name] -> q [[DKind]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Name -> q [DKind]
    forall (q :: * -> *). DsMonad q => Name -> q [DKind]
    getKind [Name]
    names
      [DCon]
    ctors <- (Name -> [DKind] -> q DCon) -> [Name] -> [[DKind]] -> q [DCon]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (Bool -> Name -> [DKind] -> q DCon
    forall (q :: * -> *).
    DsMonad q =>
    Bool -> Name -> [DKind] -> q DCon
    mkCtor Bool
    True) [Name]
    names [[DKind]]
    kinds
      let repDecl :: DDec
    repDecl = NewOrData
    -> [DKind]
    -> Name
    -> [DTyVarBndr]
    -> Maybe DKind
    -> [DCon]
    -> [DDerivClause]
    -> DDec
    DDataD NewOrData
    Data [] Name
    repName [] (DKind -> Maybe DKind
    forall a. a -> Maybe a
    Just (Name -> DKind
    DConT Name
    typeKindName)) [DCon]
    ctors
                             [Maybe DDerivStrategy -> [DKind] -> DDerivClause
    DDerivClause Maybe DDerivStrategy
    forall a. Maybe a
    Nothing ((Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DKind
    DConT [''Eq, ''Ord, ''Read, ''Show])]
      [DCon]
    fakeCtors <- (Name -> [DKind] -> q DCon) -> [Name] -> [[DKind]] -> q [DCon]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (Bool -> Name -> [DKind] -> q DCon
    forall (q :: * -> *).
    DsMonad q =>
    Bool -> Name -> [DKind] -> q DCon
    mkCtor Bool
    False) [Name]
    names [[DKind]]
    kinds
      let dataDecl :: DataDecl
    dataDecl = Name -> [DTyVarBndr] -> [DCon] -> DataDecl
    DataDecl Name
    repName [] [DCon]
    fakeCtors
      -- Why do we need withLocalDeclarations here? It's because we end up
      -- expanding type synonyms when deriving instances for Rep, which requires
      -- reifying Rep itself. Since Rep hasn't been spliced in yet, we must put it
      -- into the local declarations.
      [Dec] -> DsM q [Dec] -> q [Dec]
    forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
    withLocalDeclarations (DDec -> [Dec]
    decToTH DDec
    repDecl) (DsM q [Dec] -> q [Dec]) -> DsM q [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ do
        -- We opt to infer the constraints for the Eq instance here so that when it's
        -- promoted, Rep will be promoted to Type.
        [DKind]
    dataDeclEqCxt <- DKind -> DKind -> [DCon] -> DsM q [DKind]
    forall (q :: * -> *).
    DsMonad q =>
    DKind -> DKind -> [DCon] -> q [DKind]
    inferConstraints (Name -> DKind
    DConT ''Eq) (Name -> DKind
    DConT Name
    repName) [DCon]
    fakeCtors
        let dataDeclEqInst :: DerivedDecl Eq
    dataDeclEqInst = Maybe [DKind] -> DKind -> Name -> DataDecl -> DerivedDecl Eq
    forall (cls :: * -> Constraint).
    Maybe [DKind] -> DKind -> Name -> DataDecl -> DerivedDecl cls
    DerivedDecl ([DKind] -> Maybe [DKind]
    forall a. a -> Maybe a
    Just [DKind]
    dataDeclEqCxt) (Name -> DKind
    DConT Name
    repName) Name
    repName DataDecl
    dataDecl
        UInstDecl
    ordInst  <- DerivDesc (DsM q)
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkOrdInstance Maybe [DKind]
    forall a. Maybe a
    Nothing (Name -> DKind
    DConT Name
    repName) DataDecl
    dataDecl
        UInstDecl
    showInst <- ShowMode -> DerivDesc (DsM q)
    forall (q :: * -> *). DsMonad q => ShowMode -> DerivDesc q
    mkShowInstance ShowMode
    ForPromotion Maybe [DKind]
    forall a. Maybe a
    Nothing (Name -> DKind
    DConT Name
    repName) DataDecl
    dataDecl
        (pInsts :: [AInstDecl]
    pInsts, promDecls :: [DDec]
    promDecls) <- [Dec] -> PrM [AInstDecl] -> DsM q ([AInstDecl], [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> PrM a -> q (a, [DDec])
    promoteM [] (PrM [AInstDecl] -> DsM q ([AInstDecl], [DDec]))
    -> PrM [AInstDecl] -> DsM q ([AInstDecl], [DDec])
    forall a b. (a -> b) -> a -> b
    $ do DataDecl -> PrM ()
    promoteDataDec DataDecl
    dataDecl
                                                DerivedDecl Eq -> PrM ()
    promoteDerivedEqDec DerivedDecl Eq
    dataDeclEqInst
                                                (UInstDecl -> PrM AInstDecl) -> [UInstDecl] -> PrM [AInstDecl]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (OMap Name DKind -> UInstDecl -> PrM AInstDecl
    promoteInstanceDec OMap Name DKind
    forall a. Monoid a => a
    mempty)
                                                  [UInstDecl
    ordInst, UInstDecl
    showInst]
        [DDec]
    singletonDecls <- [Dec] -> SgM [DDec] -> DsM q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> SgM [DDec] -> q [DDec]
    singDecsM [] (SgM [DDec] -> DsM q [DDec]) -> SgM [DDec] -> DsM q [DDec]
    forall a b. (a -> b) -> a -> b
    $ do [DDec]
    decs1 <- DataDecl -> SgM [DDec]
    singDataD DataDecl
    dataDecl
                                            [DDec]
    decs2 <- DerivedDecl Eq -> SgM [DDec]
    singDerivedEqDecs DerivedDecl Eq
    dataDeclEqInst
                                            [DDec]
    decs3 <- (AInstDecl -> SgM DDec) -> [AInstDecl] -> SgM [DDec]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse AInstDecl -> SgM DDec
    singInstD [AInstDecl]
    pInsts
                                            [DDec] -> SgM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec]
    decs1 [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    decs2 [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    decs3)
        [Dec] -> DsM q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> DsM q [Dec]) -> [Dec] -> DsM q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH ([DDec] -> [Dec]) -> [DDec] -> [Dec]
    forall a b. (a -> b) -> a -> b
    $ DDec
    repDecl DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :
                            [DDec]
    promDecls [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++
                            [DDec]
    singletonDecls
      where -- get the kinds of the arguments to the tycon with the given name
            getKind :: DsMonad q => Name -> q [DKind]
            getKind :: Name -> q [DKind]
    getKind name :: Name
    name = do
              Info
    info <- Name -> q Info
    forall (q :: * -> *). DsMonad q => Name -> q Info
    reifyWithLocals Name
    name
              DInfo
    dinfo <- Info -> q DInfo
    forall (q :: * -> *). DsMonad q => Info -> q DInfo
    dsInfo Info
    info
              case DInfo
    dinfo of
                DTyConI (DDataD _ (_:_) _ _ _ _ _) _ ->
                   String -> q [DKind]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Cannot make a representation of a constrained data type"
                DTyConI (DDataD _ [] _ tvbs :: [DTyVarBndr]
    tvbs mk :: Maybe DKind
    mk _ _) _ -> do
                   [DTyVarBndr]
    all_tvbs <- [DTyVarBndr] -> Maybe DKind -> q [DTyVarBndr]
    forall (q :: * -> *).
    DsMonad q =>
    [DTyVarBndr] -> Maybe DKind -> q [DTyVarBndr]
    buildDataDTvbs [DTyVarBndr]
    tvbs Maybe DKind
    mk
                   [DKind] -> q [DKind]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DKind] -> q [DKind]) -> [DKind] -> q [DKind]
    forall a b. (a -> b) -> a -> b
    $ (DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map (DKind -> Maybe DKind -> DKind
    forall a. a -> Maybe a -> a
    fromMaybe (Name -> DKind
    DConT Name
    typeKindName) (Maybe DKind -> DKind)
    -> (DTyVarBndr -> Maybe DKind) -> DTyVarBndr -> DKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DTyVarBndr -> Maybe DKind
    extractTvbKind) [DTyVarBndr]
    all_tvbs
                DTyConI (DTySynD _ tvbs :: [DTyVarBndr]
    tvbs _) _ ->
                   [DKind] -> q [DKind]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DKind] -> q [DKind]) -> [DKind] -> q [DKind]
    forall a b. (a -> b) -> a -> b
    $ (DTyVarBndr -> DKind) -> [DTyVarBndr] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map (DKind -> Maybe DKind -> DKind
    forall a. a -> Maybe a -> a
    fromMaybe (Name -> DKind
    DConT Name
    typeKindName) (Maybe DKind -> DKind)
    -> (DTyVarBndr -> Maybe DKind) -> DTyVarBndr -> DKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DTyVarBndr -> Maybe DKind
    extractTvbKind) [DTyVarBndr]
    tvbs
                DPrimTyConI _ n :: Int
    n _ ->
                   [DKind] -> q [DKind]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DKind] -> q [DKind]) -> [DKind] -> q [DKind]
    forall a b. (a -> b) -> a -> b
    $ Int -> DKind -> [DKind]
    forall a. Int -> a -> [a]
    replicate Int
    n (DKind -> [DKind]) -> DKind -> [DKind]
    forall a b. (a -> b) -> a -> b
    $ Name -> DKind
    DConT Name
    typeKindName
                _ -> String -> q [DKind]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> q [DKind]) -> String -> q [DKind]
    forall a b. (a -> b) -> a -> b
    $ "Invalid thing for representation: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Name -> String
    forall a. Show a => a -> String
    show Name
    name)

            -- first parameter is whether this is a real ctor (with a fresh name)
            -- or a fake ctor (when the name is actually a Haskell type)
            mkCtor :: DsMonad q => Bool -> Name -> [DKind] -> q DCon
            mkCtor :: Bool -> Name -> [DKind] -> q DCon
    mkCtor real :: Bool
    real name :: Name
    name args :: [DKind]
    args = do
              (types :: [DKind]
    types, vars :: [Name]
    vars) <- QWithAux [Name] q [DKind] -> q ([DKind], [Name])
    forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
    evalForPair (QWithAux [Name] q [DKind] -> q ([DKind], [Name]))
    -> QWithAux [Name] q [DKind] -> q ([DKind], [Name])
    forall a b. (a -> b) -> a -> b
    $ (DKind -> QWithAux [Name] q DKind)
    -> [DKind] -> QWithAux [Name] q [DKind]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ([DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType []) [DKind]
    args
              Name
    dataName <- if Bool
    real then String -> q Name
    forall (q :: * -> *). Quasi q => String -> q Name
    mkDataName (Name -> String
    nameBase Name
    name) else Name -> q Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    name
              DCon -> q DCon
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DCon -> q DCon) -> DCon -> q DCon
    forall a b. (a -> b) -> a -> b
    $ [DTyVarBndr] -> [DKind] -> Name -> DConFields -> DKind -> DCon
    DCon ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    vars) [] Name
    dataName
                            (Bool -> [DBangType] -> DConFields
    DNormalC Bool
    False ((DKind -> DBangType) -> [DKind] -> [DBangType]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ty :: DKind
    ty -> (Bang
    noBang, DKind
    ty)) [DKind]
    types))
                            (Name -> DKind
    DConT Name
    repName)
                where
                  noBang :: Bang
    noBang = SourceUnpackedness -> SourceStrictness -> Bang
    Bang SourceUnpackedness
    NoSourceUnpackedness SourceStrictness
    NoSourceStrictness

            -- demote a kind back to a type, accumulating any unbound parameters
            kindToType :: DsMonad q => [DTypeArg] -> DKind -> QWithAux [Name] q DType
            kindToType :: [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType _    (DForallT _ _ _) = String -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Explicit forall encountered in kind"
            kindToType args :: [DTypeArg]
    args (DAppT f :: DKind
    f a :: DKind
    a) = do
              DKind
    a' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType [] DKind
    a
              [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType (DKind -> DTypeArg
    DTANormal DKind
    a' DTypeArg -> [DTypeArg] -> [DTypeArg]
    forall a. a -> [a] -> [a]
    : [DTypeArg]
    args) DKind
    f
            kindToType args :: [DTypeArg]
    args (DAppKindT f :: DKind
    f a :: DKind
    a) = do
              DKind
    a' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType [] DKind
    a
              [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType (DKind -> DTypeArg
    DTyArg DKind
    a' DTypeArg -> [DTypeArg] -> [DTypeArg]
    forall a. a -> [a] -> [a]
    : [DTypeArg]
    args) DKind
    f
            kindToType args :: [DTypeArg]
    args (DSigT t :: DKind
    t k :: DKind
    k) = do
              DKind
    t' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType [] DKind
    t
              DKind
    k' <- [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    forall (q :: * -> *).
    DsMonad q =>
    [DTypeArg] -> DKind -> QWithAux [Name] q DKind
    kindToType [] DKind
    k
              DKind -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DKind -> QWithAux [Name] q DKind)
    -> DKind -> QWithAux [Name] q DKind
    forall a b. (a -> b) -> a -> b
    $ DKind -> DKind -> DKind
    DSigT DKind
    t' DKind
    k' DKind -> [DTypeArg] -> DKind
    `applyDType` [DTypeArg]
    args
            kindToType args :: [DTypeArg]
    args (DVarT n :: Name
    n) = do
              Name -> QWithAux [Name] q ()
    forall (q :: * -> *) elt. Quasi q => elt -> QWithAux [elt] q ()
    addElement Name
    n
              DKind -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DKind -> QWithAux [Name] q DKind)
    -> DKind -> QWithAux [Name] q DKind
    forall a b. (a -> b) -> a -> b
    $ Name -> DKind
    DVarT Name
    n DKind -> [DTypeArg] -> DKind
    `applyDType` [DTypeArg]
    args
            kindToType args :: [DTypeArg]
    args (DConT n :: Name
    n)    = DKind -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DKind -> QWithAux [Name] q DKind)
    -> DKind -> QWithAux [Name] q DKind
    forall a b. (a -> b) -> a -> b
    $ Name -> DKind
    DConT Name
    name DKind -> [DTypeArg] -> DKind
    `applyDType` [DTypeArg]
    args
              where name :: Name
    name | Name -> Bool
    isTypeKindName Name
    n = Name
    repName
                         | Bool
    otherwise        = Name
    n
            kindToType args :: [DTypeArg]
    args DArrowT      = DKind -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DKind -> QWithAux [Name] q DKind)
    -> DKind -> QWithAux [Name] q DKind
    forall a b. (a -> b) -> a -> b
    $ DKind
    DArrowT    DKind -> [DTypeArg] -> DKind
    `applyDType` [DTypeArg]
    args
            kindToType args :: [DTypeArg]
    args k :: DKind
    k@(DLitT {}) = DKind -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DKind -> QWithAux [Name] q DKind)
    -> DKind -> QWithAux [Name] q DKind
    forall a b. (a -> b) -> a -> b
    $ DKind
    k          DKind -> [DTypeArg] -> DKind
    `applyDType` [DTypeArg]
    args
            kindToType args :: [DTypeArg]
    args DWildCardT   = DKind -> QWithAux [Name] q DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DKind -> QWithAux [Name] q DKind)
    -> DKind -> QWithAux [Name] q DKind
    forall a b. (a -> b) -> a -> b
    $ DKind
    DWildCardT DKind -> [DTypeArg] -> DKind
    `applyDType` [DTypeArg]
    args