{- 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'