    {- Data/Singletons/Names.hs

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

    Defining names and manipulations on names for use in promotion and singling.
    -}

    {-# LANGUAGE TemplateHaskell #-}

    module Data.Singletons.Names where

    import Data.Singletons.Internal
    import Data.Singletons.SuppressUnusedWarnings
    import Data.Singletons.Decide
    import Language.Haskell.TH.Syntax
    import Language.Haskell.TH.Desugar
    import GHC.TypeLits ( Nat, Symbol )
    import GHC.Exts ( Constraint )
    import GHC.Show ( showCommaSpace, showSpace )
    import Data.Type.Equality ( TestEquality(..) )
    import Data.Type.Coercion ( TestCoercion(..) )
    import Data.Typeable ( TypeRep )
    import Data.Singletons.Util
    import Control.Applicative
    import Control.Monad

    boolName, andName, tyEqName, compareName, minBoundName,
      maxBoundName, repName,
      nilName, consName, listName, tyFunArrowName,
      applyName, applyTyConName, applyTyConAux1Name,
      natName, symbolName, typeRepName, stringName,
      eqName, ordName, boundedName, orderingName,
      singFamilyName, singIName, singMethName, demoteName, withSingIName,
      singKindClassName, sEqClassName, sEqMethName, sconsName, snilName, strueName,
      sIfName,
      someSingTypeName, someSingDataName,
      sListName, sDecideClassName, sDecideMethName,
      testEqualityClassName, testEqualityMethName, decideEqualityName,
      testCoercionClassName, testCoercionMethName, decideCoercionName,
      provedName, disprovedName, reflName, toSingName, fromSingName,
      equalityName, applySingName, suppressClassName, suppressMethodName,
      thenCmpName,
      sameKindName, tyFromIntegerName, tyNegateName, sFromIntegerName,
      sNegateName, errorName, foldlName, cmpEQName, cmpLTName, cmpGTName,
      singletonsToEnumName, singletonsFromEnumName, enumName, singletonsEnumName,
      equalsName, constraintName,
      showName, showSName, showCharName, showCommaSpaceName, showParenName, showsPrecName,
      showSpaceName, showStringName, showSingName, showSing'Name,
      composeName, gtName, tyFromStringName, sFromStringName,
      foldableName, foldMapName, memptyName, mappendName, foldrName,
      functorName, fmapName, replaceName,
      traversableName, traverseName, pureName, apName, liftA2Name :: Name
    boolName :: Name
    boolName = ''Bool
    andName :: Name
    andName = '(&&)
    compareName :: Name
    compareName = 'compare
    minBoundName :: Name
    minBoundName = 'minBound
    maxBoundName :: Name
    maxBoundName = 'maxBound
    tyEqName :: Name
    tyEqName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Eq" "=="
    repName :: Name
    repName = String -> Name
    mkName "Rep"   -- this is actually defined in client code!
    nilName :: Name
    nilName = '[]
    consName :: Name
    consName = '(:)
    listName :: Name
    listName = ''[]
    tyFunArrowName :: Name
    tyFunArrowName = ''(~>)
    applyName :: Name
    applyName = ''Apply
    applyTyConName :: Name
    applyTyConName = ''ApplyTyCon
    applyTyConAux1Name :: Name
    applyTyConAux1Name = ''ApplyTyConAux1
    symbolName :: Name
    symbolName = ''Symbol
    natName :: Name
    natName = ''Nat
    typeRepName :: Name
    typeRepName = ''TypeRep
    stringName :: Name
    stringName = ''String
    eqName :: Name
    eqName = ''Eq
    ordName :: Name
    ordName = ''Ord
    boundedName :: Name
    boundedName = ''Bounded
    orderingName :: Name
    orderingName = ''Ordering
    singFamilyName :: Name
    singFamilyName = ''Sing
    singIName :: Name
    singIName = ''SingI
    singMethName :: Name
    singMethName = 'sing
    toSingName :: Name
    toSingName = 'toSing
    fromSingName :: Name
    fromSingName = 'fromSing
    demoteName :: Name
    demoteName = ''Demote
    withSingIName :: Name
    withSingIName = 'withSingI
    singKindClassName :: Name
    singKindClassName = ''SingKind
    sEqClassName :: Name
    sEqClassName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Eq" "SEq"
    sEqMethName :: Name
    sEqMethName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Eq" "%=="
    sIfName :: Name
    sIfName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Bool" "sIf"
    sconsName :: Name
    sconsName = String -> String -> Name
    mk_name_d "Data.Singletons.Prelude.Instances" "SCons"
    snilName :: Name
    snilName = String -> String -> Name
    mk_name_d "Data.Singletons.Prelude.Instances" "SNil"
    strueName :: Name
    strueName = String -> String -> Name
    mk_name_d "Data.Singletons.Prelude.Instances" "STrue"
    someSingTypeName :: Name
    someSingTypeName = ''SomeSing
    someSingDataName :: Name
    someSingDataName = 'SomeSing
    sListName :: Name
    sListName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Instances" "SList"
    sDecideClassName :: Name
    sDecideClassName = ''SDecide
    sDecideMethName :: Name
    sDecideMethName = '(%~)
    testEqualityClassName :: Name
    testEqualityClassName = ''TestEquality
    testEqualityMethName :: Name
    testEqualityMethName = 'testEquality
    decideEqualityName :: Name
    decideEqualityName = 'decideEquality
    testCoercionClassName :: Name
    testCoercionClassName = ''TestCoercion
    testCoercionMethName :: Name
    testCoercionMethName = 'testCoercion
    decideCoercionName :: Name
    decideCoercionName = 'decideCoercion
    provedName :: Name
    provedName = 'Proved
    disprovedName :: Name
    disprovedName = 'Disproved
    reflName :: Name
    reflName = 'Refl
    equalityName :: Name
    equalityName = ''(~)
    applySingName :: Name
    applySingName = 'applySing
    suppressClassName :: Name
    suppressClassName = ''SuppressUnusedWarnings
    suppressMethodName :: Name
    suppressMethodName = 'suppressUnusedWarnings
    thenCmpName :: Name
    thenCmpName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Ord" "thenCmp"
    sameKindName :: Name
    sameKindName = ''SameKind
    tyFromIntegerName :: Name
    tyFromIntegerName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Num" "FromInteger"
    tyNegateName :: Name
    tyNegateName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Num" "Negate"
    sFromIntegerName :: Name
    sFromIntegerName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Num" "sFromInteger"
    sNegateName :: Name
    sNegateName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Num" "sNegate"
    errorName :: Name
    errorName = 'error
    foldlName :: Name
    foldlName = 'foldl
    cmpEQName :: Name
    cmpEQName = 'EQ
    cmpLTName :: Name
    cmpLTName = 'LT
    cmpGTName :: Name
    cmpGTName = 'GT
    singletonsToEnumName :: Name
    singletonsToEnumName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Enum" "toEnum"
    singletonsFromEnumName :: Name
    singletonsFromEnumName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.Enum" "fromEnum"
    enumName :: Name
    enumName = ''Enum
    singletonsEnumName :: Name
    singletonsEnumName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Enum" "Enum"
    equalsName :: Name
    equalsName = '(==)
    constraintName :: Name
    constraintName = ''Constraint
    showName :: Name
    showName = ''Show
    showSName :: Name
    showSName = ''ShowS
    showCharName :: Name
    showCharName = 'showChar
    showParenName :: Name
    showParenName = 'showParen
    showSpaceName :: Name
    showSpaceName = 'showSpace
    showsPrecName :: Name
    showsPrecName = 'showsPrec
    showStringName :: Name
    showStringName = 'showString
    showSingName :: Name
    showSingName = String -> String -> Name
    mk_name_tc "Data.Singletons.ShowSing" "ShowSing"
    showSing'Name :: Name
    showSing'Name = String -> String -> Name
    mk_name_tc "Data.Singletons.ShowSing" "ShowSing'"
    composeName :: Name
    composeName = '(.)
    gtName :: Name
    gtName = '(>)
    showCommaSpaceName :: Name
    showCommaSpaceName = 'showCommaSpace
    tyFromStringName :: Name
    tyFromStringName = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.IsString" "FromString"
    sFromStringName :: Name
    sFromStringName = String -> String -> Name
    mk_name_v "Data.Singletons.Prelude.IsString" "sFromString"
    foldableName :: Name
    foldableName = ''Foldable
    foldMapName :: Name
    foldMapName = 'foldMap
    memptyName :: Name
    memptyName = 'mempty
    mappendName :: Name
    mappendName = 'mappend
    foldrName :: Name
    foldrName = 'foldr
    functorName :: Name
    functorName = ''Functor
    fmapName :: Name
    fmapName = 'fmap
    replaceName :: Name
    replaceName = '(<$)
    traversableName :: Name
    traversableName = ''Traversable
    traverseName :: Name
    traverseName = 'traverse
    pureName :: Name
    pureName = 'pure
    apName :: Name
    apName = '(<*>)
    liftA2Name :: Name
    liftA2Name = 'liftA2

    singPkg :: String
    singPkg :: String
    singPkg = $( (LitE . StringL . loc_package) `liftM` location )

    mk_name_tc :: String -> String -> Name
    mk_name_tc :: String -> String -> Name
    mk_name_tc = String -> String -> String -> Name
    mkNameG_tc String
    singPkg

    mk_name_d :: String -> String -> Name
    mk_name_d :: String -> String -> Name
    mk_name_d = String -> String -> String -> Name
    mkNameG_d String
    singPkg

    mk_name_v :: String -> String -> Name
    mk_name_v :: String -> String -> Name
    mk_name_v = String -> String -> String -> Name
    mkNameG_v String
    singPkg

    mkTupleTypeName :: Int -> Name
    mkTupleTypeName :: Int -> Name
    mkTupleTypeName n :: Int
    n = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Instances" (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $
                        "STuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int -> String
    forall a. Show a => a -> String
    show Int
    n)

    mkTupleDataName :: Int -> Name
    mkTupleDataName :: Int -> Name
    mkTupleDataName n :: Int
    n = String -> String -> Name
    mk_name_d "Data.Singletons.Prelude.Instances" (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $
                        "STuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int -> String
    forall a. Show a => a -> String
    show Int
    n)

    -- used when a value name appears in a pattern context
    -- works only for proper variables (lower-case names)
    promoteValNameLhs :: Name -> Name
    promoteValNameLhs :: Name -> Name
    promoteValNameLhs = (String, String) -> Name -> Name
    promoteValNameLhsPrefix (String, String)
    noPrefix

    -- like promoteValNameLhs, but adds a prefix to the promoted name
    promoteValNameLhsPrefix :: (String, String) -> Name -> Name
    promoteValNameLhsPrefix :: (String, String) -> Name -> Name
    promoteValNameLhsPrefix pres :: (String, String)
    pres@(alpha :: String
    alpha, _) n :: Name
    n
        -- We can't promote promote idenitifers beginning with underscores to
        -- type names, so we work around the issue by prepending "US" at the
        -- front of the name (#229).
      | Just (us :: String
    us, rest :: String
    rest) <- String -> Maybe (String, String)
    splitUnderscores (Name -> String
    nameBase Name
    n)
      = String -> Name
    mkName (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ String
    alpha String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "US" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rest

      | Bool
    otherwise
      = String -> Name
    mkName (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ (String, String) -> Name -> String
    toUpcaseStr (String, String)
    pres Name
    n

    -- used when a value name appears in an expression context
    -- works for both variables and datacons
    promoteValRhs :: Name -> DType
    promoteValRhs :: Name -> DType
    promoteValRhs name :: Name
    name
      | Name
    name Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    nilName
      = Name -> DType
    DConT Name
    nilName   -- workaround for #21

      | Bool
    otherwise
      = Name -> DType
    DConT (Name -> DType) -> Name -> DType
    forall a b. (a -> b) -> a -> b
    $ Name -> Int -> Name
    promoteTySym Name
    name 0

    -- generates type-level symbol for a given name. Int parameter represents
    -- saturation: 0 - no parameters passed to the symbol, 1 - one parameter
    -- passed to the symbol, and so on. Works on both promoted and unpromoted
    -- names.
    promoteTySym :: Name -> Int -> Name
    promoteTySym :: Name -> Int -> Name
    promoteTySym name :: Name
    name sat :: Int
    sat
          -- We can't promote promote idenitifers beginning with underscores to
          -- type names, so we work around the issue by prepending "US" at the
          -- front of the name (#229).
        | Just (us :: String
    us, rest :: String
    rest) <- String -> Maybe (String, String)
    splitUnderscores (Name -> String
    nameBase Name
    name)
        = Name -> Name
    default_case (String -> Name
    mkName (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ "US" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    rest)

        | Name
    name Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    nilName
        = String -> Name
    mkName (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ "NilSym" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int -> String
    forall a. Show a => a -> String
    show Int
    sat)

           -- treat unboxed tuples like tuples
        | Just degree :: Int
    degree <- Name -> Maybe Int
    tupleNameDegree_maybe Name
    name Maybe Int -> Maybe Int -> Maybe Int
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
                         Name -> Maybe Int
    unboxedTupleNameDegree_maybe Name
    name
        = String -> String -> Name
    mk_name_tc "Data.Singletons.Prelude.Instances" (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $
                     "Tuple" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    degree String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "Sym" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int -> String
    forall a. Show a => a -> String
    show Int
    sat)

        | Bool
    otherwise
        = Name -> Name
    default_case Name
    name
      where
        default_case :: Name -> Name
        default_case :: Name -> Name
    default_case name' :: Name
    name' =
          let capped :: String
    capped = (String, String) -> Name -> String
    toUpcaseStr (String, String)
    noPrefix Name
    name' in
          if Char -> Bool
    isHsLetter (String -> Char
    forall a. [a] -> a
    head String
    capped)
          then String -> Name
    mkName (String
    capped String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "Sym" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int -> String
    forall a. Show a => a -> String
    show Int
    sat))
          else String -> Name
    mkName (String
    capped String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "@#@" -- See Note [Defunctionalization symbol suffixes]
                              String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (Int
    sat Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 1) '$'))

    promoteClassName :: Name -> Name
    promoteClassName :: Name -> Name
    promoteClassName = String -> String -> Name -> Name
    prefixName "P" "#"

    mkTyName :: Quasi q => Name -> q Name
    mkTyName :: Name -> q Name
    mkTyName tmName :: Name
    tmName = do
      let nameStr :: String
    nameStr  = Name -> String
    nameBase Name
    tmName
          symbolic :: Bool
    symbolic = Bool -> Bool
    not (Char -> Bool
    isHsLetter (String -> Char
    forall a. [a] -> a
    head String
    nameStr))
      String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName (if Bool
    symbolic then "ty" else String
    nameStr)

    mkTyConName :: Int -> Name
    mkTyConName :: Int -> Name
    mkTyConName i :: Int
    i = String -> String -> Name
    mk_name_tc "Data.Singletons.Internal" (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ "TyCon" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i

    falseTySym :: DType
    falseTySym :: DType
    falseTySym = Name -> DType
    promoteValRhs Name
    falseName

    trueTySym :: DType
    trueTySym :: DType
    trueTySym = Name -> DType
    promoteValRhs Name
    trueName

    boolKi :: DKind
    boolKi :: DType
    boolKi = Name -> DType
    DConT Name
    boolName

    andTySym :: DType
    andTySym :: DType
    andTySym = Name -> DType
    promoteValRhs Name
    andName

    -- Singletons

    singDataConName :: Name -> Name
    singDataConName :: Name -> Name
    singDataConName nm :: Name
    nm
      | Name
    nm Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    nilName                                  = Name
    snilName
      | Name
    nm Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    consName                                 = Name
    sconsName
      | Just degree :: Int
    degree <- Name -> Maybe Int
    tupleNameDegree_maybe Name
    nm        = Int -> Name
    mkTupleDataName Int
    degree
      | Just degree :: Int
    degree <- Name -> Maybe Int
    unboxedTupleNameDegree_maybe Name
    nm = Int -> Name
    mkTupleDataName Int
    degree
      | Bool
    otherwise                                      = String -> String -> Name -> Name
    prefixConName "S" "%" Name
    nm

    singTyConName :: Name -> Name
    singTyConName :: Name -> Name
    singTyConName name :: Name
    name
      | Name
    name Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    listName                                 = Name
    sListName
      | Just degree :: Int
    degree <- Name -> Maybe Int
    tupleNameDegree_maybe Name
    name        = Int -> Name
    mkTupleTypeName Int
    degree
      | Just degree :: Int
    degree <- Name -> Maybe Int
    unboxedTupleNameDegree_maybe Name
    name = Int -> Name
    mkTupleTypeName Int
    degree
      | Bool
    otherwise                                        = String -> String -> Name -> Name
    prefixName "S" "%" Name
    name

    singClassName :: Name -> Name
    singClassName :: Name -> Name
    singClassName = Name -> Name
    singTyConName

    singValName :: Name -> Name
    singValName :: Name -> Name
    singValName n :: Name
    n
         -- Push the 's' past the underscores, as this lets us avoid some unused
         -- variable warnings (#229).
      | Just (us :: String
    us, rest :: String
    rest) <- String -> Maybe (String, String)
    splitUnderscores (Name -> String
    nameBase Name
    n)
      = String -> String -> Name -> Name
    prefixName (String
    us String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "s") "%" (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ String -> Name
    mkName String
    rest
      | Bool
    otherwise
      = String -> String -> Name -> Name
    prefixName "s" "%" (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    upcase Name
    n

    singFamily :: DType
    singFamily :: DType
    singFamily = Name -> DType
    DConT Name
    singFamilyName

    singKindConstraint :: DKind -> DPred
    singKindConstraint :: DType -> DType
    singKindConstraint = DType -> DType -> DType
    DAppT (Name -> DType
    DConT Name
    singKindClassName)

    demote :: DType
    demote :: DType
    demote = Name -> DType
    DConT Name
    demoteName

    apply :: DType -> DType -> DType
    apply :: DType -> DType -> DType
    apply t1 :: DType
    t1 t2 :: DType
    t2 = DType -> DType -> DType
    DAppT (DType -> DType -> DType
    DAppT (Name -> DType
    DConT Name
    applyName) DType
    t1) DType
    t2

    mkListE :: [DExp] -> DExp
    mkListE :: [DExp] -> DExp
    mkListE =
      (DExp -> DExp -> DExp) -> DExp -> [DExp] -> DExp
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\h :: DExp
    h t :: DExp
    t -> Name -> DExp
    DConE Name
    consName DExp -> DExp -> DExp
    `DAppE` DExp
    h DExp -> DExp -> DExp
    `DAppE` DExp
    t) (Name -> DExp
    DConE Name
    nilName)

    -- apply a type to a list of types using Apply type family
    -- This is defined here, not in Utils, to avoid cyclic dependencies
    foldApply :: DType -> [DType] -> DType
    foldApply :: DType -> [DType] -> DType
    foldApply = (DType -> DType -> DType) -> DType -> [DType] -> DType
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl DType -> DType -> DType
    apply

    -- make an equality predicate
    mkEqPred :: DType -> DType -> DPred
    mkEqPred :: DType -> DType -> DType
    mkEqPred ty1 :: DType
    ty1 ty2 :: DType
    ty2 = DType -> [DType] -> DType
    foldType (Name -> DType
    DConT Name
    equalityName) [DType
    ty1, DType
    ty2]

    -- | If a 'String' begins with one or more underscores, return
    -- @'Just' (us, rest)@, where @us@ contain all of the underscores at the
    -- beginning of the 'String' and @rest@ contains the remainder of the 'String'.
    -- Otherwise, return 'Nothing'.
    splitUnderscores :: String -> Maybe (String, String)
    splitUnderscores :: String -> Maybe (String, String)
    splitUnderscores s :: String
    s = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '_') String
    s of
                           ([], _) -> Maybe (String, String)
    forall a. Maybe a
    Nothing
                           res :: (String, String)
    res     -> (String, String) -> Maybe (String, String)
    forall a. a -> Maybe a
    Just (String, String)
    res

    -- Walk a DType, applying a function to all occurrences of constructor names.
    modifyConNameDType :: (Name -> Name) -> DType -> DType
    modifyConNameDType :: (Name -> Name) -> DType -> DType
    modifyConNameDType mod_con_name :: Name -> Name
    mod_con_name = DType -> DType
    go
      where
        go :: DType -> DType
    go (DForallT tvbs :: [DTyVarBndr]
    tvbs cxt :: [DType]
    cxt p :: DType
    p) = [DTyVarBndr] -> [DType] -> DType -> DType
    DForallT [DTyVarBndr]
    tvbs ((DType -> DType) -> [DType] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DType -> DType
    go [DType]
    cxt) (DType -> DType
    go DType
    p)
        go (DAppT     p :: DType
    p t :: DType
    t)       = DType -> DType -> DType
    DAppT     (DType -> DType
    go DType
    p) DType
    t
        go (DAppKindT p :: DType
    p k :: DType
    k)       = DType -> DType -> DType
    DAppKindT (DType -> DType
    go DType
    p) DType
    k
        go (DSigT     p :: DType
    p k :: DType
    k)       = DType -> DType -> DType
    DSigT     (DType -> DType
    go DType
    p) DType
    k
        go p :: DType
    p@(DVarT _)           = DType
    p
        go (DConT n :: Name
    n)             = Name -> DType
    DConT (Name -> Name
    mod_con_name Name
    n)
        go p :: DType
    p@DType
    DWildCardT          = DType
    p
        go p :: DType
    p@(DLitT {})          = DType
    p
        go p :: DType
    p@DType
    DArrowT             = DType
    p

    {-
    Note [Defunctionalization symbol suffixes]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Before, we used to denote defunctionalization symbols by simply appending dollar
    signs at the end (e.g., (+$) and (+$$)). But this can lead to ambiguity when you
    have function names that consist of solely $ characters. For instance, if you
    tried to promote ($) and ($$) simultaneously, you'd get these promoted types:

    $
    $$

    And these defunctionalization symbols:

    $$
    $$$

    But now there's a name clash between the promoted type for ($) and the
    defunctionalization symbol for ($$)! The solution is to use a precede these
    defunctionalization dollar signs with another string (we choose @#@).
    So now the new defunctionalization symbols would be:

    $@#@$
    $@#@$$

    And there is no conflict.
    -}