{- Data/Singletons/TH/Single/Data.hs

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

Singletonizes constructors.
-}

module Data.Singletons.TH.Single.Data
  ( singDataD
  , singCtor
  ) where

import Language.Haskell.TH.Desugar as Desugar
import Language.Haskell.TH.Syntax
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import Data.Maybe
import Data.Traversable (mapAccumL)
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Single.Defun
import Data.Singletons.TH.Single.Fixity
import Data.Singletons.TH.Single.Monad
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Control.Monad

-- 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 DataFlavor
df Name
name [DTyVarBndrVis]
tvbs [DCon]
ctors) = do
  Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let reqTvbNames :: [Name]
reqTvbNames   = (DTyVarBndrVis -> Name) -> [DTyVarBndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName ([DTyVarBndrVis] -> [Name]) -> [DTyVarBndrVis] -> [Name]
forall a b. (a -> b) -> a -> b
$
                      (DTyVarBndrVis -> Bool) -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. (a -> Bool) -> [a] -> [a]
filter (\DTyVarBndrVis
tvb -> DTyVarBndrVis -> BndrVis
forall flag. DTyVarBndr flag -> flag
extractTvbFlag DTyVarBndrVis
tvb BndrVis -> BndrVis -> Bool
forall a. Eq a => a -> a -> Bool
== BndrVis
BndrReq) [DTyVarBndrVis]
tvbs
      ctor_names :: [Name]
ctor_names    = (DCon -> Name) -> [DCon] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DCon -> Name
extractName [DCon]
ctors
      rec_sel_names :: [Name]
rec_sel_names = (DCon -> [Name]) -> [DCon] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DCon -> [Name]
extractRecSelNames [DCon]
ctors
  DKind
k <- DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType (DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
name) [DTyVarBndrVis]
tvbs)
  Maybe DKind
mb_data_sak <- Name -> SgM (Maybe DKind)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DKind)
dsReifyType Name
name
  [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name -> DCon -> SgM DCon
singCtor Name
name) [DCon]
ctors
  [DDec]
fixityDecs <- [Name] -> SgM [DDec]
forall (q :: * -> *). OptionsMonad q => [Name] -> q [DDec]
singReifiedInfixDecls ([Name] -> SgM [DDec]) -> [Name] -> SgM [DDec]
forall a b. (a -> b) -> a -> b
$ [Name]
ctor_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
rec_sel_names
  -- 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM DCon -> SgM DClause
mkToSingClause [DCon]
ctors
  DClause
emptyToSingClause   <- SgM DClause
mkEmptyToSingClause
  let singKindInst :: DDec
singKindInst =
        Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                   ((Name -> DKind) -> [Name] -> DCxt
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]
reqTvbNames)
                   (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 [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                      (Name -> DKind
DConT Name
demoteName DKind -> DKind -> DKind
`DAppT` DKind
k)
                      (DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
name)
                        ((Name -> DKind) -> [Name] -> DCxt
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]
reqTvbNames))
                   , 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 = Options -> Name -> Name
singledDataTypeName Options
opts 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 [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                                (Name -> DKind
DConT Name
singFamilyName DKind -> DKind -> DKind
`DAppKindT` DKind
k)
                                (Name -> DKind
DConT Name
singDataName)

      -- Note that we always include an explicit result kind in the body of the
      -- singleton data type declaration, even if it has a standalone kind
      -- signature that would make this explicit result kind redudant.
      -- See Note [Keep redundant kind information for Haddocks]
      -- in D.S.TH.Promote.
      mk_data_dec :: DKind -> DDec
mk_data_dec DKind
kind =
        DataFlavor
-> DCxt
-> Name
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD DataFlavor
Data [] Name
singDataName [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
kind) [DCon]
ctors' []

  [DDec]
data_decs <- case Maybe DKind
mb_data_sak of
    -- No standalone kind signature. Try to figure out the order of kind
    -- variables on a best-effort basis.
    Maybe DKind
Nothing -> do
      let sing_tvbs :: [DTyVarBndr Specificity]
sing_tvbs = Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndrUnit] -> [DTyVarBndr Specificity])
-> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$
                      DCxt -> [DTyVarBndrUnit]
toposortTyVarsOf (DCxt -> [DTyVarBndrUnit]) -> DCxt -> [DTyVarBndrUnit]
forall a b. (a -> b) -> a -> b
$ (DTyVarBndrVis -> DKind) -> [DTyVarBndrVis] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> DKind
forall flag. DTyVarBndr flag -> DKind
dTyVarBndrToDType [DTyVarBndrVis]
tvbs
          kinded_sing_ty :: DKind
kinded_sing_ty = DForallTelescope -> DKind -> DKind
DForallT ([DTyVarBndr Specificity] -> DForallTelescope
DForallInvis [DTyVarBndr Specificity]
sing_tvbs) (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 a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [DKind -> DDec
mk_data_dec DKind
kinded_sing_ty]

    -- A standalone kind signature is provided, so use that to determine the
    -- order of kind variables.
    Just DKind
data_sak -> do
      DKind
sing_data_sak <- DKind -> [DTyVarBndrVis] -> DKind -> SgM DKind
forall (q :: * -> *).
MonadFail q =>
DKind -> [DTyVarBndrVis] -> DKind -> q DKind
singDataSAK DKind
data_sak [DTyVarBndrVis]
tvbs DKind
k
      [DDec] -> SgM [DDec]
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Name -> DKind -> DDec
DKiSigD Name
singDataName DKind
sing_data_sak
           , DKind -> DDec
mk_data_dec DKind
sing_data_sak
           ]

  [DDec] -> SgM [DDec]
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
forall a b. (a -> b) -> a -> b
$ [DDec]
data_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
           DDec
singSynInst DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:
           [ DDec
singKindInst | Options -> Bool
genSingKindInsts Options
opts
                          , -- `type data` data constructors only exist at the
                            -- type level. As such, we cannot define SingKind
                            -- instances for them, as they require term-level
                            -- data constructors to implement.
                            DataFlavor
df DataFlavor -> DataFlavor -> Bool
forall a. Eq a => a -> a -> Bool
/= DataFlavor
Desugar.TypeData
                          ] [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++
           [DDec]
fixityDecs
  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 a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return

        mkFromSingClause :: DCon -> SgM DClause
        mkFromSingClause :: DCon -> SgM DClause
mkFromSingClause DCon
c = do
          Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
          let (Name
cname, 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 String
"b")
          DClause -> SgM DClause
forall a. a -> SgM a
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 -> DCxt -> [DPat] -> DPat
DConP (Options -> Name -> Name
singledDataConName Options
opts 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 [DTyVarBndr Specificity]
_tvbs DCxt
_cxt Name
cname DConFields
fields DKind
_rty) = do
          Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
          let types :: DCxt
types = DConFields -> DCxt
tysOfConFields DConFields
fields
          [Name]
varNames  <- (DKind -> SgM Name) -> DCxt -> SgM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 String
"b") DCxt
types
          [Name]
svarNames <- (DKind -> SgM Name) -> DCxt -> SgM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 String
"c") DCxt
types
          DCxt
promoted  <- (DKind -> SgM DKind) -> DCxt -> SgM DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType DCxt
types
          Name
cname' <- Name -> SgM Name
mkConName Name
cname
          let varPats :: [DPat]
varPats        = (Name -> DKind -> DPat) -> [Name] -> DCxt -> [DPat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DPat
mkToSingVarPat [Name]
varNames DCxt
promoted
              recursiveCalls :: [DExp]
recursiveCalls = (Name -> DKind -> DExp) -> [Name] -> DCxt -> [DExp]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> DKind -> DExp
mkRecursiveCall [Name]
varNames DCxt
promoted
          DClause -> SgM DClause
forall a. a -> SgM a
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 -> DCxt -> [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 -> DCxt -> [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 (Options -> Name -> Name
singledDataConName Options
opts 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 Name
varName 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 Name
var_name 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 String
"x"
          DClause -> SgM DClause
forall a. a -> SgM a
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 String
"x"
          DClause -> SgM DClause
forall a. a -> SgM a
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) []

-- Single 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 Name
dataName (DCon [DTyVarBndr Specificity]
con_tvbs DCxt
cxt Name
name DConFields
fields DKind
rty)
  | Bool -> Bool
not (DCxt -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null DCxt
cxt)
  = String -> SgM DCon
forall a. String -> SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Singling of constrained constructors not yet supported"
  | Bool
otherwise
  = do
  Options
opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let types :: DCxt
types = DConFields -> DCxt
tysOfConFields DConFields
fields
      numTypes :: Int
numTypes = DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
types
      sName :: Name
sName = Options -> Name -> Name
singledDataConName Options
opts Name
name
      sCon :: DExp
sCon = Name -> DExp
DConE Name
sName
      pCon :: DKind
pCon = Name -> DKind
DConT (Name -> DKind) -> Name -> DKind
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
  DKind -> SgM ()
forall (m :: * -> *). MonadFail m => DKind -> m ()
checkVanillaDType (DKind -> SgM ()) -> DKind -> SgM ()
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr Specificity] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndr Specificity]
con_tvbs [] DCxt
types DKind
rty
  [Name]
indexNames <- (DKind -> SgM Name) -> DCxt -> SgM [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 String
"n") DCxt
types
  DCxt
kinds <- (DKind -> SgM DKind) -> DCxt -> SgM DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DCxt
types
  DKind
rty' <- DKind -> SgM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DKind
rty
  let indices :: DCxt
indices = (Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
indexNames
      kindedIndices :: DCxt
kindedIndices = (DKind -> DKind -> DKind) -> DCxt -> DCxt -> DCxt
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DKind -> DKind -> DKind
DSigT DCxt
indices DCxt
kinds
      -- The approach we use for singling data constructor types differs
      -- slightly from the approach taken in D.S.TH.Single.Type.singType in that
      -- we always explicitly quantify all type variables in a singled data
      -- constructor, regardless of whether the original data constructor
      -- explicitly quantified them or not. This explains the use of
      -- toposortTyVarsOf below.
      -- See Note [Preserve the order of type variables during singling]
      -- (wrinkle 1) in D.S.TH.Single.Type.
      kvbs :: [DTyVarBndr Specificity]
kvbs | [DTyVarBndr Specificity] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndr Specificity]
con_tvbs
           = Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec (DCxt -> [DTyVarBndrUnit]
toposortTyVarsOf (DCxt
kinds DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DKind
rty'])) [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++
             [DTyVarBndr Specificity]
con_tvbs
           | Bool
otherwise
           = [DTyVarBndr Specificity]
con_tvbs
      all_tvbs :: [DTyVarBndr Specificity]
all_tvbs = [DTyVarBndr Specificity]
kvbs [DTyVarBndr Specificity]
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. [a] -> [a] -> [a]
++ (Name -> DKind -> DTyVarBndr Specificity)
-> [Name] -> DCxt -> [DTyVarBndr Specificity]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> Specificity -> DKind -> DTyVarBndr Specificity
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
`DKindedTV` Specificity
SpecifiedSpec) [Name]
indexNames DCxt
kinds

  -- @mb_SingI_dec k@ returns 'Just' an instance of @SingI<k>@ if @k@ is
  -- less than or equal to the number of fields in the data constructor.
  -- Otherwise, it returns 'Nothing'.
  let mb_SingI_dec :: Int -> Maybe DDec
      mb_SingI_dec :: Int -> Maybe DDec
mb_SingI_dec Int
k
        | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
numTypes
        = let take_until_k :: [a] -> [a]
take_until_k = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take (Int
numTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) in
          DDec -> Maybe DDec
forall a. a -> Maybe a
Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                   ((DKind -> DKind) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT Name
singIName)) (DCxt -> DCxt
forall {a}. [a] -> [a]
take_until_k DCxt
indices))
                   (DKind -> DKind -> DKind
DAppT (Name -> DKind
DConT (Int -> Name
mkSingIName Int
k))
                          (DKind -> DCxt -> DKind
foldType DKind
pCon (DCxt -> DCxt
forall {a}. [a] -> [a]
take_until_k DCxt
kindedIndices)))
                   [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP (Int -> Name
mkSingMethName Int
k))
                          (DExp -> [DExp] -> DExp
foldExp DExp
sCon (Int -> DExp -> [DExp]
forall a. Int -> a -> [a]
replicate (Int
numTypes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k) (Name -> DExp
DVarE Name
singMethName)))]
        | Bool
otherwise
        = Maybe DDec
forall a. Maybe a
Nothing

  -- SingI instance for data constructor
  [DDec] -> SgM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> SgM ()) -> [DDec] -> SgM ()
forall a b. (a -> b) -> a -> b
$ (Int -> Maybe DDec) -> [Int] -> [DDec]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Int -> Maybe DDec
mb_SingI_dec [Int
0, Int
1, Int
2]
  -- 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 -> DCxt -> [Maybe DKind] -> Maybe DKind -> SgM [DDec]
singDefuns Name
name NameSpace
DataName [] ((DKind -> Maybe DKind) -> DCxt -> [Maybe DKind]
forall a b. (a -> b) -> [a] -> [b]
map DKind -> Maybe DKind
forall a. a -> Maybe a
Just DCxt
kinds) (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
rty')

  DConFields
conFields <- case DConFields
fields of
    DNormalC Bool
dInfix [DBangType]
bts -> Bool -> [DBangType] -> DConFields
DNormalC Bool
dInfix ([DBangType] -> DConFields) -> SgM [DBangType] -> SgM DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                           (DBangType -> DKind -> SgM DBangType)
-> [DBangType] -> DCxt -> SgM [DBangType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Bang
b, DKind
_) DKind
index -> Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index)
                                    [DBangType]
bts DCxt
indices
    DRecC [DVarBangType]
vbts          -> Bool -> [DBangType] -> DConFields
DNormalC Bool
False ([DBangType] -> DConFields) -> SgM [DBangType] -> SgM DConFields
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                           (DVarBangType -> DKind -> SgM DBangType)
-> [DVarBangType] -> DCxt -> SgM [DBangType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\(Name
_, Bang
b, DKind
_) DKind
index -> Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index)
                                    [DVarBangType]
vbts DCxt
indices
                      -- Don't bother looking at record selectors, as they are
                      -- handled separately in singTopLevelDecs.
                      -- See Note [singletons-th and record selectors]
  DCon -> SgM DCon
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return (DCon -> SgM DCon) -> DCon -> SgM DCon
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr Specificity]
-> DCxt -> Name -> DConFields -> DKind -> DCon
DCon [DTyVarBndr Specificity]
all_tvbs [] Name
sName DConFields
conFields
                (Name -> DKind
DConT (Options -> Name -> Name
singledDataTypeName Options
opts Name
dataName) DKind -> DKind -> DKind
`DAppT`
                  (DKind -> DCxt -> DKind
foldType DKind
pCon DCxt
indices DKind -> DKind -> DKind
`DSigT` DKind
rty'))
                  -- Make sure to include an explicit `rty'` kind annotation.
                  -- See Note [Preserve the order of type variables during singling],
                  -- wrinkle 3, in D.S.TH.Single.Type.
  where
    mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
    mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness SourceUnpackedness
su = case SourceUnpackedness
su of
      SourceUnpackedness
NoSourceUnpackedness -> SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
su
      SourceUnpackedness
SourceNoUnpack       -> SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
su
      SourceUnpackedness
SourceUnpack         -> do
        -- {-# UNPACK #-} is essentially useless in a singletons setting, since
        -- all singled data types are GADTs. See GHC#10016.
        String -> SgM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning String
"{-# UNPACK #-} pragmas are ignored by `singletons-th`."
        SourceUnpackedness -> SgM SourceUnpackedness
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SourceUnpackedness
NoSourceUnpackedness

    mk_bang :: Bang -> SgM Bang
    mk_bang :: Bang -> SgM Bang
mk_bang (Bang SourceUnpackedness
su SourceStrictness
ss) = do SourceUnpackedness
su' <- SourceUnpackedness -> SgM SourceUnpackedness
mk_source_unpackedness SourceUnpackedness
su
                              Bang -> SgM Bang
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bang -> SgM Bang) -> Bang -> SgM Bang
forall a b. (a -> b) -> a -> b
$ SourceUnpackedness -> SourceStrictness -> Bang
Bang SourceUnpackedness
su' SourceStrictness
ss

    mk_bang_type :: Bang -> DType -> SgM DBangType
    mk_bang_type :: Bang -> DKind -> SgM DBangType
mk_bang_type Bang
b DKind
index = do Bang
b' <- Bang -> SgM Bang
mk_bang Bang
b
                              DBangType -> SgM DBangType
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bang
b', DKind -> DKind -> DKind
DAppT DKind
singFamily DKind
index)

-- @'singDataSAK' sak data_bndrs@ produces a standalone kind signature for a
-- singled data declaration, using the original data type's standalone kind
-- signature (@sak@) and its user-written binders (@data_bndrs@) as a template.
-- For this example:
--
-- @
-- type D :: forall j k. k -> j -> Type
-- data D @j @l (a :: l) b = ...
-- @
--
-- We would produce the following standalone kind signature:
--
-- @
-- type SD :: forall j l (a :: l) (b :: j). D @j @l (a :: l) b -> Type
-- @
--
-- Note that:
--
-- * This function has a precondition that the length of @data_bndrs@ must
--   always be equal to the number of visible quantifiers (i.e., the number of
--   function arrows plus the number of visible @forall@–bound variables) in
--   @sak@. @singletons-th@ maintains this invariant when constructing a
--   'DataDecl' (see the 'buildDataDTvbs' function).
--
-- * The order of the invisible quantifiers is preserved, so both
--   @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would
--   expect it to.
--
-- * Whenever possible, this function reuses type variable names from the data
--   type's user-written binders. This is why the standalone kind signature uses
--   @forall j l@ instead of @forall j k@, since the @(a :: l)@ binder uses @l@
--   instead of @k@. We could have just as well chose the other way around, but
--   we chose to pick variable names from the data type binders since they scope
--   over other parts of the data type declaration (e.g., in @deriving@
--   clauses), so keeping these names avoids having to perform some
--   alpha-renaming.
singDataSAK ::
     MonadFail q
  => DKind
     -- ^ The standalone kind signature for the original data type
  -> [DTyVarBndrVis]
     -- ^ The user-written binders for the original data type
  -> DKind
     -- ^ The original data type, promoted to a kind
  -> q DKind
     -- ^ The standalone kind signature for the singled data type
singDataSAK :: forall (q :: * -> *).
MonadFail q =>
DKind -> [DTyVarBndrVis] -> DKind -> q DKind
singDataSAK DKind
data_sak [DTyVarBndrVis]
data_bndrs DKind
data_k = do
  -- (1) First, explicitly quantify any free kind variables in `data_sak` using
  -- an invisible @forall@. This is done to ensure that precondition (2) in
  -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function).
  let data_sak_free_tvbs :: [DTyVarBndr Specificity]
data_sak_free_tvbs =
        Specificity -> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndrUnit] -> [DTyVarBndr Specificity])
-> [DTyVarBndrUnit] -> [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ DCxt -> [DTyVarBndrUnit]
toposortTyVarsOf [DKind
data_sak]
      data_sak' :: DKind
data_sak' = DForallTelescope -> DKind -> DKind
DForallT ([DTyVarBndr Specificity] -> DForallTelescope
DForallInvis [DTyVarBndr Specificity]
data_sak_free_tvbs) DKind
data_sak

  -- (2) Next, compute type variable binders for the singled data type's
  -- standalone kind signature using `matchUpSigWithDecl`. Note that these can
  -- be biased towards type variable names mention in `data_sak` over names
  -- mentioned in `data_bndrs`, but we will fix that up in the next step.
  let (DFunArgs
data_sak_args, DKind
_) = DKind -> (DFunArgs, DKind)
unravelDType DKind
data_sak'
  [DTyVarBndr Specificity]
sing_sak_tvbs <- DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
forall (q :: * -> *).
MonadFail q =>
DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
matchUpSigWithDecl DFunArgs
data_sak_args [DTyVarBndrVis]
data_bndrs

  -- (3) Swizzle the type variable names so that names in `data_bndrs` are
  -- preferred over names in `data_sak`.
  --
  -- This is heavily inspired by similar code in GHC:
  -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616
  let invis_data_sak_args :: [DTyVarBndr Specificity]
invis_data_sak_args = DFunArgs -> [DTyVarBndr Specificity]
filterInvisTvbArgs DFunArgs
data_sak_args
      invis_data_sak_arg_nms :: [Name]
invis_data_sak_arg_nms = (DTyVarBndr Specificity -> Name)
-> [DTyVarBndr Specificity] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr Specificity -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndr Specificity]
invis_data_sak_args

      invis_data_bndrs :: [DTyVarBndrUnit]
invis_data_bndrs = [DTyVarBndrVis] -> [DTyVarBndrUnit]
forall flag. [DTyVarBndr flag] -> [DTyVarBndrUnit]
toposortKindVarsOfTvbs [DTyVarBndrVis]
data_bndrs
      invis_data_bndr_nms :: [Name]
invis_data_bndr_nms = (DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndrUnit]
invis_data_bndrs

      swizzle_env :: Map Name Name
swizzle_env =
        [(Name, Name)] -> Map Name Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, Name)] -> Map Name Name)
-> [(Name, Name)] -> Map Name Name
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name] -> [(Name, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
invis_data_sak_arg_nms [Name]
invis_data_bndr_nms
      (DSubst
_, [DTyVarBndr Specificity]
swizzled_sing_sak_tvbs) =
        (DSubst
 -> DTyVarBndr Specificity -> (DSubst, DTyVarBndr Specificity))
-> DSubst
-> [DTyVarBndr Specificity]
-> (DSubst, [DTyVarBndr Specificity])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (Map Name Name
-> DSubst
-> DTyVarBndr Specificity
-> (DSubst, DTyVarBndr Specificity)
swizzleTvb Map Name Name
swizzle_env) DSubst
forall k a. Map k a
Map.empty [DTyVarBndr Specificity]
sing_sak_tvbs

  -- (4) Finally, construct the kind of the singled data type.
  DKind -> q DKind
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DKind -> q DKind) -> DKind -> q DKind
forall a b. (a -> b) -> a -> b
$ DForallTelescope -> DKind -> DKind
DForallT ([DTyVarBndr Specificity] -> DForallTelescope
DForallInvis [DTyVarBndr Specificity]
swizzled_sing_sak_tvbs)
       (DKind -> DKind) -> DKind -> DKind
forall a b. (a -> b) -> a -> b
$ DKind
DArrowT DKind -> DKind -> DKind
`DAppT` DKind
data_k DKind -> DKind -> DKind
`DAppT` Name -> DKind
DConT Name
typeKindName

-- Match the quantifiers in a data type's standalone kind signature with the
-- binders in the data type declaration. This function assumes the following
-- preconditions:
--
-- 1. The number of required binders in the data type declaration is equal to
--    the number of visible quantifiers (i.e., the number of function arrows
--    plus the number of visible @forall@–bound variables) in the standalone
--    kind signature.
--
-- 2. The number of invisible \@-binders in the data type declaration is less
--    than or equal to the number of invisible quantifiers (i.e., the number of
--    invisible @forall@–bound variables) in the standalone kind signature.
--
-- The implementation of this function is heavily based on a GHC function of
-- the same name:
-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2645-2715
matchUpSigWithDecl ::
     forall q.
     MonadFail q
  => DFunArgs
     -- ^ The quantifiers in the data type's standalone kind signature
  -> [DTyVarBndrVis]
     -- ^ The user-written binders in the data type declaration
  -> q [DTyVarBndrSpec]
matchUpSigWithDecl :: forall (q :: * -> *).
MonadFail q =>
DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
matchUpSigWithDecl = DSubst -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
go_fun_args DSubst
forall k a. Map k a
Map.empty
  where
    go_fun_args ::
         DSubst
         -- ^ A substitution from the names of @forall@-bound variables in the
         -- standalone kind signature to corresponding binder names in the
         -- user-written binders. (See the Haddocks for `singDataSAK` for an
         -- explanation of why we perform this substitution.) For example:
         --
         -- @
         -- type T :: forall a. forall b -> Maybe (a, b) -> Type
         -- data T @x y z
         -- @
         --
         -- After matching up the @a@ in @forall a.@ with @x@ and
         -- the @b@ in @forall b ->@ with @y@, this substitution will be
         -- extended with @[a :-> x, b :-> y]@. This ensures that we will
         -- produce @Maybe (x, y)@ instead of @Maybe (a, b)@ in
         -- the kind for @z@.
      -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec]
    go_fun_args :: DSubst -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
go_fun_args DSubst
_ DFunArgs
DFANil [] =
      [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    -- This should not happen, per the function's precondition
    go_fun_args DSubst
_ DFunArgs
DFANil [DTyVarBndrVis]
data_bndrs =
      String -> q [DTyVarBndr Specificity]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q [DTyVarBndr Specificity])
-> String -> q [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ String
"matchUpSigWithDecl.go_fun_args: Too many binders: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrVis] -> String
forall a. Show a => a -> String
show [DTyVarBndrVis]
data_bndrs
    -- GHC now disallows kind-level constraints, per this GHC proposal:
    -- https://github.com/ghc-proposals/ghc-proposals/blob/b0687d96ce8007294173b7f628042ac4260cc738/proposals/0547-no-kind-equalities.rst
    go_fun_args DSubst
_ (DFACxt{}) [DTyVarBndrVis]
_ =
      String -> q [DTyVarBndr Specificity]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"matchUpSigWithDecl.go_fun_args: Unexpected kind-level constraint"
    go_fun_args DSubst
subst (DFAForalls (DForallInvis [DTyVarBndr Specificity]
tvbs) DFunArgs
sig_args) [DTyVarBndrVis]
data_bndrs =
      DSubst
-> [DTyVarBndr Specificity]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_invis_tvbs DSubst
subst [DTyVarBndr Specificity]
tvbs DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
    go_fun_args DSubst
subst (DFAForalls (DForallVis [DTyVarBndrUnit]
tvbs) DFunArgs
sig_args) [DTyVarBndrVis]
data_bndrs =
      DSubst
-> [DTyVarBndrUnit]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_vis_tvbs DSubst
subst [DTyVarBndrUnit]
tvbs DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
    go_fun_args DSubst
subst (DFAAnon DKind
anon DFunArgs
sig_args) (DTyVarBndrVis
data_bndr:[DTyVarBndrVis]
data_bndrs) = do
      let data_bndr_name :: Name
data_bndr_name = DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrVis
data_bndr
          mb_data_bndr_kind :: Maybe DKind
mb_data_bndr_kind = DTyVarBndrVis -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrVis
data_bndr
          anon' :: DKind
anon' = DSubst -> DKind -> DKind
substType DSubst
subst DKind
anon

          anon'' :: DKind
anon'' =
            case Maybe DKind
mb_data_bndr_kind of
              Maybe DKind
Nothing -> DKind
anon'
              Just DKind
data_bndr_kind ->
                let mb_match_subst :: Maybe DSubst
mb_match_subst = IgnoreKinds -> DKind -> DKind -> Maybe DSubst
matchTy IgnoreKinds
NoIgnore DKind
data_bndr_kind DKind
anon' in
                DKind -> (DSubst -> DKind) -> Maybe DSubst -> DKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DKind
data_bndr_kind (DSubst -> DKind -> DKind
`substType` DKind
data_bndr_kind) Maybe DSubst
mb_match_subst
      [DTyVarBndr Specificity]
sig_args' <- DSubst -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
go_fun_args DSubst
subst DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
      [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr Specificity] -> q [DTyVarBndr Specificity])
-> [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ Name -> Specificity -> DKind -> DTyVarBndr Specificity
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
data_bndr_name Specificity
SpecifiedSpec DKind
anon'' DTyVarBndr Specificity
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. a -> [a] -> [a]
: [DTyVarBndr Specificity]
sig_args'
    -- This should not happen, per precondition (1).
    go_fun_args DSubst
_ DFunArgs
_ [] =
      String -> q [DTyVarBndr Specificity]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"matchUpSigWithDecl.go_fun_args: Too few binders"

    go_invis_tvbs :: DSubst -> [DTyVarBndrSpec] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec]
    go_invis_tvbs :: DSubst
-> [DTyVarBndr Specificity]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_invis_tvbs DSubst
subst [] DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs =
      DSubst -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
go_fun_args DSubst
subst DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
    -- This should not happen, per precondition (2).
    go_invis_tvbs DSubst
_ (DTyVarBndr Specificity
_:[DTyVarBndr Specificity]
_) DFunArgs
_ [] =
      String -> q [DTyVarBndr Specificity]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q [DTyVarBndr Specificity])
-> String -> q [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ String
"matchUpSigWithDecl.go_invis_tvbs: Too few binders"
    go_invis_tvbs DSubst
subst (DTyVarBndr Specificity
invis_tvb:[DTyVarBndr Specificity]
invis_tvbs) DFunArgs
sig_args data_bndrss :: [DTyVarBndrVis]
data_bndrss@(DTyVarBndrVis
data_bndr:[DTyVarBndrVis]
data_bndrs) =
      case DTyVarBndrVis -> BndrVis
forall flag. DTyVarBndr flag -> flag
extractTvbFlag DTyVarBndrVis
data_bndr of
        -- If the next data_bndr is required, then we have a invisible forall in
        -- the kind without a corresponding invisible @-binder, which is
        -- allowed. In this case, we simply apply the substitution and recurse.
        BndrVis
BndrReq -> do
          let (DSubst
subst', DTyVarBndr Specificity
invis_tvb') = DSubst
-> DTyVarBndr Specificity -> (DSubst, DTyVarBndr Specificity)
forall flag. DSubst -> DTyVarBndr flag -> (DSubst, DTyVarBndr flag)
substTvb DSubst
subst DTyVarBndr Specificity
invis_tvb
          [DTyVarBndr Specificity]
sig_args' <- DSubst
-> [DTyVarBndr Specificity]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_invis_tvbs DSubst
subst' [DTyVarBndr Specificity]
invis_tvbs DFunArgs
sig_args [DTyVarBndrVis]
data_bndrss
          [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr Specificity] -> q [DTyVarBndr Specificity])
-> [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ DTyVarBndr Specificity
invis_tvb' DTyVarBndr Specificity
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. a -> [a] -> [a]
: [DTyVarBndr Specificity]
sig_args'
        -- If the next data_bndr is an invisible @-binder, then we must match it
        -- against the invisible forall–bound variable in the kind.
        BndrVis
BndrInvis -> do
          let (DSubst
subst', DTyVarBndr Specificity
sig_tvb) = DSubst
-> DTyVarBndr Specificity
-> DTyVarBndrVis
-> (DSubst, DTyVarBndr Specificity)
forall flag.
DSubst
-> DTyVarBndr flag
-> DTyVarBndrVis
-> (DSubst, DTyVarBndr Specificity)
match_tvbs DSubst
subst DTyVarBndr Specificity
invis_tvb DTyVarBndrVis
data_bndr
          [DTyVarBndr Specificity]
sig_args' <- DSubst
-> [DTyVarBndr Specificity]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_invis_tvbs DSubst
subst' [DTyVarBndr Specificity]
invis_tvbs DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
          [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DTyVarBndr Specificity
sig_tvb DTyVarBndr Specificity
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. a -> [a] -> [a]
: [DTyVarBndr Specificity]
sig_args')

    go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec]
    go_vis_tvbs :: DSubst
-> [DTyVarBndrUnit]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_vis_tvbs DSubst
subst [] DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs =
      DSubst -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr Specificity]
go_fun_args DSubst
subst DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
    -- This should not happen, per precondition (1).
    go_vis_tvbs DSubst
_ (DTyVarBndrUnit
_:[DTyVarBndrUnit]
_) DFunArgs
_ [] =
      String -> q [DTyVarBndr Specificity]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q [DTyVarBndr Specificity])
-> String -> q [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ String
"matchUpSigWithDecl.go_vis_tvbs: Too few binders"
    go_vis_tvbs DSubst
subst (DTyVarBndrUnit
vis_tvb:[DTyVarBndrUnit]
vis_tvbs) DFunArgs
sig_args (DTyVarBndrVis
data_bndr:[DTyVarBndrVis]
data_bndrs) = do
      case DTyVarBndrVis -> BndrVis
forall flag. DTyVarBndr flag -> flag
extractTvbFlag DTyVarBndrVis
data_bndr of
        -- If the next data_bndr is required, then we must match it against the
        -- visible forall–bound variable in the kind.
        BndrVis
BndrReq -> do
          let (DSubst
subst', DTyVarBndr Specificity
sig_tvb) = DSubst
-> DTyVarBndrUnit
-> DTyVarBndrVis
-> (DSubst, DTyVarBndr Specificity)
forall flag.
DSubst
-> DTyVarBndr flag
-> DTyVarBndrVis
-> (DSubst, DTyVarBndr Specificity)
match_tvbs DSubst
subst DTyVarBndrUnit
vis_tvb DTyVarBndrVis
data_bndr
          [DTyVarBndr Specificity]
sig_args' <- DSubst
-> [DTyVarBndrUnit]
-> DFunArgs
-> [DTyVarBndrVis]
-> q [DTyVarBndr Specificity]
go_vis_tvbs DSubst
subst' [DTyVarBndrUnit]
vis_tvbs DFunArgs
sig_args [DTyVarBndrVis]
data_bndrs
          [DTyVarBndr Specificity] -> q [DTyVarBndr Specificity]
forall a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DTyVarBndr Specificity
sig_tvb DTyVarBndr Specificity
-> [DTyVarBndr Specificity] -> [DTyVarBndr Specificity]
forall a. a -> [a] -> [a]
: [DTyVarBndr Specificity]
sig_args')
        -- We have a visible forall in the kind, but an invisible @-binder as
        -- the next data_bndr. This is ill kinded, so throw an error.
        BndrVis
BndrInvis ->
          String -> q [DTyVarBndr Specificity]
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q [DTyVarBndr Specificity])
-> String -> q [DTyVarBndr Specificity]
forall a b. (a -> b) -> a -> b
$ String
"matchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: "
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ DTyVarBndrVis -> String
forall a. Show a => a -> String
show DTyVarBndrVis
data_bndr

    -- @match_tvbs subst sig_tvb data_bndr@ will match the kind of @data_bndr@
    -- against the kind of @sig_tvb@ to produce a new kind. This function
    -- produces two values as output:
    --
    -- 1. A new @subst@ that has been extended such that the name of @sig_tvb@
    --    maps to the name of @data_bndr@. (See the Haddocks for the 'DSubst'
    --    argument to @go_fun_args@ for an explanation of why we do this.)
    --
    -- 2. A 'DTyVarBndrSpec' that has the name of @data_bndr@, but with the new
    --    kind resulting from matching.
    match_tvbs :: DSubst -> DTyVarBndr flag -> DTyVarBndrVis -> (DSubst, DTyVarBndrSpec)
    match_tvbs :: forall flag.
DSubst
-> DTyVarBndr flag
-> DTyVarBndrVis
-> (DSubst, DTyVarBndr Specificity)
match_tvbs DSubst
subst DTyVarBndr flag
sig_tvb DTyVarBndrVis
data_bndr =
      let data_bndr_name :: Name
data_bndr_name = DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrVis
data_bndr
          mb_data_bndr_kind :: Maybe DKind
mb_data_bndr_kind = DTyVarBndrVis -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrVis
data_bndr

          sig_tvb_name :: Name
sig_tvb_name = DTyVarBndr flag -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndr flag
sig_tvb
          mb_sig_tvb_kind :: Maybe DKind
mb_sig_tvb_kind = DSubst -> DKind -> DKind
substType DSubst
subst (DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DTyVarBndr flag -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndr flag
sig_tvb

          mb_kind :: Maybe DKind
          mb_kind :: Maybe DKind
mb_kind =
            case (Maybe DKind
mb_data_bndr_kind, Maybe DKind
mb_sig_tvb_kind) of
              (Maybe DKind
Nothing,             Maybe DKind
Nothing)           -> Maybe DKind
forall a. Maybe a
Nothing
              (Just DKind
data_bndr_kind, Maybe DKind
Nothing)           -> DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
data_bndr_kind
              (Maybe DKind
Nothing,             Just DKind
sig_tvb_kind) -> DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sig_tvb_kind
              (Just DKind
data_bndr_kind, Just DKind
sig_tvb_kind) -> do
                DSubst
match_subst <- IgnoreKinds -> DKind -> DKind -> Maybe DSubst
matchTy IgnoreKinds
NoIgnore DKind
data_bndr_kind DKind
sig_tvb_kind
                DKind -> Maybe DKind
forall a. a -> Maybe a
Just (DKind -> Maybe DKind) -> DKind -> Maybe DKind
forall a b. (a -> b) -> a -> b
$ DSubst -> DKind -> DKind
substType DSubst
match_subst DKind
data_bndr_kind

          subst' :: DSubst
subst' = Name -> DKind -> DSubst -> DSubst
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
sig_tvb_name (Name -> DKind
DVarT Name
data_bndr_name) DSubst
subst
          sig_tvb' :: DTyVarBndr Specificity
sig_tvb' = case Maybe DKind
mb_kind of
            Maybe DKind
Nothing   -> Name -> Specificity -> DTyVarBndr Specificity
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV  Name
data_bndr_name Specificity
SpecifiedSpec
            Just DKind
kind -> Name -> Specificity -> DKind -> DTyVarBndr Specificity
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
data_bndr_name Specificity
SpecifiedSpec DKind
kind in

      (DSubst
subst', DTyVarBndr Specificity
sig_tvb')

-- This is heavily inspired by the `swizzleTcb` function in GHC:
-- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2741-2755
swizzleTvb :: Map Name Name -> DSubst -> DTyVarBndrSpec -> (DSubst, DTyVarBndrSpec)
swizzleTvb :: Map Name Name
-> DSubst
-> DTyVarBndr Specificity
-> (DSubst, DTyVarBndr Specificity)
swizzleTvb Map Name Name
swizzle_env DSubst
subst DTyVarBndr Specificity
tvb =
  (DSubst
subst', DTyVarBndr Specificity
tvb2)
  where
    subst' :: DSubst
subst' = Name -> DKind -> DSubst -> DSubst
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
tvb_name (Name -> DKind
DVarT (DTyVarBndr Specificity -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndr Specificity
tvb2)) DSubst
subst
    tvb_name :: Name
tvb_name = DTyVarBndr Specificity -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndr Specificity
tvb
    tvb1 :: DTyVarBndr Specificity
tvb1 = (DKind -> DKind)
-> DTyVarBndr Specificity -> DTyVarBndr Specificity
forall flag. (DKind -> DKind) -> DTyVarBndr flag -> DTyVarBndr flag
mapDTVKind (DSubst -> DKind -> DKind
substType DSubst
subst) DTyVarBndr Specificity
tvb
    tvb2 :: DTyVarBndr Specificity
tvb2 =
      case Name -> Map Name Name -> Maybe Name
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
tvb_name Map Name Name
swizzle_env of
        Just Name
user_name -> (Name -> Name) -> DTyVarBndr Specificity -> DTyVarBndr Specificity
forall flag. (Name -> Name) -> DTyVarBndr flag -> DTyVarBndr flag
mapDTVName (Name -> Name -> Name
forall a b. a -> b -> a
const Name
user_name) DTyVarBndr Specificity
tvb1
        Maybe Name
Nothing        -> DTyVarBndr Specificity
tvb1

{-
Note [singletons-th and record selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Record selectors are annoying to deal with in singletons-th for various reasons:

1. There is no record syntax at the type level, so promoting code that involves
   records in some way is not straightforward.
2. One can define record selectors for singled data types, but they're rife
   with peril. Some pitfalls include:

   * Singling record updates often produces code that does not typecheck. For
     example, this works:

       let i = Identity True in i { runIdentity = False }

     But this does /not/ work:

       let si = SIdentity STrue in si { sRunIdentity = SFalse }

       error:
           • Record update for insufficiently polymorphic field:
               sRunIdentity :: Sing n
           • In the expression: si {sRunIdentity = SFalse}
             In the expression:
               let si = SIdentity STrue in si {sRunIdentity = SFalse}

     Ugh. See GHC#16501.

   * Singling a data type with multiple constructors that share a record
     selector name will /also/ not typecheck. While this works:

       data X = X1 {y :: Bool} | X2 {y :: Bool}

     This does not:

       data SX :: X -> Type where
         SX1 :: { sY :: Sing n } -> SX ('X1 n)
         SY1 :: { sY :: Sing n } -> SX ('X2 n)

       error:
           • Constructors SX1 and SX2 have a common field ‘sY’,
               but have different result types
           • In the data type declaration for ‘SX’

     Double ugh. See GHC#8673/GHC#12159.

   * Even if a data type only has a single constructor with record selectors,
     singling it can induce headaches. One might be tempted to single this type:

       newtype Unit = MkUnit { runUnit :: () }

     With this code:

       data SUnit :: Unit -> Type where
         SMkUnit :: { sRunUnit :: Sing u } -> SUnit (MkUnit u)

     Somewhat surprisingly, the type of sRunUnit:

       sRunUnit :: Sing (MkUnit u) -> Sing u

     Is not general enough to handle common uses of record selectors. For
     example, if you try to single this function:

       f :: Unit -> ()
       f = runUnit

     Then the resulting code:

       sF :: Sing (x :: Unit) -> Sing (F x :: ())
       sF = sRunUnit

     Will not typecheck. Note that sRunUnit expects an argument of type
     `Sing (MkUnit u)`, but there is no way to know a priori that the `x` in
     `Sing (x :: Unit)` is `MkUnit u` without pattern-matching on SMkUnit.

Hopefully I have convinced you that handling records in singletons-th is a bit of
a nightmare. Thankfully, there is a simple trick to avoid most of the pitfalls
above: just desugar code (using th-desugar) to avoid records!
In more concrete terms, we do the following:

* A record constructions desugars to a normal constructor application. For example:

    MkT{a = x, b = y}

      ==>

    MkT x y

  Something similar occurs for record syntax in patterns.

* A record update desugars to a case expression. For example:

    t{a = x}

      ==>

    case t of MkT _ y => MkT x y

We can't easily desugar away all uses of records, however. After all, records
can be used as ordinary functions as well. We leave such uses of records alone
when desugaring and accommodate them during promotion and singling by generating
"manual" record selectors. As a running example, consider the earlier Unit example:

  newtype Unit = MkUnit { runUnit :: () }

When singling Unit, we do not give SMkUnit a record selector:

  data SUnit :: Unit -> Type where
    SMkUnit :: Sing u -> SUnit (MkUnit u)

Instead, we generate a top-level function that behaves equivalently to runUnit.
This function then gets promoted and singled (in D.S.TH.Promote.promoteDecs and
D.S.TH.Single.singTopLevelDecs):

  type family RunUnit (x :: Unit) :: () where
    RunUnit (MkUnit x) = x

  sRunUnit :: Sing (x :: Unit) -> Sing (RunUnit x :: ())
  sRunUnit (SMkUnit sx) = sx

Now promoting/singling uses of runUnit as an ordinary function work as expected
since the types of RunUnit/sRunUnit are sufficiently general. This technique also
scales up to data types with multiple constructors sharing a record selector name.
For instance, in the earlier X example:

  data X = X1 {y :: Bool} | X2 {y :: Bool}

We would promote/single `y` like so:

  type family Y (x :: X) :: Bool where
    Y (X1 y) = y
    Y (X2 y) = y

  sY :: Sing (x :: X) -> Sing (Y x :: Bool)
  sY (SX1 sy) = sy
  sY (SX2 sy) = sy

Manual record selectors cannot be used in record constructions or updates, but
for most use cases this won't be an issue, since singletons-th makes an effort to
desugar away fancy uses of records anyway. The only time this would bite is if
you wanted to use record syntax in hand-written singletons code.
-}