{- 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.
-}