diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. 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.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). 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.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 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@ @@. . @@ -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 diff --git a/src/Data/Singletons/TH/Partition.hs b/src/Data/Singletons/TH/Partition.hs --- a/src/Data/Singletons/TH/Partition.hs +++ b/src/Data/Singletons/TH/Partition.hs @@ -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) 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 @@ -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 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 @@ -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 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 @@ -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 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 @@ -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 diff --git a/src/Data/Singletons/TH/Single/Fixity.hs b/src/Data/Singletons/TH/Single/Fixity.hs --- a/src/Data/Singletons/TH/Single/Fixity.hs +++ b/src/Data/Singletons/TH/Single/Fixity.hs @@ -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 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 @@ -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 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 @@ -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