    {- Data/Singletons/Single/Data.hs

    (c) Richard Eisenberg 2013
    rae@cs.brynmawr.edu

    Singletonizes constructors.
    -}

    {-# LANGUAGE ParallelListComp, TupleSections, LambdaCase #-}

    module Data.Singletons.Single.Data where

    import Language.Haskell.TH.Desugar
    import Language.Haskell.TH.Desugar.OSet (OSet)
    import Language.Haskell.TH.Syntax
    import Data.Singletons.Single.Defun
    import Data.Singletons.Single.Monad
    import Data.Singletons.Single.Type
    import Data.Singletons.Single.Fixity
    import Data.Singletons.Promote.Type
    import Data.Singletons.Util
    import Data.Singletons.Names
    import Data.Singletons.Syntax
    import Control.Monad
    import Data.Foldable

    -- We wish to consider the promotion of "Rep" to be *
    -- not a promoted data constructor.
    singDataD :: DataDecl -> SgM [DDec]
    singDataD :: DataDecl -> SgM [DDec]
    singDataD (DataDecl name :: Name
    name tvbs :: [DTyVarBndr]
    tvbs ctors :: [DCon]
    ctors) = do
      let tvbNames :: [Name]
    tvbNames = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    tvbs
      DKind
    k <- DKind -> SgM DKind
    forall (m :: * -> *). MonadFail m => DKind -> m DKind
    promoteType (DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT Name
    name) ((Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DKind
    DVarT [Name]
    tvbNames))
      [DCon]
    ctors' <- (DCon -> SgM DCon) -> [DCon] -> SgM [DCon]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name -> DCon -> SgM DCon
    singCtor Name
    name) [DCon]
    ctors
      [DDec]
    ctorFixities <-
        -- try to reify the fixity declarations for the constructors and then
        -- singletonize them. In case the reification fails, we default to an
        -- empty list of singletonized fixity declarations.
        -- why this works:
        -- 1. if we're in a call to 'genSingletons', the data type was defined
        --    earlier and its constructors are in scope, the reification succeeds.
        -- 2. if we're in a call to 'singletons', the reification will fail, but
        --    the fixity declaration will get singletonized by itself (not from
        --    here, look for other invocations of 'singInfixDecl')
        [Name] -> SgM [DDec]
    forall (q :: * -> *). DsMonad q => [Name] -> q [DDec]
    singFixityDeclarations [ Name
    n | DCon _ _ n :: Name
    n _ _ <- [DCon]
    ctors ]
      -- instance for SingKind
      [DClause]
    fromSingClauses     <- (DCon -> SgM DClause) -> [DCon] -> SgM [DClause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DCon -> SgM DClause
    mkFromSingClause [DCon]
    ctors
      DClause
    emptyFromSingClause <- SgM DClause
    mkEmptyFromSingClause
      [DClause]
    toSingClauses       <- (DCon -> SgM DClause) -> [DCon] -> SgM [DClause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DCon -> SgM DClause
    mkToSingClause [DCon]
    ctors
      DClause
    emptyToSingClause   <- SgM DClause
    mkEmptyToSingClause
      let singKindInst :: DDec
    singKindInst =
            Maybe Overlap
    -> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                       ((Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map (DKind -> DKind
    singKindConstraint (DKind -> DKind) -> (Name -> DKind) -> Name -> DKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> DKind
    DVarT) [Name]
    tvbNames)
                       (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    singKindClassName) DKind
    k)
                       [ DTySynEqn -> DDec
    DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
    forall a b. (a -> b) -> a -> b
    $ Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                          (Name -> DKind
    DConT Name
    demoteName DKind -> DKind -> DKind
    `DAppT` DKind
    k)
                          (DKind -> [DKind] -> DKind
    foldType (Name -> DKind
    DConT Name
    name)
                            ((Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map (DKind -> DKind -> DKind
    DAppT DKind
    demote (DKind -> DKind) -> (Name -> DKind) -> Name -> DKind
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> DKind
    DVarT) [Name]
    tvbNames))
                       , DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Name -> [DClause] -> DLetDec
    DFunD Name
    fromSingName
                                   ([DClause]
    fromSingClauses [DClause] -> [DClause] -> [DClause]
    forall a. [a] -> [a] -> [a]
    `orIfEmpty` [DClause
    emptyFromSingClause])
                       , DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Name -> [DClause] -> DLetDec
    DFunD Name
    toSingName
                                   ([DClause]
    toSingClauses   [DClause] -> [DClause] -> [DClause]
    forall a. [a] -> [a] -> [a]
    `orIfEmpty` [DClause
    emptyToSingClause]) ]

      let singDataName :: Name
    singDataName = Name -> Name
    singTyConName Name
    name
          -- e.g. type instance Sing @Nat = SNat
          singSynInst :: DDec
    singSynInst =
            DTySynEqn -> DDec
    DTySynInstD (DTySynEqn -> DDec) -> DTySynEqn -> DDec
    forall a b. (a -> b) -> a -> b
    $ Maybe [DTyVarBndr] -> DKind -> DKind -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                                    (Name -> DKind
    DConT Name
    singFamilyName DKind -> DKind -> DKind
    `DAppKindT` DKind
    k)
                                    (Name -> DKind
    DConT Name
    singDataName)
          kindedSingTy :: DKind
    kindedSingTy = [DTyVarBndr] -> [DKind] -> DKind -> DKind
    DForallT ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    tvbNames) [] (DKind -> DKind) -> DKind -> DKind
    forall a b. (a -> b) -> a -> b
    $
                         DKind
    DArrowT DKind -> DKind -> DKind
    `DAppT` DKind
    k DKind -> DKind -> DKind
    `DAppT` Name -> DKind
    DConT Name
    typeKindName

      [DDec] -> SgM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
    forall a b. (a -> b) -> a -> b
    $ (NewOrData
    -> [DKind]
    -> Name
    -> [DTyVarBndr]
    -> Maybe DKind
    -> [DCon]
    -> [DDerivClause]
    -> DDec
    DDataD NewOrData
    Data [] Name
    singDataName [] (DKind -> Maybe DKind
    forall a. a -> Maybe a
    Just DKind
    kindedSingTy) [DCon]
    ctors' []) DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :
               DDec
    singSynInst DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :
               DDec
    singKindInst DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :
               [DDec]
    ctorFixities
      where -- in the Rep case, the names of the constructors are in the wrong scope
            -- (they're types, not datacons), so we have to reinterpret them.
            mkConName :: Name -> SgM Name
            mkConName :: Name -> SgM Name
    mkConName
              | Name -> String
    nameBase Name
    name String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> String
    nameBase Name
    repName = String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    mkDataName (String -> SgM Name) -> (Name -> String) -> Name -> SgM Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> String
    nameBase
              | Bool
    otherwise                         = Name -> SgM Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return

            mkFromSingClause :: DCon -> SgM DClause
            mkFromSingClause :: DCon -> SgM DClause
    mkFromSingClause c :: DCon
    c = do
              let (cname :: Name
    cname, numArgs :: Int
    numArgs) = DCon -> (Name, Int)
    extractNameArgs DCon
    c
              Name
    cname' <- Name -> SgM Name
    mkConName Name
    cname
              [Name]
    varNames <- Int -> SgM Name -> SgM [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    numArgs (String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "b")
              DClause -> SgM DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> SgM DClause) -> DClause -> SgM DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [Name -> [DPat] -> DPat
    DConP (Name -> Name
    singDataConName Name
    cname) ((Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    varNames)]
                               (DExp -> [DExp] -> DExp
    foldExp
                                  (Name -> DExp
    DConE Name
    cname')
                                  ((Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DVarE Name
    fromSingName) (DExp -> DExp) -> (Name -> DExp) -> Name -> DExp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> DExp
    DVarE) [Name]
    varNames))

            mkToSingClause :: DCon -> SgM DClause
            mkToSingClause :: DCon -> SgM DClause
    mkToSingClause (DCon _tvbs :: [DTyVarBndr]
    _tvbs _cxt :: [DKind]
    _cxt cname :: Name
    cname fields :: DConFields
    fields _rty :: DKind
    _rty) = do
              let types :: [DKind]
    types = DConFields -> [DKind]
    tysOfConFields DConFields
    fields
              [Name]
    varNames  <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (SgM Name -> DKind -> SgM Name
    forall a b. a -> b -> a
    const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
    forall a b. (a -> b) -> a -> b
    $ String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "b") [DKind]
    types
              [Name]
    svarNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (SgM Name -> DKind -> SgM Name
    forall a b. a -> b -> a
    const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
    forall a b. (a -> b) -> a -> b
    $ String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "c") [DKind]
    types
              [DKind]
    promoted  <- (DKind -> SgM DKind) -> [DKind] -> SgM [DKind]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DKind -> SgM DKind
    forall (m :: * -> *). MonadFail m => DKind -> m DKind
    promoteType [DKind]
    types
              Name
    cname' <- Name -> SgM Name
    mkConName Name
    cname
              let varPats :: [DPat]
    varPats        = (Name -> DKind -> DPat) -> [Name] -> [DKind] -> [DPat]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DKind -> DPat
    mkToSingVarPat [Name]
    varNames [DKind]
    promoted
                  recursiveCalls :: [DExp]
    recursiveCalls = (Name -> DKind -> DExp) -> [Name] -> [DKind] -> [DExp]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DKind -> DExp
    mkRecursiveCall [Name]
    varNames [DKind]
    promoted
              DClause -> SgM DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> SgM DClause) -> DClause -> SgM DClause
    forall a b. (a -> b) -> a -> b
    $
                [DPat] -> DExp -> DClause
    DClause [Name -> [DPat] -> DPat
    DConP Name
    cname' [DPat]
    varPats]
                        ([DExp] -> [DPat] -> DExp -> DExp
    multiCase [DExp]
    recursiveCalls
                                   ((Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> [DPat] -> DPat
    DConP Name
    someSingDataName ([DPat] -> DPat) -> (Name -> [DPat]) -> Name -> DPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DPat -> [DPat]
    forall a. a -> [a]
    listify (DPat -> [DPat]) -> (Name -> DPat) -> Name -> [DPat]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> DPat
    DVarP)
                                        [Name]
    svarNames)
                                   (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DConE Name
    someSingDataName)
                                             (DExp -> [DExp] -> DExp
    foldExp (Name -> DExp
    DConE (Name -> Name
    singDataConName Name
    cname))
                                                      ((Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    svarNames))))

            mkToSingVarPat :: Name -> DKind -> DPat
            mkToSingVarPat :: Name -> DKind -> DPat
    mkToSingVarPat varName :: Name
    varName ki :: DKind
    ki =
              DPat -> DKind -> DPat
    DSigP (Name -> DPat
    DVarP Name
    varName) (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    demoteName) DKind
    ki)

            mkRecursiveCall :: Name -> DKind -> DExp
            mkRecursiveCall :: Name -> DKind -> DExp
    mkRecursiveCall var_name :: Name
    var_name ki :: DKind
    ki =
              DExp -> DKind -> DExp
    DSigE (DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DVarE Name
    toSingName) (Name -> DExp
    DVarE Name
    var_name))
                    (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    someSingTypeName) DKind
    ki)

            mkEmptyFromSingClause :: SgM DClause
            mkEmptyFromSingClause :: SgM DClause
    mkEmptyFromSingClause = do
              Name
    x <- String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "x"
              DClause -> SgM DClause
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DClause -> SgM DClause) -> DClause -> SgM DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [Name -> DPat
    DVarP Name
    x]
                   (DExp -> DClause) -> DExp -> DClause
    forall a b. (a -> b) -> a -> b
    $ DExp -> [DMatch] -> DExp
    DCaseE (Name -> DExp
    DVarE Name
    x) []

            mkEmptyToSingClause :: SgM DClause
            mkEmptyToSingClause :: SgM DClause
    mkEmptyToSingClause = do
              Name
    x <- String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "x"
              DClause -> SgM DClause
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DClause -> SgM DClause) -> DClause -> SgM DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [Name -> DPat
    DVarP Name
    x]
                   (DExp -> DClause) -> DExp -> DClause
    forall a b. (a -> b) -> a -> b
    $ Name -> DExp
    DConE Name
    someSingDataName DExp -> DExp -> DExp
    `DAppE` DExp -> [DMatch] -> DExp
    DCaseE (Name -> DExp
    DVarE Name
    x) []

    -- refine a constructor.
    singCtor :: Name -> DCon -> SgM DCon
     -- polymorphic constructors are handled just
     -- like monomorphic ones -- the polymorphism in
     -- the kind is automatic
    singCtor :: Name -> DCon -> SgM DCon
    singCtor dataName :: Name
    dataName (DCon _tvbs :: [DTyVarBndr]
    _tvbs cxt :: [DKind]
    cxt name :: Name
    name fields :: DConFields
    fields rty :: DKind
    rty)
      | Bool -> Bool
    not ([DKind] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [DKind]
    cxt)
      = String -> SgM DCon
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of constrained constructors not yet supported"
      | Bool
    otherwise
      = do
      let types :: [DKind]
    types = DConFields -> [DKind]
    tysOfConFields DConFields
    fields
          sName :: Name
    sName = Name -> Name
    singDataConName Name
    name
          sCon :: DExp
    sCon = Name -> DExp
    DConE Name
    sName
          pCon :: DKind
    pCon = Name -> DKind
    DConT Name
    name
      [Name]
    indexNames <- (DKind -> SgM Name) -> [DKind] -> SgM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (SgM Name -> DKind -> SgM Name
    forall a b. a -> b -> a
    const (SgM Name -> DKind -> SgM Name) -> SgM Name -> DKind -> SgM Name
    forall a b. (a -> b) -> a -> b
    $ String -> SgM Name
    forall (q :: * -> *). Quasi q => String -> q Name
    qNewName "n") [DKind]
    types
      let indices :: [DKind]
    indices = (Name -> DKind) -> [Name] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DKind
    DVarT [Name]
    indexNames
      [DKind]
    kinds <- (DKind -> SgM DKind) -> [DKind] -> SgM [DKind]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DKind -> SgM DKind
    forall (m :: * -> *). MonadFail m => DKind -> m DKind
    promoteType [DKind]
    types
      let bound_kvs :: OSet Name
    bound_kvs = (DKind -> OSet Name) -> [DKind] -> OSet Name
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap DKind -> OSet Name
    fvDType [DKind]
    kinds
      [DKind]
    args <- (DKind -> DKind -> SgM DKind) -> [DKind] -> [DKind] -> SgM [DKind]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (OSet Name -> DKind -> DKind -> SgM DKind
    buildArgType OSet Name
    bound_kvs) [DKind]
    types [DKind]
    indices
      DKind
    rty' <- DKind -> SgM DKind
    forall (m :: * -> *). MonadFail m => DKind -> m DKind
    promoteType DKind
    rty
      let tvbs :: [DTyVarBndr]
    tvbs = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV (OSet Name -> [Name]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList OSet Name
    bound_kvs) [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> DKind -> DTyVarBndr) -> [Name] -> [DKind] -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DKind -> DTyVarBndr
    DKindedTV [Name]
    indexNames [DKind]
    kinds
          kindedIndices :: [DKind]
    kindedIndices = (DKind -> DKind -> DKind) -> [DKind] -> [DKind] -> [DKind]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith DKind -> DKind -> DKind
    DSigT [DKind]
    indices [DKind]
    kinds

      -- SingI instance for data constructor
      [DDec] -> SgM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs
        [Maybe Overlap
    -> Maybe [DTyVarBndr] -> [DKind] -> DKind -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                    ((DKind -> DKind) -> [DKind] -> [DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    singIName)) [DKind]
    indices)
                    (DKind -> DKind -> DKind
    DAppT (Name -> DKind
    DConT Name
    singIName)
                           (DKind -> [DKind] -> DKind
    foldType DKind
    pCon [DKind]
    kindedIndices))
                    [DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ DPat -> DExp -> DLetDec
    DValD (Name -> DPat
    DVarP Name
    singMethName)
                           (DExp -> [DExp] -> DExp
    foldExp DExp
    sCon ((DKind -> DExp) -> [DKind] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map (DExp -> DKind -> DExp
    forall a b. a -> b -> a
    const (DExp -> DKind -> DExp) -> DExp -> DKind -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> DExp
    DVarE Name
    singMethName) [DKind]
    types))]]
      -- SingI instances for defunctionalization symbols. Note that we don't
      -- support contexts in constructors at the moment, so it's fine for now to
      -- just assume that the context is always ().
      [DDec] -> SgM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs ([DDec] -> SgM ()) -> SgM [DDec] -> SgM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Name
    -> NameSpace
    -> [DKind]
    -> [Maybe DKind]
    -> Maybe DKind
    -> SgM [DDec]
    singDefuns Name
    name NameSpace
    DataName [] ((DKind -> Maybe DKind) -> [DKind] -> [Maybe DKind]
    forall a b. (a -> b) -> [a] -> [b]
    map DKind -> Maybe DKind
    forall a. a -> Maybe a
    Just [DKind]
    kinds) (DKind -> Maybe DKind
    forall a. a -> Maybe a
    Just DKind
    rty')

      let noBang :: Bang
    noBang    = SourceUnpackedness -> SourceStrictness -> Bang
    Bang SourceUnpackedness
    NoSourceUnpackedness SourceStrictness
    NoSourceStrictness
          conFields :: DConFields
    conFields = case DConFields
    fields of
                        DNormalC dInfix :: Bool
    dInfix _ -> Bool -> [DBangType] -> DConFields
    DNormalC Bool
    dInfix ([DBangType] -> DConFields) -> [DBangType] -> DConFields
    forall a b. (a -> b) -> a -> b
    $ (DKind -> DBangType) -> [DKind] -> [DBangType]
    forall a b. (a -> b) -> [a] -> [b]
    map (Bang
    noBang,) [DKind]
    args
                        DRecC rec_fields :: [DVarBangType]
    rec_fields ->
                          [DVarBangType] -> DConFields
    DRecC [ (Name -> Name
    singValName Name
    field_name, Bang
    noBang, DKind
    arg)
                                | (field_name :: Name
    field_name, _, _) <- [DVarBangType]
    rec_fields
                                | DKind
    arg <- [DKind]
    args ]
      DCon -> SgM DCon
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DCon -> SgM DCon) -> DCon -> SgM DCon
    forall a b. (a -> b) -> a -> b
    $ [DTyVarBndr] -> [DKind] -> Name -> DConFields -> DKind -> DCon
    DCon [DTyVarBndr]
    tvbs
                    []
                    Name
    sName
                    DConFields
    conFields
                    (Name -> DKind
    DConT (Name -> Name
    singTyConName Name
    dataName) DKind -> DKind -> DKind
    `DAppT` DKind -> [DKind] -> DKind
    foldType DKind
    pCon [DKind]
    indices)
      where buildArgType :: OSet Name -> DType -> DType -> SgM DType
            buildArgType :: OSet Name -> DKind -> DKind -> SgM DKind
    buildArgType bound_kvs :: OSet Name
    bound_kvs ty :: DKind
    ty index :: DKind
    index = do
              (ty' :: DKind
    ty', _, _, _, _, _) <- OSet Name
    -> DKind
    -> DKind
    -> SgM (DKind, Int, [Name], [DKind], [DKind], DKind)
    singType OSet Name
    bound_kvs DKind
    index DKind
    ty
              DKind -> SgM DKind
    forall (m :: * -> *) a. Monad m => a -> m a
    return DKind
    ty'