From 148f6947a1f88993f692ca3055919562798a92d8 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 9 Nov 2019 09:10:54 -0500 Subject: [PATCH] Introduce Options and OptionsMonad This patch introduces an `Options` data type and an `mtl`-like `OptionsMonad` class for monads that carry `Options`. At present, the only things one can do with `Options` are: * Toggle the generation of `SingKind` instances. Suppressing `SingKind` instances provides an effective workaround for #150. * Hook into the TH machinery's naming conventions for promoted and singled names. This fixes #204. The vast majority of this patch simply adds plumbing by using `OptionsMonad` in places that need it. See the `D.S.TH.Options` module for where most of the new code is housed, as well as the `T150` and `T204` test cases for examples of how to use it. --- CHANGES.md | 19 + README.md | 23 ++ singletons.cabal | 1 + src/Data/Singletons/CustomStar.hs | 3 +- src/Data/Singletons/Deriving/Show.hs | 232 +++++------ src/Data/Singletons/Names.hs | 100 ----- src/Data/Singletons/Partition.hs | 7 +- src/Data/Singletons/Promote.hs | 111 ++--- src/Data/Singletons/Promote/Defun.hs | 8 +- src/Data/Singletons/Promote/Eq.hs | 31 +- src/Data/Singletons/Promote/Monad.hs | 24 +- src/Data/Singletons/Single.hs | 149 ++++--- src/Data/Singletons/Single/Data.hs | 19 +- src/Data/Singletons/Single/Defun.hs | 21 +- src/Data/Singletons/Single/Eq.hs | 30 +- src/Data/Singletons/Single/Fixity.hs | 15 +- src/Data/Singletons/Single/Monad.hs | 33 +- src/Data/Singletons/Single/Type.hs | 4 +- src/Data/Singletons/TH.hs | 7 +- src/Data/Singletons/TH/Options.hs | 228 +++++++++++ tests/SingletonsTestSuite.hs | 3 + tests/compile-and-dump/Singletons/T150.golden | 384 ++++++++++++++++++ tests/compile-and-dump/Singletons/T150.hs | 53 +++ tests/compile-and-dump/Singletons/T204.golden | 94 +++++ tests/compile-and-dump/Singletons/T204.hs | 17 + 25 files changed, 1214 insertions(+), 402 deletions(-) create mode 100644 src/Data/Singletons/TH/Options.hs create mode 100644 tests/compile-and-dump/Singletons/T150.golden create mode 100644 tests/compile-and-dump/Singletons/T150.hs create mode 100644 tests/compile-and-dump/Singletons/T204.golden create mode 100644 tests/compile-and-dump/Singletons/T204.hs diff --git a/CHANGES.md b/CHANGES.md index bbf01e7c..8e6f7004 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,6 +4,25 @@ Changelog for singletons project 2.7 --- * Require GHC 8.10. +* The Template Haskell machinery now supports fine-grained configuration in + the way of an `Options` data type, which lives in the new + `Data.Singletons.TH.Options` module. Besides `Options`, this module also + contains: + * `Options`' record selectors. Currently, these include ways to toggle + generating `SingKind` instances and configure how `singletons` generates + the names of promoted or singled types. In the future, there may be + additional options. + * A `defaultOptions` value. + * An `mtl`-like `OptionsMonad` class for monads that support carrying + `Option`s. This includes `Q`, which uses `defaultOptions` if it is the + top of the monad transformer stack. + * An `OptionM` monad transformer that turns any `DsMonad` into an + `OptionsMonad`. + * A `withOptions` function which allows passing `Options` to TH functions + (e.g., `promote` or `singletons`). See the `README` for a full example + of how to use `withOptions`. + Most TH functions are now polymorphic over `OptionsMonad` instead of + `DsMonad`. * `singletons` now does a much better job of preserving the order of type variables when singling the type signatures of top-level functions and data constructors. See the `Support for TypeApplications` section of the `README` diff --git a/README.md b/README.md index 9da16110..cc42dd0c 100644 --- a/README.md +++ b/README.md @@ -545,6 +545,23 @@ treatment): All functions that begin with leading underscores are treated similarly. +If desired, you can pick your own naming conventions by using the +`Data.Singletons.TH.Options` module. Here is an example of how this module can +be used to prefix a singled data constructor with `MyS` instead of `S`: + +```hs +import Control.Monad.Trans.Class +import Data.Singletons.TH +import Data.Singletons.TH.Options +import Language.Haskell.TH (Name, mkName, nameBase) + +$(let myPrefix :: Name -> Name + myPrefix name = mkName ("MyS" ++ nameBase name) in + + withOptions defaultOptions{singledDataConName = myPrefix} $ + singletons $ lift [d| data T = MkT |]) +``` + Supported Haskell constructs ---------------------------- @@ -780,3 +797,9 @@ Known bugs method :: [a] method = [] ``` +* Singling GADTs is likely to fail due to the generated `SingKind` instances + not typechecking. (See + [#150](https://github.com/goldfirere/singletons/issues/150)). + However, one can often work around the issue by suppressing the generation + of `SingKind` instances by using custom `Options`. See the `T150` test case + for an example. diff --git a/singletons.cabal b/singletons.cabal index 55eaf5f7..0f1f17f5 100644 --- a/singletons.cabal +++ b/singletons.cabal @@ -73,6 +73,7 @@ library Data.Singletons.CustomStar Data.Singletons.TypeRepTYPE Data.Singletons.TH + Data.Singletons.TH.Options Data.Singletons.Prelude Data.Singletons.Prelude.Applicative Data.Singletons.Prelude.Base diff --git a/src/Data/Singletons/CustomStar.hs b/src/Data/Singletons/CustomStar.hs index f2c04d16..bb2be564 100644 --- a/src/Data/Singletons/CustomStar.hs +++ b/src/Data/Singletons/CustomStar.hs @@ -37,6 +37,7 @@ import Data.Singletons.Single import Data.Singletons.Syntax import Data.Singletons.Names import Data.Singletons.TH +import Data.Singletons.TH.Options import Control.Monad import Data.Maybe import Language.Haskell.TH.Desugar @@ -70,7 +71,7 @@ import Data.Singletons.Prelude.Bool -- @Bool@, and @Maybe@, not just promoted data constructors. -- -- Please note that this function is /very/ experimental. Use at your own risk. -singletonStar :: DsMonad q +singletonStar :: OptionsMonad q => [Name] -- ^ A list of Template Haskell @Name@s for types -> q [Dec] singletonStar names = do diff --git a/src/Data/Singletons/Deriving/Show.hs b/src/Data/Singletons/Deriving/Show.hs index 4e7694dd..5ba44df2 100644 --- a/src/Data/Singletons/Deriving/Show.hs +++ b/src/Data/Singletons/Deriving/Show.hs @@ -20,6 +20,7 @@ module Data.Singletons.Deriving.Show ( import Language.Haskell.TH.Syntax hiding (showName) import Language.Haskell.TH.Desugar import Data.Singletons.Names +import Data.Singletons.TH.Options import Data.Singletons.Util import Data.Singletons.Syntax import Data.Singletons.Deriving.Infer @@ -28,7 +29,7 @@ import Data.Maybe (fromMaybe) import GHC.Lexeme (startsConSym, startsVarSym) import GHC.Show (appPrec, appPrec1) -mkShowInstance :: DsMonad q => ShowMode -> DerivDesc q +mkShowInstance :: OptionsMonad q => ShowMode -> DerivDesc q mkShowInstance mode mb_ctxt ty (DataDecl _ _ cons) = do clauses <- mk_showsPrec mode cons constraints <- inferConstraintsDef (fmap (mkShowSingContext mode) mb_ctxt) @@ -41,7 +42,7 @@ mkShowInstance mode mb_ctxt ty (DataDecl _ _ cons) = do , id_sigs = mempty , id_meths = [ (showsPrecName, UFunction clauses) ] } -mk_showsPrec :: DsMonad q => ShowMode -> [DCon] -> q [DClause] +mk_showsPrec :: OptionsMonad q => ShowMode -> [DCon] -> q [DClause] mk_showsPrec mode cons = do p <- newUniqueName "p" -- The precedence argument (not always used) if null cons @@ -49,119 +50,123 @@ mk_showsPrec mode cons = do pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])] else mapM (mk_showsPrec_clause mode p) cons -mk_showsPrec_clause :: forall q. DsMonad q +mk_showsPrec_clause :: forall q. OptionsMonad q => ShowMode -> Name -> DCon -> q DClause mk_showsPrec_clause mode p (DCon _ _ con_name con_fields _) = go con_fields where - con_name' :: Name - con_name' = case mode of - ForPromotion -> con_name - ForShowSing{} -> singDataConName con_name - go :: DConFields -> q DClause - - -- No fields: print just the constructor name, with no parentheses - go (DNormalC _ []) = return $ - DClause [DWildP, DConP con_name' []] $ - DVarE showStringName `DAppE` dStringE (parenInfixConName con_name' "") - - -- Infix constructors have special Show treatment. - go (DNormalC True tys@[_, _]) - -- Although the (:) constructor is infix, its singled counterpart SCons - -- is not, which matters if we're deriving a ShowSing instance. - -- Unless we remove this special case (see #234), we will simply - -- shunt it along as if we were dealing with a prefix constructor. - | ForShowSing{} <- mode - , con_name == consName - = go (DNormalC False tys) - - | otherwise - = do argL <- newUniqueName "argL" - argR <- newUniqueName "argR" - argTyL <- newUniqueName "argTyL" - argTyR <- newUniqueName "argTyR" - fi <- fromMaybe defaultFixity <$> reifyFixityWithLocals con_name' - let con_prec = case fi of Fixity prec _ -> prec - op_name = nameBase con_name' - infixOpE = DAppE (DVarE showStringName) . dStringE $ - if isInfixDataCon op_name - then " " ++ op_name ++ " " - -- Make sure to handle infix data constructors - -- like (Int `Foo` Int) - else " `" ++ op_name ++ "` " - return $ DClause [ DVarP p - , DConP con_name' $ - zipWith (mk_Show_arg_pat mode) [argL, argR] [argTyL, argTyR] - ] $ - mk_Show_rhs_sig mode [argTyL, argTyR] $ - (DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p - `DAppE` dIntegerE con_prec)) - `DAppE` (DVarE composeName - `DAppE` showsPrecE (con_prec + 1) argL - `DAppE` (DVarE composeName - `DAppE` infixOpE - `DAppE` showsPrecE (con_prec + 1) argR)) - - go (DNormalC _ tys) = do - args <- mapM (const $ newUniqueName "arg") tys - argTys <- mapM (const $ newUniqueName "argTy") tys - let show_args = map (showsPrecE appPrec1) args - composed_args = foldr1 (\v q -> DVarE composeName - `DAppE` v - `DAppE` (DVarE composeName - `DAppE` DVarE showSpaceName - `DAppE` q)) show_args - named_args = DVarE composeName - `DAppE` (DVarE showStringName - `DAppE` dStringE (parenInfixConName con_name' " ")) - `DAppE` composed_args - return $ DClause [ DVarP p - , DConP con_name' $ - zipWith (mk_Show_arg_pat mode) args argTys - ] $ - mk_Show_rhs_sig mode argTys $ - DVarE showParenName - `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) - `DAppE` named_args - - -- We show a record constructor with no fields the same way we'd show a - -- normal constructor with no fields. - go (DRecC []) = go (DNormalC False []) - - go (DRecC tys) = do - args <- mapM (const $ newUniqueName "arg") tys - argTys <- mapM (const $ newUniqueName "argTy") tys - let show_args = - concatMap (\((arg_name, _, _), arg) -> - let arg_name' = case mode of - ForPromotion -> arg_name - ForShowSing{} -> singValName arg_name - arg_nameBase = nameBase arg_name' - infix_rec = showParen (isSym arg_nameBase) - (showString arg_nameBase) "" - in [ DVarE showStringName `DAppE` dStringE (infix_rec ++ " = ") - , showsPrecE 0 arg - , DVarE showCommaSpaceName - ]) - (zip tys args) - brace_comma_args = (DVarE showCharName `DAppE` dCharE mode '{') - : take (length show_args - 1) show_args - composed_args = foldr (\x y -> DVarE composeName `DAppE` x `DAppE` y) - (DVarE showCharName `DAppE` dCharE mode '}') - brace_comma_args - named_args = DVarE composeName - `DAppE` (DVarE showStringName - `DAppE` dStringE (parenInfixConName con_name' " ")) - `DAppE` composed_args - return $ DClause [ DVarP p - , DConP con_name' $ - zipWith (mk_Show_arg_pat mode) args argTys - ] $ - mk_Show_rhs_sig mode argTys $ - DVarE showParenName - `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) - `DAppE` named_args + go con_fields' = do + opts <- getOptions + + let con_name' :: Name + con_name' = case mode of + ForPromotion -> con_name + ForShowSing{} -> singledDataConName opts con_name + + case con_fields' of + + -- No fields: print just the constructor name, with no parentheses + DNormalC _ [] -> return $ + DClause [DWildP, DConP con_name' []] $ + DVarE showStringName `DAppE` dStringE (parenInfixConName con_name' "") + + -- Infix constructors have special Show treatment. + DNormalC True tys@[_, _] + -- Although the (:) constructor is infix, its singled counterpart SCons + -- is not, which matters if we're deriving a ShowSing instance. + -- Unless we remove this special case (see #234), we will simply + -- shunt it along as if we were dealing with a prefix constructor. + | ForShowSing{} <- mode + , con_name == consName + -> go (DNormalC False tys) + + | otherwise + -> do argL <- newUniqueName "argL" + argR <- newUniqueName "argR" + argTyL <- newUniqueName "argTyL" + argTyR <- newUniqueName "argTyR" + fi <- fromMaybe defaultFixity <$> reifyFixityWithLocals con_name' + let con_prec = case fi of Fixity prec _ -> prec + op_name = nameBase con_name' + infixOpE = DAppE (DVarE showStringName) . dStringE $ + if isInfixDataCon op_name + then " " ++ op_name ++ " " + -- Make sure to handle infix data constructors + -- like (Int `Foo` Int) + else " `" ++ op_name ++ "` " + return $ DClause [ DVarP p + , DConP con_name' $ + zipWith (mk_Show_arg_pat mode) [argL, argR] [argTyL, argTyR] + ] $ + mk_Show_rhs_sig mode [argTyL, argTyR] $ + (DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p + `DAppE` dIntegerE con_prec)) + `DAppE` (DVarE composeName + `DAppE` showsPrecE (con_prec + 1) argL + `DAppE` (DVarE composeName + `DAppE` infixOpE + `DAppE` showsPrecE (con_prec + 1) argR)) + + DNormalC _ tys -> do + args <- mapM (const $ newUniqueName "arg") tys + argTys <- mapM (const $ newUniqueName "argTy") tys + let show_args = map (showsPrecE appPrec1) args + composed_args = foldr1 (\v q -> DVarE composeName + `DAppE` v + `DAppE` (DVarE composeName + `DAppE` DVarE showSpaceName + `DAppE` q)) show_args + named_args = DVarE composeName + `DAppE` (DVarE showStringName + `DAppE` dStringE (parenInfixConName con_name' " ")) + `DAppE` composed_args + return $ DClause [ DVarP p + , DConP con_name' $ + zipWith (mk_Show_arg_pat mode) args argTys + ] $ + mk_Show_rhs_sig mode argTys $ + DVarE showParenName + `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) + `DAppE` named_args + + -- We show a record constructor with no fields the same way we'd show a + -- normal constructor with no fields. + DRecC [] -> go (DNormalC False []) + + DRecC tys -> do + args <- mapM (const $ newUniqueName "arg") tys + argTys <- mapM (const $ newUniqueName "argTy") tys + let show_args = + concatMap (\((arg_name, _, _), arg) -> + let arg_name' = case mode of + ForPromotion -> arg_name + ForShowSing{} -> singledValueName opts arg_name + arg_nameBase = nameBase arg_name' + infix_rec = showParen (isSym arg_nameBase) + (showString arg_nameBase) "" + in [ DVarE showStringName `DAppE` dStringE (infix_rec ++ " = ") + , showsPrecE 0 arg + , DVarE showCommaSpaceName + ]) + (zip tys args) + brace_comma_args = (DVarE showCharName `DAppE` dCharE mode '{') + : take (length show_args - 1) show_args + composed_args = foldr (\x y -> DVarE composeName `DAppE` x `DAppE` y) + (DVarE showCharName `DAppE` dCharE mode '}') + brace_comma_args + named_args = DVarE composeName + `DAppE` (DVarE showStringName + `DAppE` dStringE (parenInfixConName con_name' " ")) + `DAppE` composed_args + return $ DClause [ DVarP p + , DConP con_name' $ + zipWith (mk_Show_arg_pat mode) args argTys + ] $ + mk_Show_rhs_sig mode argTys $ + DVarE showParenName + `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) + `DAppE` named_args -- | Parenthesize an infix constructor name if it is being applied as a prefix -- function (e.g., data Amp a = (:&) a a) @@ -218,14 +223,15 @@ mk_Show_name :: ShowMode -> Name mk_Show_name ForPromotion = showName mk_Show_name ForShowSing{} = showSingName --- If we're creating a 'Show' instance for a singleon type, decorate the type +-- If we're creating a 'Show' instance for a singleton type, decorate the type -- appropriately (e.g., turn @Maybe a@ into @SMaybe (z :: Maybe a)@). -- Otherwise, return the type (@Maybe a@) unchanged. -mk_Show_inst_ty :: Quasi q => ShowMode -> DType -> q DType +mk_Show_inst_ty :: OptionsMonad q => ShowMode -> DType -> q DType mk_Show_inst_ty ForPromotion ty = pure ty mk_Show_inst_ty (ForShowSing ty_tycon) ty = do + opts <- getOptions z <- qNewName "z" - pure $ DConT (singTyConName ty_tycon) `DAppT` (DVarT z `DSigT` ty) + pure $ DConT (singledDataTypeName opts ty_tycon) `DAppT` (DVarT z `DSigT` ty) -- If we're creating a 'Show' instance for a singleton type, create a pattern -- of the form @(sx :: Sing x)@. Otherwise, simply return the pattern @sx@. diff --git a/src/Data/Singletons/Names.hs b/src/Data/Singletons/Names.hs index c4dea969..de92e46d 100644 --- a/src/Data/Singletons/Names.hs +++ b/src/Data/Singletons/Names.hs @@ -170,68 +170,6 @@ mkTupleDataName :: Int -> Name mkTupleDataName n = mk_name_d "Data.Singletons.Prelude.Instances" $ "STuple" ++ (show n) --- used when a value name appears in a pattern context --- works only for proper variables (lower-case names) -promoteValNameLhs :: Name -> Name -promoteValNameLhs = promoteValNameLhsPrefix noPrefix - --- like promoteValNameLhs, but adds a prefix to the promoted name -promoteValNameLhsPrefix :: (String, String) -> Name -> Name -promoteValNameLhsPrefix pres@(alpha, _) 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, rest) <- splitUnderscores (nameBase n) - = mkName $ alpha ++ "US" ++ us ++ rest - - | otherwise - = mkName $ toUpcaseStr pres n - --- used when a value name appears in an expression context --- works for both variables and datacons -promoteValRhs :: Name -> DType -promoteValRhs name - | name == nilName - = DConT nilName -- workaround for #21 - - | otherwise - = DConT $ promoteTySym 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 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, rest) <- splitUnderscores (nameBase name) - = default_case (mkName $ "US" ++ us ++ rest) - - | name == nilName - = mkName $ "NilSym" ++ (show sat) - - -- treat unboxed tuples like tuples - | Just degree <- tupleNameDegree_maybe name `mplus` - unboxedTupleNameDegree_maybe name - = mk_name_tc "Data.Singletons.Prelude.Instances" $ - "Tuple" ++ show degree ++ "Sym" ++ (show sat) - - | otherwise - = default_case name - where - default_case :: Name -> Name - default_case name' = - let capped = toUpcaseStr noPrefix name' in - if isHsLetter (head capped) - then mkName (capped ++ "Sym" ++ (show sat)) - else mkName (capped ++ "@#@" -- See Note [Defunctionalization symbol suffixes] - ++ (replicate (sat + 1) '$')) - -promoteClassName :: Name -> Name -promoteClassName = prefixName "P" "#" - mkTyName :: Quasi q => Name -> q Name mkTyName tmName = do let nameStr = nameBase tmName @@ -241,47 +179,9 @@ mkTyName tmName = do mkTyConName :: Int -> Name mkTyConName i = mk_name_tc "Data.Singletons.Internal" $ "TyCon" ++ show i -falseTySym :: DType -falseTySym = promoteValRhs falseName - -trueTySym :: DType -trueTySym = promoteValRhs trueName - boolKi :: DKind boolKi = DConT boolName -andTySym :: DType -andTySym = promoteValRhs andName - --- Singletons - -singDataConName :: Name -> Name -singDataConName nm - | nm == nilName = snilName - | nm == consName = sconsName - | Just degree <- tupleNameDegree_maybe nm = mkTupleDataName degree - | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree - | otherwise = prefixConName "S" "%" nm - -singTyConName :: Name -> Name -singTyConName name - | name == listName = sListName - | Just degree <- tupleNameDegree_maybe name = mkTupleTypeName degree - | Just degree <- unboxedTupleNameDegree_maybe name = mkTupleTypeName degree - | otherwise = prefixName "S" "%" name - -singClassName :: Name -> Name -singClassName = singTyConName - -singValName :: Name -> Name -singValName n - -- Push the 's' past the underscores, as this lets us avoid some unused - -- variable warnings (#229). - | Just (us, rest) <- splitUnderscores (nameBase n) - = prefixName (us ++ "s") "%" $ mkName rest - | otherwise - = prefixName "s" "%" $ upcase n - singFamily :: DType singFamily = DConT singFamilyName diff --git a/src/Data/Singletons/Partition.hs b/src/Data/Singletons/Partition.hs index eb826366..180f6627 100644 --- a/src/Data/Singletons/Partition.hs +++ b/src/Data/Singletons/Partition.hs @@ -27,6 +27,7 @@ import Data.Singletons.Deriving.Show import Data.Singletons.Deriving.Traversable import Data.Singletons.Deriving.Util import Data.Singletons.Names +import Data.Singletons.TH.Options import Language.Haskell.TH.Syntax hiding (showName) import Language.Haskell.TH.Ppr import Language.Haskell.TH.Desugar @@ -63,10 +64,10 @@ instance Monoid PartitionedDecs where -- | Split up a @[DDec]@ into its pieces, extracting 'Ord' instances -- from deriving clauses -partitionDecs :: DsMonad m => [DDec] -> m PartitionedDecs +partitionDecs :: OptionsMonad m => [DDec] -> m PartitionedDecs partitionDecs = concatMapM partitionDec -partitionDec :: DsMonad m => DDec -> m PartitionedDecs +partitionDec :: OptionsMonad m => DDec -> m PartitionedDecs partitionDec (DLetDec (DPragmaD {})) = return mempty partitionDec (DLetDec letdec) = return $ mempty { pd_let_decs = [letdec] } @@ -194,7 +195,7 @@ partitionInstanceDec _ = fail "Only method bodies can be promoted within an instance." partitionDeriving - :: forall m. DsMonad m + :: forall m. OptionsMonad m => Maybe DDerivStrategy -- ^ The deriving strategy, if present. -> DPred -- ^ The class being derived (e.g., 'Eq'), possibly applied to diff --git a/src/Data/Singletons/Promote.hs b/src/Data/Singletons/Promote.hs index 55625e46..420f11eb 100644 --- a/src/Data/Singletons/Promote.hs +++ b/src/Data/Singletons/Promote.hs @@ -30,6 +30,7 @@ import Data.Singletons.Deriving.Enum import Data.Singletons.Deriving.Show import Data.Singletons.Deriving.Util import Data.Singletons.Partition +import Data.Singletons.TH.Options import Data.Singletons.Util import Data.Singletons.Syntax import Prelude hiding (exp) @@ -44,7 +45,7 @@ import qualified GHC.LanguageExtensions.Type as LangExt -- | Generate promoted definitions from a type that is already defined. -- This is generally only useful with classes. -genPromotions :: DsMonad q => [Name] -> q [Dec] +genPromotions :: OptionsMonad q => [Name] -> q [Dec] genPromotions names = do checkForRep names infos <- mapM reifyWithLocals names @@ -53,7 +54,7 @@ genPromotions names = do return $ decsToTH ddecs -- | Promote every declaration given to the type level, retaining the originals. -promote :: DsMonad q => q [Dec] -> q [Dec] +promote :: OptionsMonad q => q [Dec] -> q [Dec] promote qdec = do decls <- qdec ddecls <- withLocalDeclarations decls $ dsDecs decls @@ -63,7 +64,7 @@ promote qdec = do -- | Promote each declaration, discarding the originals. Note that a promoted -- datatype uses the same definition as an original datatype, so this will -- not work with datatypes. Classes, instances, and functions are all fine. -promoteOnly :: DsMonad q => q [Dec] -> q [Dec] +promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec] promoteOnly qdec = do decls <- qdec ddecls <- dsDecs decls @@ -101,7 +102,7 @@ promoteOnly qdec = do -- @MyProxySym0@ will be slightly more general, which means that under rare -- circumstances, you may have to provide extra type signatures if you write -- code which exploits the dependency in @MyProxy@'s kind. -genDefunSymbols :: DsMonad q => [Name] -> q [Dec] +genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec] genDefunSymbols names = do checkForRep names infos <- mapM (dsInfo <=< reifyWithLocals) names @@ -109,43 +110,43 @@ genDefunSymbols names = do return $ decsToTH decs -- | Produce instances for @(==)@ (type-level equality) from the given types -promoteEqInstances :: DsMonad q => [Name] -> q [Dec] +promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec] promoteEqInstances = concatMapM promoteEqInstance -- | Produce instances for 'POrd' from the given types -promoteOrdInstances :: DsMonad q => [Name] -> q [Dec] +promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec] promoteOrdInstances = concatMapM promoteOrdInstance -- | Produce an instance for 'POrd' from the given type -promoteOrdInstance :: DsMonad q => Name -> q [Dec] +promoteOrdInstance :: OptionsMonad q => Name -> q [Dec] promoteOrdInstance = promoteInstance mkOrdInstance "Ord" -- | Produce instances for 'PBounded' from the given types -promoteBoundedInstances :: DsMonad q => [Name] -> q [Dec] +promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec] promoteBoundedInstances = concatMapM promoteBoundedInstance -- | Produce an instance for 'PBounded' from the given type -promoteBoundedInstance :: DsMonad q => Name -> q [Dec] +promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec] promoteBoundedInstance = promoteInstance mkBoundedInstance "Bounded" -- | Produce instances for 'PEnum' from the given types -promoteEnumInstances :: DsMonad q => [Name] -> q [Dec] +promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec] promoteEnumInstances = concatMapM promoteEnumInstance -- | Produce an instance for 'PEnum' from the given type -promoteEnumInstance :: DsMonad q => Name -> q [Dec] +promoteEnumInstance :: OptionsMonad q => Name -> q [Dec] promoteEnumInstance = promoteInstance mkEnumInstance "Enum" -- | Produce instances for 'PShow' from the given types -promoteShowInstances :: DsMonad q => [Name] -> q [Dec] +promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec] promoteShowInstances = concatMapM promoteShowInstance -- | Produce an instance for 'PShow' from the given type -promoteShowInstance :: DsMonad q => Name -> q [Dec] +promoteShowInstance :: OptionsMonad q => Name -> q [Dec] promoteShowInstance = promoteInstance (mkShowInstance ForPromotion) "Show" -- | Produce an instance for @(==)@ (type-level equality) from the given type -promoteEqInstance :: DsMonad q => Name -> q [Dec] +promoteEqInstance :: OptionsMonad q => Name -> q [Dec] promoteEqInstance name = do (tvbs, cons) <- getDataD "I cannot make an instance of (==) for it." name tvbs' <- mapM dsTvb tvbs @@ -155,7 +156,7 @@ promoteEqInstance name = do inst_decs <- mkEqTypeInstance kind cons' return $ decsToTH inst_decs -promoteInstance :: DsMonad q => DerivDesc q -> String -> Name -> q [Dec] +promoteInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec] promoteInstance mk_inst class_name name = do (tvbs, cons) <- getDataD ("I cannot make an instance of " ++ class_name ++ " for it.") name @@ -256,12 +257,13 @@ promoteLetDecs :: (String, String) -- (alpha, symb) prefixes to use -> [DLetDec] -> PrM ([LetBind], ALetDecEnv) -- See Note [Promoting declarations in two stages] promoteLetDecs prefixes decls = do + opts <- getOptions let_dec_env <- buildLetDecEnv decls all_locals <- allLocals let binds = [ (name, foldType (DConT sym) (map DVarT all_locals)) | (name, _) <- OMap.assocs $ lde_defns let_dec_env - , let proName = promoteValNameLhsPrefix prefixes name - sym = promoteTySym proName (length all_locals) ] + , let proName = promotedValueNamePrefix opts prefixes name + sym = defunctionalizedName opts proName (length all_locals) ] (decs, let_dec_env') <- letBind binds $ promoteLetDecEnv prefixes let_dec_env emitDecs decs return (binds, let_dec_env' { lde_proms = OMap.fromList binds }) @@ -294,7 +296,8 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name { lde_defns = defaults , lde_types = meth_sigs , lde_infix = infix_decls } }) = do - let pClsName = promoteClassName cls_name + opts <- getOptions + let pClsName = promotedClassName opts cls_name forallBind cls_kvs_to_bind $ do let meth_sigs_list = OMap.assocs meth_sigs meth_names = map fst meth_sigs_list @@ -326,7 +329,8 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name promote_sig :: Name -> DType -> PrM DDec promote_sig name ty = do - let proName = promoteValNameLhs name + opts <- getOptions + let proName = promotedValueName opts name (argKs, resK) <- promoteUnraveled ty args <- mapM (const $ qNewName "arg") argKs let proTvbs = zipWith DKindedTV args argKs @@ -350,9 +354,11 @@ promoteInstanceDec orig_meth_sigs cls_tvbs_map , id_arg_tys = inst_tys , id_sigs = inst_sigs , id_meths = meths }) = do + opts <- getOptions cls_tvb_names <- lookup_cls_tvb_names inst_kis <- mapM promoteType inst_tys - let kvs_to_bind = foldMap fvDType inst_kis + let pClsName = promotedClassName opts cls_name + kvs_to_bind = foldMap fvDType inst_kis forallBind kvs_to_bind $ do let subst = Map.fromList $ zip cls_tvb_names inst_kis meth_impl = InstanceMethods inst_sigs subst @@ -362,8 +368,6 @@ promoteInstanceDec orig_meth_sigs cls_tvbs_map inst_kis) meths'] return (decl { id_meths = zip (map fst meths) ann_rhss }) where - pClsName = promoteClassName cls_name - lookup_cls_tvb_names :: PrM [Name] lookup_cls_tvb_names = -- First, try consulting the map of class names to their type variables. @@ -378,7 +382,9 @@ promoteInstanceDec orig_meth_sigs cls_tvbs_map reify_cls_tvb_names :: PrM [Name] reify_cls_tvb_names = do - let mk_tvb_names = extract_tvb_names (dsReifyTypeNameInfo pClsName) + opts <- getOptions + let pClsName = promotedClassName opts cls_name + mk_tvb_names = extract_tvb_names (dsReifyTypeNameInfo pClsName) <|> extract_tvb_names (dsReifyTypeNameInfo cls_name) -- See Note [Using dsReifyTypeNameInfo when promoting instances] mb_tvb_names <- runMaybeT mk_tvb_names @@ -444,9 +450,11 @@ promoteMethod :: MethodSort -> PrM (DDec, ALetDecRHS, DType) -- returns (type instance, ALetDecRHS, promoted RHS) promoteMethod meth_sort orig_sigs_map (meth_name, meth_rhs) = do + opts <- getOptions (meth_arg_kis, meth_res_ki) <- promote_meth_ty meth_arg_tvs <- mapM (const $ qNewName "a") meth_arg_kis - let helperNameBase = case nameBase proName of + let proName = promotedValueName opts meth_name + helperNameBase = case nameBase proName of first:_ | not (isHsLetter first) -> "TFHelper" alpha -> alpha @@ -464,6 +472,7 @@ promoteMethod meth_sort orig_sigs_map (meth_name, meth_rhs) = do -- strictly necessary, as kind inference can figure them out just as well. family_args = map DVarT meth_arg_tvs helperName <- newUniqueName helperNameBase + let helperDefunName = defunctionalizedName0 opts helperName (pro_dec, defun_decs, ann_rhs) <- promoteLetDecRHS (ClassMethodRHS meth_arg_kis meth_res_ki) OMap.empty OMap.empty noPrefix helperName meth_rhs @@ -471,12 +480,10 @@ promoteMethod meth_sort orig_sigs_map (meth_name, meth_rhs) = do return ( DTySynInstD (DTySynEqn Nothing (foldType (DConT proName) family_args) - (foldApply (promoteValRhs helperName) (map DVarT meth_arg_tvs))) + (foldApply (DConT helperDefunName) (map DVarT meth_arg_tvs))) , ann_rhs - , DConT (promoteTySym helperName 0) ) + , DConT helperDefunName ) where - proName = promoteValNameLhs meth_name - -- Promote the type of a class method. For a default method, "the type" is -- simply the type of the original method. For an instance method, -- "the type" is like the type of the original method, but substituted for @@ -510,7 +517,9 @@ promoteMethod meth_sort orig_sigs_map (meth_name, meth_rhs) = do -- Attempt to look up a class method's original type. lookup_meth_ty :: PrM ([DKind], DKind) - lookup_meth_ty = + lookup_meth_ty = do + opts <- getOptions + let proName = promotedValueName opts meth_name case OMap.lookup meth_name orig_sigs_map of Just ty -> -- The type of the method is in scope, so promote that. @@ -585,8 +594,9 @@ promoteLetDecEnv prefixes (LetDecEnv { lde_defns = value_env return (decs, let_dec_env') -- Promote a fixity declaration. -promoteInfixDecl :: forall q. DsMonad q => Name -> Fixity -> q (Maybe DDec) +promoteInfixDecl :: forall q. OptionsMonad q => Name -> Fixity -> q (Maybe DDec) promoteInfixDecl name fixity = do + opts <- getOptions mb_ns <- reifyNameSpace name case mb_ns of -- If we can't find the Name for some odd reason, @@ -598,7 +608,7 @@ promoteInfixDecl name fixity = do mb_info <- dsReify name case mb_info of Just (DTyConI DClassD{} _) - -> finish $ promoteClassName name + -> finish $ promotedClassName opts name _ -> never_mind where -- Produce the fixity declaration. @@ -615,20 +625,19 @@ promoteInfixDecl name fixity = do -- Certain function names do not change when promoted (e.g., infix names), -- so don't bother with them. promote_infix_val :: q (Maybe DDec) - promote_infix_val - | nameBase name == nameBase promoted_name - = never_mind - | otherwise - = finish promoted_name - - promoted_name :: Name - promoted_name = promoteValNameLhs name + promote_infix_val = do + opts <- getOptions + let promoted_name :: Name + promoted_name = promotedValueName opts name + if nameBase name == nameBase promoted_name + then never_mind + else finish promoted_name -- Try producing promoted fixity declarations for Names by reifying them -- /without/ consulting quoted declarations. If reification fails, recover and -- return the empty list. -- See [singletons and fixity declarations] in D.S.Single.Fixity, wrinkle 2. -promoteReifiedInfixDecls :: forall q. DsMonad q => [Name] -> q [DDec] +promoteReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec] promoteReifiedInfixDecls = mapMaybeM tryPromoteFixityDeclaration where tryPromoteFixityDeclaration :: Name -> q (Maybe DDec) @@ -662,13 +671,15 @@ promoteLetDecRHS :: LetDecRHSSort , [DDec] -- defunctionalization , ALetDecRHS ) -- annotated RHS promoteLetDecRHS rhs_sort type_env fix_env prefixes name let_dec_rhs = do + opts <- getOptions all_locals <- allLocals case let_dec_rhs of UValue exp -> do (m_argKs, m_resK, ty_num_args) <- promote_let_dec_ty 0 if ty_num_args == 0 then - let prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals in + let proName = promotedValueNamePrefix opts prefixes name + prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals in promote_let_dec_rhs all_locals m_argKs m_resK 0 (promoteExp exp) (\exp' -> [DTySynEqn Nothing prom_fun_lhs exp']) @@ -684,8 +695,10 @@ promoteLetDecRHS rhs_sort type_env fix_env prefixes name let_dec_rhs = do promote_function_rhs :: [Name] -> [DClause] -> PrM (DDec, [DDec], ALetDecRHS) promote_function_rhs all_locals clauses = do + opts <- getOptions numArgs <- count_args clauses - let prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals + let proName = promotedValueNamePrefix opts prefixes name + prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals (m_argKs, m_resK, ty_num_args) <- promote_let_dec_ty numArgs expClauses <- mapM (etaContractOrExpand ty_num_args numArgs) clauses promote_let_dec_rhs all_locals m_argKs m_resK ty_num_args @@ -709,8 +722,10 @@ promoteLetDecRHS rhs_sort type_env fix_env prefixes name let_dec_rhs = do -> PrM (DDec, [DDec], ALetDecRHS) promote_let_dec_rhs all_locals m_argKs m_resK ty_num_args promote_thing mk_prom_eqns mk_alet_dec_rhs = do + opts <- getOptions tyvarNames <- mapM (const $ qNewName "a") m_argKs - let local_tvbs = map DPlainTV all_locals + let proName = promotedValueNamePrefix opts prefixes name + local_tvbs = map DPlainTV all_locals m_fixity = OMap.lookup name fix_env args = zipWith inferMaybeKindTV tyvarNames m_argKs all_args = local_tvbs ++ args @@ -724,9 +739,6 @@ promoteLetDecRHS rhs_sort type_env fix_env prefixes name let_dec_rhs = do , defun_decs , mk_alet_dec_rhs prom_fun_rhs ty_num_args thing ) - proName :: Name - proName = promoteValNameLhsPrefix prefixes name - promote_let_dec_ty :: Int -- The number of arguments to default to if the -- type cannot be inferred. This is 0 for UValues -- and the number of arguments in a single clause @@ -836,7 +848,9 @@ promotePat DWildP = return (DWildCardT, ADWildP) promoteExp :: DExp -> PrM (DType, ADExp) promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name -promoteExp (DConE name) = return $ (promoteValRhs name, ADConE name) +promoteExp (DConE name) = do + opts <- getOptions + return (DConT $ defunctionalizedName0 opts name, ADConE name) promoteExp (DLitE lit) = fmap (, ADLitE lit) $ promoteLitExp lit promoteExp (DAppE exp1 exp2) = do (exp1', ann_exp1) <- promoteExp exp1 @@ -847,6 +861,7 @@ promoteExp (DAppTypeE exp _) = do qReportWarning "Visible type applications are ignored by `singletons`." promoteExp exp promoteExp (DLamE names exp) = do + opts <- getOptions lambdaName <- newUniqueName "Lambda" tyNames <- mapM mkTyName names let var_proms = zip names tyNames @@ -865,7 +880,7 @@ promoteExp (DLamE names exp) = do map DVarT (all_locals ++ tyNames)) rhs]] emitDecsM $ defunctionalize lambdaName Nothing tvbs Nothing - let promLambda = foldl apply (DConT (promoteTySym lambdaName 0)) + let promLambda = foldl apply (DConT (defunctionalizedName opts lambdaName 0)) (map DVarT all_locals) return (promLambda, ADLamE tyNames promLambda names ann_exp) promoteExp (DCaseE exp matches) = do diff --git a/src/Data/Singletons/Promote/Defun.hs b/src/Data/Singletons/Promote/Defun.hs index ce702e91..1a067403 100644 --- a/src/Data/Singletons/Promote/Defun.hs +++ b/src/Data/Singletons/Promote/Defun.hs @@ -17,6 +17,7 @@ import Data.Singletons.Promote.Type import Data.Singletons.Names import Language.Haskell.TH.Syntax import Data.Singletons.Syntax +import Data.Singletons.TH.Options import Data.Singletons.Util import Control.Monad import Data.Foldable @@ -213,6 +214,7 @@ defunctionalize :: Name -> Maybe Fixity -- The name's fixity, if one was declared. -> [DTyVarBndr] -> Maybe DKind -> PrM [DDec] defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do + opts <- getOptions (m_arg_tvbs, m_res_kind) <- eta_expand (noExactTyVars m_arg_tvbs') (noExactTyVars m_res_kind') extra_name <- qNewName "arg" @@ -264,8 +266,8 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do let (m_result, decls) = go (n+1) (arg_tvbs ++ [res_tvb]) res_tvbs tyfun_name = extractTvbName res_tvb - data_name = promoteTySym name n - next_name = promoteTySym name (n+1) + data_name = defunctionalizedName opts name n + next_name = defunctionalizedName opts name (n+1) con_name = prefixName "" ":" $ suffixName "KindInference" "###" data_name m_tyfun = buildTyFunArrow_maybe (extractTvbKind res_tvb) m_result arg_params = -- Implements part (2)(ii) from @@ -323,7 +325,7 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do in (m_tyfun, suppress : data_decl : app_decl : fixity_decl ++ decls) let num_args = length m_arg_tvbs - sat_name = promoteTySym name num_args + sat_name = defunctionalizedName opts name num_args sat_dec = DTySynD sat_name m_arg_tvbs $ foldTypeTvbs (DConT name) m_arg_tvbs sat_fixity_dec = maybeToList $ fmap (mk_fix_decl sat_name) m_fixity diff --git a/src/Data/Singletons/Promote/Eq.hs b/src/Data/Singletons/Promote/Eq.hs index af5159b6..825b7544 100644 --- a/src/Data/Singletons/Promote/Eq.hs +++ b/src/Data/Singletons/Promote/Eq.hs @@ -12,19 +12,21 @@ module Data.Singletons.Promote.Eq where import Language.Haskell.TH.Syntax import Language.Haskell.TH.Desugar import Data.Singletons.Names +import Data.Singletons.TH.Options import Data.Singletons.Util import Control.Monad -- produce a closed type family helper and the instance -- for (==) over the given list of ctors -mkEqTypeInstance :: Quasi q => DKind -> [DCon] -> q [DDec] +mkEqTypeInstance :: OptionsMonad q => DKind -> [DCon] -> q [DDec] mkEqTypeInstance kind cons = do + opts <- getOptions helperName <- newUniqueName "Equals" aName <- qNewName "a" bName <- qNewName "b" true_branches <- mapM (mk_branch helperName) cons - let null_branch = catch_all_case helperName trueName - false_branch = catch_all_case helperName falseName + let null_branch = catch_all_case opts helperName trueName + false_branch = catch_all_case opts helperName falseName branches | null cons = [null_branch] | otherwise = true_branches ++ [false_branch] closedFam = DClosedTypeFamilyD (DTypeFamilyHead helperName @@ -41,13 +43,14 @@ mkEqTypeInstance kind cons = do DTySynEqn Nothing (DConT tyEqName `DAppT` DVarT aName `DAppT` DVarT bName) (foldType (DConT helperName) [DVarT aName, DVarT bName]) - inst = DInstanceD Nothing Nothing [] ((DConT $ promoteClassName eqName) `DAppT` + inst = DInstanceD Nothing Nothing [] ((DConT $ promotedClassName opts eqName) `DAppT` kind) [eqInst] return [closedFam, inst] - where mk_branch :: Quasi q => Name -> DCon -> q DTySynEqn + where mk_branch :: OptionsMonad q => Name -> DCon -> q DTySynEqn mk_branch helper_name con = do + opts <- getOptions let (name, numArgs) = extractNameArgs con lnames <- replicateM numArgs (qNewName "a") rnames <- replicateM numArgs (qNewName "b") @@ -56,21 +59,23 @@ mkEqTypeInstance kind cons = do ltype = foldType (DConT name) lvars rtype = foldType (DConT name) rvars results = zipWith (\l r -> foldType (DConT tyEqName) [l, r]) lvars rvars - result = tyAll results + result = tyAll opts results return $ DTySynEqn Nothing (DConT helper_name `DAppT` ltype `DAppT` rtype) result - catch_all_case :: Name -> Name -> DTySynEqn - catch_all_case helper_name returned_val_name = + catch_all_case :: Options -> Name -> Name -> DTySynEqn + catch_all_case opts helper_name returned_val_name = DTySynEqn Nothing (DConT helper_name `DAppT` DSigT DWildCardT kind `DAppT` DSigT DWildCardT kind) - (promoteValRhs returned_val_name) + (DConT $ defunctionalizedName0 opts returned_val_name) - tyAll :: [DType] -> DType -- "all" at the type level - tyAll [] = (promoteValRhs trueName) - tyAll [one] = one - tyAll (h:t) = foldType (DConT $ promoteValNameLhs andName) [h, (tyAll t)] + tyAll :: Options -> [DType] -> DType -- "all" at the type level + tyAll opts = go + where + go [] = DConT $ defunctionalizedName0 opts trueName + go [one] = one + go (h:t) = foldType (DConT $ promotedValueName opts andName) [h, (go t)] -- I could use the Apply nonsense here, but there's no reason to diff --git a/src/Data/Singletons/Promote/Monad.hs b/src/Data/Singletons/Promote/Monad.hs index ce926151..6e1d039a 100644 --- a/src/Data/Singletons/Promote/Monad.hs +++ b/src/Data/Singletons/Promote/Monad.hs @@ -26,21 +26,23 @@ import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap import Language.Haskell.TH.Desugar.OMap.Strict (OMap) import qualified Language.Haskell.TH.Desugar.OSet as OSet import Language.Haskell.TH.Desugar.OSet (OSet) -import Data.Singletons.Names import Data.Singletons.Syntax +import Data.Singletons.TH.Options type LetExpansions = OMap Name DType -- from **term-level** name -- environment during promotion data PrEnv = - PrEnv { pr_lambda_bound :: OMap Name Name + PrEnv { pr_options :: Options + , pr_lambda_bound :: OMap Name Name , pr_let_bound :: LetExpansions , pr_forall_bound :: OSet Name -- See Note [Explicitly binding kind variables] , pr_local_decls :: [Dec] } emptyPrEnv :: PrEnv -emptyPrEnv = PrEnv { pr_lambda_bound = OMap.empty +emptyPrEnv = PrEnv { pr_options = defaultOptions + , pr_lambda_bound = OMap.empty , pr_let_bound = OMap.empty , pr_forall_bound = OSet.empty , pr_local_decls = [] } @@ -54,6 +56,9 @@ newtype PrM a = PrM (ReaderT PrEnv (WriterT [DDec] Q) a) instance DsMonad PrM where localDeclarations = asks pr_local_decls +instance OptionsMonad PrM where + getOptions = asks pr_options + -- return *type-level* names allLocals :: MonadReader PrEnv m => m [Name] allLocals = do @@ -92,10 +97,11 @@ letBind binds = local add_binds lookupVarE :: Name -> PrM DType lookupVarE n = do + opts <- getOptions lets <- asks pr_let_bound case OMap.lookup n lets of Just ty -> return ty - Nothing -> return $ promoteValRhs n + Nothing -> return $ DConT $ defunctionalizedName0 opts n -- Add to the set of bound kind variables currently in scope. -- See Note [Explicitly binding kind variables] @@ -109,20 +115,22 @@ forallBind kvs1 = allBoundKindVars :: PrM (OSet Name) allBoundKindVars = asks pr_forall_bound -promoteM :: DsMonad q => [Dec] -> PrM a -> q (a, [DDec]) +promoteM :: OptionsMonad q => [Dec] -> PrM a -> q (a, [DDec]) promoteM locals (PrM rdr) = do + opts <- getOptions other_locals <- localDeclarations - let wr = runReaderT rdr (emptyPrEnv { pr_local_decls = other_locals ++ locals }) + let wr = runReaderT rdr (emptyPrEnv { pr_options = opts + , pr_local_decls = other_locals ++ locals }) q = runWriterT wr runQ q -promoteM_ :: DsMonad q => [Dec] -> PrM () -> q [DDec] +promoteM_ :: OptionsMonad q => [Dec] -> PrM () -> q [DDec] promoteM_ locals thing = do ((), decs) <- promoteM locals thing return decs -- promoteM specialized to [DDec] -promoteMDecs :: DsMonad q => [Dec] -> PrM [DDec] -> q [DDec] +promoteMDecs :: OptionsMonad q => [Dec] -> PrM [DDec] -> q [DDec] promoteMDecs locals thing = do (decs1, decs2) <- promoteM locals thing return $ decs1 ++ decs2 diff --git a/src/Data/Singletons/Single.hs b/src/Data/Singletons/Single.hs index 899ad830..1ab2204f 100644 --- a/src/Data/Singletons/Single.hs +++ b/src/Data/Singletons/Single.hs @@ -31,6 +31,7 @@ import Data.Singletons.Single.Defun import Data.Singletons.Single.Fixity import Data.Singletons.Single.Eq import Data.Singletons.Syntax +import Data.Singletons.TH.Options import Data.Singletons.Partition import Language.Haskell.TH.Desugar import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap @@ -85,7 +86,7 @@ contract constructors. This is the point of buildDataLets. -- > $(genSingletons [''Bool, ''Maybe, ''Either, ''[]]) -- -- to generate singletons for Prelude types. -genSingletons :: DsMonad q => [Name] -> q [Dec] +genSingletons :: OptionsMonad q => [Name] -> q [Dec] genSingletons names = do checkForRep names ddecs <- concatMapM (singInfo <=< dsInfo <=< reifyWithLocals) names @@ -95,7 +96,7 @@ genSingletons names = do -- the original declarations. -- See for -- further explanation. -singletons :: DsMonad q => q [Dec] -> q [Dec] +singletons :: OptionsMonad q => q [Dec] -> q [Dec] singletons qdecs = do decs <- qdecs ddecs <- withLocalDeclarations decs $ dsDecs decs @@ -106,15 +107,15 @@ singletons qdecs = do -- the original declarations. Note that a singleton based on a datatype needs -- the original datatype, so this will fail if it sees any datatype declarations. -- Classes, instances, and functions are all fine. -singletonsOnly :: DsMonad q => q [Dec] -> q [Dec] +singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec] singletonsOnly = (>>= wrapDesugar singTopLevelDecs) -- | Create instances of 'SEq' and type-level @(==)@ for each type in the list -singEqInstances :: DsMonad q => [Name] -> q [Dec] +singEqInstances :: OptionsMonad q => [Name] -> q [Dec] singEqInstances = concatMapM singEqInstance -- | Create instance of 'SEq' and type-level @(==)@ for the given type -singEqInstance :: DsMonad q => Name -> q [Dec] +singEqInstance :: OptionsMonad q => Name -> q [Dec] singEqInstance name = do promotion <- promoteEqInstance name dec <- singEqualityInstance sEqClassDesc name @@ -122,26 +123,26 @@ singEqInstance name = do -- | Create instances of 'SEq' (only -- no instance for @(==)@, which 'SEq' generally -- relies on) for each type in the list -singEqInstancesOnly :: DsMonad q => [Name] -> q [Dec] +singEqInstancesOnly :: OptionsMonad q => [Name] -> q [Dec] singEqInstancesOnly = concatMapM singEqInstanceOnly -- | Create instances of 'SEq' (only -- no instance for @(==)@, which 'SEq' generally -- relies on) for the given type -singEqInstanceOnly :: DsMonad q => Name -> q [Dec] +singEqInstanceOnly :: OptionsMonad q => Name -> q [Dec] singEqInstanceOnly name = singEqualityInstance sEqClassDesc name -- | Create instances of 'SDecide', 'TestEquality', and 'TestCoercion' for each -- type in the list. -singDecideInstances :: DsMonad q => [Name] -> q [Dec] +singDecideInstances :: OptionsMonad q => [Name] -> q [Dec] singDecideInstances = concatMapM singDecideInstance -- | Create instance of 'SDecide', 'TestEquality', and 'TestCoercion' for the -- given type. -singDecideInstance :: DsMonad q => Name -> q [Dec] +singDecideInstance :: OptionsMonad q => Name -> q [Dec] singDecideInstance name = singEqualityInstance sDecideClassDesc name -- generalized function for creating equality instances -singEqualityInstance :: DsMonad q => EqualityClassDesc q -> Name -> q [Dec] +singEqualityInstance :: OptionsMonad q => EqualityClassDesc q -> Name -> q [Dec] singEqualityInstance desc@(_, _, className, _) name = do (tvbs, cons) <- getDataD ("I cannot make an instance of " ++ show className ++ " for it.") name @@ -160,45 +161,45 @@ singEqualityInstance desc@(_, _, className, _) name = do return $ decsToTH (eqInstance:testInstances) -- | Create instances of 'SOrd' for the given types -singOrdInstances :: DsMonad q => [Name] -> q [Dec] +singOrdInstances :: OptionsMonad q => [Name] -> q [Dec] singOrdInstances = concatMapM singOrdInstance -- | Create instance of 'SOrd' for the given type -singOrdInstance :: DsMonad q => Name -> q [Dec] +singOrdInstance :: OptionsMonad q => Name -> q [Dec] singOrdInstance = singInstance mkOrdInstance "Ord" -- | Create instances of 'SBounded' for the given types -singBoundedInstances :: DsMonad q => [Name] -> q [Dec] +singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec] singBoundedInstances = concatMapM singBoundedInstance -- | Create instance of 'SBounded' for the given type -singBoundedInstance :: DsMonad q => Name -> q [Dec] +singBoundedInstance :: OptionsMonad q => Name -> q [Dec] singBoundedInstance = singInstance mkBoundedInstance "Bounded" -- | Create instances of 'SEnum' for the given types -singEnumInstances :: DsMonad q => [Name] -> q [Dec] +singEnumInstances :: OptionsMonad q => [Name] -> q [Dec] singEnumInstances = concatMapM singEnumInstance -- | Create instance of 'SEnum' for the given type -singEnumInstance :: DsMonad q => Name -> q [Dec] +singEnumInstance :: OptionsMonad q => Name -> q [Dec] singEnumInstance = singInstance mkEnumInstance "Enum" -- | Create instance of 'SShow' for the given type -- -- (Not to be confused with 'showShowInstance'.) -singShowInstance :: DsMonad q => Name -> q [Dec] +singShowInstance :: OptionsMonad q => Name -> q [Dec] singShowInstance = singInstance (mkShowInstance ForPromotion) "Show" -- | Create instances of 'SShow' for the given types -- -- (Not to be confused with 'showSingInstances'.) -singShowInstances :: DsMonad q => [Name] -> q [Dec] +singShowInstances :: OptionsMonad q => [Name] -> q [Dec] singShowInstances = concatMapM singShowInstance -- | Create instance of 'Show' for the given singleton type -- -- (Not to be confused with 'singShowInstance'.) -showSingInstance :: DsMonad q => Name -> q [Dec] +showSingInstance :: OptionsMonad q => Name -> q [Dec] showSingInstance name = do (tvbs, cons) <- getDataD ("I cannot make an instance of Show for it.") name dtvbs <- mapM dsTvb tvbs @@ -217,7 +218,7 @@ showSingInstance name = do -- | Create instances of 'Show' for the given singleton types -- -- (Not to be confused with 'singShowInstances'.) -showSingInstances :: DsMonad q => [Name] -> q [Dec] +showSingInstances :: OptionsMonad q => [Name] -> q [Dec] showSingInstances = concatMapM showSingInstance -- | Create an instance for @'SingI' TyCon{N}@, where @N@ is the positive @@ -269,7 +270,7 @@ singITyConInstance n DVarE withSingIName `DAppE` DVarE x `DAppE` DVarE singMethName]] -singInstance :: DsMonad q => DerivDesc q -> String -> Name -> q [Dec] +singInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec] singInstance mk_inst inst_name name = do (tvbs, cons) <- getDataD ("I cannot make an instance of " ++ inst_name ++ " for it.") name @@ -283,7 +284,7 @@ singInstance mk_inst inst_name name = do decs' <- singDecsM [] $ (:[]) <$> singInstD a_inst return $ decsToTH (decs ++ decs') -singInfo :: DsMonad q => DInfo -> q [DDec] +singInfo :: OptionsMonad q => DInfo -> q [DDec] singInfo (DTyConI dec _) = singTopLevelDecs [] [dec] singInfo (DPrimTyConI _name _numArgs _unlifted) = @@ -295,7 +296,7 @@ singInfo (DTyVarI _name _ty) = singInfo (DPatSynI {}) = fail "Singling of pattern synonym info not supported" -singTopLevelDecs :: DsMonad q => [Dec] -> [DDec] -> q [DDec] +singTopLevelDecs :: OptionsMonad q => [Dec] -> [DDec] -> q [DDec] singTopLevelDecs locals raw_decls = withLocalDeclarations locals $ do decls <- expand raw_decls -- expand type synonyms PDecs { pd_let_decs = letDecls @@ -320,8 +321,9 @@ singTopLevelDecs locals raw_decls = withLocalDeclarations locals $ do return (letDecEnv, classes', insts') singDecsM locals $ do - let letBinds = concatMap buildDataLets datas - ++ concatMap buildMethLets classes + dataLetBinds <- concatMapM buildDataLets datas + methLetBinds <- concatMapM buildMethLets classes + let letBinds = dataLetBinds ++ methLetBinds (newLetDecls, singIDefunDecls, newDecls) <- bindLets letBinds $ singLetDecEnv letDecEnv $ do @@ -337,32 +339,36 @@ singTopLevelDecs locals raw_decls = withLocalDeclarations locals $ do return $ promDecls ++ (map DLetDec newLetDecls) ++ singIDefunDecls ++ newDecls -- see comment at top of file -buildDataLets :: DataDecl -> [(Name, DExp)] -buildDataLets (DataDecl _name _tvbs cons) = - concatMap con_num_args cons +buildDataLets :: OptionsMonad q => DataDecl -> q [(Name, DExp)] +buildDataLets (DataDecl _name _tvbs cons) = do + opts <- getOptions + pure $ concatMap (con_num_args opts) cons where - con_num_args :: DCon -> [(Name, DExp)] - con_num_args (DCon _tvbs _cxt name fields _rty) = + con_num_args :: Options -> DCon -> [(Name, DExp)] + con_num_args opts (DCon _tvbs _cxt name fields _rty) = (name, wrapSingFun (length (tysOfConFields fields)) - (promoteValRhs name) (DConE $ singDataConName name)) - : rec_selectors fields + (DConT $ defunctionalizedName0 opts name) + (DConE $ singledDataConName opts name)) + : rec_selectors opts fields - rec_selectors :: DConFields -> [(Name, DExp)] - rec_selectors (DNormalC {}) = [] - rec_selectors (DRecC fields) = + rec_selectors :: Options -> DConFields -> [(Name, DExp)] + rec_selectors _ (DNormalC {}) = [] + rec_selectors opts (DRecC fields) = let names = map fstOf3 fields in - [ (name, wrapSingFun 1 (promoteValRhs name) (DVarE $ singValName name)) + [ (name, wrapSingFun 1 (DConT $ defunctionalizedName0 opts name) + (DVarE $ singledValueName opts name)) | name <- names ] -- see comment at top of file -buildMethLets :: UClassDecl -> [(Name, DExp)] -buildMethLets (ClassDecl { cd_lde = LetDecEnv { lde_types = meth_sigs } }) = - map mk_bind (OMap.assocs meth_sigs) +buildMethLets :: OptionsMonad q => UClassDecl -> q [(Name, DExp)] +buildMethLets (ClassDecl { cd_lde = LetDecEnv { lde_types = meth_sigs } }) = do + opts <- getOptions + pure $ map (mk_bind opts) (OMap.assocs meth_sigs) where - mk_bind (meth_name, meth_ty) = + mk_bind opts (meth_name, meth_ty) = ( meth_name - , wrapSingFun (countArgs meth_ty) (promoteValRhs meth_name) - (DVarE $ singValName meth_name) ) + , wrapSingFun (countArgs meth_ty) (DConT $ defunctionalizedName0 opts meth_name) + (DVarE $ singledValueName opts meth_name) ) singClassD :: AClassDecl -> SgM DDec singClassD (ClassDecl { cd_cxt = cls_cxt @@ -375,13 +381,16 @@ singClassD (ClassDecl { cd_cxt = cls_cxt , lde_proms = promoted_defaults , lde_bound_kvs = meth_bound_kvs } }) = bindContext [foldTypeTvbs (DConT cls_name) cls_tvbs] $ do + opts <- getOptions cls_infix_decls <- singReifiedInfixDecls $ cls_name:meth_names (sing_sigs, _, tyvar_names, cxts, res_kis, singIDefunss) <- unzip6 <$> zipWithM (singTySig no_meth_defns meth_sigs meth_bound_kvs) - meth_names (map promoteValRhs meth_names) + meth_names + (map (DConT . defunctionalizedName0 opts) meth_names) emitDecs $ cls_infix_decls ++ concat singIDefunss let default_sigs = catMaybes $ - zipWith4 mk_default_sig meth_names sing_sigs tyvar_names res_kis + zipWith4 (mk_default_sig opts) meth_names sing_sigs + tyvar_names res_kis res_ki_map = Map.fromList (zip meth_names (map (fromMaybe always_sig) res_kis)) sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList tyvar_names) @@ -391,7 +400,7 @@ singClassD (ClassDecl { cd_cxt = cls_cxt fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs fixities cls_cxt' <- mapM singPred cls_cxt return $ DClassD cls_cxt' - (singClassName cls_name) + (singledClassName opts cls_name) cls_tvbs cls_fundeps -- they are fine without modification (map DLetDec (sing_sigs ++ sing_meths ++ fixities') ++ default_sigs) @@ -400,11 +409,11 @@ singClassD (ClassDecl { cd_cxt = cls_cxt always_sig = error "Internal error: no signature for default method" meth_names = map fst $ OMap.assocs meth_sigs - mk_default_sig meth_name (DSigD s_name sty) bound_kvs (Just res_ki) = - DDefaultSigD s_name <$> add_constraints meth_name sty bound_kvs res_ki - mk_default_sig _ _ _ _ = error "Internal error: a singled signature isn't a signature." + mk_default_sig opts meth_name (DSigD s_name sty) bound_kvs (Just res_ki) = + DDefaultSigD s_name <$> add_constraints opts meth_name sty bound_kvs res_ki + mk_default_sig _ _ _ _ _ = error "Internal error: a singled signature isn't a signature." - add_constraints meth_name sty (_, bound_kvs) res_ki = do -- Maybe monad + add_constraints opts meth_name sty (_, bound_kvs) res_ki = do -- Maybe monad (tvbs, cxt, args, res) <- unravelVanillaDType sty prom_dflt <- OMap.lookup meth_name promoted_defaults @@ -425,11 +434,12 @@ singClassD (ClassDecl { cd_cxt = cls_cxt -- Which applies Bar/BarDefault to b, which shouldn't happen. let tvs = map tvbToType $ filter (\tvb -> extractTvbName tvb `Set.member` bound_kv_set) tvbs + prom_meth = DConT $ defunctionalizedName0 opts meth_name default_pred = foldType (DConT equalityName) -- NB: Need the res_ki here to prevent ambiguous -- kinds in result-inferred default methods. -- See #175 - [ foldApply (promoteValRhs meth_name) tvs `DSigT` res_ki + [ foldApply prom_meth tvs `DSigT` res_ki , foldApply prom_dflt tvs ] return $ DForallT ForallInvis tvbs $ DConstrainedT (default_pred : cxt) (ravel args res) @@ -439,6 +449,8 @@ singClassD (ClassDecl { cd_cxt = cls_cxt singInstD :: AInstDecl -> SgM DDec singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys , id_sigs = inst_sigs, id_meths = ann_meths }) = do + opts <- getOptions + let s_inst_name = singledClassName opts inst_name bindContext cxt $ do cxt' <- mapM singPred cxt inst_kis <- mapM promoteType inst_tys @@ -450,11 +462,10 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys meths) where - s_inst_name = singClassName inst_name - sing_meth :: Name -> ALetDecRHS -> SgM [DDec] sing_meth name rhs = do - mb_s_info <- dsReify (singValName name) + opts <- getOptions + mb_s_info <- dsReify (singledValueName opts name) inst_kis <- mapM promoteType inst_tys let mk_subst cls_tvbs = Map.fromList $ zip (map extractTvbName vis_cls_tvbs) inst_kis where @@ -476,7 +487,7 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys -- resulted in #167. raw_ty <- expand inner_ty (s_ty, _num_args, tyvar_names, ctxt, _arg_kis, res_ki) - <- singType bound_kvs (promoteValRhs name) raw_ty + <- singType bound_kvs (DConT $ defunctionalizedName0 opts name) raw_ty pure (s_ty, tyvar_names, ctxt, res_ki) (s_ty, tyvar_names, ctxt, m_res_ki) <- case OMap.lookup name inst_sigs of @@ -520,7 +531,7 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys meth' <- singLetDecRHS (Map.singleton name tyvar_names) (Map.singleton name ctxt) kind_map name rhs - return $ map DLetDec [DSigD (singValName name) s_ty, meth'] + return $ map DLetDec [DSigD (singledValueName opts name) s_ty, meth'] singLetDecEnv :: ALetDecEnv -> SgM a @@ -562,8 +573,9 @@ singTySig :: OMap Name ALetDecRHS -- definitions , Maybe DKind -- the result kind in the tysig , [DDec] -- SingI instances for defun symbols ) -singTySig defns types bound_kvs name prom_ty = - let sName = singValName name in +singTySig defns types bound_kvs name prom_ty = do + opts <- getOptions + let sName = singledValueName opts name case OMap.lookup name types of Nothing -> do num_args <- guess_num_args @@ -620,11 +632,12 @@ singLetDecRHS :: Map Name [Name] -- (might not be known) -> Map Name DKind -- result kind (might not be known) -> Name -> ALetDecRHS -> SgM DLetDec -singLetDecRHS bound_names cxts res_kis name ld_rhs = +singLetDecRHS bound_names cxts res_kis name ld_rhs = do + opts <- getOptions bindContext (Map.findWithDefault [] name cxts) $ case ld_rhs of AValue prom num_arrows exp -> - DValD (DVarP (singValName name)) <$> + DValD (DVarP (singledValueName opts name)) <$> (wrapUnSingFun num_arrows prom <$> singExp exp (Map.lookup name res_kis)) AFunction prom_fun num_arrows clauses -> let tyvar_names = case Map.lookup name bound_names of @@ -632,7 +645,7 @@ singLetDecRHS bound_names cxts res_kis name ld_rhs = Just ns -> ns res_ki = Map.lookup name res_kis in - DFunD (singValName name) <$> + DFunD (singledValueName opts name) <$> mapM (singClause prom_fun num_arrows tyvar_names res_ki) clauses singClause :: DType -- the promoted function @@ -671,12 +684,16 @@ singPat var_proms = go go (ADLitP _lit) = fail "Singling of literal patterns not yet supported" go (ADVarP name) = do + opts <- getOptions tyname <- case Map.lookup name var_proms of Nothing -> fail "Internal error: unknown variable when singling pattern" Just tyname -> return tyname - pure $ DVarP (singValName name) `DSigP` (singFamily `DAppT` DVarT tyname) - go (ADConP name pats) = DConP (singDataConName name) <$> mapM go pats + pure $ DVarP (singledValueName opts name) + `DSigP` (singFamily `DAppT` DVarT tyname) + go (ADConP name pats) = do + opts <- getOptions + DConP (singledDataConName opts name) <$> mapM go pats go (ADTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern during singleton generation." @@ -815,8 +832,9 @@ singExp :: ADExp -> Maybe DKind -- the kind of the expression, if known -> SgM DExp -- See Note [Why error is so special] singExp (ADVarE err `ADAppE` arg) _res_ki - | err == errorName = DAppE (DVarE (singValName err)) <$> - singExp arg (Just (DConT symbolName)) + | err == errorName = do opts <- getOptions + DAppE (DVarE (singledValueName opts err)) <$> + singExp arg (Just (DConT symbolName)) singExp (ADVarE name) _res_ki = lookupVarE name singExp (ADConE name) _res_ki = lookupConE name singExp (ADLitE lit) _res_ki = singLit lit @@ -829,7 +847,8 @@ singExp (ADAppE e1 e2) _res_ki = do then return $ e1' `DAppE` e2' else return $ (DVarE applySingName) `DAppE` e1' `DAppE` e2' singExp (ADLamE ty_names prom_lam names exp) _res_ki = do - let sNames = map singValName names + opts <- getOptions + let sNames = map (singledValueName opts) names exp' <- singExp exp Nothing -- we need to bind the type variables... but DLamE doesn't allow SigT patterns. -- So: build a case diff --git a/src/Data/Singletons/Single/Data.hs b/src/Data/Singletons/Single/Data.hs index c5db20a0..2d3624a4 100644 --- a/src/Data/Singletons/Single/Data.hs +++ b/src/Data/Singletons/Single/Data.hs @@ -20,12 +20,14 @@ import Data.Singletons.Promote.Type import Data.Singletons.Util import Data.Singletons.Names import Data.Singletons.Syntax +import Data.Singletons.TH.Options import Control.Monad -- We wish to consider the promotion of "Rep" to be * -- not a promoted data constructor. singDataD :: DataDecl -> SgM [DDec] singDataD (DataDecl name tvbs ctors) = do + opts <- getOptions let tvbNames = map extractTvbName tvbs k <- promoteType (foldType (DConT name) (map DVarT tvbNames)) ctors' <- mapM (singCtor name) ctors @@ -48,7 +50,7 @@ singDataD (DataDecl name tvbs ctors) = do , DLetDec $ DFunD toSingName (toSingClauses `orIfEmpty` [emptyToSingClause]) ] - let singDataName = singTyConName name + let singDataName = singledDataTypeName opts name -- e.g. type instance Sing @Nat = SNat singSynInst = DTySynInstD $ DTySynEqn Nothing @@ -59,7 +61,7 @@ singDataD (DataDecl name tvbs ctors) = do return $ (DDataD Data [] singDataName [] (Just kindedSingTy) ctors' []) : singSynInst : - singKindInst : + [singKindInst | genSingKindInsts opts] ++ ctorFixities where -- in the Rep case, the names of the constructors are in the wrong scope -- (they're types, not datacons), so we have to reinterpret them. @@ -70,16 +72,18 @@ singDataD (DataDecl name tvbs ctors) = do mkFromSingClause :: DCon -> SgM DClause mkFromSingClause c = do + opts <- getOptions let (cname, numArgs) = extractNameArgs c cname' <- mkConName cname varNames <- replicateM numArgs (qNewName "b") - return $ DClause [DConP (singDataConName cname) (map DVarP varNames)] + return $ DClause [DConP (singledDataConName opts cname) (map DVarP varNames)] (foldExp (DConE cname') (map (DAppE (DVarE fromSingName) . DVarE) varNames)) mkToSingClause :: DCon -> SgM DClause mkToSingClause (DCon _tvbs _cxt cname fields _rty) = do + opts <- getOptions let types = tysOfConFields fields varNames <- mapM (const $ qNewName "b") types svarNames <- mapM (const $ qNewName "c") types @@ -93,7 +97,7 @@ singDataD (DataDecl name tvbs ctors) = do (map (DConP someSingDataName . listify . DVarP) svarNames) (DAppE (DConE someSingDataName) - (foldExp (DConE (singDataConName cname)) + (foldExp (DConE (singledDataConName opts cname)) (map DVarE svarNames)))) mkToSingVarPat :: Name -> DKind -> DPat @@ -127,8 +131,9 @@ singCtor dataName (DCon con_tvbs cxt name fields rty) = fail "Singling of constrained constructors not yet supported" | otherwise = do + opts <- getOptions let types = tysOfConFields fields - sName = singDataConName name + sName = singledDataConName opts name sCon = DConE sName pCon = DConT name checkVanillaDType $ DForallT ForallInvis con_tvbs $ ravel types rty @@ -158,11 +163,11 @@ singCtor dataName (DCon con_tvbs cxt name fields rty) conFields = case fields of DNormalC dInfix _ -> DNormalC dInfix $ map (noBang,) args DRecC rec_fields -> - DRecC [ (singValName field_name, noBang, arg) + DRecC [ (singledValueName opts field_name, noBang, arg) | (field_name, _, _) <- rec_fields | arg <- args ] return $ DCon all_tvbs [] sName conFields - (DConT (singTyConName dataName) `DAppT` + (DConT (singledDataTypeName opts dataName) `DAppT` (foldType pCon indices `DSigT` rty')) -- Make sure to include an explicit `rty'` kind annotation. -- See Note [Preserve the order of type variables during singling], diff --git a/src/Data/Singletons/Single/Defun.hs b/src/Data/Singletons/Single/Defun.hs index 92c2b688..f4b17798 100644 --- a/src/Data/Singletons/Single/Defun.hs +++ b/src/Data/Singletons/Single/Defun.hs @@ -19,6 +19,7 @@ import Data.Singletons.Names import Data.Singletons.Promote.Defun import Data.Singletons.Single.Monad import Data.Singletons.Single.Type +import Data.Singletons.TH.Options import Data.Singletons.Util import Language.Haskell.TH.Desugar import Language.Haskell.TH.Syntax @@ -57,10 +58,11 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res = case mb_ty_args of [] -> pure [] -- If a function has no arguments, then it has no -- defunctionalization symbols, so there's nothing to be done. - _ -> do sty_ctxt <- mapM singPred ty_ctxt + _ -> do opts <- getOptions + sty_ctxt <- mapM singPred ty_ctxt names <- replicateM (length mb_ty_args) $ qNewName "d" let tvbs = zipWith inferMaybeKindTV names mb_ty_args - (_, insts) = go 0 sty_ctxt [] tvbs + (_, insts) = go opts 0 sty_ctxt [] tvbs pure insts where num_ty_args :: Int @@ -100,15 +102,15 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res = -- the @arg_tvbs@ list at each iteration. In practice, this is unlikely -- to be a performance bottleneck since the number of arguments rarely -- gets to be that large. - go :: Int -> DCxt -> [DTyVarBndr] -> [DTyVarBndr] + go :: Options -> Int -> DCxt -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DKind, [DDec]) - go _ _ _ [] = (mb_ty_res, []) - go sym_num sty_ctxt arg_tvbs (res_tvb:res_tvbs) = + go _ _ _ _ [] = (mb_ty_res, []) + go opts sym_num sty_ctxt arg_tvbs (res_tvb:res_tvbs) = (mb_new_res, new_inst:insts) where mb_res :: Maybe DKind insts :: [DDec] - (mb_res, insts) = go (sym_num + 1) sty_ctxt (arg_tvbs ++ [res_tvb]) res_tvbs + (mb_res, insts) = go opts (sym_num + 1) sty_ctxt (arg_tvbs ++ [res_tvb]) res_tvbs mb_new_res :: Maybe DKind mb_new_res = mk_inst_kind res_tvb mb_res @@ -152,12 +154,13 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res = $ mk_sing_fun_expr sing_exp ] where defun_inst_ty :: DType - defun_inst_ty = foldType (DConT (promoteTySym n sym_num)) arg_tvb_tys + defun_inst_ty = foldType (DConT (defunctionalizedName opts n sym_num)) + arg_tvb_tys sing_exp :: DExp sing_exp = case ns of - DataName -> DConE $ singDataConName n - _ -> DVarE $ singValName n + DataName -> DConE $ singledDataConName opts n + _ -> DVarE $ singledValueName opts n {- Note [singDefuns and type inference] diff --git a/src/Data/Singletons/Single/Eq.hs b/src/Data/Singletons/Single/Eq.hs index 5b791197..aa602968 100644 --- a/src/Data/Singletons/Single/Eq.hs +++ b/src/Data/Singletons/Single/Eq.hs @@ -11,6 +11,7 @@ module Data.Singletons.Single.Eq where import Language.Haskell.TH.Syntax import Language.Haskell.TH.Desugar import Data.Singletons.Deriving.Infer +import Data.Singletons.TH.Options import Data.Singletons.Util import Data.Singletons.Names import Control.Monad @@ -18,7 +19,7 @@ import Control.Monad -- making the SEq instance and the SDecide instance are rather similar, -- so we generalize type EqualityClassDesc q = ((DCon, DCon) -> q DClause, q DClause, Name, Name) -sEqClassDesc, sDecideClassDesc :: Quasi q => EqualityClassDesc q +sEqClassDesc, sDecideClassDesc :: OptionsMonad q => EqualityClassDesc q sEqClassDesc = (mkEqMethClause, mkEmptyEqMethClause, sEqClassName, sEqMethName) sDecideClassDesc = (mkDecideMethClause, mkEmptyDecideMethClause, sDecideClassName, sDecideMethName) @@ -41,16 +42,17 @@ data TestInstance = TestEquality | TestCoercion -- Make an instance of TestEquality or TestCoercion by leveraging SDecide. -mkTestInstance :: DsMonad q => Maybe DCxt -> DKind +mkTestInstance :: OptionsMonad q => Maybe DCxt -> DKind -> Name -- ^ The name of the data type -> [DCon] -- ^ The /original/ constructors (for inferring the instance context) -> TestInstance -> q DDec mkTestInstance mb_ctxt k data_name ctors ti = do + opts <- getOptions constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) k ctors pure $ DInstanceD Nothing Nothing constraints (DAppT (DConT tiClassName) - (DConT (singTyConName data_name) + (DConT (singledDataTypeName opts data_name) `DSigT` (DArrowT `DAppT` k `DAppT` DConT typeKindName))) [DLetDec $ DFunD tiMethName [DClause [] (DVarE tiDefaultName)]] @@ -60,9 +62,10 @@ mkTestInstance mb_ctxt k data_name ctors ti = do TestEquality -> (testEqualityClassName, testEqualityMethName, decideEqualityName) TestCoercion -> (testCoercionClassName, testCoercionMethName, decideCoercionName) -mkEqMethClause :: Quasi q => (DCon, DCon) -> q DClause +mkEqMethClause :: OptionsMonad q => (DCon, DCon) -> q DClause mkEqMethClause (c1, c2) | lname == rname = do + opts <- getOptions lnames <- replicateM lNumArgs (qNewName "a") rnames <- replicateM lNumArgs (qNewName "b") let lpats = map DVarP lnames @@ -71,17 +74,20 @@ mkEqMethClause (c1, c2) rvars = map DVarE rnames return $ DClause [DConP lname lpats, DConP rname rpats] - (allExp (zipWith (\l r -> foldExp (DVarE sEqMethName) [l, r]) - lvars rvars)) - | otherwise = + (allExp opts (zipWith (\l r -> foldExp (DVarE sEqMethName) [l, r]) + lvars rvars)) + | otherwise = do + opts <- getOptions return $ DClause [DConP lname (replicate lNumArgs DWildP), DConP rname (replicate rNumArgs DWildP)] - (DConE $ singDataConName falseName) - where allExp :: [DExp] -> DExp - allExp [] = DConE $ singDataConName trueName - allExp [one] = one - allExp (h:t) = DAppE (DAppE (DVarE $ singValName andName) h) (allExp t) + (DConE $ singledDataConName opts falseName) + where allExp :: Options -> [DExp] -> DExp + allExp opts = go + where + go [] = DConE $ singledDataConName opts trueName + go [one] = one + go (h:t) = DAppE (DAppE (DVarE $ singledValueName opts andName) h) (go t) (lname, lNumArgs) = extractNameArgs c1 (rname, rNumArgs) = extractNameArgs c2 diff --git a/src/Data/Singletons/Single/Fixity.hs b/src/Data/Singletons/Single/Fixity.hs index 855af71b..bd98b2d2 100644 --- a/src/Data/Singletons/Single/Fixity.hs +++ b/src/Data/Singletons/Single/Fixity.hs @@ -4,25 +4,26 @@ module Data.Singletons.Single.Fixity where import Prelude hiding ( exp ) import Language.Haskell.TH hiding ( cxt ) import Language.Haskell.TH.Syntax (NameSpace(..), Quasi(..)) +import Data.Singletons.TH.Options import Data.Singletons.Util -import Data.Singletons.Names import Language.Haskell.TH.Desugar -- Single a fixity declaration. -singInfixDecl :: forall q. DsMonad q => Name -> Fixity -> q (Maybe DLetDec) +singInfixDecl :: forall q. OptionsMonad q => Name -> Fixity -> q (Maybe DLetDec) singInfixDecl name fixity = do + opts <- getOptions mb_ns <- reifyNameSpace name case mb_ns of -- If we can't find the Name for some odd reason, -- fall back to singValName - Nothing -> finish $ singValName name - Just VarName -> finish $ singValName name - Just DataName -> finish $ singDataConName name + Nothing -> finish $ singledValueName opts name + Just VarName -> finish $ singledValueName opts name + Just DataName -> finish $ singledDataConName opts name Just TcClsName -> do mb_info <- dsReify name case mb_info of Just (DTyConI DClassD{} _) - -> finish $ singTyConName name + -> finish $ singledClassName opts name _ -> pure Nothing -- Don't produce anything for other type constructors (type synonyms, -- type families, data types, etc.). @@ -35,7 +36,7 @@ singInfixDecl name fixity = do -- /without/ consulting quoted declarations. If reification fails, recover and -- return the empty list. -- See [singletons and fixity declarations], wrinkle 2. -singReifiedInfixDecls :: forall q. DsMonad q => [Name] -> q [DDec] +singReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec] singReifiedInfixDecls = mapMaybeM trySingFixityDeclaration where trySingFixityDeclaration :: Name -> q (Maybe DDec) diff --git a/src/Data/Singletons/Single/Monad.hs b/src/Data/Singletons/Single/Monad.hs index 5a71e1c3..40a1f7eb 100644 --- a/src/Data/Singletons/Single/Monad.hs +++ b/src/Data/Singletons/Single/Monad.hs @@ -21,7 +21,7 @@ import Prelude hiding ( exp ) import Data.Map ( Map ) import qualified Data.Map as Map import Data.Singletons.Promote.Monad ( emitDecs, emitDecsM ) -import Data.Singletons.Names +import Data.Singletons.TH.Options import Data.Singletons.Util import Data.Singletons.Internal import Language.Haskell.TH.Syntax hiding ( lift ) @@ -32,13 +32,15 @@ import Control.Applicative -- environment during singling data SgEnv = - SgEnv { sg_let_binds :: Map Name DExp -- from the *original* name + SgEnv { sg_options :: Options + , sg_let_binds :: Map Name DExp -- from the *original* name , sg_context :: DCxt -- See Note [Tracking the current type signature context] , sg_local_decls :: [Dec] } emptySgEnv :: SgEnv -emptySgEnv = SgEnv { sg_let_binds = Map.empty +emptySgEnv = SgEnv { sg_options = defaultOptions + , sg_let_binds = Map.empty , sg_context = [] , sg_local_decls = [] } @@ -91,6 +93,9 @@ instance Quasi SgM where instance DsMonad SgM where localDeclarations = asks sg_local_decls +instance OptionsMonad SgM where + getOptions = asks sg_options + bindLets :: [(Name, DExp)] -> SgM a -> SgM a bindLets lets1 = local (\env@(SgEnv { sg_let_binds = lets2 }) -> @@ -109,13 +114,20 @@ askContext :: SgM DCxt askContext = asks sg_context lookupVarE :: Name -> SgM DExp -lookupVarE = lookup_var_con singValName (DVarE . singValName) +lookupVarE name = do + opts <- getOptions + lookup_var_con (singledValueName opts) + (DVarE . singledValueName opts) name lookupConE :: Name -> SgM DExp -lookupConE = lookup_var_con singDataConName (DConE . singDataConName) +lookupConE name = do + opts <- getOptions + lookup_var_con (singledDataConName opts) + (DConE . singledDataConName opts) name lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp lookup_var_con mk_sing_name mk_exp name = do + opts <- getOptions letExpansions <- asks sg_let_binds sName <- mkDataName (nameBase (mk_sing_name name)) -- we want *term* names! case Map.lookup name letExpansions of @@ -126,7 +138,8 @@ lookup_var_con mk_sing_name mk_exp name = do case m_dinfo of Just (DVarI _ ty _) -> let num_args = countArgs ty in - return $ wrapSingFun num_args (promoteValRhs name) (mk_exp name) + return $ wrapSingFun num_args (DConT $ defunctionalizedName0 opts name) + (mk_exp name) _ -> return $ mk_exp name -- lambda-bound Just exp -> return exp @@ -160,14 +173,16 @@ wrapUnSingFun n ty = in (unwrap_fun `DAppTypeE` ty `DAppE`) -singM :: DsMonad q => [Dec] -> SgM a -> q (a, [DDec]) +singM :: OptionsMonad q => [Dec] -> SgM a -> q (a, [DDec]) singM locals (SgM rdr) = do + opts <- getOptions other_locals <- localDeclarations - let wr = runReaderT rdr (emptySgEnv { sg_local_decls = other_locals ++ locals }) + let wr = runReaderT rdr (emptySgEnv { sg_options = opts + , sg_local_decls = other_locals ++ locals }) q = runWriterT wr runQ q -singDecsM :: DsMonad q => [Dec] -> SgM [DDec] -> q [DDec] +singDecsM :: OptionsMonad q => [Dec] -> SgM [DDec] -> q [DDec] singDecsM locals thing = do (decs1, decs2) <- singM locals thing return $ decs1 ++ decs2 diff --git a/src/Data/Singletons/Single/Type.hs b/src/Data/Singletons/Single/Type.hs index 10506032..de2dce9c 100644 --- a/src/Data/Singletons/Single/Type.hs +++ b/src/Data/Singletons/Single/Type.hs @@ -14,6 +14,7 @@ import Language.Haskell.TH.Syntax import Data.Singletons.Names import Data.Singletons.Single.Monad import Data.Singletons.Promote.Type +import Data.Singletons.TH.Options import Data.Singletons.Util import Control.Monad import Data.Foldable @@ -106,8 +107,9 @@ singPredRec ctx (DConT n) | n == equalityName = fail "Singling of type equality constraints not yet supported" | otherwise = do + opts <- getOptions kis <- mapM promoteTypeArg_NC ctx - let sName = singClassName n + let sName = singledClassName opts n return $ applyDType (DConT sName) kis singPredRec _ctx DWildCardT = return DWildCardT -- it just might work singPredRec _ctx DArrowT = diff --git a/src/Data/Singletons/TH.hs b/src/Data/Singletons/TH.hs index 8b848479..7c6d14cd 100644 --- a/src/Data/Singletons/TH.hs +++ b/src/Data/Singletons/TH.hs @@ -129,9 +129,9 @@ import Data.Singletons.Prelude.Ord import Data.Singletons.Prelude.Show import Data.Singletons.Prelude.Traversable import Data.Singletons.Decide +import Data.Singletons.TH.Options import Data.Singletons.TypeLits import Data.Singletons.SuppressUnusedWarnings -import Data.Singletons.Names import Language.Haskell.TH.Desugar import Language.Haskell.TH @@ -163,17 +163,18 @@ cases tyName expq bodyq = do -- each constructor is treated the same. For 'sCases', unlike 'cases', the -- scrutinee is a singleton. But make sure to pass in the name of the /original/ -- datatype, preferring @''Maybe@ over @''SMaybe@. -sCases :: DsMonad q +sCases :: OptionsMonad q => Name -- ^ The head of the type the scrutinee's type is based on. -- (Like @''Maybe@ or @''Bool@.) -> q Exp -- ^ The scrutinee, in a Template Haskell quote -> q Exp -- ^ The body, in a Template Haskell quote -> q Exp sCases tyName expq bodyq = do + opts <- getOptions dinfo <- dsReify tyName case dinfo of Just (DTyConI (DDataD _ _ _ _ _ ctors _) _) -> - let ctor_stuff = map (first singDataConName . extractNameArgs) ctors in + let ctor_stuff = map (first (singledDataConName opts) . extractNameArgs) ctors in expToTH <$> buildCases ctor_stuff expq bodyq Just _ -> fail $ "Using <> with something other than a type constructor: " diff --git a/src/Data/Singletons/TH/Options.hs b/src/Data/Singletons/TH/Options.hs new file mode 100644 index 00000000..c284dd5b --- /dev/null +++ b/src/Data/Singletons/TH/Options.hs @@ -0,0 +1,228 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TemplateHaskell #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Singletons.TH.Options +-- Copyright : (C) 2019 Ryan Scott +-- License : BSD-style (see LICENSE) +-- Maintainer : Ryan Scott +-- Stability : experimental +-- Portability : non-portable +-- +-- This module defines 'Options' that control finer details of how the Template +-- Haskell machinery works, as well as an @mtl@-like 'OptionsMonad' class +-- and an 'OptionsM' monad transformer. +-- +---------------------------------------------------------------------------- + +module Data.Singletons.TH.Options + ( -- * Options + Options, defaultOptions + -- ** Options record selectors + , genSingKindInsts + , promotedClassName + , promotedValueNamePrefix + , singledDataTypeName + , singledClassName + , singledDataConName + , singledValueName + , defunctionalizedName + -- ** Derived functions over Options + , promotedValueName + , defunctionalizedName0 + + -- * OptionsMonad + , OptionsMonad(..), OptionsM, withOptions + ) where + +import Control.Applicative +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Reader (ReaderT(..), ask) +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 + , mk_name_tc, mkTupleDataName, mkTupleTypeName + , sconsName, sListName, snilName + , splitUnderscores + ) +import Data.Singletons.Util +import Language.Haskell.TH.Desugar +import Language.Haskell.TH.Syntax hiding (Lift(..)) + +-- | Options that control the finer details of how @singletons@' Template +-- Haskell machinery works. +data Options = Options + { 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 + -- ^ Controls how promoted type classes are named. + , promotedValueNamePrefix :: (String, String) -> Name -> Name + -- ^ Controls how promoted values are named. The @(String, String)@ is a + -- pair of prefixes to be attached to the front of the name, where the + -- first element of the pair is used if the name is alphanumeric and the + -- second element of the pair is used if the name is symbolic. + , singledDataTypeName :: Name -> Name + -- ^ Controls how singled data types are named. + , singledClassName :: Name -> Name + -- ^ Controls how singled type classes are named. + , singledDataConName :: Name -> Name + -- ^ Controls how singled data constructors are named. + , singledValueName :: Name -> Name + -- ^ Controls how singled values are named. + , defunctionalizedName :: Name -> Int -> Name + -- ^ Controls how defunctionalization symbols are named. The 'Int' argument + -- represents how saturated the symbol is. For instance, 0 indicates that + -- no parameters are passed to the symbol, 1 indicates that one parameter + -- is passed to the symbol, and so on. + } + +-- | Sensible default 'Options'. +defaultOptions :: Options +defaultOptions = Options + { genSingKindInsts = True + , promotedClassName = promoteClassName + , promotedValueNamePrefix = promoteValNameLhsPrefix + , singledDataTypeName = singTyConName + , singledClassName = singClassName + , singledDataConName = singDataConName + , singledValueName = singValName + , defunctionalizedName = promoteTySym + } + +-- | Generate a promoted value name with no prefixes. +promotedValueName :: Options -> Name -> Name +promotedValueName opts = promotedValueNamePrefix opts noPrefix + +-- | Generate a defunctionalization symbol with no arguments. +defunctionalizedName0 :: Options -> Name -> Name +defunctionalizedName0 opts name + | name == nilName + = nilName -- workaround for #21 + + | otherwise + = defunctionalizedName opts name 0 + +-- | Class that describes monads that contain 'Options'. +class DsMonad m => OptionsMonad m where + getOptions :: m Options + +instance OptionsMonad Q where + getOptions = pure defaultOptions + +instance OptionsMonad m => OptionsMonad (DsM m) where + getOptions = lift getOptions + +instance (OptionsMonad q, Monoid m) => OptionsMonad (QWithAux m q) where + getOptions = lift getOptions + +instance OptionsMonad m => OptionsMonad (ReaderT r m) where + getOptions = lift getOptions + +instance OptionsMonad m => OptionsMonad (StateT s m) where + getOptions = lift getOptions + +instance (OptionsMonad m, Monoid w) => OptionsMonad (WriterT w m) where + getOptions = lift getOptions + +instance (OptionsMonad m, Monoid w) => OptionsMonad (RWST r w s m) where + getOptions = lift getOptions + +-- | A convenient implementation of the 'OptionsMonad' class. Use by calling +-- 'withOptions'. +newtype OptionsM m a = OptionsM (ReaderT Options m a) + deriving ( Functor, Applicative, Monad, MonadTrans + , Quasi, MonadFail, MonadIO, DsMonad ) + +-- | Turn any 'DsMonad' into an 'OptionsMonad'. +instance DsMonad m => OptionsMonad (OptionsM m) where + getOptions = OptionsM ask + +-- | Declare the 'Options' that a TH computation should use. +withOptions :: Options -> OptionsM m a -> m a +withOptions opts (OptionsM x) = runReaderT x opts + +-- used when a value name appears in a pattern context +-- works only for proper variables (lower-case names) +-- the (String, String) is a pair of prefixes to prepend, where the first +-- element is used for alphanumeric names and the second element is used for +-- symbolic names. +promoteValNameLhsPrefix :: (String, String) -> Name -> Name +promoteValNameLhsPrefix pres@(alpha, _) 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, rest) <- splitUnderscores (nameBase n) + = mkName $ alpha ++ "US" ++ us ++ rest + + | otherwise + = mkName $ toUpcaseStr pres n + +-- 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 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, rest) <- splitUnderscores (nameBase name) + = default_case (mkName $ "US" ++ us ++ rest) + + | name == nilName + = mkName $ "NilSym" ++ (show sat) + + -- treat unboxed tuples like tuples + | Just degree <- tupleNameDegree_maybe name <|> + unboxedTupleNameDegree_maybe name + = mk_name_tc "Data.Singletons.Prelude.Instances" $ + "Tuple" ++ show degree ++ "Sym" ++ (show sat) + + | otherwise + = default_case name + where + default_case :: Name -> Name + default_case name' = + let capped = toUpcaseStr noPrefix name' in + if isHsLetter (head capped) + then mkName (capped ++ "Sym" ++ (show sat)) + else mkName (capped ++ "@#@" -- See Note [Defunctionalization symbol suffixes] + ++ (replicate (sat + 1) '$')) + +promoteClassName :: Name -> Name +promoteClassName = prefixName "P" "#" + +-- Singletons + +singDataConName :: Name -> Name +singDataConName nm + | nm == nilName = snilName + | nm == consName = sconsName + | Just degree <- tupleNameDegree_maybe nm = mkTupleDataName degree + | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree + | otherwise = prefixConName "S" "%" nm + +singTyConName :: Name -> Name +singTyConName name + | name == listName = sListName + | Just degree <- tupleNameDegree_maybe name = mkTupleTypeName degree + | Just degree <- unboxedTupleNameDegree_maybe name = mkTupleTypeName degree + | otherwise = prefixName "S" "%" name + +singClassName :: Name -> Name +singClassName = singTyConName + +singValName :: Name -> Name +singValName n + -- Push the 's' past the underscores, as this lets us avoid some unused + -- variable warnings (#229). + | Just (us, rest) <- splitUnderscores (nameBase n) + = prefixName (us ++ "s") "%" $ mkName rest + | otherwise + = prefixName "s" "%" $ upcase n diff --git a/tests/SingletonsTestSuite.hs b/tests/SingletonsTestSuite.hs index 45afe3d1..593506ec 100644 --- a/tests/SingletonsTestSuite.hs +++ b/tests/SingletonsTestSuite.hs @@ -75,6 +75,8 @@ tests = , compileAndDumpStdTest "T145" , compileAndDumpStdTest "PolyKinds" , compileAndDumpStdTest "PolyKindsApp" + , afterSingletonsNat . + compileAndDumpStdTest "T150" , compileAndDumpStdTest "T160" , compileAndDumpStdTest "T163" , compileAndDumpStdTest "T166" @@ -92,6 +94,7 @@ tests = , compileAndDumpStdTest "T197" , compileAndDumpStdTest "T197b" , compileAndDumpStdTest "T200" + , compileAndDumpStdTest "T204" , compileAndDumpStdTest "T206" , compileAndDumpStdTest "T209" , compileAndDumpStdTest "T216" diff --git a/tests/compile-and-dump/Singletons/T150.golden b/tests/compile-and-dump/Singletons/T150.golden new file mode 100644 index 00000000..f31ea8c7 --- /dev/null +++ b/tests/compile-and-dump/Singletons/T150.golden @@ -0,0 +1,384 @@ +Singletons/T150.hs:(0,0)-(0,0): Splicing declarations + withOptions defaultOptions {genSingKindInsts = False} + $ singletons + $ lift + [d| headVec :: Vec (Succ n) a -> a + headVec (VCons x _) = x + tailVec :: Vec (Succ n) a -> Vec n a + tailVec (VCons _ xs) = xs + (!) :: Vec n a -> Fin n -> a + VCons x _ ! FZ = x + VCons _ xs ! FS n = xs ! n + VNil ! n = case n of + mapVec :: (a -> b) -> Vec n a -> Vec n b + mapVec _ VNil = VNil + mapVec f (VCons x xs) = VCons (f x) (mapVec f xs) + symmetry :: Equal a b -> Equal b a + symmetry Reflexive = Reflexive + transitivity :: Equal a b -> Equal b c -> Equal a c + transitivity Reflexive Reflexive = Reflexive + + data Fin :: Nat -> Type + where + FZ :: Fin (Succ n) + FS :: Fin n -> Fin (Succ n) + data Foo :: Type -> Type + where + MkFoo1 :: Foo Bool + MkFoo2 :: Foo Ordering + data Vec :: Nat -> Type -> Type + where + VNil :: Vec Zero a + VCons :: a -> Vec n a -> Vec (Succ n) a + data Equal :: Type -> Type -> Type where Reflexive :: Equal a a + data HList :: [Type] -> Type + where + HNil :: HList '[] + HCons :: x -> HList xs -> HList (x : xs) + data Obj :: Type where Obj :: a -> Obj |] + ======> + data Fin :: Nat -> Type + where + FZ :: Fin ('Succ n) + FS :: (Fin n) -> Fin ('Succ n) + data Foo :: Type -> Type + where + MkFoo1 :: Foo Bool + MkFoo2 :: Foo Ordering + data Vec :: Nat -> Type -> Type + where + VNil :: Vec 'Zero a + VCons :: a -> (Vec n a) -> Vec ('Succ n) a + headVec :: Vec ('Succ n) a -> a + headVec (VCons x _) = x + tailVec :: Vec ('Succ n) a -> Vec n a + tailVec (VCons _ xs) = xs + (!) :: Vec n a -> Fin n -> a + (!) (VCons x _) FZ = x + (!) (VCons _ xs) (FS n) = (xs ! n) + (!) VNil n = case n of + mapVec :: (a -> b) -> Vec n a -> Vec n b + mapVec _ VNil = VNil + mapVec f (VCons x xs) = (VCons (f x)) ((mapVec f) xs) + data Equal :: Type -> Type -> Type where Reflexive :: Equal a a + symmetry :: Equal a b -> Equal b a + symmetry Reflexive = Reflexive + transitivity :: Equal a b -> Equal b c -> Equal a c + transitivity Reflexive Reflexive = Reflexive + data HList :: [Type] -> Type + where + HNil :: HList '[] + HCons :: x -> (HList xs) -> HList ('(:) x xs) + data Obj :: Type where Obj :: a -> Obj + type FZSym0 = FZ + instance SuppressUnusedWarnings FSSym0 where + suppressUnusedWarnings = snd (((,) FSSym0KindInference) ()) + data FSSym0 :: forall n0123456789876543210. + (~>) (Fin n0123456789876543210) (Fin ('Succ n0123456789876543210)) + where + FSSym0KindInference :: forall t0123456789876543210 + arg. SameKind (Apply FSSym0 arg) (FSSym1 arg) => + FSSym0 t0123456789876543210 + type instance Apply FSSym0 t0123456789876543210 = FSSym1 t0123456789876543210 + type FSSym1 (t0123456789876543210 :: Fin n0123456789876543210) = + FS t0123456789876543210 + type MkFoo1Sym0 = MkFoo1 + type MkFoo2Sym0 = MkFoo2 + type VNilSym0 = VNil + instance SuppressUnusedWarnings VConsSym0 where + suppressUnusedWarnings = snd (((,) VConsSym0KindInference) ()) + data VConsSym0 :: forall a0123456789876543210 n0123456789876543210. + (~>) a0123456789876543210 ((~>) (Vec n0123456789876543210 a0123456789876543210) (Vec ('Succ n0123456789876543210) a0123456789876543210)) + where + VConsSym0KindInference :: forall t0123456789876543210 + arg. SameKind (Apply VConsSym0 arg) (VConsSym1 arg) => + VConsSym0 t0123456789876543210 + type instance Apply VConsSym0 t0123456789876543210 = VConsSym1 t0123456789876543210 + instance SuppressUnusedWarnings (VConsSym1 t0123456789876543210) where + suppressUnusedWarnings = snd (((,) VConsSym1KindInference) ()) + data VConsSym1 (t0123456789876543210 :: a0123456789876543210) :: forall n0123456789876543210. + (~>) (Vec n0123456789876543210 a0123456789876543210) (Vec ('Succ n0123456789876543210) a0123456789876543210) + where + VConsSym1KindInference :: forall t0123456789876543210 + t0123456789876543210 + arg. SameKind (Apply (VConsSym1 t0123456789876543210) arg) (VConsSym2 t0123456789876543210 arg) => + VConsSym1 t0123456789876543210 t0123456789876543210 + type instance Apply (VConsSym1 t0123456789876543210) t0123456789876543210 = VConsSym2 t0123456789876543210 t0123456789876543210 + type VConsSym2 (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: Vec n0123456789876543210 a0123456789876543210) = + VCons t0123456789876543210 t0123456789876543210 + type ReflexiveSym0 = Reflexive + type HNilSym0 = HNil + instance SuppressUnusedWarnings HConsSym0 where + suppressUnusedWarnings = snd (((,) HConsSym0KindInference) ()) + data HConsSym0 :: forall x0123456789876543210 + xs0123456789876543210. + (~>) x0123456789876543210 ((~>) (HList xs0123456789876543210) (HList ('(:) x0123456789876543210 xs0123456789876543210))) + where + HConsSym0KindInference :: forall t0123456789876543210 + arg. SameKind (Apply HConsSym0 arg) (HConsSym1 arg) => + HConsSym0 t0123456789876543210 + type instance Apply HConsSym0 t0123456789876543210 = HConsSym1 t0123456789876543210 + instance SuppressUnusedWarnings (HConsSym1 t0123456789876543210) where + suppressUnusedWarnings = snd (((,) HConsSym1KindInference) ()) + data HConsSym1 (t0123456789876543210 :: x0123456789876543210) :: forall xs0123456789876543210. + (~>) (HList xs0123456789876543210) (HList ('(:) x0123456789876543210 xs0123456789876543210)) + where + HConsSym1KindInference :: forall t0123456789876543210 + t0123456789876543210 + arg. SameKind (Apply (HConsSym1 t0123456789876543210) arg) (HConsSym2 t0123456789876543210 arg) => + HConsSym1 t0123456789876543210 t0123456789876543210 + type instance Apply (HConsSym1 t0123456789876543210) t0123456789876543210 = HConsSym2 t0123456789876543210 t0123456789876543210 + type HConsSym2 (t0123456789876543210 :: x0123456789876543210) (t0123456789876543210 :: HList xs0123456789876543210) = + HCons t0123456789876543210 t0123456789876543210 + instance SuppressUnusedWarnings ObjSym0 where + suppressUnusedWarnings = snd (((,) ObjSym0KindInference) ()) + data ObjSym0 :: forall a0123456789876543210. + (~>) a0123456789876543210 Obj + where + ObjSym0KindInference :: forall t0123456789876543210 + arg. SameKind (Apply ObjSym0 arg) (ObjSym1 arg) => + ObjSym0 t0123456789876543210 + type instance Apply ObjSym0 t0123456789876543210 = ObjSym1 t0123456789876543210 + type ObjSym1 (t0123456789876543210 :: a0123456789876543210) = + Obj t0123456789876543210 + type family Case_0123456789876543210 n t where + instance SuppressUnusedWarnings TransitivitySym0 where + suppressUnusedWarnings + = snd (((,) TransitivitySym0KindInference) ()) + data TransitivitySym0 :: forall a0123456789876543210 + b0123456789876543210 + c0123456789876543210. + (~>) (Equal a0123456789876543210 b0123456789876543210) ((~>) (Equal b0123456789876543210 c0123456789876543210) (Equal a0123456789876543210 c0123456789876543210)) + where + TransitivitySym0KindInference :: forall a0123456789876543210 + arg. SameKind (Apply TransitivitySym0 arg) (TransitivitySym1 arg) => + TransitivitySym0 a0123456789876543210 + type instance Apply TransitivitySym0 a0123456789876543210 = TransitivitySym1 a0123456789876543210 + instance SuppressUnusedWarnings (TransitivitySym1 a0123456789876543210) where + suppressUnusedWarnings + = snd (((,) TransitivitySym1KindInference) ()) + data TransitivitySym1 (a0123456789876543210 :: Equal a0123456789876543210 b0123456789876543210) :: forall c0123456789876543210. + (~>) (Equal b0123456789876543210 c0123456789876543210) (Equal a0123456789876543210 c0123456789876543210) + where + TransitivitySym1KindInference :: forall a0123456789876543210 + a0123456789876543210 + arg. SameKind (Apply (TransitivitySym1 a0123456789876543210) arg) (TransitivitySym2 a0123456789876543210 arg) => + TransitivitySym1 a0123456789876543210 a0123456789876543210 + type instance Apply (TransitivitySym1 a0123456789876543210) a0123456789876543210 = TransitivitySym2 a0123456789876543210 a0123456789876543210 + type TransitivitySym2 (a0123456789876543210 :: Equal a0123456789876543210 b0123456789876543210) (a0123456789876543210 :: Equal b0123456789876543210 c0123456789876543210) = + Transitivity a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings SymmetrySym0 where + suppressUnusedWarnings = snd (((,) SymmetrySym0KindInference) ()) + data SymmetrySym0 :: forall a0123456789876543210 + b0123456789876543210. + (~>) (Equal a0123456789876543210 b0123456789876543210) (Equal b0123456789876543210 a0123456789876543210) + where + SymmetrySym0KindInference :: forall a0123456789876543210 + arg. SameKind (Apply SymmetrySym0 arg) (SymmetrySym1 arg) => + SymmetrySym0 a0123456789876543210 + type instance Apply SymmetrySym0 a0123456789876543210 = SymmetrySym1 a0123456789876543210 + type SymmetrySym1 (a0123456789876543210 :: Equal a0123456789876543210 b0123456789876543210) = + Symmetry a0123456789876543210 + instance SuppressUnusedWarnings MapVecSym0 where + suppressUnusedWarnings = snd (((,) MapVecSym0KindInference) ()) + data MapVecSym0 :: forall a0123456789876543210 + b0123456789876543210 + n0123456789876543210. + (~>) ((~>) a0123456789876543210 b0123456789876543210) ((~>) (Vec n0123456789876543210 a0123456789876543210) (Vec n0123456789876543210 b0123456789876543210)) + where + MapVecSym0KindInference :: forall a0123456789876543210 + arg. SameKind (Apply MapVecSym0 arg) (MapVecSym1 arg) => + MapVecSym0 a0123456789876543210 + type instance Apply MapVecSym0 a0123456789876543210 = MapVecSym1 a0123456789876543210 + instance SuppressUnusedWarnings (MapVecSym1 a0123456789876543210) where + suppressUnusedWarnings = snd (((,) MapVecSym1KindInference) ()) + data MapVecSym1 (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) :: forall n0123456789876543210. + (~>) (Vec n0123456789876543210 a0123456789876543210) (Vec n0123456789876543210 b0123456789876543210) + where + MapVecSym1KindInference :: forall a0123456789876543210 + a0123456789876543210 + arg. SameKind (Apply (MapVecSym1 a0123456789876543210) arg) (MapVecSym2 a0123456789876543210 arg) => + MapVecSym1 a0123456789876543210 a0123456789876543210 + type instance Apply (MapVecSym1 a0123456789876543210) a0123456789876543210 = MapVecSym2 a0123456789876543210 a0123456789876543210 + type MapVecSym2 (a0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (a0123456789876543210 :: Vec n0123456789876543210 a0123456789876543210) = + MapVec a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (!@#@$) where + suppressUnusedWarnings = snd (((,) (:!@#@$###)) ()) + data (!@#@$) :: forall n0123456789876543210 a0123456789876543210. + (~>) (Vec n0123456789876543210 a0123456789876543210) ((~>) (Fin n0123456789876543210) a0123456789876543210) + where + (:!@#@$###) :: forall a0123456789876543210 + arg. SameKind (Apply (!@#@$) arg) ((!@#@$$) arg) => + (!@#@$) a0123456789876543210 + type instance Apply (!@#@$) a0123456789876543210 = (!@#@$$) a0123456789876543210 + instance SuppressUnusedWarnings ((!@#@$$) a0123456789876543210) where + suppressUnusedWarnings = snd (((,) (:!@#@$$###)) ()) + data (!@#@$$) (a0123456789876543210 :: Vec n0123456789876543210 a0123456789876543210) :: (~>) (Fin n0123456789876543210) a0123456789876543210 + where + (:!@#@$$###) :: forall a0123456789876543210 + a0123456789876543210 + arg. SameKind (Apply ((!@#@$$) a0123456789876543210) arg) ((!@#@$$$) a0123456789876543210 arg) => + (!@#@$$) a0123456789876543210 a0123456789876543210 + type instance Apply ((!@#@$$) a0123456789876543210) a0123456789876543210 = (!@#@$$$) a0123456789876543210 a0123456789876543210 + type (!@#@$$$) (a0123456789876543210 :: Vec n0123456789876543210 a0123456789876543210) (a0123456789876543210 :: Fin n0123456789876543210) = + (!) a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings TailVecSym0 where + suppressUnusedWarnings = snd (((,) TailVecSym0KindInference) ()) + data TailVecSym0 :: forall n0123456789876543210 + a0123456789876543210. + (~>) (Vec ('Succ n0123456789876543210) a0123456789876543210) (Vec n0123456789876543210 a0123456789876543210) + where + TailVecSym0KindInference :: forall a0123456789876543210 + arg. SameKind (Apply TailVecSym0 arg) (TailVecSym1 arg) => + TailVecSym0 a0123456789876543210 + type instance Apply TailVecSym0 a0123456789876543210 = TailVecSym1 a0123456789876543210 + type TailVecSym1 (a0123456789876543210 :: Vec ('Succ n0123456789876543210) a0123456789876543210) = + TailVec a0123456789876543210 + instance SuppressUnusedWarnings HeadVecSym0 where + suppressUnusedWarnings = snd (((,) HeadVecSym0KindInference) ()) + data HeadVecSym0 :: forall n0123456789876543210 + a0123456789876543210. + (~>) (Vec ('Succ n0123456789876543210) a0123456789876543210) a0123456789876543210 + where + HeadVecSym0KindInference :: forall a0123456789876543210 + arg. SameKind (Apply HeadVecSym0 arg) (HeadVecSym1 arg) => + HeadVecSym0 a0123456789876543210 + type instance Apply HeadVecSym0 a0123456789876543210 = HeadVecSym1 a0123456789876543210 + type HeadVecSym1 (a0123456789876543210 :: Vec ('Succ n0123456789876543210) a0123456789876543210) = + HeadVec a0123456789876543210 + type family Transitivity (a :: Equal a b) (a :: Equal b c) :: Equal a c where + Transitivity Reflexive Reflexive = ReflexiveSym0 + type family Symmetry (a :: Equal a b) :: Equal b a where + Symmetry Reflexive = ReflexiveSym0 + type family MapVec (a :: (~>) a b) (a :: Vec n a) :: Vec n b where + MapVec _ VNil = VNilSym0 + MapVec f (VCons x xs) = Apply (Apply VConsSym0 (Apply f x)) (Apply (Apply MapVecSym0 f) xs) + type family (!) (a :: Vec n a) (a :: Fin n) :: a where + (!) (VCons x _) FZ = x + (!) (VCons _ xs) (FS n) = Apply (Apply (!@#@$) xs) n + (!) VNil n = Case_0123456789876543210 n n + type family TailVec (a :: Vec ('Succ n) a) :: Vec n a where + TailVec (VCons _ xs) = xs + type family HeadVec (a :: Vec ('Succ n) a) :: a where + HeadVec (VCons x _) = x + sTransitivity :: + forall a b c (t :: Equal a b) (t :: Equal b c). + Sing t + -> Sing t -> Sing (Apply (Apply TransitivitySym0 t) t :: Equal a c) + sSymmetry :: + forall a b (t :: Equal a b). + Sing t -> Sing (Apply SymmetrySym0 t :: Equal b a) + sMapVec :: + forall a b n (t :: (~>) a b) (t :: Vec n a). + Sing t -> Sing t -> Sing (Apply (Apply MapVecSym0 t) t :: Vec n b) + (%!) :: + forall n a (t :: Vec n a) (t :: Fin n). + Sing t -> Sing t -> Sing (Apply (Apply (!@#@$) t) t :: a) + sTailVec :: + forall n a (t :: Vec ('Succ n) a). + Sing t -> Sing (Apply TailVecSym0 t :: Vec n a) + sHeadVec :: + forall n a (t :: Vec ('Succ n) a). + Sing t -> Sing (Apply HeadVecSym0 t :: a) + sTransitivity SReflexive SReflexive = SReflexive + sSymmetry SReflexive = SReflexive + sMapVec _ SVNil = SVNil + sMapVec (sF :: Sing f) (SVCons (sX :: Sing x) (sXs :: Sing xs)) + = (applySing + ((applySing ((singFun2 @VConsSym0) SVCons)) ((applySing sF) sX))) + ((applySing ((applySing ((singFun2 @MapVecSym0) sMapVec)) sF)) sXs) + (%!) (SVCons (sX :: Sing x) _) SFZ = sX + (%!) (SVCons _ (sXs :: Sing xs)) (SFS (sN :: Sing n)) + = (applySing ((applySing ((singFun2 @(!@#@$)) (%!))) sXs)) sN + (%!) SVNil (sN :: Sing n) + = (id @(Sing (Case_0123456789876543210 n n :: a))) (case sN of) + sTailVec (SVCons _ (sXs :: Sing xs)) = sXs + sHeadVec (SVCons (sX :: Sing x) _) = sX + instance SingI (TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))) where + sing = (singFun2 @TransitivitySym0) sTransitivity + instance SingI d => + SingI (TransitivitySym1 (d :: Equal a b) :: (~>) (Equal b c) (Equal a c)) where + sing + = (singFun1 @(TransitivitySym1 (d :: Equal a b))) + (sTransitivity (sing @d)) + instance SingI (SymmetrySym0 :: (~>) (Equal a b) (Equal b a)) where + sing = (singFun1 @SymmetrySym0) sSymmetry + instance SingI (MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b))) where + sing = (singFun2 @MapVecSym0) sMapVec + instance SingI d => + SingI (MapVecSym1 (d :: (~>) a b) :: (~>) (Vec n a) (Vec n b)) where + sing = (singFun1 @(MapVecSym1 (d :: (~>) a b))) (sMapVec (sing @d)) + instance SingI ((!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a)) where + sing = (singFun2 @(!@#@$)) (%!) + instance SingI d => + SingI ((!@#@$$) (d :: Vec n a) :: (~>) (Fin n) a) where + sing = (singFun1 @((!@#@$$) (d :: Vec n a))) ((%!) (sing @d)) + instance SingI (TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a)) where + sing = (singFun1 @TailVecSym0) sTailVec + instance SingI (HeadVecSym0 :: (~>) (Vec ('Succ n) a) a) where + sing = (singFun1 @HeadVecSym0) sHeadVec + data SFin :: forall a. Fin a -> Type + where + SFZ :: forall n. SFin (FZ :: Fin ('Succ n)) + SFS :: forall n (n :: Fin n). + (Sing n) -> SFin (FS n :: Fin ('Succ n)) + type instance Sing @(Fin a) = SFin + data SFoo :: forall a. Foo a -> Type + where + SMkFoo1 :: SFoo (MkFoo1 :: Foo Bool) + SMkFoo2 :: SFoo (MkFoo2 :: Foo Ordering) + type instance Sing @(Foo a) = SFoo + data SVec :: forall a a. Vec a a -> Type + where + SVNil :: forall a. SVec (VNil :: Vec 'Zero a) + SVCons :: forall a n (n :: a) (n :: Vec n a). + (Sing n) -> (Sing n) -> SVec (VCons n n :: Vec ('Succ n) a) + type instance Sing @(Vec a a) = SVec + data SEqual :: forall a a. Equal a a -> Type + where SReflexive :: forall a. SEqual (Reflexive :: Equal a a) + type instance Sing @(Equal a a) = SEqual + data SHList :: forall a. HList a -> Type + where + SHNil :: SHList (HNil :: HList '[]) + SHCons :: forall x xs (n :: x) (n :: HList xs). + (Sing n) -> (Sing n) -> SHList (HCons n n :: HList ('(:) x xs)) + type instance Sing @(HList a) = SHList + data SObj :: Obj -> Type + where SObj :: forall a (n :: a). (Sing n) -> SObj (Obj n :: Obj) + type instance Sing @Obj = SObj + instance SingI FZ where + sing = SFZ + instance SingI n => SingI (FS (n :: Fin n)) where + sing = SFS sing + instance SingI (FSSym0 :: (~>) (Fin n) (Fin ('Succ n))) where + sing = (singFun1 @FSSym0) SFS + instance SingI MkFoo1 where + sing = SMkFoo1 + instance SingI MkFoo2 where + sing = SMkFoo2 + instance SingI VNil where + sing = SVNil + instance (SingI n, SingI n) => + SingI (VCons (n :: a) (n :: Vec n a)) where + sing = (SVCons sing) sing + instance SingI (VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a))) where + sing = (singFun2 @VConsSym0) SVCons + instance SingI d => + SingI (VConsSym1 (d :: a) :: (~>) (Vec n a) (Vec ('Succ n) a)) where + sing = (singFun1 @(VConsSym1 (d :: a))) (SVCons (sing @d)) + instance SingI Reflexive where + sing = SReflexive + instance SingI HNil where + sing = SHNil + instance (SingI n, SingI n) => + SingI (HCons (n :: x) (n :: HList xs)) where + sing = (SHCons sing) sing + instance SingI (HConsSym0 :: (~>) x ((~>) (HList xs) (HList ('(:) x xs)))) where + sing = (singFun2 @HConsSym0) SHCons + instance SingI d => + SingI (HConsSym1 (d :: x) :: (~>) (HList xs) (HList ('(:) x xs))) where + sing = (singFun1 @(HConsSym1 (d :: x))) (SHCons (sing @d)) + instance SingI n => SingI (Obj (n :: a)) where + sing = SObj sing + instance SingI (ObjSym0 :: (~>) a Obj) where + sing = (singFun1 @ObjSym0) SObj diff --git a/tests/compile-and-dump/Singletons/T150.hs b/tests/compile-and-dump/Singletons/T150.hs new file mode 100644 index 00000000..984e060e --- /dev/null +++ b/tests/compile-and-dump/Singletons/T150.hs @@ -0,0 +1,53 @@ +module T150 where + +import Control.Monad.Trans.Class +import Data.Kind +import Data.Singletons.TH +import Data.Singletons.TH.Options +import Singletons.Nat + +$(withOptions defaultOptions{genSingKindInsts = False} $ + singletons $ lift + [d| data Fin :: Nat -> Type where + FZ :: Fin (Succ n) + FS :: Fin n -> Fin (Succ n) + + data Foo :: Type -> Type where + MkFoo1 :: Foo Bool + MkFoo2 :: Foo Ordering + + data Vec :: Nat -> Type -> Type where + VNil :: Vec Zero a + VCons :: a -> Vec n a -> Vec (Succ n) a + + headVec :: Vec (Succ n) a -> a + headVec (VCons x _) = x + + tailVec :: Vec (Succ n) a -> Vec n a + tailVec (VCons _ xs) = xs + + (!) :: Vec n a -> Fin n -> a + VCons x _ ! FZ = x + VCons _ xs ! FS n = xs ! n + VNil ! n = case n of {} + + mapVec :: (a -> b) -> Vec n a -> Vec n b + mapVec _ VNil = VNil + mapVec f (VCons x xs) = VCons (f x) (mapVec f xs) + + data Equal :: Type -> Type -> Type where + Reflexive :: Equal a a + + symmetry :: Equal a b -> Equal b a + symmetry Reflexive = Reflexive + + transitivity :: Equal a b -> Equal b c -> Equal a c + transitivity Reflexive Reflexive = Reflexive + + data HList :: [Type] -> Type where + HNil :: HList '[] + HCons :: x -> HList xs -> HList (x:xs) + + data Obj :: Type where + Obj :: a -> Obj + |]) diff --git a/tests/compile-and-dump/Singletons/T204.golden b/tests/compile-and-dump/Singletons/T204.golden new file mode 100644 index 00000000..c19a502b --- /dev/null +++ b/tests/compile-and-dump/Singletons/T204.golden @@ -0,0 +1,94 @@ +Singletons/T204.hs:(0,0)-(0,0): Splicing declarations + let + sing_data_con_name :: Name -> Name + sing_data_con_name n + = case nameBase n of + ':' : '%' : rest -> mkName $ ":^%" ++ rest + _ -> singledDataConName defaultOptions n + in + withOptions + defaultOptions {singledDataConName = sing_data_con_name} + $ singletons + $ lift + [d| data Ratio1 a = a :% a + data Ratio2 a = a :%% a |] + ======> + data Ratio1 a = a :% a + data Ratio2 a = a :%% a + instance SuppressUnusedWarnings (:%@#@$) where + suppressUnusedWarnings = snd (((,) (::%@#@$###)) ()) + data (:%@#@$) :: forall a0123456789876543210. + (~>) a0123456789876543210 ((~>) a0123456789876543210 (Ratio1 a0123456789876543210)) + where + (::%@#@$###) :: forall t0123456789876543210 + arg. SameKind (Apply (:%@#@$) arg) ((:%@#@$$) arg) => + (:%@#@$) t0123456789876543210 + type instance Apply (:%@#@$) t0123456789876543210 = (:%@#@$$) t0123456789876543210 + instance SuppressUnusedWarnings ((:%@#@$$) t0123456789876543210) where + suppressUnusedWarnings = snd (((,) (::%@#@$$###)) ()) + data (:%@#@$$) (t0123456789876543210 :: a0123456789876543210) :: (~>) a0123456789876543210 (Ratio1 a0123456789876543210) + where + (::%@#@$$###) :: forall t0123456789876543210 + t0123456789876543210 + arg. SameKind (Apply ((:%@#@$$) t0123456789876543210) arg) ((:%@#@$$$) t0123456789876543210 arg) => + (:%@#@$$) t0123456789876543210 t0123456789876543210 + type instance Apply ((:%@#@$$) t0123456789876543210) t0123456789876543210 = (:%@#@$$$) t0123456789876543210 t0123456789876543210 + type (:%@#@$$$) (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: a0123456789876543210) = + (:%) t0123456789876543210 t0123456789876543210 + instance SuppressUnusedWarnings (:%%@#@$) where + suppressUnusedWarnings = snd (((,) (::%%@#@$###)) ()) + data (:%%@#@$) :: forall a0123456789876543210. + (~>) a0123456789876543210 ((~>) a0123456789876543210 (Ratio2 a0123456789876543210)) + where + (::%%@#@$###) :: forall t0123456789876543210 + arg. SameKind (Apply (:%%@#@$) arg) ((:%%@#@$$) arg) => + (:%%@#@$) t0123456789876543210 + type instance Apply (:%%@#@$) t0123456789876543210 = (:%%@#@$$) t0123456789876543210 + instance SuppressUnusedWarnings ((:%%@#@$$) t0123456789876543210) where + suppressUnusedWarnings = snd (((,) (::%%@#@$$###)) ()) + data (:%%@#@$$) (t0123456789876543210 :: a0123456789876543210) :: (~>) a0123456789876543210 (Ratio2 a0123456789876543210) + where + (::%%@#@$$###) :: forall t0123456789876543210 + t0123456789876543210 + arg. SameKind (Apply ((:%%@#@$$) t0123456789876543210) arg) ((:%%@#@$$$) t0123456789876543210 arg) => + (:%%@#@$$) t0123456789876543210 t0123456789876543210 + type instance Apply ((:%%@#@$$) t0123456789876543210) t0123456789876543210 = (:%%@#@$$$) t0123456789876543210 t0123456789876543210 + type (:%%@#@$$$) (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: a0123456789876543210) = + (:%%) t0123456789876543210 t0123456789876543210 + data SRatio1 :: forall a. Ratio1 a -> GHC.Types.Type + where + (:^%) :: forall a (n :: a) (n :: a). + (Sing n) -> (Sing n) -> SRatio1 ((:%) n n :: Ratio1 a) + type instance Sing @(Ratio1 a) = SRatio1 + instance SingKind a => SingKind (Ratio1 a) where + type Demote (Ratio1 a) = Ratio1 (Demote a) + fromSing ((:^%) b b) = ((:%) (fromSing b)) (fromSing b) + toSing ((:%) (b :: Demote a) (b :: Demote a)) + = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing a) of { + (,) (SomeSing c) (SomeSing c) -> SomeSing (((:^%) c) c) } + data SRatio2 :: forall a. Ratio2 a -> GHC.Types.Type + where + (:^%%) :: forall a (n :: a) (n :: a). + (Sing n) -> (Sing n) -> SRatio2 ((:%%) n n :: Ratio2 a) + type instance Sing @(Ratio2 a) = SRatio2 + instance SingKind a => SingKind (Ratio2 a) where + type Demote (Ratio2 a) = Ratio2 (Demote a) + fromSing ((:^%%) b b) = ((:%%) (fromSing b)) (fromSing b) + toSing ((:%%) (b :: Demote a) (b :: Demote a)) + = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing a) of { + (,) (SomeSing c) (SomeSing c) -> SomeSing (((:^%%) c) c) } + instance (SingI n, SingI n) => SingI ((:%) (n :: a) (n :: a)) where + sing = ((:^%) sing) sing + instance SingI ((:%@#@$) :: (~>) a ((~>) a (Ratio1 a))) where + sing = (singFun2 @(:%@#@$)) (:^%) + instance SingI d => + SingI ((:%@#@$$) (d :: a) :: (~>) a (Ratio1 a)) where + sing = (singFun1 @((:%@#@$$) (d :: a))) ((:^%) (sing @d)) + instance (SingI n, SingI n) => + SingI ((:%%) (n :: a) (n :: a)) where + sing = ((:^%%) sing) sing + instance SingI ((:%%@#@$) :: (~>) a ((~>) a (Ratio2 a))) where + sing = (singFun2 @(:%%@#@$)) (:^%%) + instance SingI d => + SingI ((:%%@#@$$) (d :: a) :: (~>) a (Ratio2 a)) where + sing = (singFun1 @((:%%@#@$$) (d :: a))) ((:^%%) (sing @d)) diff --git a/tests/compile-and-dump/Singletons/T204.hs b/tests/compile-and-dump/Singletons/T204.hs new file mode 100644 index 00000000..cb1f91d0 --- /dev/null +++ b/tests/compile-and-dump/Singletons/T204.hs @@ -0,0 +1,17 @@ +module T204 where + +import Control.Monad.Trans.Class +import Data.Singletons.TH +import Data.Singletons.TH.Options +import Language.Haskell.TH + +$(let sing_data_con_name :: Name -> Name + sing_data_con_name n = + case nameBase n of + ':':'%':rest -> mkName $ ":^%" ++ rest + _ -> singledDataConName defaultOptions n in + withOptions defaultOptions{singledDataConName = sing_data_con_name} $ + singletons $ lift + [d| data Ratio1 a = a :% a + data Ratio2 a = a :%% a + |])