Add promotedDataTypeName option to make working with arrows/literals easier

[RyanGlScott]

The current state of the art for promoting data types that contain arrow or literal types is rather shoddy. First, you have to declare a base type, like so:

newtype Age' n = MkAge n

Next, you have to explicitly create term- and type-level versions of this base type:

-- Term-level
type Age = Age' Numeric.Natural.Natural
-- Type-level
type PAge = Age' GHC.TypeNats.Nat

type SAge :: PAge -> Type
data SAge age where
  SMkAge :: Sing n -> SAge (MkAge n)
type instance Sing = SAge

instance SingKind PAge where
  type Demote PAge = Age
  ...

As shown in the Sing and SingKind instances above, if you want to actually use these types, it is almost guaranteed that you won't be able to use singletons' TH machinery to do so. This is because singletons is not aware of the relationship between Age and PAge, so it cannot know to promote Age to PAge. As a result, you basically have no choice but to promote all of your Age-related code by hand. Bummer.

But things don't have to be this terrible. Now that singletons has the ability to hook into how it generates names during promotion, there is a viable way to teach singletons to promote Age to PAge. In particular, I propose doing the following:

1. Add a new field to D.S.TH.Options.Options called promotedDataTypeName :: Name -> Name (in the spirit of the existing singledDataTypeName). By default, promotedDataTypeName = id since DataKinds automatically promotes data type names. The interesting part comes next:
2. Declare Age', Age, and PAge as above. However, we no longer need to write out the Sing, SingKind, etc. instances by hand. Instead, we can let the TH machinery do it by hooking into promotedDataTypeName like so:

$(let handleAge :: Name -> Name
      handleAge n
        | n == ''Age = ''PAge
        | otherwise  = n in
  
  withOptions defaultOptions{promotedDataTypeName = handleAge} $
  genSingletons [''Age])

Now, singletons will have the foresight to promote Age to PAge automatically. This should make using Age/PAge much less painful in practice.

[RyanGlScott]

If we're going to add promotedDataTypeName as a counterpart to singledDataTypeName, we should probably add promotedDataConName as a a counterpart to singledDataConName as well. While promotedDataConName isn't strictly necessary for the trick above, I could foresee someone wanting to improve the type inference for the MkAge data constructor like so:

newtype Age' n = MkAge' n

type Age  = Age' Natural
type PAge = Age' Nat

type MkAge  = MkAge' :: Natural -> Age
type PMkAge = MkAge' :: Nat -> Age

If so, then they could override promotedDataConName to ensure that MkAge gets promoted to PMkAge.

[RyanGlScott]

After some further thought, I'm less enthusiastic about this idea than I once was. The main reason is that actually implementing this idea could lead to slower compile times, even for code that doesn't make use of promotedDataTypeName. To see why, consider this part of promoteType:

singletons/src/Data/Singletons/Promote/Type.hs

Lines 60 to 67 in 46d0d74

	go [] (DConT name)
	| name == typeRepName = return $ DConT typeKindName
	| nameBase name == nameBase repName = return $ DConT typeKindName
	go args (DConT name)
	| Just n <- unboxedTupleNameDegree_maybe name
	= return $ applyDType (DConT (tupleTypeName n)) args
	| otherwise
	= return $ applyDType (DConT name) args

This is definitely a place where we'd need to hook Options into, since it controls how certain Names are promoted. But here's a conundrum: should we hook it into promotedDataTypeName or promotedDataConName? Actually, it could be either! DConT can be used for promoted and non-promoted names alike, so the only way to know for sure which one to use would be to look up the Name's namespace with reifyNameSpace.

I'm very reluctant to make promoteType invoke reifyNameSpace every single time it comes across a DConT, however. It's not uncommon for singletons' TH machinery to promote code like this:

$(promote [d|
  data Foo = ...

  f :: Foo -> Foo -> Foo
  f = ...

  ...

In order to ascertain the NameSpace of a NameU like Foo, singletons must use localDeclarations, which traverses the entire list of local declarations each time. Moreover, this will happen once per occurrence of Foo in a type to be promoted. In the type of f alone, that accounts for three traversals! I could foresee this becoming a huge compile-time performance bottleneck in some of singletons' larger modules.

There are some ways we could mitigate this problem, but I'm not particularly enthusiastic about them either:

1. Combine promotedDataTypeName and promotedDataConName into a single hook and always use on a DConT, regardless of the namespace.
2. Tweak Options so that it can somehow detect when the defaults have been overridden. If the defaults for promotedDataTypeName/promotedDataConName are not overridden, then use a fast path where reifyNameSpace is not invoked. Otherwise, invoke the slow reifyNameSpace path.

[goldfirere]

We could, er, reify this design pattern by giving users a way to say that Age has been promoted by hand. That is, have some (finite) mapping from regular names to promoted names as a part of the options. Then, a client doesn't need to change the overall promotion policy to handle just a few cases.

[RyanGlScott]

Ah, that is a design I hadn't considered. I'll try that and see if there are any complications.

[RyanGlScott]

After some brief experimentation, I realized that the design in #450 (comment) is actually not that different from option (1) in #450 (comment). In fact, I was surprised to find that option (1) was the least clunky to use in practice, so despite my prior lack of enthusiasm for it, I think that is the best way forward. Here is a WIP patch that implements a promotedDataTypeOrConName :: Name -> Name option:

diff --git a/src/Data/Singletons/Promote.hs b/src/Data/Singletons/Promote.hs
index 06efc97..d9022a8 100644
--- a/src/Data/Singletons/Promote.hs
+++ b/src/Data/Singletons/Promote.hs
@@ -1021,13 +1021,10 @@ promotePat (DVarP name) = do
   tell $ PromDPatInfos [(name, tyName)] OSet.empty
   return (DVarT tyName, ADVarP name)
 promotePat (DConP name pats) = do
+  opts <- getOptions
   (types, pats') <- mapAndUnzipM promotePat pats
-  let name' = unboxed_tuple_to_tuple name
+  let name' = promotedDataTypeOrConName opts name
   return (foldType (DConT name') types, ADConP name pats')
-  where
-    unboxed_tuple_to_tuple n
-      | Just deg <- unboxedTupleNameDegree_maybe n = tupleDataName deg
-      | otherwise                                  = n
 promotePat (DTildeP pat) = do
   qReportWarning "Lazy pattern converted into regular pattern in promotion"
   second ADTildeP <$> promotePat pat
diff --git a/src/Data/Singletons/Promote/Defun.hs b/src/Data/Singletons/Promote/Defun.hs
index dcbb41a..d6fa7ca 100644
--- a/src/Data/Singletons/Promote/Defun.hs
+++ b/src/Data/Singletons/Promote/Defun.hs
@@ -146,12 +146,14 @@ buildDefunSymsDataD ctors =
   where
     promoteCtor :: DCon -> PrM [DDec]
     promoteCtor (DCon tvbs _ name fields res_ty) = do
-      let arg_tys = tysOfConFields fields
+      opts <- getOptions
+      let name'   = promotedDataTypeOrConName opts name
+          arg_tys = tysOfConFields fields
       arg_kis <- traverse promoteType_NC arg_tys
       res_ki  <- promoteType_NC res_ty
       let con_ki = ravelVanillaDType tvbs [] arg_kis res_ki
-      m_fixity <- reifyFixityWithLocals name
-      defunctionalize name m_fixity $ DefunSAK con_ki
+      m_fixity <- reifyFixityWithLocals name'
+      defunctionalize name' m_fixity $ DefunSAK con_ki
 
 -- Generate defunctionalization symbols for a name, using reifyFixityWithLocals
 -- to determine what the fixity of each symbol should be
diff --git a/src/Data/Singletons/Promote/Type.hs b/src/Data/Singletons/Promote/Type.hs
index 23eae12..5cad645 100644
--- a/src/Data/Singletons/Promote/Type.hs
+++ b/src/Data/Singletons/Promote/Type.hs
@@ -13,14 +13,11 @@ module Data.Singletons.Promote.Type
 
 import Language.Haskell.TH.Desugar
 import Data.Singletons.Names
+import Data.Singletons.TH.Options
 import Data.Singletons.Util
-import Language.Haskell.TH
 
 -- Promote a DType to the kind level.
---
--- NB: the only monadic thing we do here is fail. This allows the function
--- to be used from the Singletons module.
-promoteType :: MonadFail m => DType -> m DKind
+promoteType :: OptionsMonad m => DType -> m DKind
 promoteType ty = do
   checkVanillaDType ty
   promoteType_NC ty
@@ -28,10 +25,10 @@ promoteType ty = do
 -- Promote a DType to the kind level. This is suffixed with "_NC" because
 -- we do not invoke checkVanillaDType here.
 -- See [Vanilla-type validity checking during promotion].
-promoteType_NC :: MonadFail m => DType -> m DKind
+promoteType_NC :: OptionsMonad m => DType -> m DKind
 promoteType_NC = go []
   where
-    go :: MonadFail m => [DTypeArg] -> DType -> m DKind
+    go :: OptionsMonad m => [DTypeArg] -> DType -> m DKind
     go []       (DForallT fvf tvbs ty) = do
       ty' <- go [] ty
       pure $ DForallT fvf tvbs ty'
@@ -57,14 +54,9 @@ promoteType_NC = go []
       -- No need to promote 'ki' - it is already a kind.
       return $ applyDType (DSigT ty' ki) args
     go args     (DVarT name) = return $ applyDType (DVarT name) args
-    go []       (DConT name)
-      | name == typeRepName               = return $ DConT typeKindName
-      | nameBase name == nameBase repName = return $ DConT typeKindName
-    go args     (DConT name)
-      | Just n <- unboxedTupleNameDegree_maybe name
-      = return $ applyDType (DConT (tupleTypeName n)) args
-      | otherwise
-      = return $ applyDType (DConT name) args
+    go args     (DConT name) = do
+      opts <- getOptions
+      return $ applyDType (DConT (promotedDataTypeOrConName opts name)) args
     go [DTANormal k1, DTANormal k2] DArrowT
       = return $ DConT tyFunArrowName `DAppT` k1 `DAppT` k2
     go _        ty@DLitT{} = pure ty
@@ -76,13 +68,13 @@ promoteType_NC = go []
 -- | Promote a DTypeArg to the kind level. This is suffixed with "_NC" because
 -- we do not invoke checkVanillaDType here.
 -- See [Vanilla-type validity checking during promotion].
-promoteTypeArg_NC :: MonadFail m => DTypeArg -> m DTypeArg
+promoteTypeArg_NC :: OptionsMonad m => DTypeArg -> m DTypeArg
 promoteTypeArg_NC (DTANormal t) = DTANormal <$> promoteType_NC t
 promoteTypeArg_NC ta@(DTyArg _) = pure ta -- Kinds are already promoted
 
 -- | Promote a DType to the kind level, splitting it into its type variable
 -- binders, argument types, and result type in the process.
-promoteUnraveled :: MonadFail m
+promoteUnraveled :: OptionsMonad m
                  => DType -> m ([DTyVarBndr], [DKind], DKind)
 promoteUnraveled ty = do
   (tvbs, _, arg_tys, res_ty) <- unravelVanillaDType ty
diff --git a/src/Data/Singletons/Single/Data.hs b/src/Data/Singletons/Single/Data.hs
index bad5cf6..a2f2cc9 100644
--- a/src/Data/Singletons/Single/Data.hs
+++ b/src/Data/Singletons/Single/Data.hs
@@ -170,7 +170,7 @@ singCtor dataName (DCon con_tvbs cxt name fields rty)
   let types = tysOfConFields fields
       sName = singledDataConName opts name
       sCon = DConE sName
-      pCon = DConT name
+      pCon = DConT $ promotedDataTypeOrConName opts name
   checkVanillaDType $ ravelVanillaDType con_tvbs [] types rty
   indexNames <- mapM (const $ qNewName "n") types
   kinds <- mapM promoteType_NC types
diff --git a/src/Data/Singletons/TH/Options.hs b/src/Data/Singletons/TH/Options.hs
index de410c9..2daf274 100644
--- a/src/Data/Singletons/TH/Options.hs
+++ b/src/Data/Singletons/TH/Options.hs
@@ -22,6 +22,7 @@ module Data.Singletons.TH.Options
     -- ** Options record selectors
   , genQuotedDecs
   , genSingKindInsts
+  , promotedDataTypeOrConName
   , promotedClassName
   , promotedValueName
   , singledDataTypeName
@@ -45,7 +46,7 @@ import Control.Monad.RWS (RWST)
 import Control.Monad.State (StateT)
 import Control.Monad.Trans.Class (MonadTrans(..))
 import Control.Monad.Writer (WriterT)
-import Data.Singletons.Names (consName, listName, nilName, splitUnderscores)
+import Data.Singletons.Names
 import Data.Singletons.Util
 import Language.Haskell.TH.Desugar
 import Language.Haskell.TH.Syntax hiding (Lift(..))
@@ -53,19 +54,21 @@ import Language.Haskell.TH.Syntax hiding (Lift(..))
 -- | Options that control the finer details of how @singletons@' Template
 -- Haskell machinery works.
 data Options = Options
-  { genQuotedDecs        :: Bool
+  { genQuotedDecs :: Bool
     -- ^ If 'True', then quoted declarations will be generated alongside their
     --   promoted and singled counterparts. If 'False', then quoted
     --   declarations will be discarded.
-  , genSingKindInsts     :: Bool
+  , genSingKindInsts :: Bool
     -- ^ If 'True', then 'SingKind' instances will be generated. If 'False',
     --   they will be omitted entirely. This can be useful in scenarios where
     --   TH-generated 'SingKind' instances do not typecheck (for instance,
     --   when generating singletons for GADTs).
-  , promotedClassName    :: Name -> Name
+  , promotedDataTypeOrConName :: Name -> Name
+    -- ^ TODO RGS: Docs
+  , promotedClassName :: Name -> Name
     -- ^ Given the name of the original, unrefined class, produces the name of
     --   the promoted equivalent of the class.
-  , promotedValueName    :: Name -> Maybe Uniq -> Name
+  , promotedValueName :: Name -> Maybe Uniq -> Name
     -- ^ Given the name of the original, unrefined value, produces the name of
     --   the promoted equivalent of the value. This is used for both top-level
     --   and @let@-bound names, and the difference is encoded in the
@@ -74,16 +77,16 @@ data Options = Options
     --   @Just uniq@, where @uniq@ is a globally unique number that can be used
     --   to distinguish the name from other local definitions of the same name
     --   (e.g., if two functions both use @let x = ... in x@).
-  , singledDataTypeName  :: Name -> Name
+  , singledDataTypeName :: Name -> Name
     -- ^ Given the name of the original, unrefined data type, produces the name
     --   of the corresponding singleton type.
-  , singledClassName     :: Name -> Name
+  , singledClassName :: Name -> Name
     -- ^ Given the name of the original, unrefined class, produces the name of
     --   the singled equivalent of the class.
-  , singledDataConName   :: Name -> Name
+  , singledDataConName :: Name -> Name
     -- ^ Given the name of the original, unrefined data constructor, produces
     --   the name of the corresponding singleton data constructor.
-  , singledValueName     :: Name -> Name
+  , singledValueName :: Name -> Name
     -- ^ Given the name of the original, unrefined value, produces the name of
     --   the singled equivalent of the value.
   , defunctionalizedName :: Name -> Int -> Name
@@ -113,15 +116,16 @@ data Options = Options
 -- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@.
 defaultOptions :: Options
 defaultOptions = Options
-  { genQuotedDecs        = True
-  , genSingKindInsts     = True
-  , promotedClassName    = promoteClassName
-  , promotedValueName    = promoteValNameLhs
-  , singledDataTypeName  = singTyConName
-  , singledClassName     = singClassName
-  , singledDataConName   = singDataConName
-  , singledValueName     = singValName
-  , defunctionalizedName = promoteTySym
+  { genQuotedDecs             = True
+  , genSingKindInsts          = True
+  , promotedDataTypeOrConName = promoteDataTypeOrConName
+  , promotedClassName         = promoteClassName
+  , promotedValueName         = promoteValNameLhs
+  , singledDataTypeName       = singTyConName
+  , singledClassName          = singClassName
+  , singledDataConName        = singDataConName
+  , singledValueName          = singValName
+  , defunctionalizedName      = promoteTySym
   }
 
 -- | Given the name of the original, unrefined, top-level value, produces the
@@ -235,6 +239,20 @@ promoteTySym name sat
 promoteClassName :: Name -> Name
 promoteClassName = prefixName "P" "#"
 
+-- TODO RGS: Docs
+promoteDataTypeOrConName :: Name -> Name
+promoteDataTypeOrConName nm
+  | nm == typeRepName               = typeKindName
+  | nameBase nm == nameBase repName = typeKindName
+  | Just degree <- unboxedTupleNameDegree_maybe nm
+  = if isDataName nm then tupleDataName degree else tupleTypeName degree
+  | otherwise = nm
+  where
+    -- Is this name a data constructor name? A 'False' answer means "unsure".
+    isDataName :: Name -> Bool
+    isDataName (Name _ (NameG DataName _ _)) = True
+    isDataName _                             = False
+
 -- Singletons
 
 singDataConName :: Name -> Name

Now, for some good and bad news. I'll start with the bad news: the design I put forth in #450 (comment) doesn't work as well as I'd hoped. I had dreamed of being able to do this:

newtype Age' n = MkAge n
-- Term-level
type Age = Age' Numeric.Natural.Natural
-- Type-level
type PAge = Age' GHC.TypeNats.Nat

$(let handleAge :: Name -> Name
      handleAge n
        | n == ''Age = ''PAge
        | otherwise  = n in
  
  withOptions defaultOptions{promotedDataTypeOrConName = handleAge} $
  genSingletons [''Age])

However, that doesn't quite do what I would expect. Because Age is a mere type synonym, passing it to genSingletons will cause it the type synonym itself to be defunctionalized, but nothing else. That is, you won't get a Sing instance for PAge or any of the other goodies you might expect. I could envision some further special-casing in the internals of singletons to allow it to recognize situations like this, but this seems like a lot of work for little payoff.

The good news is that you can make this work if you just make Age and PAge be distinct data types. Here is an example that demonstrates this in action:

newtype Age  = MkAge  Natural
newtype PAge = PMkAge Nat

$(let customPromote :: Name -> Name
      customPromote n
        | n == ''Age     = ''PAge
        | n == 'MkAge    = 'PMkAge
        | n == ''Natural = ''Nat
        | otherwise      = promotedDataTypeOrConName defaultOptions n

      customDefun :: Name -> Int -> Name
      customDefun n sat = defunctionalizedName defaultOptions (customPromote n) sat in

  withOptions defaultOptions{ promotedDataTypeOrConName = customPromote
                            , defunctionalizedName      = customDefun
                            } $ do
    decs1 <- genSingletons [''Age]
    decs2 <- singletons $ lift [d|
               f :: Age -> Age
               f (MkAge (n :: Natural)) = MkAge (n :: Natural)
               |]
    return $ decs1 ++ decs2)

There are a couple of interesting remarks to be made here:

• In addition to hard-coding the knowledge that Age should be promoted to PAge, one must hard-code the knowledge that Natural should be promoted to Nat. This is necessary in order to ensure that the generated code mentions Nat in the right places (e.g., in the explicit annotations in f). In fact, I wonder if this would be a satisfactory way to fix Promote datatypes with arrows, among others #82?
• In addition to overriding the hook for promoting data type/constructor names, one also has to override the hook for defunctionalizing names so that singletons generates PMkAgeSym0 instead of MkAgeSym0.

I think I'm happy with this approach. Do others have any opinions on this design?

[RyanGlScott]

I heard no objections, so I'll go ahead and move forward with this. See #462.