diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,15 @@ Changelog for the `singletons-th` project ========================================= +3.1 [2021.10.30] +---------------- +* Require building with GHC 9.2. +* Allow promoting and singling type applications in data constructor patterns. +* Make the Template Haskell machinery generate `SingI1` and `SingI2` instances + when possible. +* Make `genDefunSymbols` and related functions less likely to trigger + [GHC#19743](https://gitlab.haskell.org/ghc/ghc/-/issues/19743). + 3.0 [2021.03.12] ---------------- * The `singletons` library has been split into three libraries: diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -14,7 +14,7 @@ `singletons-th` generates code that relies on bleeding-edge GHC language extensions. As such, `singletons-th` only supports the latest major version -of GHC (currently GHC 9.0). For more information, +of GHC (currently GHC 9.2). For more information, consult the `singletons` [`README`](https://github.com/goldfirere/singletons/blob/master/README.md). diff --git a/singletons-th.cabal b/singletons-th.cabal --- a/singletons-th.cabal +++ b/singletons-th.cabal @@ -1,5 +1,5 @@ name: singletons-th -version: 3.0 +version: 3.1 cabal-version: 1.24 synopsis: A framework for generating singleton types homepage: http://www.github.com/goldfirere/singletons @@ -8,7 +8,7 @@ maintainer: Ryan Scott bug-reports: https://github.com/goldfirere/singletons/issues stability: experimental -tested-with: GHC == 9.0.1 +tested-with: GHC == 9.2.1 extra-source-files: README.md, CHANGES.md license: BSD3 license-file: LICENSE @@ -26,7 +26,7 @@ . @singletons-th@ generates code that relies on bleeding-edge GHC language extensions. As such, @singletons-th@ only supports the latest major version - of GHC (currently GHC 9.0). For more information, + of GHC (currently GHC 9.2). For more information, consult the @singletons@ @@. . @@ -42,7 +42,7 @@ type: git location: https://github.com/goldfirere/singletons.git subdir: singletons-th - tag: v3.0 + tag: v3.1 source-repository head type: git @@ -52,14 +52,14 @@ library hs-source-dirs: src - build-depends: base >= 4.15 && < 4.16, + build-depends: base >= 4.16 && < 4.17, containers >= 0.5, mtl >= 2.2.1, ghc-boot-th, - singletons == 3.0.*, + singletons == 3.0.1, syb >= 0.4, - template-haskell >= 2.17 && < 2.18, - th-desugar >= 1.12 && < 1.13, + template-haskell >= 2.18 && < 2.19, + th-desugar >= 1.13 && < 1.14, th-orphans >= 0.13.11 && < 0.14, transformers >= 0.5.2 default-language: Haskell2010 diff --git a/src/Data/Singletons/TH.hs b/src/Data/Singletons/TH.hs --- a/src/Data/Singletons/TH.hs +++ b/src/Data/Singletons/TH.hs @@ -121,4 +121,4 @@ where conToPat :: (Name, Int) -> DPat conToPat (name, num_fields) = - DConP name (replicate num_fields DWildP) + DConP name [] (replicate num_fields DWildP) diff --git a/src/Data/Singletons/TH/Deriving/Enum.hs b/src/Data/Singletons/TH/Deriving/Enum.hs --- a/src/Data/Singletons/TH/Deriving/Enum.hs +++ b/src/Data/Singletons/TH/Deriving/Enum.hs @@ -45,11 +45,11 @@ to_enum_rhs [] _ = DVarE errorName `DAppE` DLitE (StringL "toEnum: bad argument") to_enum_rhs (DCon _ _ name _ _ : rest) (num:nums) = DCaseE (DVarE equalsName `DAppE` DVarE n `DAppE` DLitE (IntegerL num)) - [ DMatch (DConP trueName []) (DConE name) - , DMatch (DConP falseName []) (to_enum_rhs rest nums) ] + [ DMatch (DConP trueName [] []) (DConE name) + , DMatch (DConP falseName [] []) (to_enum_rhs rest nums) ] to_enum_rhs _ _ = error "Internal error: exhausted infinite list in to_enum_rhs" - from_enum = UFunction (zipWith (\i con -> DClause [DConP (extractName con) []] + from_enum = UFunction (zipWith (\i con -> DClause [DConP (extractName con) [] []] (DLitE (IntegerL i))) [0..] cons) return (InstDecl { id_cxt = fromMaybe [] mb_ctxt diff --git a/src/Data/Singletons/TH/Deriving/Eq.hs b/src/Data/Singletons/TH/Deriving/Eq.hs --- a/src/Data/Singletons/TH/Deriving/Eq.hs +++ b/src/Data/Singletons/TH/Deriving/Eq.hs @@ -44,13 +44,13 @@ lvars = map DVarE lnames rvars = map DVarE rnames pure $ DClause - [DConP lname lpats, DConP rname rpats] + [DConP lname [] lpats, DConP rname [] rpats] (andExp (zipWith (\l r -> foldExp (DVarE equalsName) [l, r]) lvars rvars)) | otherwise = pure $ DClause - [DConP lname (replicate lNumArgs DWildP), - DConP rname (replicate rNumArgs DWildP)] + [DConP lname [] (replicate lNumArgs DWildP), + DConP rname [] (replicate rNumArgs DWildP)] (DConE falseName) where andExp :: [DExp] -> DExp diff --git a/src/Data/Singletons/TH/Deriving/Ord.hs b/src/Data/Singletons/TH/Deriving/Ord.hs --- a/src/Data/Singletons/TH/Deriving/Ord.hs +++ b/src/Data/Singletons/TH/Deriving/Ord.hs @@ -45,8 +45,8 @@ let tys = tysOfConFields fields a_names <- mapM (const $ newUniqueName "a") tys b_names <- mapM (const $ newUniqueName "b") tys - let pat1 = DConP name (map DVarP a_names) - pat2 = DConP name (map DVarP b_names) + let pat1 = DConP name [] (map DVarP a_names) + pat2 = DConP name [] (map DVarP b_names) return $ DClause [pat1, pat2] (DVarE foldlName `DAppE` DVarE thenCmpName `DAppE` DConE cmpEQName `DAppE` @@ -63,8 +63,8 @@ EQ -> DConE cmpEQName GT -> DConE cmpGTName) where - pat1 = DConP name1 (map (const DWildP) (tysOfConFields fields1)) - pat2 = DConP name2 (map (const DWildP) (tysOfConFields fields2)) + pat1 = DConP name1 [] (map (const DWildP) (tysOfConFields fields1)) + pat2 = DConP name2 [] (map (const DWildP) (tysOfConFields fields2)) -- A variant of mk_equal_clause tailored to empty datatypes mk_empty_clause :: DClause diff --git a/src/Data/Singletons/TH/Deriving/Show.hs b/src/Data/Singletons/TH/Deriving/Show.hs --- a/src/Data/Singletons/TH/Deriving/Show.hs +++ b/src/Data/Singletons/TH/Deriving/Show.hs @@ -57,7 +57,7 @@ -- No fields: print just the constructor name, with no parentheses DNormalC _ [] -> return $ - DClause [DWildP, DConP con_name []] $ + DClause [DWildP, DConP con_name [] []] $ DVarE showStringName `DAppE` dStringE (parenInfixConName con_name "") -- Infix constructors have special Show treatment. @@ -73,7 +73,7 @@ -- Make sure to handle infix data constructors -- like (Int `Foo` Int) else " `" ++ op_name ++ "` " - return $ DClause [DVarP p, DConP con_name [DVarP argL, DVarP argR]] $ + return $ DClause [DVarP p, DConP con_name [] [DVarP argL, DVarP argR]] $ (DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE con_prec)) `DAppE` (DVarE composeName @@ -94,7 +94,7 @@ `DAppE` (DVarE showStringName `DAppE` dStringE (parenInfixConName con_name " ")) `DAppE` composed_args - return $ DClause [DVarP p, DConP con_name $ map DVarP args] $ + return $ DClause [DVarP p, DConP con_name [] $ map DVarP args] $ DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) `DAppE` named_args @@ -124,7 +124,7 @@ `DAppE` (DVarE showStringName `DAppE` dStringE (parenInfixConName con_name " ")) `DAppE` composed_args - return $ DClause [DVarP p, DConP con_name $ map DVarP args] $ + return $ DClause [DVarP p, DConP con_name [] $ map DVarP args] $ DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) `DAppE` named_args @@ -140,8 +140,7 @@ showsPrecE prec n = DVarE showsPrecName `DAppE` dIntegerE prec `DAppE` DVarE n dCharE :: Char -> DExp -dCharE c = DLitE $ StringL [c] -- There aren't type-level characters yet, - -- so fake it with a string +dCharE = DLitE . CharL dStringE :: String -> DExp dStringE = DLitE . StringL diff --git a/src/Data/Singletons/TH/Deriving/Util.hs b/src/Data/Singletons/TH/Deriving/Util.hs --- a/src/Data/Singletons/TH/Deriving/Util.hs +++ b/src/Data/Singletons/TH/Deriving/Util.hs @@ -284,7 +284,7 @@ -> q DClause mkSimpleConClause fold extra_pats (DCon _ _ con_name _ _) insides = do vars_needed <- replicateM (length insides) $ newUniqueName "a" - let pat = DConP con_name (map DVarP vars_needed) + let pat = DConP con_name [] (map DVarP vars_needed) rhs = fold con_name (zipWith (\i v -> i `DAppE` DVarE v) insides vars_needed) pure $ DClause (extra_pats ++ [pat]) rhs diff --git a/src/Data/Singletons/TH/Names.hs b/src/Data/Singletons/TH/Names.hs --- a/src/Data/Singletons/TH/Names.hs +++ b/src/Data/Singletons/TH/Names.hs @@ -17,7 +17,7 @@ import Data.Singletons.TH.Util import Language.Haskell.TH.Syntax import Language.Haskell.TH.Desugar -import GHC.TypeLits ( Nat, Symbol ) +import GHC.TypeLits ( Symbol ) import GHC.Exts ( Constraint ) import GHC.Show ( showCommaSpace, showSpace ) import Data.String (fromString) @@ -60,9 +60,10 @@ maxBoundName, repName, nilName, consName, listName, tyFunArrowName, applyName, applyTyConName, applyTyConAux1Name, - natName, symbolName, stringName, + symbolName, stringName, eqName, ordName, boundedName, orderingName, - singFamilyName, singIName, singMethName, demoteName, withSingIName, + singFamilyName, singIName, singI1Name, singI2Name, + singMethName, liftSingName, liftSing2Name, demoteName, withSingIName, singKindClassName, someSingTypeName, someSingDataName, sDecideClassName, sDecideMethName, testEqualityClassName, testEqualityMethName, decideEqualityName, @@ -93,7 +94,6 @@ applyTyConName = ''ApplyTyCon applyTyConAux1Name = ''ApplyTyConAux1 symbolName = ''Symbol -natName = ''Nat stringName = ''String eqName = ''Eq ordName = ''Ord @@ -101,7 +101,11 @@ orderingName = ''Ordering singFamilyName = ''Sing singIName = ''SingI +singI1Name = ''SingI1 +singI2Name = ''SingI2 singMethName = 'sing +liftSingName = 'liftSing +liftSing2Name = 'liftSing2 toSingName = 'toSing fromSingName = 'fromSing demoteName = ''Demote @@ -172,6 +176,18 @@ mkTyConName :: Int -> Name mkTyConName i = mkName $ "TyCon" ++ show i + +mkSingIName :: Int -> Name +mkSingIName 0 = singIName +mkSingIName 1 = singI1Name +mkSingIName 2 = singI2Name +mkSingIName n = error $ "SingI" ++ show n ++ " does not exist" + +mkSingMethName :: Int -> Name +mkSingMethName 0 = singMethName +mkSingMethName 1 = liftSingName +mkSingMethName 2 = liftSing2Name +mkSingMethName n = error $ "SingI" ++ show n ++ " does not exist" boolKi :: DKind boolKi = DConT boolName diff --git a/src/Data/Singletons/TH/Promote.hs b/src/Data/Singletons/TH/Promote.hs --- a/src/Data/Singletons/TH/Promote.hs +++ b/src/Data/Singletons/TH/Promote.hs @@ -1050,11 +1050,18 @@ tyName <- mkTyName name tell $ PromDPatInfos [(name, tyName)] OSet.empty return (DVarT tyName, ADVarP name) -promotePat (DConP name pats) = do +promotePat (DConP name tys pats) = do opts <- getOptions + kis <- traverse (promoteType_options conOptions) tys (types, pats') <- mapAndUnzipM promotePat pats let name' = promotedDataTypeOrConName opts name - return (foldType (DConT name') types, ADConP name pats') + return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats') + where + -- Currently, visible type patterns of data constructors are the one place + -- in `singletons-th` where it makes sense to promote wildcard types, as it + -- will produce code that GHC will accept. + conOptions :: PromoteTypeOptions + conOptions = defaultPromoteTypeOptions{ptoAllowWildcards = True} promotePat (DTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern in promotion" second ADTildeP <$> promotePat pat @@ -1149,8 +1156,9 @@ pure $ if os_enabled then DConT (promotedValueName opts fromStringName Nothing) `DAppT` prom_str_lit else prom_str_lit +promoteLitExp (CharL c) = return $ DLitT (CharTyLit c) promoteLitExp lit = - fail ("Only string and natural number literals can be promoted: " ++ show lit) + fail ("Only string, natural number, and character literals can be promoted: " ++ show lit) promoteLitPat :: MonadFail m => Lit -> m DType promoteLitPat (IntegerL n) @@ -1159,5 +1167,6 @@ fail $ "Negative literal patterns are not allowed,\n" ++ "because literal patterns are promoted to natural numbers." promoteLitPat (StringL str) = return $ DLitT (StrTyLit str) +promoteLitPat (CharL c) = return $ DLitT (CharTyLit c) promoteLitPat lit = - fail ("Only string and natural number literals can be promoted: " ++ show lit) + fail ("Only string, natural number, and character literals can be promoted: " ++ show lit) diff --git a/src/Data/Singletons/TH/Promote/Defun.hs b/src/Data/Singletons/TH/Promote/Defun.hs --- a/src/Data/Singletons/TH/Promote/Defun.hs +++ b/src/Data/Singletons/TH/Promote/Defun.hs @@ -205,7 +205,7 @@ opts <- getOptions extra_name <- qNewName "arg" let sak_arg_n = length sak_arg_kis - -- Use noExactName below to avoid #17537. + -- Use noExactName below to avoid GHC#17537. arg_names <- replicateM sak_arg_n (noExactName <$> qNewName "a") let -- The inner loop. @go n arg_nks res_nks@ returns @(res_k, decls)@. @@ -285,7 +285,7 @@ defun_fallback tvbs' m_res' = do opts <- getOptions extra_name <- qNewName "arg" - -- Use noExactTyVars below to avoid #11812. + -- Use noExactTyVars below to avoid GHC#11812. (tvbs, m_res) <- eta_expand (noExactTyVars tvbs') (noExactTyVars m_res') let tvbs_n = length tvbs @@ -413,7 +413,9 @@ mk_extra_tvb vfa = case vfa of DVisFADep tvb -> pure tvb - DVisFAAnon k -> (\n -> DKindedTV n () k) <$> qNewName "e" + DVisFAAnon k -> (\n -> DKindedTV n () k) <$> + -- Use noExactName below to avoid GHC#19743. + (noExactName <$> qNewName "e") mk_fix_decl :: Name -> Fixity -> DDec mk_fix_decl n f = DLetDec $ DInfixD f n diff --git a/src/Data/Singletons/TH/Promote/Type.hs b/src/Data/Singletons/TH/Promote/Type.hs --- a/src/Data/Singletons/TH/Promote/Type.hs +++ b/src/Data/Singletons/TH/Promote/Type.hs @@ -6,37 +6,76 @@ This file implements promotion of types into kinds. -} +{-# LANGUAGE ScopedTypeVariables #-} + module Data.Singletons.TH.Promote.Type - ( promoteType, promoteType_NC + ( promoteType, promoteType_NC, promoteType_options + , PromoteTypeOptions(..), defaultPromoteTypeOptions , promoteTypeArg_NC, promoteUnraveled ) where +import Control.Monad (when) +import Language.Haskell.TH (pprint) import Language.Haskell.TH.Desugar import Data.Singletons.TH.Names import Data.Singletons.TH.Options import Data.Singletons.TH.Util --- Promote a DType to the kind level. +-- | Promote a 'DType' to the kind level and invoke 'checkVanillaDType'. +-- See @Note [Vanilla-type validity checking during promotion]@. promoteType :: OptionsMonad m => DType -> m DKind -promoteType ty = do - checkVanillaDType ty - promoteType_NC ty +promoteType = promoteType_options defaultPromoteTypeOptions{ptoCheckVanilla = True} --- Promote a DType to the kind level. This is suffixed with "_NC" because --- we do not invoke checkVanillaDType here. --- See [Vanilla-type validity checking during promotion]. -promoteType_NC :: OptionsMonad m => DType -> m DKind -promoteType_NC = go [] +-- | Promote a 'DType' to the kind level. This is suffixed with \"_NC\" because +-- we do not invoke 'checkVanillaDType' here. +-- See @Note [Vanilla-type validity checking during promotion]@. +promoteType_NC :: forall m. OptionsMonad m => DType -> m DKind +promoteType_NC = promoteType_options defaultPromoteTypeOptions + +-- | Options for controlling how types are promoted at a fine granularity. +data PromoteTypeOptions = PromoteTypeOptions + { ptoCheckVanilla :: Bool + -- ^ If 'True', invoke 'checkVanillaDType' on the argument type being + -- promoted. See @Note [Vanilla-type validity checking during promotion]@. + , ptoAllowWildcards :: Bool + -- ^ If 'True', allow promoting wildcard types. Otherwise, throw an error. + -- In most places, GHC disallows kind-level wildcard types, so rather + -- than promoting such wildcards and getting an error message from GHC + -- /post facto/, we can catch such wildcards early and give a more + -- descriptive error message instead. + } deriving Show + +-- | The default 'PromoteTypeOptions': +-- +-- * 'checkVanillaDType' is not invoked. +-- +-- * Throw an error when attempting to promote a wildcard type. +defaultPromoteTypeOptions :: PromoteTypeOptions +defaultPromoteTypeOptions = PromoteTypeOptions + { ptoCheckVanilla = False + , ptoAllowWildcards = False + } + +-- | Promote a 'DType' to the kind level. This is the workhorse for +-- 'promoteType' and 'promoteType_NC'. +promoteType_options :: forall m. OptionsMonad m => PromoteTypeOptions -> DType -> m DKind +promoteType_options pto typ = do + -- See Note [Vanilla-type validity checking during promotion] + when (ptoCheckVanilla pto) $ + checkVanillaDType typ + go [] typ where - go :: OptionsMonad m => [DTypeArg] -> DType -> m DKind + go :: [DTypeArg] -> DType -> m DKind go [] (DForallT tele ty) = do ty' <- go [] ty pure $ DForallT tele ty' + go args ty@DForallT{} = illegal args ty -- We don't need to worry about constraints: they are used to express -- static guarantees at runtime. But, because we don't need to do -- anything special to keep static guarantees at compile time, we don't -- need to promote them. go [] (DConstrainedT _cxt ty) = go [] ty + go args ty@DConstrainedT{} = illegal args ty go args (DAppT t1 t2) = do k2 <- go [] t2 go (DTANormal k2 : args) t1 @@ -59,15 +98,29 @@ return $ applyDType (DConT (promotedDataTypeOrConName opts name)) args go [DTANormal k1, DTANormal k2] DArrowT = return $ DConT tyFunArrowName `DAppT` k1 `DAppT` k2 - go _ ty@DLitT{} = pure ty + go args ty@DArrowT = illegal args ty + go [] ty@DLitT{} = pure ty + go args ty@DLitT{} = illegal args ty + go args ty@DWildCardT{} + | ptoAllowWildcards pto + = pure $ applyDType ty args + | otherwise + = fail $ unlines + [ "`singletons-th` does not support wildcard types" + , "\tunless they appear in visible type patterns of data constructors" + , "\tIn the type: " ++ pprint (sweeten typ) + ] - go args hd = fail $ "Illegal Haskell construct encountered:\n" ++ - "headed by: " ++ show hd ++ "\n" ++ - "applied to: " ++ show args + illegal :: [DTypeArg] -> DType -> m a + illegal args hd = fail $ unlines + [ "Illegal Haskell construct encountered:" + , "\theaded by: " ++ show hd + , "\tapplied to: " ++ show args + ] -- | Promote a DTypeArg to the kind level. This is suffixed with "_NC" because -- we do not invoke checkVanillaDType here. --- See [Vanilla-type validity checking during promotion]. +-- See @Note [Vanilla-type validity checking during promotion]@. promoteTypeArg_NC :: OptionsMonad m => DTypeArg -> m DTypeArg promoteTypeArg_NC (DTANormal t) = DTANormal <$> promoteType_NC t promoteTypeArg_NC ta@(DTyArg _) = pure ta -- Kinds are already promoted diff --git a/src/Data/Singletons/TH/Single.hs b/src/Data/Singletons/TH/Single.hs --- a/src/Data/Singletons/TH/Single.hs +++ b/src/Data/Singletons/TH/Single.hs @@ -790,9 +790,9 @@ Just tyname -> return tyname pure $ DVarP (singledValueName opts name) `DSigP` (singFamily `DAppT` DVarT tyname) - go (ADConP name pats) = do + go (ADConP name tys pats) = do opts <- getOptions - DConP (singledDataConName opts name) <$> mapM go pats + DConP (singledDataConName opts name) tys <$> mapM go pats go (ADTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern during singleton generation." @@ -1065,8 +1065,10 @@ pure $ if os_enabled then DVarE (singledValueName opts fromStringName) `DAppE` sing_str_lit else sing_str_lit +singLit (CharL c) = + return $ DVarE singMethName `DSigE` (singFamily `DAppT` DLitT (CharTyLit c)) singLit lit = - fail ("Only string and natural number literals can be singled: " ++ show lit) + fail ("Only string, natural number, and character literals can be singled: " ++ show lit) {- Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization] diff --git a/src/Data/Singletons/TH/Single/Data.hs b/src/Data/Singletons/TH/Single/Data.hs --- a/src/Data/Singletons/TH/Single/Data.hs +++ b/src/Data/Singletons/TH/Single/Data.hs @@ -12,6 +12,7 @@ import Language.Haskell.TH.Desugar import Language.Haskell.TH.Syntax +import Data.Maybe import Data.Singletons.TH.Names import Data.Singletons.TH.Options import Data.Singletons.TH.Promote.Type @@ -117,7 +118,7 @@ let (cname, numArgs) = extractNameArgs c cname' <- mkConName cname varNames <- replicateM numArgs (qNewName "b") - return $ DClause [DConP (singledDataConName opts cname) (map DVarP varNames)] + return $ DClause [DConP (singledDataConName opts cname) [] (map DVarP varNames)] (foldExp (DConE cname') (map (DAppE (DVarE fromSingName) . DVarE) varNames)) @@ -133,9 +134,9 @@ let varPats = zipWith mkToSingVarPat varNames promoted recursiveCalls = zipWith mkRecursiveCall varNames promoted return $ - DClause [DConP cname' varPats] + DClause [DConP cname' [] varPats] (multiCase recursiveCalls - (map (DConP someSingDataName . listify . DVarP) + (map (DConP someSingDataName [] . listify . DVarP) svarNames) (DAppE (DConE someSingDataName) (foldExp (DConE (singledDataConName opts cname)) @@ -174,6 +175,7 @@ = do opts <- getOptions let types = tysOfConFields fields + numTypes = length types sName = singledDataConName opts name sCon = DConE sName pCon = DConT $ promotedDataTypeOrConName opts name @@ -186,14 +188,24 @@ kvbs = singTypeKVBs con_tvbs kinds [] rty' mempty all_tvbs = kvbs ++ zipWith (`DKindedTV` SpecifiedSpec) indexNames kinds + -- @mb_SingI_dec k@ returns 'Just' an instance of @SingI@ if @k@ is + -- less than or equal to the number of fields in the data constructor. + -- Otherwise, it returns 'Nothing'. + let mb_SingI_dec :: Int -> Maybe DDec + mb_SingI_dec k + | k <= numTypes + = let take_until_k = take (numTypes - k) in + Just $ DInstanceD Nothing Nothing + (map (DAppT (DConT singIName)) (take_until_k indices)) + (DAppT (DConT (mkSingIName k)) + (foldType pCon (take_until_k kindedIndices))) + [DLetDec $ DValD (DVarP (mkSingMethName k)) + (foldExp sCon (replicate (numTypes - k) (DVarE singMethName)))] + | otherwise + = Nothing + -- SingI instance for data constructor - emitDecs - [DInstanceD Nothing Nothing - (map (DAppT (DConT singIName)) indices) - (DAppT (DConT singIName) - (foldType pCon kindedIndices)) - [DLetDec $ DValD (DVarP singMethName) - (foldExp sCon (map (const $ DVarE singMethName) types))]] + emitDecs $ mapMaybe mb_SingI_dec [0, 1, 2] -- SingI instances for defunctionalization symbols. Note that we don't -- support contexts in constructors at the moment, so it's fine for now to -- just assume that the context is always (). diff --git a/src/Data/Singletons/TH/Single/Decide.hs b/src/Data/Singletons/TH/Single/Decide.hs --- a/src/Data/Singletons/TH/Single/Decide.hs +++ b/src/Data/Singletons/TH/Single/Decide.hs @@ -61,7 +61,7 @@ mkDecideMethClause (c1, c2) | lname == rname = if lNumArgs == 0 - then return $ DClause [DConP lname [], DConP rname []] + then return $ DClause [DConP lname [] [], DConP rname [] []] (DAppE (DConE provedName) (DConE reflName)) else do lnames <- replicateM lNumArgs (qNewName "a") @@ -73,20 +73,20 @@ rvars = map DVarE rnames refl <- qNewName "refl" return $ DClause - [DConP lname lpats, DConP rname rpats] + [DConP lname [] lpats, DConP rname [] rpats] (DCaseE (mkTupleDExp $ zipWith (\l r -> foldExp (DVarE sDecideMethName) [l, r]) lvars rvars) ((DMatch (mkTupleDPat (replicate lNumArgs - (DConP provedName [DConP reflName []]))) + (DConP provedName [] [DConP reflName [] []]))) (DAppE (DConE provedName) (DConE reflName))) : [DMatch (mkTupleDPat (replicate i DWildP ++ - DConP disprovedName [DVarP contra] : + DConP disprovedName [] [DVarP contra] : replicate (lNumArgs - i - 1) DWildP)) (DAppE (DConE disprovedName) (DLamE [refl] $ DCaseE (DVarE refl) - [DMatch (DConP reflName []) $ + [DMatch (DConP reflName [] []) $ (DAppE (DVarE contra) (DConE reflName))])) | i <- [0..lNumArgs-1] ])) @@ -94,8 +94,8 @@ | otherwise = do x <- qNewName "x" return $ DClause - [DConP lname (replicate lNumArgs DWildP), - DConP rname (replicate rNumArgs DWildP)] + [DConP lname [] (replicate lNumArgs DWildP), + DConP rname [] (replicate rNumArgs DWildP)] (DAppE (DConE disprovedName) (DLamE [x] (DCaseE (DVarE x) []))) where diff --git a/src/Data/Singletons/TH/Single/Defun.hs b/src/Data/Singletons/TH/Single/Defun.hs --- a/src/Data/Singletons/TH/Single/Defun.hs +++ b/src/Data/Singletons/TH/Single/Defun.hs @@ -25,7 +25,7 @@ import Language.Haskell.TH.Syntax -- Given the Name of something, take the defunctionalization symbols for its --- promoted counterpart and create SingI instances for them. As a concrete +-- promoted counterpart and create SingI{,1,2} instances for them. As a concrete -- example, if you have: -- -- foo :: Eq a => a -> a -> Bool @@ -36,7 +36,7 @@ -- FooSym0 :: a ~> a ~> Bool -- FooSym1 :: a -> a ~> Bool -- --- We can declare SingI instances for these two symbols like so: +-- We can declare SingI and SingI1 instances for these two symbols like so: -- -- instance SEq a => SingI (FooSym0 :: a ~> a ~> Bool) where -- sing = singFun2 sFoo @@ -44,6 +44,14 @@ -- instance (SEq a, SingI x) => SingI (FooSym1 x :: a ~> Bool) where -- sing = singFun1 (sFoo (sing @_ @x)) -- +-- instance SEq a => SingI1 (FooSym1 :: a -> a ~> Bool) where +-- liftSing s = singFun1 (sFoo s) +-- +-- Only FooSym1 will have a SingI1 instance, as unlike FooSym0, it is able to +-- be partially applied (using normal function application) to a single +-- argument. Neither FooSym0 nor FooSym1 can be partially applied to two +-- arguments, so neither will receive a SingI2 instance. +-- -- Note that singDefuns takes Maybe DKinds for the promoted argument and result -- types, in case we have an entity whose type needs to be inferred. -- See Note [singDefuns and type inference]. @@ -61,8 +69,8 @@ _ -> 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 opts 0 sty_ctxt [] tvbs + let tvbs = zipWith inferMaybeKindTV names mb_ty_args + (_, insts) <- go opts 0 sty_ctxt [] tvbs pure insts where num_ty_args :: Int @@ -103,64 +111,95 @@ -- to be a performance bottleneck since the number of arguments rarely -- gets to be that large. go :: Options -> Int -> DCxt -> [DTyVarBndrUnit] -> [DTyVarBndrUnit] - -> (Maybe DKind, [DDec]) - go _ _ _ _ [] = (mb_ty_res, []) - go opts sym_num sty_ctxt arg_tvbs (res_tvb:res_tvbs) = - (mb_new_res, new_inst:insts) + -> SgM (Maybe DKind, [DDec]) + go _ _ _ _ [] = pure (mb_ty_res, []) + go opts sym_num sty_ctxt arg_tvbs (res_tvb:res_tvbs) = do + (mb_res, insts) <- go opts (sym_num + 1) sty_ctxt (arg_tvbs ++ [res_tvb]) res_tvbs + new_insts <- mapMaybeM (mb_new_inst mb_res) [0, 1, 2] + pure (mk_inst_kind [] res_tvb mb_res, new_insts ++ insts) where - mb_res :: Maybe DKind - insts :: [DDec] - (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 - sing_fun_num :: Int sing_fun_num = num_ty_args - sym_num - mk_sing_fun_expr :: DExp -> DExp - mk_sing_fun_expr sing_expr = - foldl' (\f tvb_n -> f `DAppE` (DVarE singMethName `DAppTypeE` DVarT tvb_n)) - sing_expr - (map extractTvbName arg_tvbs) - - singI_ctxt :: DCxt - singI_ctxt = map (DAppT (DConT singIName) . tvbToType) arg_tvbs - - mk_inst_ty :: DType -> DType - mk_inst_ty inst_head - = case mb_new_res of - Just inst_kind -> inst_head `DSigT` inst_kind - Nothing -> inst_head - - arg_tvb_tys :: [DType] - arg_tvb_tys = map dTyVarBndrToDType arg_tvbs - -- Construct the arrow kind used to annotate the defunctionalization - -- symbol (e.g., the `a ~> a ~> Bool` in - -- `SingI (FooSym0 :: a ~> a ~> Bool)`). + -- symbol. For example, this constructs the `a -> b -> c ~> Bool` in + -- `SingI1 (FooSym1 :: a -> b -> c ~> Bool)`, where: + -- + -- * The first argument to `mk_inst_kind` gives the kinds [a, b], which + -- are used with normal function arrows. + -- * The second argumen to `mk_inst_kind` gives the kind `c`, which is + -- used with a defunctionalized function arrow. + -- -- If any of the argument kinds or result kind isn't known (i.e., is -- Nothing), then we opt not to construct this arrow kind altogether. -- See Note [singDefuns and type inference] - mk_inst_kind :: DTyVarBndrUnit -> Maybe DKind -> Maybe DKind - mk_inst_kind tvb' = buildTyFunArrow_maybe (extractTvbKind tvb') + mk_inst_kind :: [DTyVarBndrUnit] -> DTyVarBndrUnit -> Maybe DKind -> Maybe DKind + mk_inst_kind funTvbs defunTvb mbKind = + foldr buildFunArrow_maybe + (buildTyFunArrow_maybe (extractTvbKind defunTvb) mbKind) + (map extractTvbKind funTvbs) - new_inst :: DDec - new_inst = DInstanceD Nothing Nothing - (sty_ctxt ++ singI_ctxt) - (DConT singIName `DAppT` mk_inst_ty defun_inst_ty) - [DLetDec $ DValD (DVarP singMethName) - $ wrapSingFun sing_fun_num defun_inst_ty - $ mk_sing_fun_expr sing_exp ] + -- @mb_new_inst mb_res k@ returns 'Just' an instance of @SingI@ if + -- @k@ is less than or equal to the number of arguments to which the + -- defunctionalization symbol can be partially applied using normal + -- function application. Otherwise, it returns 'Nothing'. + mb_new_inst :: Maybe DKind -> Int -> SgM (Maybe DDec) + mb_new_inst mb_res k + | k <= sym_num + = do vs <- replicateM k $ qNewName "s" + let sing_vs = zipWith (\v arg_tvb -> + DSigP (DVarP v) + (singFamily `DAppT` dTyVarBndrToDType arg_tvb)) + vs last_arg_tvbs + pure $ Just $ + DInstanceD Nothing Nothing + (sty_ctxt ++ singI_ctxt) + (DConT (mkSingIName k) `DAppT` mk_inst_ty (mk_defun_inst_ty init_arg_tvbs)) + [ DLetDec $ DFunD (mkSingMethName k) + [ DClause sing_vs + $ wrapSingFun sing_fun_num (mk_defun_inst_ty arg_tvbs) + $ mk_sing_fun_expr sing_exp vs + ] + ] + | otherwise + = pure Nothing where - defun_inst_ty :: DType - defun_inst_ty = foldType (DConT (defunctionalizedName opts n sym_num)) - arg_tvb_tys + init_arg_tvbs, last_arg_tvbs :: [DTyVarBndrUnit] + (init_arg_tvbs, last_arg_tvbs) = splitAt (sym_num - k) arg_tvbs + mk_defun_inst_ty :: [DTyVarBndrUnit] -> DType + mk_defun_inst_ty tvbs = + foldType (DConT (defunctionalizedName opts n sym_num)) + (map dTyVarBndrToDType tvbs) + sing_exp :: DExp sing_exp = case ns of DataName -> DConE $ singledDataConName opts n _ -> DVarE $ singledValueName opts n + + mk_sing_fun_expr :: DExp -> [Name] -> DExp + mk_sing_fun_expr sing_expr vs = + foldl' DAppE sing_expr + (map (\arg_tvb -> DVarE singMethName `DAppTypeE` + DVarT (extractTvbName arg_tvb)) + init_arg_tvbs ++ + map DVarE vs) + + singI_ctxt :: DCxt + singI_ctxt = map (DAppT (DConT singIName) . tvbToType) init_arg_tvbs + + mk_inst_ty :: DType -> DType + mk_inst_ty inst_head + = case mk_inst_kind last_arg_tvbs res_tvb mb_res of + Just inst_kind -> inst_head `DSigT` inst_kind + Nothing -> inst_head + +-- Shorthand for building (k1 -> k2) +buildFunArrow :: DKind -> DKind -> DKind +buildFunArrow k1 k2 = DArrowT `DAppT` k1 `DAppT` k2 + +buildFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind +buildFunArrow_maybe m_k1 m_k2 = buildFunArrow <$> m_k1 <*> m_k2 {- Note [singDefuns and type inference] diff --git a/src/Data/Singletons/TH/Syntax.hs b/src/Data/Singletons/TH/Syntax.hs --- a/src/Data/Singletons/TH/Syntax.hs +++ b/src/Data/Singletons/TH/Syntax.hs @@ -114,7 +114,7 @@ -- A DPat with a pattern-signature node annotated with its type-level equivalent data ADPat = ADLitP Lit | ADVarP Name - | ADConP Name [ADPat] + | ADConP Name [DType] [ADPat] | ADTildeP ADPat | ADBangP ADPat | ADSigP DType -- The promoted pattern. Will not contain any wildcards, diff --git a/src/Data/Singletons/TH/Util.hs b/src/Data/Singletons/TH/Util.hs --- a/src/Data/Singletons/TH/Util.hs +++ b/src/Data/Singletons/TH/Util.hs @@ -370,7 +370,7 @@ replaceTvbKind (DVisFADep tvb) _ = tvb replaceTvbKind (DVisFAAnon k) tvb = DKindedTV (extractTvbName tvb) () k --- changes all TyVars not to be NameU's. Workaround for GHC#11812/#17537 +-- changes all TyVars not to be NameU's. Workaround for GHC#11812/#17537/#19743 noExactTyVars :: Data a => a -> a noExactTyVars = everywhere go where @@ -390,7 +390,7 @@ fix_inj_ann (InjectivityAnn lhs rhs) = InjectivityAnn (noExactName lhs) (map noExactName rhs) --- changes a Name not to be a NameU. Workaround for GHC#11812/#17537 +-- changes a Name not to be a NameU. Workaround for GHC#11812/#17537/#19743 noExactName :: Name -> Name noExactName (Name (OccName occ) (NameU unique)) = mkName (occ ++ show unique) noExactName n = n