singletons-th 3.0 → 3.1
raw patch · 19 files changed
+265/−124 lines, 19 filesdep ~basedep ~singletonsdep ~template-haskell
Dependency ranges changed: base, singletons, template-haskell, th-desugar
Files
- CHANGES.md +9/−0
- README.md +1/−1
- singletons-th.cabal +8/−8
- src/Data/Singletons/TH.hs +1/−1
- src/Data/Singletons/TH/Deriving/Enum.hs +3/−3
- src/Data/Singletons/TH/Deriving/Eq.hs +3/−3
- src/Data/Singletons/TH/Deriving/Ord.hs +4/−4
- src/Data/Singletons/TH/Deriving/Show.hs +5/−6
- src/Data/Singletons/TH/Deriving/Util.hs +1/−1
- src/Data/Singletons/TH/Names.hs +20/−4
- src/Data/Singletons/TH/Promote.hs +13/−4
- src/Data/Singletons/TH/Promote/Defun.hs +5/−3
- src/Data/Singletons/TH/Promote/Type.hs +69/−16
- src/Data/Singletons/TH/Single.hs +5/−3
- src/Data/Singletons/TH/Single/Data.hs +22/−10
- src/Data/Singletons/TH/Single/Decide.hs +7/−7
- src/Data/Singletons/TH/Single/Defun.hs +86/−47
- src/Data/Singletons/TH/Syntax.hs +1/−1
- src/Data/Singletons/TH/Util.hs +2/−2
CHANGES.md view
@@ -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:
README.md view
@@ -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).
singletons-th.cabal view
@@ -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 <ryan.gl.scott@gmail.com> 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@ @<https://github.com/goldfirere/singletons/blob/master/README.md README>@. .@@ -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
src/Data/Singletons/TH.hs view
@@ -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)
src/Data/Singletons/TH/Deriving/Enum.hs view
@@ -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
src/Data/Singletons/TH/Deriving/Eq.hs view
@@ -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
src/Data/Singletons/TH/Deriving/Ord.hs view
@@ -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
src/Data/Singletons/TH/Deriving/Show.hs view
@@ -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
src/Data/Singletons/TH/Deriving/Util.hs view
@@ -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
src/Data/Singletons/TH/Names.hs view
@@ -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
src/Data/Singletons/TH/Promote.hs view
@@ -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)
src/Data/Singletons/TH/Promote/Defun.hs view
@@ -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
src/Data/Singletons/TH/Promote/Type.hs view
@@ -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
src/Data/Singletons/TH/Single.hs view
@@ -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]
src/Data/Singletons/TH/Single/Data.hs view
@@ -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<k>@ 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 ().
src/Data/Singletons/TH/Single/Decide.hs view
@@ -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
src/Data/Singletons/TH/Single/Defun.hs view
@@ -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<k>@ 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]
src/Data/Singletons/TH/Syntax.hs view
@@ -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,
src/Data/Singletons/TH/Util.hs view
@@ -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