singletons-th 3.3 → 3.4
raw patch · 11 files changed
+160/−24 lines, 11 filesdep ~basedep ~template-haskelldep ~th-desugar
Dependency ranges changed: base, template-haskell, th-desugar
Files
- CHANGES.md +14/−0
- README.md +1/−1
- singletons-th.cabal +6/−6
- src/Data/Singletons/TH/Partition.hs +1/−1
- src/Data/Singletons/TH/Promote.hs +81/−5
- src/Data/Singletons/TH/Promote/Defun.hs +30/−8
- src/Data/Singletons/TH/Single.hs +1/−0
- src/Data/Singletons/TH/Single/Defun.hs +0/−1
- src/Data/Singletons/TH/Single/Fixity.hs +1/−1
- src/Data/Singletons/TH/Syntax.hs +1/−1
- src/Data/Singletons/TH/Util.hs +24/−0
CHANGES.md view
@@ -1,6 +1,20 @@ Changelog for the `singletons-th` project ========================================= +3.4 [2024.05.12]+----------------+* Require building with GHC 9.10.+* GHC 9.10 removes arity inference when kind-checking type families with+ standalone kind signatures, persuant to [this GHC+ proposal](https://github.com/ghc-proposals/ghc-proposals/blob/10290a668608d608c3f6c6010be265cf7a02e1fc/proposals/0425-decl-invis-binders.rst#breakage-2-arity-inference).+ In order to promote functions to type families with correct arities,+ `singletons-th` uses `TypeAbstractions` to bind type variable binders in the+ headers of promoted type families. As such, it is quite likely that you will+ need to enable `TypeAbstractions` in order to make GHC accept code that+ `singletons-th` generates.+* Fix a bug causing definitions with type signatures using inferred type+ variable binders (e.g., `forall a {b}. a -> b -> a`) to fail to promote.+ 3.3 [2023.10.13] ---------------- * Require building with GHC 9.8.
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.8). For more information,+of GHC (currently GHC 9.10). 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.3+version: 3.4 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.8.1+tested-with: GHC == 9.10.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.8). For more information,+ of GHC (currently GHC 9.10). For more information, consult the @singletons@ @<https://github.com/goldfirere/singletons/blob/master/README.md README>@. .@@ -52,14 +52,14 @@ library hs-source-dirs: src- build-depends: base >= 4.19 && < 4.20,+ build-depends: base >= 4.20 && < 4.21, containers >= 0.5, mtl >= 2.2.1 && < 2.4, ghc-boot-th, singletons == 3.0.*, syb >= 0.4,- template-haskell >= 2.21 && < 2.22,- th-desugar >= 1.16 && < 1.17,+ template-haskell >= 2.22 && < 2.23,+ th-desugar >= 1.17 && < 1.18, th-orphans >= 0.13.11 && < 0.14, transformers >= 0.5.2 default-language: GHC2021
src/Data/Singletons/TH/Partition.hs view
@@ -163,7 +163,7 @@ pure (valueBinding name (UValue exp), mempty) partitionClassDec (DLetDec (DFunD name clauses)) = pure (valueBinding name (UFunction clauses), mempty)-partitionClassDec (DLetDec (DInfixD fixity name)) =+partitionClassDec (DLetDec (DInfixD fixity _ name)) = pure (infixDecl fixity name, mempty) partitionClassDec (DLetDec (DPragmaD {})) = pure (mempty, mempty)
src/Data/Singletons/TH/Promote.hs view
@@ -637,7 +637,7 @@ where -- Produce the fixity declaration. finish :: Name -> q (Maybe DDec)- finish = pure . Just . DLetDec . DInfixD fixity+ finish = pure . Just . DLetDec . DInfixD fixity NoNamespaceSpecifier -- Don't produce a fixity declaration at all. This can happen in the -- following circumstances:@@ -786,6 +786,15 @@ ) -- 2(b). We have a standalone kind signature. Just sak ->+ -- Compute the type variable binders needed to give the type+ -- family the correct arity.+ -- See Note [Generating type families with the correct arity].+ let tvbs' | null tvbs+ = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf (argKs ++ [resK])+ | otherwise+ = tvbs+ arg_tvbs' = tvbSpecsToBndrVis tvbs' ++ arg_tvbs in ( lde_kvs_to_bind' , Just $ DKiSigD proName sak , DefunSAK sak@@ -793,7 +802,7 @@ -- the body of the type family declaration even if it is -- given a standalone kind signature. -- See Note [Keep redundant kind information for Haddocks].- , mk_tf_head arg_tvbs (DKindSig resK)+ , mk_tf_head arg_tvbs' (DKindSig resK) ) defun_decs <- defunctionalize proName m_fixity defun_ki@@ -957,6 +966,56 @@ work around this limitation by generating the redundant argument and kind information anyway. Thankfully, this is simple to accomplish, as we already compute this information to begin with.++Note [Generating type families with the correct arity]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+As of GHC 9.10, GHC no longer performs arity inference when kind-checking type+family declarations with standalone kind signatures. This is an important+consideration when promoting functions with top-level type signatures. For+example, we would not want to take this definition:++ f :: Either a Bool+ f = Right True++And promote it to this type family:++ type F :: Either a Bool+ type family F where+ F = Right True++GHC would reject this type family because it would expect F to have arity 0,+but its definition requires arity 1. This is because the definition of F is+tantamount to writing:++ F @a = Right @a @Bool True -- This takes 1 argument, hence arity 1++In order to make F kind-check, we need to generate a type family header that+explicitly declares it to have arity 1, not arity 0:++ type F :: Either a Bool+ type family F @a where+ F = Right True++Note the @a binder after F in the type family header.++If the standalone kind signature lacks an outermost forall, then we simply bind+the type variables in left-to-right order, preserving dependencies (using+`toposortTyVarsOf`). If the standalone kind signature does have an outermost+`forall`, then we bind the type variables according to the order in which it+appears in the `forall`, making sure to filter out any inferred type variable+binders. For example, we would want to take this definition (from #585):++ konst :: forall a {b}. a -> b -> a+ konst x _ = x++And promote it to this type family:++ type Konst :: forall a {b}. a -> b -> a+ type family Konst @a x y where+ Konst @a (x :: a) (_ :: b) = x++Note that we do not bind @b here. The `tvbSpecsToBndrVis` function is+responsible for filtering out inferred type variable binders. -} promoteClause :: Maybe Uniq@@ -1045,6 +1104,8 @@ tell $ PromDPatInfos [] (fvDType ki) return (DSigT promoted ki, ADSigP promoted pat' ki) promotePat DWildP = return (DWildCardT, ADWildP)+promotePat p@(DTypeP _) = fail ("Embedded type patterns cannot be promoted: " ++ show p)+promotePat p@(DInvisP _) = fail ("Invisible type patterns cannot be promoted: " ++ show p) promoteExp :: DExp -> PrM (DType, ADExp) promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name@@ -1106,6 +1167,7 @@ promoteExp e@(DStaticE _) = fail ("Static expressions cannot be promoted: " ++ show e) promoteExp e@(DTypedBracketE _) = fail ("Typed bracket expressions cannot be promoted: " ++ show e) promoteExp e@(DTypedSpliceE _) = fail ("Typed splice expressions cannot be promoted: " ++ show e)+promoteExp e@(DTypeE _) = fail ("Embedded type expressions cannot be promoted: " ++ show e) promoteLitExp :: OptionsMonad q => Lit -> q DType promoteLitExp (IntegerL n) = do@@ -1162,9 +1224,23 @@ Just (LDRKI m_sak tvbs _ _) | isJust m_sak -- Per the comments on LetDecRHSKindInfo, `isJust m_sak` is only True- -- if there are no local variables. Return the scoped type variables- -- `tvbs` as invisible arguments using `DTyArg`...- -> map (DTyArg . DVarT . extractTvbName) tvbs+ -- if there are no local variables. Convert the scoped type variables+ -- `tvbs` to invisible arguments, making sure to use+ -- `tvbSpecsToBndrVis` to filter out any inferred type variable+ -- binders. For instance, we want to promote this example (from #585):+ --+ -- konst :: forall a {b}. a -> b -> a+ -- konst x _ = x+ --+ -- To this type family:+ --+ -- type Konst :: forall a {b}. a -> b -> a+ -- type family Konst @a x y where+ -- Konst @a (x :: a) (_ :: b) = x+ --+ -- Note that we apply `a` in `Konst @a` but _not_ `b`, as `b` is+ -- bound using an inferred type variable binder.+ -> map dTyVarBndrVisToDTypeArg $ tvbSpecsToBndrVis tvbs _ -> -- ...otherwise, return the local variables as explicit arguments -- using DTANormal. map (DTANormal . DVarT) all_locals
src/Data/Singletons/TH/Promote/Defun.hs view
@@ -263,7 +263,16 @@ case res_nkss of [] -> let sat_sak_dec = mk_sak_dec sak_res_ki- sat_decs = mk_sat_decs opts n arg_tvbs (Just sak_res_ki)+ -- Compute the type variable binders needed to give the type+ -- family the correct arity.+ -- See Note [Generating type families with the correct arity]+ -- in D.S.TH.Promote.+ sak_tvbs' | null sak_tvbs+ = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf (sak_arg_kis ++ [sak_res_ki])+ | otherwise+ = sak_tvbs+ sat_decs = mk_sat_decs opts n sak_tvbs' arg_tvbs (Just sak_res_ki) in (sak_res_ki, sat_sak_dec:sat_decs) res_nk:res_nks -> let (res_ki, decs) = go (n+1) (arg_nks ++ [res_nk]) res_nks@@ -316,7 +325,7 @@ go n arg_tvbs res_tvbss = case res_tvbss of [] ->- let sat_decs = mk_sat_decs opts n arg_tvbs m_res+ let sat_decs = mk_sat_decs opts n [] arg_tvbs m_res in (m_res, sat_decs) res_tvb:res_tvbs -> let (m_res_ki, decs) = go (n+1) (arg_tvbs ++ [res_tvb]) res_tvbs@@ -380,15 +389,28 @@ -- Generate a "fully saturated" defunction symbol, along with a fixity -- declaration (if needed). -- See Note [Fully saturated defunctionalization symbols].- mk_sat_decs :: Options -> Int -> [DTyVarBndrVis] -> Maybe DKind -> [DDec]- mk_sat_decs opts n sat_tvbs m_sat_res =+ mk_sat_decs ::+ Options+ -> Int+ -> [DTyVarBndrSpec]+ -- ^ The invisible type variable binders to put in the type family+ -- head in order to give it the correct arity.+ -- See Note [Generating type families with the correct arity] in+ -- D.S.TH.Promote.+ -> [DTyVarBndrVis]+ -- ^ The visible kind arguments.+ -> Maybe DKind+ -- ^ The result kind (if known).+ -> [DDec]+ mk_sat_decs opts n sat_tvbs sat_args m_sat_res = let sat_name = defunctionalizedName opts name n sat_dec = DClosedTypeFamilyD- (DTypeFamilyHead sat_name sat_tvbs+ (DTypeFamilyHead sat_name+ (tvbSpecsToBndrVis sat_tvbs ++ sat_args) (maybeKindToResultSig m_sat_res) Nothing) [DTySynEqn Nothing- (foldTypeTvbs (DConT sat_name) sat_tvbs)- (foldTypeTvbs (DConT name) sat_tvbs)]+ (foldTypeTvbs (DConT sat_name) sat_args)+ (foldTypeTvbs (DConT name) sat_args)] sat_fixity_dec = maybeToList $ fmap (mk_fix_decl sat_name) m_fixity in sat_dec : sat_fixity_dec @@ -421,7 +443,7 @@ (noExactName <$> qNewName "e") mk_fix_decl :: Name -> Fixity -> DDec- mk_fix_decl n f = DLetDec $ DInfixD f n+ mk_fix_decl n f = DLetDec $ DInfixD f NoNamespaceSpecifier n -- Indicates whether the type being defunctionalized has a standalone kind -- signature. If it does, DefunSAK contains the kind. If not, DefunNoSAK
src/Data/Singletons/TH/Single.hs view
@@ -1003,6 +1003,7 @@ isException (DStaticE e) = isException e isException (DTypedBracketE e) = isException e isException (DTypedSpliceE e) = isException e+isException (DTypeE _) = False singMatch :: ADMatch -> SgM DMatch singMatch (ADMatch var_proms pat exp) = do
src/Data/Singletons/TH/Single/Defun.hs view
@@ -14,7 +14,6 @@ module Data.Singletons.TH.Single.Defun (singDefuns) where import Control.Monad-import Data.Foldable import Data.Singletons.TH.Names import Data.Singletons.TH.Options import Data.Singletons.TH.Promote.Defun
src/Data/Singletons/TH/Single/Fixity.hs view
@@ -34,7 +34,7 @@ -- See [singletons-th and fixity declarations], wrinkle 1. where finish :: Name -> q (Maybe DLetDec)- finish = pure . Just . DInfixD fixity+ finish = pure . Just . DInfixD fixity NoNamespaceSpecifier never_mind :: q (Maybe DLetDec) never_mind = pure Nothing
src/Data/Singletons/TH/Syntax.hs view
@@ -196,7 +196,7 @@ go acc (flattened ++ rest) go acc (DSigD name ty : rest) = go (typeBinding name ty <> acc) rest- go acc (DInfixD f n : rest) =+ go acc (DInfixD f _ n : rest) = go (infixDecl f n <> acc) rest go acc (DPragmaD{} : rest) = go acc rest
src/Data/Singletons/TH/Util.hs view
@@ -250,6 +250,30 @@ maybeSigT ty Nothing = ty maybeSigT ty (Just ki) = ty `DSigT` ki +-- | Convert a list of 'DTyVarBndrSpec's to a list of 'DTyVarBndrVis'es. Type+-- variable binders with a 'SpecifiedSpec' are converted to 'BndrInvis', and+-- type variable binders with an 'InferredSpec' are dropped entirely.+--+-- As an example, if you have this list of 'DTyVarBndrSpec's:+--+-- @+-- forall a {b} c {d e} f. <...>+-- @+--+-- The corresponding list of 'DTyVarBndrVis'es would be:+--+-- @+-- \@a \@b \@f+-- @+--+-- Note that note of @b@, @d@, or @e@ appear in the list.+tvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]+tvbSpecsToBndrVis = mapMaybe (traverse specificityToBndrVis)+ where+ specificityToBndrVis :: Specificity -> Maybe BndrVis+ specificityToBndrVis SpecifiedSpec = Just BndrInvis+ specificityToBndrVis InferredSpec = Nothing+ -- Reconstruct a vanilla function type from its individual type variable -- binders, constraints, argument types, and result type. (See -- Note [Vanilla-type validity checking during promotion] in