diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,53 @@ `th-desugar` release notes ========================== +Version 1.11 [????.??.??] +------------------------- +* Support GHC 8.10. +* Add support for visible dependent quantification. As part of this change, + the way `th-desugar` represents `forall` and constraint types has been + overhauled: + * The existing `DForallT` constructor has been split into two smaller + constructors: + + ```diff + data DType + = ... + - | DForallT [DTyVarBndr] DCxt DType + + | DForallT ForallVisFlag [DTyVarBndr] DType + + | DConstrainedT DCxt DType + | ... + + +data ForallVisFlag + + = ForallVis + + | ForallInvis + ``` + + The previous design combined `forall`s and constraints into a single + constructor, while the new design puts them in distinct constructors + `DForallT` and `DConstrainedT`, respectively. The new `DForallT` + constructor also has a `ForallVisFlag` field to distinguish invisible + `forall`s (e.g., `forall a. a`) from visible `forall`s (e.g., + `forall a -> a`). + * The `unravel` function has been renamed to `unravelDType` and now returns + `(DFunArgs, DType)`, where `DFunArgs` is a data type that represents + the possible arguments in a function type (see the Haddocks for `DFunArgs` + for more details). There is also an `unravelDType` counterpart for `Type`s + named `unravelType`, complete with its own `FunArgs` data type. + + `{D}FunArgs` also have some supporting operations, including + `filter{D}VisFunArgs` (to obtain only the visible arguments) and + `ravel{D}Type` (to construct a function type using `{D}FunArgs` and + a return `{D}Type`). +* Support standalone kind signatures by adding a `DKiSigD` constructor to + `DDec`. +* Add `dsReifyType`, `reifyTypeWithLocals_maybe`, and `reifyTypeWithLocals`, + which allow looking up the types or kinds of locally declared entities. +* Fix a bug in which `reifyFixityWithLocals` would not look into local fixity + declarations inside of type classes. +* Fix a bug in which `reifyFixityWithLocals` would return incorrect results + for classes with associated type family defaults. + Version 1.10 ------------ * Support GHC 8.8. Drop support for GHC 7.6. diff --git a/Language/Haskell/TH/Desugar.hs b/Language/Haskell/TH/Desugar.hs --- a/Language/Haskell/TH/Desugar.hs +++ b/Language/Haskell/TH/Desugar.hs @@ -5,7 +5,8 @@ -} {-# LANGUAGE CPP, MultiParamTypeClasses, FunctionalDependencies, - TypeSynonymInstances, FlexibleInstances, LambdaCase #-} + TypeSynonymInstances, FlexibleInstances, LambdaCase, + ScopedTypeVariables #-} ----------------------------------------------------------------------------- -- | @@ -23,7 +24,8 @@ module Language.Haskell.TH.Desugar ( -- * Desugared data types - DExp(..), DLetDec(..), DPat(..), DType(..), DKind, DCxt, DPred, + DExp(..), DLetDec(..), DPat(..), + DType(..), ForallVisFlag(..), DKind, DCxt, DPred, DTyVarBndr(..), DMatch(..), DClause(..), DDec(..), DDerivClause(..), DDerivStrategy(..), DPatSynDir(..), DPatSynType, Overlap(..), PatSynArgs(..), NewOrData(..), @@ -65,10 +67,11 @@ -- * Reification reifyWithWarning, - -- | The following definitions allow you to register a list of - -- @Dec@s to be used in reification queries. - withLocalDeclarations, dsReify, + -- ** Local reification + -- $localReification + withLocalDeclarations, dsReify, dsReifyType, reifyWithLocals_maybe, reifyWithLocals, reifyFixityWithLocals, + reifyTypeWithLocals_maybe, reifyTypeWithLocals, lookupValueNameWithLocals, lookupTypeNameWithLocals, mkDataNameWithLocals, mkTypeNameWithLocals, reifyNameSpace, @@ -97,9 +100,15 @@ #if __GLASGOW_HASKELL__ >= 800 bindIP, #endif - unravel, conExistentialTvbs, mkExtraDKindBinders, + conExistentialTvbs, mkExtraDKindBinders, dTyVarBndrToDType, toposortTyVarsOf, + -- ** 'FunArgs' and 'VisFunArg' + FunArgs(..), VisFunArg(..), filterVisFunArgs, ravelType, unravelType, + + -- ** 'DFunArgs' and 'DVisFunArg' + DFunArgs(..), DVisFunArg(..), filterDVisFunArgs, ravelDType, unravelDType, + -- ** 'TypeArg' TypeArg(..), applyType, filterTANormals, unfoldType, @@ -130,6 +139,10 @@ import qualified Data.Set as S import Prelude hiding ( exp ) +#if __GLASGOW_HASKELL__ < 710 +import Control.Applicative +#endif + -- | This class relates a TH type with its th-desugar type and allows -- conversions back and forth. The functional dependency goes only one -- way because `Type` and `Kind` are type synonyms, but they desugar @@ -242,7 +255,7 @@ con_ex_tvbs <- conExistentialTvbs arg_ty con let con_univ_tvbs = deleteFirstsBy ((==) `on` dtvbName) con_tvbs con_ex_tvbs con_ex_tvb_set = OS.fromList $ map dtvbName con_ex_tvbs - forall' = DForallT con_univ_tvbs [] + forall' = DForallT ForallInvis con_univ_tvbs num_pats = length fields return $ concat [ [ DSigD name (forall' $ DArrowT `DAppT` con_ret_ty `DAppT` field_ty) @@ -332,8 +345,16 @@ -- are fresh type variable names. -- -- This expands kind synonyms if necessary. -mkExtraDKindBinders :: DsMonad q => DKind -> q [DTyVarBndr] -mkExtraDKindBinders = expandType >=> mkExtraDKindBinders' +mkExtraDKindBinders :: forall q. DsMonad q => DKind -> q [DTyVarBndr] +mkExtraDKindBinders k = do + k' <- expandType k + let (fun_args, _) = unravelDType k' + vis_fun_args = filterDVisFunArgs fun_args + mapM mk_tvb vis_fun_args + where + mk_tvb :: DVisFunArg -> q DTyVarBndr + mk_tvb (DVisFADep tvb) = return tvb + mk_tvb (DVisFAAnon ki) = DKindedTV <$> qNewName "a" <*> return ki -- | Returns all of a constructor's existentially quantified type variable -- binders. @@ -405,3 +426,60 @@ | tvb <- tvbs , M.notMember (dtvbName tvb) gadtSubt ] + +{- $localReification + +@template-haskell@ reification functions like 'reify' and 'qReify', as well as +@th-desugar@'s 'reifyWithWarning', only look through declarations that either +(1) have already been typechecked in the current module, or (2) are in scope +because of imports. We refer to this as /global/ reification. Sometimes, +however, you may wish to reify declarations that have been quoted but not +yet been typechecked, such as in the following example: + +@ +example :: IO () +example = putStrLn + $(do decs <- [d| data Foo = MkFoo |] + info <- 'reify' (mkName \"Foo\") + stringE $ pprint info) +@ + +Because @Foo@ only exists in a TH quote, it is not available globally. As a +result, the call to @'reify' (mkName \"Foo\")@ will fail. + +To make this sort of example possible, @th-desugar@ extends global reification +with /local/ reification. A function that performs local reification (such +as 'dsReify', 'reifyWithLocals', or similar functions that have a 'DsMonad' +context) looks through both typechecked (or imported) declarations /and/ quoted +declarations that are currently in scope. One can add quoted declarations in +the current scope by using the 'withLocalDeclarations' function. Here is an +example of how to repair the example above using 'withLocalDeclarations': + +@ +example2 :: IO () +example2 = putStrLn + $(do decs <- [d| data Foo = MkFoo |] + info <- 'withLocalDeclarations' decs $ + 'reifyWithLocals' (mkName \"Foo\") + stringE $ pprint info) +@ + +Note that 'withLocalDeclarations' should only be used to add quoted +declarations with names that are not duplicates of existing global or local +declarations. Adding duplicate declarations through 'withLocalDeclarations' +is undefined behavior and should be avoided. This is unlikely to happen if +you are only using 'withLocalDeclarations' in conjunction with TH quotes, +however. For instance, this is /not/ an example of duplicate declarations: + +@ +data T = MkT1 + +$(do decs <- [d| data T = MkT2 |] + info <- 'withLocalDeclarations' decs ... + ...) +@ + +The quoted @data T = MkT2@ does not conflict with the top-level @data T = Mk1@ +since declaring a data type within TH quotes gives it a fresh, unique name that +distinguishes it from any other data types already in scope. +-} diff --git a/Language/Haskell/TH/Desugar/AST.hs b/Language/Haskell/TH/Desugar/AST.hs --- a/Language/Haskell/TH/Desugar/AST.hs +++ b/Language/Haskell/TH/Desugar/AST.hs @@ -13,6 +13,7 @@ import Data.Data hiding (Fixity) import GHC.Generics hiding (Fixity) import Language.Haskell.TH +import Language.Haskell.TH.Desugar.Util (ForallVisFlag) -- | Corresponds to TH's @Exp@ type. Note that @DLamE@ takes names, not patterns. data DExp = DVarE Name @@ -40,7 +41,8 @@ -- | Corresponds to TH's @Type@ type, used to represent -- types and kinds. -data DType = DForallT [DTyVarBndr] DCxt DType +data DType = DForallT ForallVisFlag [DTyVarBndr] DType + | DConstrainedT DCxt DType | DAppT DType DType | DAppKindT DType DKind | DSigT DType DKind @@ -104,6 +106,9 @@ | DDefaultSigD Name DType | DPatSynD Name PatSynArgs DPatSynDir DPat | DPatSynSigD Name DPatSynType + | DKiSigD Name DKind + -- DKiSigD is part of DDec, not DLetDec, because standalone kind + -- signatures can only appear on the top level. deriving (Eq, Show, Typeable, Data, Generic) #if __GLASGOW_HASKELL__ < 711 diff --git a/Language/Haskell/TH/Desugar/Core.hs b/Language/Haskell/TH/Desugar/Core.hs --- a/Language/Haskell/TH/Desugar/Core.hs +++ b/Language/Haskell/TH/Desugar/Core.hs @@ -16,7 +16,6 @@ import Language.Haskell.TH hiding (match, clause, cxt) import Language.Haskell.TH.Syntax hiding (lift) -import Language.Haskell.TH.Datatype ( resolveTypeSynonyms ) #if __GLASGOW_HASKELL__ < 709 import Control.Applicative @@ -774,6 +773,9 @@ #if __GLASGOW_HASKELL__ >= 807 dsDec (ImplicitParamBindD {}) = impossible "Non-`let`-bound implicit param binding" #endif +#if __GLASGOW_HASKELL__ >= 809 +dsDec (KiSigD n ki) = (:[]) <$> (DKiSigD n <$> dsType ki) +#endif -- | Desugar a 'DataD' or 'NewtypeD'. dsDataDec :: DsMonad q @@ -817,17 +819,6 @@ <*> concatMapM (dsCon h98_tvbs h98_fam_inst_type) cons <*> mapM dsDerivClause derivings) --- Like mkExtraDKindBinders, but accepts a Maybe Kind --- argument instead of DKind. -mkExtraKindBinders :: DsMonad q => Maybe Kind -> q [DTyVarBndr] -mkExtraKindBinders = - maybe (pure (DConT typeKindName)) (runQ . resolveTypeSynonyms >=> dsType) - >=> mkExtraDKindBinders' - --- | Like mkExtraDKindBinders, but assumes kind synonyms have been expanded. -mkExtraDKindBinders' :: Quasi q => DKind -> q [DTyVarBndr] -mkExtraDKindBinders' = mkExtraKindBindersGeneric unravel DKindedTV - #if __GLASGOW_HASKELL__ > 710 -- | Desugar a @FamilyResultSig@ dsFamilyResultSig :: DsMonad q => FamilyResultSig -> q DFamilyResultSig @@ -1143,7 +1134,8 @@ -- | Desugar a type dsType :: DsMonad q => Type -> q DType -dsType (ForallT tvbs preds ty) = DForallT <$> mapM dsTvb tvbs <*> dsCxt preds <*> dsType ty +dsType (ForallT tvbs preds ty) = + mkDForallConstrainedT ForallInvis <$> mapM dsTvb tvbs <*> dsCxt preds <*> dsType ty dsType (AppT t1 t2) = DAppT <$> dsType t1 <*> dsType t2 dsType (SigT ty ki) = DSigT <$> dsType ty <*> dsType ki dsType (VarT name) = return $ DVarT name @@ -1181,6 +1173,9 @@ t' <- dsType t return $ DConT ''IP `DAppT` DLitT (StrTyLit n) `DAppT` t' #endif +#if __GLASGOW_HASKELL__ >= 809 +dsType (ForallVisT tvbs ty) = DForallT ForallVis <$> mapM dsTvb tvbs <*> dsType ty +#endif -- | Desugar a @TyVarBndr@ dsTvb :: DsMonad q => TyVarBndr -> q DTyVarBndr @@ -1245,12 +1240,7 @@ dsPred t | Just ts <- splitTuple_maybe t = concatMapM dsPred ts -dsPred (ForallT tvbs cxt p) = do - ps' <- dsPred p - case ps' of - [p'] -> (:[]) <$> (DForallT <$> mapM dsTvb tvbs <*> dsCxt cxt <*> pure p') - _ -> fail "Cannot desugar constraint tuples in the body of a quantified constraint" - -- See Trac #15334. +dsPred (ForallT tvbs cxt p) = dsForallPred tvbs cxt p dsPred (AppT t1 t2) = do [p1] <- dsPred t1 -- tuples can't be applied! (:[]) <$> DAppT p1 <$> dsType t2 @@ -1298,13 +1288,40 @@ t' <- dsType t return [DConT ''IP `DAppT` DLitT (StrTyLit n) `DAppT` t'] #endif +#if __GLASGOW_HASKELL__ >= 809 +dsPred t@(ForallVisT {}) = + impossible $ "Visible dependent quantifier seen as head of constraint: " ++ show t #endif +-- | Desugar a quantified constraint. +dsForallPred :: DsMonad q => [TyVarBndr] -> Cxt -> Pred -> q DCxt +dsForallPred tvbs cxt p = do + ps' <- dsPred p + case ps' of + [p'] -> (:[]) <$> (mkDForallConstrainedT ForallInvis + <$> mapM dsTvb tvbs <*> dsCxt cxt <*> pure p') + _ -> fail "Cannot desugar constraint tuples in the body of a quantified constraint" + -- See GHC #15334. +#endif + -- | Like 'reify', but safer and desugared. Uses local declarations where -- available. dsReify :: DsMonad q => Name -> q (Maybe DInfo) dsReify = traverse dsInfo <=< reifyWithLocals_maybe +-- | Like 'reifyType', but safer and desugared. Uses local declarations where +-- available. +dsReifyType :: DsMonad q => Name -> q (Maybe DType) +dsReifyType = traverse dsType <=< reifyTypeWithLocals_maybe + +-- Given a list of `forall`ed type variable binders and a context, construct +-- a DType using DForallT and DConstrainedT as appropriate. The phrase +-- "as appropriate" is used because DConstrainedT will not be used if the +-- context is empty, per Note [Desugaring and sweetening ForallT]. +mkDForallConstrainedT :: ForallVisFlag -> [DTyVarBndr] -> DCxt -> DType -> DType +mkDForallConstrainedT fvf tvbs ctxt ty = + DForallT fvf tvbs $ if null ctxt then ty else DConstrainedT ctxt ty + -- create a list of expressions in the same order as the fields in the first argument -- but with the values as given in the second argument -- if a field is missing from the second argument, use the corresponding expression @@ -1478,8 +1495,8 @@ varKindSigs = foldMap go_ty tys where go_ty :: DType -> Map Name DKind - go_ty (DForallT tvbs ctxt t) = - go_tvbs tvbs (foldMap go_ty ctxt `mappend` go_ty t) + go_ty (DForallT _ tvbs t) = go_tvbs tvbs (go_ty t) + go_ty (DConstrainedT ctxt t) = foldMap go_ty ctxt `mappend` go_ty t go_ty (DAppT t1 t2) = go_ty t1 `mappend` go_ty t2 go_ty (DAppKindT t k) = go_ty t `mappend` go_ty k go_ty (DSigT t k) = @@ -1575,17 +1592,68 @@ dtvbName (DPlainTV n) = n dtvbName (DKindedTV n _) = n --- | Decompose a function type into its type variables, its context, its --- argument types, and its result type. -unravel :: DType -> ([DTyVarBndr], [DPred], [DType], DType) -unravel (DForallT tvbs cxt ty) = - let (tvbs', cxt', tys, res) = unravel ty in - (tvbs ++ tvbs', cxt ++ cxt', tys, res) -unravel (DAppT (DAppT DArrowT t1) t2) = - let (tvbs, cxt, tys, res) = unravel t2 in - (tvbs, cxt, t1 : tys, res) -unravel t = ([], [], [], t) +-- | Reconstruct an arrow 'DType' from its argument and result types. +ravelDType :: DFunArgs -> DType -> DType +ravelDType DFANil res = res +ravelDType (DFAForalls fvf tvbs args) res = DForallT fvf tvbs (ravelDType args res) +ravelDType (DFACxt cxt args) res = DConstrainedT cxt (ravelDType args res) +ravelDType (DFAAnon t args) res = DAppT (DAppT DArrowT t) (ravelDType args res) +-- | Decompose a function 'DType' into its arguments (the 'DFunArgs') and its +-- result type (the 'DType). +unravelDType :: DType -> (DFunArgs, DType) +unravelDType (DForallT fvf tvbs ty) = + let (args, res) = unravelDType ty in + (DFAForalls fvf tvbs args, res) +unravelDType (DConstrainedT cxt ty) = + let (args, res) = unravelDType ty in + (DFACxt cxt args, res) +unravelDType (DAppT (DAppT DArrowT t1) t2) = + let (args, res) = unravelDType t2 in + (DFAAnon t1 args, res) +unravelDType t = (DFANil, t) + +-- | The list of arguments in a function 'DType'. +data DFunArgs + = DFANil + -- ^ No more arguments. + | DFAForalls ForallVisFlag [DTyVarBndr] DFunArgs + -- ^ A series of @forall@ed type variables followed by a dot (if + -- 'ForallInvis') or an arrow (if 'ForallVis'). For example, + -- the type variables @a1 ... an@ in @forall a1 ... an. r@. + | DFACxt DCxt DFunArgs + -- ^ A series of constraint arguments followed by @=>@. For example, + -- the @(c1, ..., cn)@ in @(c1, ..., cn) => r@. + | DFAAnon DType DFunArgs + -- ^ An anonymous argument followed by an arrow. For example, the @a@ + -- in @a -> r@. + deriving (Eq, Show, Typeable, Data, Generic) + +-- | A /visible/ function argument type (i.e., one that must be supplied +-- explicitly in the source code). This is in contrast to /invisible/ +-- arguments (e.g., the @c@ in @c => r@), which are instantiated without +-- the need for explicit user input. +data DVisFunArg + = DVisFADep DTyVarBndr + -- ^ A visible @forall@ (e.g., @forall a -> a@). + | DVisFAAnon DType + -- ^ An anonymous argument followed by an arrow (e.g., @a -> r@). + deriving (Eq, Show, Typeable, Data, Generic) + +-- | Filter the visible function arguments from a list of 'DFunArgs'. +filterDVisFunArgs :: DFunArgs -> [DVisFunArg] +filterDVisFunArgs DFANil = [] +filterDVisFunArgs (DFAForalls fvf tvbs args) = + case fvf of + ForallVis -> map DVisFADep tvbs ++ args' + ForallInvis -> args' + where + args' = filterDVisFunArgs args +filterDVisFunArgs (DFACxt _ args) = + filterDVisFunArgs args +filterDVisFunArgs (DFAAnon t args) = + DVisFAAnon t:filterDVisFunArgs args + -- | Decompose an applied type into its individual components. For example, this: -- -- @ @@ -1620,3 +1688,51 @@ -- version of 'undefined'.) unusedArgument :: a unusedArgument = error "Unused" + +{- +Note [Desugaring and sweetening ForallT] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The ForallT constructor from template-haskell is tremendously awkward. Because +ForallT contains both a list of type variable binders and constraint arguments, +ForallT expressions can be ambiguous when one of these lists is empty. For +example, consider this expression with no constraints: + + ForallT [PlainTV a] [] (VarT a) + +What should this desugar to in th-desugar, which must maintain a clear +separation between type variable binders and constraints? There are two +possibilities: + +1. DForallT DForallInvis [DPlainTV a] (DVarT a) + (i.e., forall a. a) +2. DForallT DForallInvis [DPlainTV a] (DConstrainedT [] (DVarT a)) + (i.e., forall a. () => a) + +Template Haskell generally drops these empty lists when splicing Template +Haskell expressions, so we would like to do the same in th-desugar to mimic +TH's behavior as closely as possible. However, there are some situations where +dropping empty lists of `forall`ed type variable binders can change the +semantics of a program. For instance, contrast `foo :: forall. a -> a` (which +is an error) with `foo :: a -> a` (which is fine). Therefore, we try to +preserve empty `forall`s to the best of our ability. + +Here is an informal specification of how th-desugar should handle different sorts +of ambiguity. First, a specification for desugaring. +Let `tvbs` and `ctxt` be non-empty: + +* `ForallT tvbs [] ty` should desugar to `DForallT DForallInvis tvbs ty`. +* `ForallT [] ctxt ty` should desguar to `DForallT DForallInvis [] (DConstrainedT ctxt ty)`. +* `ForallT [] [] ty` should desugar to `DForallT DForallInvis [] ty`. +* For all other cases, just straightforwardly desugar + `ForallT tvbs ctxt ty` to `DForallT DForallInvis tvbs (DConstraintedT ctxt ty)`. + +For sweetening: + +* `DForallT DForallInvis tvbs (DConstrainedT ctxt ty)` should sweeten to `ForallT tvbs ctxt ty`. +* `DForallT DForallInvis [] (DConstrainedT ctxt ty)` should sweeten to `ForallT [] ctxt ty`. +* `DForallT DForallInvis tvbs (DConstrainedT [] ty)` should sweeten to `ForallT tvbs [] ty`. +* `DForallT DForallInvis [] (DConstrainedT [] ty)` should sweeten to `ForallT [] [] ty`. +* For all other cases, just straightforwardly sweeten + `DForallT DForallInvis tvbs ty` to `ForallT tvbs [] ty` and + `DConstrainedT ctxt ty` to `ForallT [] ctxt ty`. +-} diff --git a/Language/Haskell/TH/Desugar/Expand.hs b/Language/Haskell/TH/Desugar/Expand.hs --- a/Language/Haskell/TH/Desugar/Expand.hs +++ b/Language/Haskell/TH/Desugar/Expand.hs @@ -59,12 +59,16 @@ expand_type ign = go [] where go :: [DTypeArg] -> DType -> q DType - go [] (DForallT tvbs cxt ty) = - DForallT <$> mapM (expand_tvb ign) tvbs - <*> mapM (expand_type ign) cxt - <*> expand_type ign ty + go [] (DForallT fvf tvbs ty) = + DForallT fvf <$> mapM (expand_tvb ign) tvbs + <*> expand_type ign ty go _ (DForallT {}) = impossible "A forall type is applied to another type." + go [] (DConstrainedT cxt ty) = + DConstrainedT <$> mapM (expand_type ign) cxt + <*> expand_type ign ty + go _ (DConstrainedT {}) = + impossible "A constrained type is applied to another type." go args (DAppT t1 t2) = do t2' <- expand_type ign t2 go (DTANormal t2' : args) t1 @@ -193,17 +197,16 @@ _ -> True -- Recursive cases - go_ty (DForallT tvbs ctxt ty) = - liftM3 (\x y z -> x && y && z) - (allM go_tvb tvbs) (allM go_ty ctxt) (go_ty ty) - go_ty (DAppT t1 t2) = liftM2 (&&) (go_ty t1) (go_ty t2) - go_ty (DAppKindT t k) = liftM2 (&&) (go_ty t) (go_ty k) - go_ty (DSigT t k) = liftM2 (&&) (go_ty t) (go_ty k) + go_ty (DForallT _ tvbs ty) = liftM2 (&&) (allM go_tvb tvbs) (go_ty ty) + go_ty (DConstrainedT ctxt ty) = liftM2 (&&) (allM go_ty ctxt) (go_ty ty) + go_ty (DAppT t1 t2) = liftM2 (&&) (go_ty t1) (go_ty t2) + go_ty (DAppKindT t k) = liftM2 (&&) (go_ty t) (go_ty k) + go_ty (DSigT t k) = liftM2 (&&) (go_ty t) (go_ty k) -- Default to True - go_ty DLitT{} = return True - go_ty DArrowT = return True - go_ty DWildCardT = return True + go_ty DLitT{} = return True + go_ty DArrowT = return True + go_ty DWildCardT = return True -- These cases are uninteresting go_tvb :: DTyVarBndr -> q Bool diff --git a/Language/Haskell/TH/Desugar/FV.hs b/Language/Haskell/TH/Desugar/FV.hs --- a/Language/Haskell/TH/Desugar/FV.hs +++ b/Language/Haskell/TH/Desugar/FV.hs @@ -27,7 +27,8 @@ fvDType = go where go :: DType -> OSet Name - go (DForallT tvbs ctxt ty) = fv_dtvbs tvbs (foldMap fvDType ctxt <> go ty) + go (DForallT _ tvbs ty) = fv_dtvbs tvbs (go ty) + go (DConstrainedT ctxt ty) = foldMap fvDType ctxt <> go ty go (DAppT t1 t2) = go t1 <> go t2 go (DAppKindT t k) = go t <> go k go (DSigT ty ki) = go ty <> go ki diff --git a/Language/Haskell/TH/Desugar/Lift.hs b/Language/Haskell/TH/Desugar/Lift.hs --- a/Language/Haskell/TH/Desugar/Lift.hs +++ b/Language/Haskell/TH/Desugar/Lift.hs @@ -23,7 +23,7 @@ import Language.Haskell.TH.Instances () import Language.Haskell.TH.Lift -$(deriveLiftMany [ ''DExp, ''DPat, ''DType, ''DTyVarBndr +$(deriveLiftMany [ ''DExp, ''DPat, ''DType, ''ForallVisFlag, ''DTyVarBndr , ''DMatch, ''DClause, ''DLetDec, ''DDec, ''DDerivClause, ''DCon , ''DConFields, ''DForeign, ''DPragma, ''DRuleBndr, ''DTySynEqn , ''DPatSynDir , ''NewOrData, ''DDerivStrategy @@ -36,5 +36,7 @@ , ''PatSynArgs #endif - , ''TypeArg, ''DTypeArg + , ''TypeArg, ''DTypeArg + , ''FunArgs, ''DFunArgs + , ''VisFunArg, ''DVisFunArg ]) diff --git a/Language/Haskell/TH/Desugar/Match.hs b/Language/Haskell/TH/Desugar/Match.hs --- a/Language/Haskell/TH/Desugar/Match.hs +++ b/Language/Haskell/TH/Desugar/Match.hs @@ -347,7 +347,10 @@ where match_group :: DsMonad q => [EquationInfo] -> q (Lit, MatchResult) match_group eqns - = do let DLitP lit = firstPat (head eqns) + = do let lit = case firstPat (head eqns) of + DLitP lit' -> lit' + _ -> error $ "Internal error in th-desugar " + ++ "(matchLiterals.match_group)" match_result <- simplCase vars (shiftEqns eqns) return (lit, match_result) matchLiterals [] _ = error "Internal error in th-desugar (matchLiterals)" diff --git a/Language/Haskell/TH/Desugar/Reify.hs b/Language/Haskell/TH/Desugar/Reify.hs --- a/Language/Haskell/TH/Desugar/Reify.hs +++ b/Language/Haskell/TH/Desugar/Reify.hs @@ -7,7 +7,7 @@ up in the environment. -} -{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-} +{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, ScopedTypeVariables #-} module Language.Haskell.TH.Desugar.Reify ( -- * Reification @@ -16,6 +16,10 @@ -- ** Fixity reification qReifyFixity, reifyFixity, reifyFixityWithLocals, reifyFixityInDecs, + -- ** Type reification + qReifyType, reifyType, + reifyTypeWithLocals_maybe, reifyTypeWithLocals, reifyTypeInDecs, + -- * Datatype lookup getDataD, dataConNameToCon, dataConNameToDataName, @@ -28,6 +32,7 @@ DsMonad(..), DsM, withLocalDeclarations ) where +import Control.Applicative import qualified Control.Monad.Fail as Fail import Control.Monad.Reader import Control.Monad.State @@ -35,12 +40,16 @@ import Control.Monad.RWS import Control.Monad.Trans.Instances () import qualified Data.Foldable as F +#if __GLASGOW_HASKELL__ < 710 +import Data.Foldable (foldMap) +#endif import Data.Function (on) import Data.List +import qualified Data.Map as Map +import Data.Map (Map) import Data.Maybe -#if __GLASGOW_HASKELL__ < 709 -import Control.Applicative -#endif +import qualified Data.Set as Set +import Data.Set (Set) import Language.Haskell.TH.Datatype import Language.Haskell.TH.Instances () @@ -107,8 +116,8 @@ _ -> badDeclaration where go tvbs mk cons = do - k <- maybe (pure (ConT typeKindName)) (runQ . resolveTypeSynonyms) mk - extra_tvbs <- mkExtraKindBindersGeneric unravelType KindedTV k + let k = fromMaybe (ConT typeKindName) mk + extra_tvbs <- mkExtraKindBinders k let all_tvbs = tvbs ++ extra_tvbs return (all_tvbs, cons) @@ -116,6 +125,31 @@ fail $ "The name (" ++ (show name) ++ ") refers to something " ++ "other than a datatype. " ++ err +-- | Create new kind variable binder names corresponding to the return kind of +-- a data type. This is useful when you have a data type like: +-- +-- @ +-- data Foo :: forall k. k -> Type -> Type where ... +-- @ +-- +-- But you want to be able to refer to the type @Foo a b@. +-- 'mkExtraKindBinders' will take the kind @forall k. k -> Type -> Type@, +-- discover that is has two visible argument kinds, and return as a result +-- two new kind variable binders @[a :: k, b :: Type]@, where @a@ and @b@ +-- are fresh type variable names. +-- +-- This expands kind synonyms if necessary. +mkExtraKindBinders :: forall q. Quasi q => Kind -> q [TyVarBndr] +mkExtraKindBinders k = do + k' <- runQ $ resolveTypeSynonyms k + let (fun_args, _) = unravelType k' + vis_fun_args = filterVisFunArgs fun_args + mapM mk_tvb vis_fun_args + where + mk_tvb :: VisFunArg -> q TyVarBndr + mk_tvb (VisFADep tvb) = return tvb + mk_tvb (VisFAAnon ki) = KindedTV <$> qNewName "a" <*> return ki + -- | From the name of a data constructor, retrive the datatype definition it -- is a part of. dataConNameToDataName :: DsMonad q => Name -> q Name @@ -210,8 +244,10 @@ reifyFixityInDecs :: Name -> [Dec] -> Maybe Fixity reifyFixityInDecs n = firstMatch match_fixity where - match_fixity (InfixD fixity n') | n `nameMatches` n' = Just fixity - match_fixity _ = Nothing + match_fixity (InfixD fixity n') | n `nameMatches` n' + = Just fixity + match_fixity (ClassD _ _ _ _ sub_decs) = firstMatch match_fixity sub_decs + match_fixity _ = Nothing -- | A reified thing along with the name of that thing. type Named a = (Name, a) @@ -279,7 +315,10 @@ reifyFixityInDecs n $ sub_decs ++ decs)) #endif reifyInDec n decs (ClassD _ _ _ _ sub_decs) - | Just info <- firstMatch (reifyInDec n (sub_decs ++ decs)) sub_decs + | Just info <- firstMatch (reifyInDec n decs) sub_decs + -- Important: don't pass (sub_decs ++ decs) to reifyInDec + -- above, or else type family defaults can be confused for + -- actual instances. See #134. = Just info #if __GLASGOW_HASKELL__ >= 711 reifyInDec n decs (InstanceD _ _ _ sub_decs) @@ -320,51 +359,83 @@ reifyInDec _ _ _ = Nothing maybeReifyCon :: Name -> [Dec] -> Name -> [TypeArg] -> [Con] -> Maybe (Named Info) -#if __GLASGOW_HASKELL__ > 710 maybeReifyCon n _decs ty_name ty_args cons | Just (n', con) <- findCon n cons - = Just (n', DataConI n (maybeForallT tvbs [] $ con_to_type con) ty_name) -#else -maybeReifyCon n decs ty_name ty_args cons - | Just (n', con) <- findCon n cons - = Just (n', DataConI n (maybeForallT tvbs [] $ con_to_type con) - ty_name fixity) + -- See Note [Use unSigType in maybeReifyCon] + , let full_con_ty = unSigType $ con_to_type h98_tvbs h98_res_ty con + = Just ( n', DataConI n full_con_ty ty_name +#if __GLASGOW_HASKELL__ < 800 + fixity #endif + ) - | Just (n', ty) <- findRecSelector n cons + | Just (n', rec_sel_info) <- findRecSelector n cons + , let (tvbs, sel_ty, con_res_ty) = extract_rec_sel_info rec_sel_info + -- See Note [Use unSigType in maybeReifyCon] + full_sel_ty = unSigType $ maybeForallT tvbs [] $ mkArrows [con_res_ty] sel_ty -- we don't try to ferret out naughty record selectors. -#if __GLASGOW_HASKELL__ > 710 - = Just (n', VarI n (maybeForallT tvbs [] $ mkArrows [result_ty] ty) Nothing) -#else - = Just (n', VarI n (maybeForallT tvbs [] $ mkArrows [result_ty] ty) Nothing fixity) + = Just ( n', VarI n full_sel_ty Nothing +#if __GLASGOW_HASKELL__ < 800 + fixity #endif + ) where - result_ty = applyType (ConT ty_name) (map unSigTypeArg ty_args) - -- Make sure to call unSigTypeArg here. Otherwise, if you have this: - -- - -- data D (a :: k) = MkD { unD :: Proxy a } - -- - -- Then the type of unD will be reified as: - -- - -- unD :: forall k (a :: k). D (a :: k) -> Proxy a - -- - -- This is contrast to GHC's own reification, which will produce `D a` - -- (without the explicit kind signature) as the type of the first argument. + extract_rec_sel_info :: RecSelInfo -> ([TyVarBndr], Type, Type) + -- Returns ( Selector type variable binders + -- , Record field type + -- , constructor result type ) + extract_rec_sel_info rec_sel_info = + case rec_sel_info of + RecSelH98 sel_ty -> (h98_tvbs, sel_ty, h98_res_ty) + RecSelGADT sel_ty con_res_ty -> + ( freeVariablesWellScoped [con_res_ty, sel_ty] + , sel_ty, con_res_ty) - con_to_type (NormalC _ stys) = mkArrows (map snd stys) result_ty - con_to_type (RecC _ vstys) = mkArrows (map thdOf3 vstys) result_ty - con_to_type (InfixC t1 _ t2) = mkArrows (map snd [t1, t2]) result_ty - con_to_type (ForallC bndrs cxt c) = ForallT bndrs cxt (con_to_type c) -#if __GLASGOW_HASKELL__ > 710 - con_to_type (GadtC _ stys rty) = mkArrows (map snd stys) rty - con_to_type (RecGadtC _ vstys rty) = mkArrows (map thdOf3 vstys) rty -#endif -#if __GLASGOW_HASKELL__ < 711 - fixity = fromMaybe defaultFixity $ reifyFixityInDecs n decs + h98_tvbs = freeVariablesWellScoped $ map probablyWrongUnTypeArg ty_args + h98_res_ty = applyType (ConT ty_name) ty_args + +#if __GLASGOW_HASKELL__ < 800 + fixity = fromMaybe defaultFixity $ reifyFixityInDecs n _decs #endif - tvbs = freeVariablesWellScoped $ map probablyWrongUnTypeArg ty_args maybeReifyCon _ _ _ _ _ = Nothing +{- +Note [Use unSigType in maybeReifyCon] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Make sure to call unSigType on the type of a reified data constructor or +record selector. Otherwise, if you have this: + + data D (a :: k) = MkD { unD :: Proxy a } + +Then the type of unD will be reified as: + + unD :: forall k (a :: k). D (a :: k) -> Proxy a + +This is contrast to GHC's own reification, which will produce `D a` +(without the explicit kind signature) as the type of the first argument. +-} + +-- Reverse-engineer the type of a data constructor. +con_to_type :: [TyVarBndr] -- The type variables bound by a data type head. + -- Only used for Haskell98-style constructors. + -> Type -- The constructor result type. + -- Only used for Haskell98-style constructors. + -> Con -> Type +con_to_type h98_tvbs h98_result_ty con = + case go con of + (is_gadt, ty) | is_gadt -> ty + | otherwise -> maybeForallT h98_tvbs [] ty + where + go :: Con -> (Bool, Type) -- The Bool is True when dealing with a GADT + go (NormalC _ stys) = (False, mkArrows (map snd stys) h98_result_ty) + go (RecC _ vstys) = (False, mkArrows (map thdOf3 vstys) h98_result_ty) + go (InfixC t1 _ t2) = (False, mkArrows (map snd [t1, t2]) h98_result_ty) + go (ForallC bndrs cxt c) = liftSnd (ForallT bndrs cxt) (go c) +#if __GLASGOW_HASKELL__ > 710 + go (GadtC _ stys rty) = (True, mkArrows (map snd stys) rty) + go (RecGadtC _ vstys rty) = (True, mkArrows (map thdOf3 vstys) rty) +#endif + mkVarI :: Name -> [Dec] -> Info mkVarI n decs = mkVarITy n decs (maybe (no_type n) snd $ findType n decs) @@ -531,6 +602,7 @@ go (SigD n ty) = Just $ SigD n $ quantifyClassMethodType cls_name cls_tvbs prepend_cls ty + go d@(TySynInstD {}) = Just d #if __GLASGOW_HASKELL__ > 710 go d@(OpenTypeFamilyD {}) = Just d go d@(DataFamilyD {}) = Just d @@ -645,18 +717,27 @@ Nothing -> Nothing #endif -findRecSelector :: Name -> [Con] -> Maybe (Named Type) +data RecSelInfo + = RecSelH98 Type -- The record field's type + | RecSelGADT Type -- The record field's type + Type -- The GADT return type + +findRecSelector :: Name -> [Con] -> Maybe (Named RecSelInfo) findRecSelector n = firstMatch match_con where - match_con (RecC _ vstys) = firstMatch match_rec_sel vstys + match_con :: Con -> Maybe (Named RecSelInfo) + match_con (RecC _ vstys) = fmap (liftSnd RecSelH98) $ + firstMatch match_rec_sel vstys #if __GLASGOW_HASKELL__ >= 800 - match_con (RecGadtC _ vstys _) = firstMatch match_rec_sel vstys + match_con (RecGadtC _ vstys ret_ty) = fmap (liftSnd (`RecSelGADT` ret_ty)) $ + firstMatch match_rec_sel vstys #endif - match_con (ForallC _ _ c) = match_con c - match_con _ = Nothing + match_con (ForallC _ _ c) = match_con c + match_con _ = Nothing - match_rec_sel (n', _, ty) | n `nameMatches` n' = Just (n', ty) - match_rec_sel _ = Nothing + match_rec_sel (n', _, sel_ty) + | n `nameMatches` n' = Just (n', sel_ty) + match_rec_sel _ = Nothing --------------------------------- -- Reifying fixities @@ -684,8 +765,8 @@ reifyFixity = qReifyFixity #endif --- | Like 'reifyWithLocals_maybe', but for fixities. Note that a return of --- @Nothing@ might mean that the name is not in scope, or it might mean +-- | Like 'reifyWithLocals_maybe', but for fixities. Note that a return value +-- of @Nothing@ might mean that the name is not in scope, or it might mean -- that the name has no assigned fixity. (Use 'reifyWithLocals_maybe' if -- you really need to tell the difference.) reifyFixityWithLocals :: DsMonad q => Name -> q (Maybe Fixity) @@ -694,7 +775,360 @@ (qReifyFixity name) -------------------------------------- --- Lookuping name value and type names +-- Reifying types +-------------------------------------- +-- +-- This section allows GHC <8.9 to call reifyFixity + +#if __GLASGOW_HASKELL__ < 809 +qReifyType :: forall m. Quasi m => Name -> m Type +qReifyType name = do + info <- qReify name + case infoType info <|> info_kind info of + Just t -> return t + Nothing -> fail $ "Could not reify the full type of " ++ nameBase name + where + info_kind :: Info -> Maybe Kind + info_kind info = do + dec <- case info of + ClassI d _ -> Just d + TyConI d -> Just d + FamilyI d _ -> Just d + _ -> Nothing + match_cusk name dec + +{- | @reifyType nm@ attempts to find the type or kind of @nm@. For example, +@reifyType 'not@ returns @Bool -> Bool@, and +@reifyType ''Bool@ returns @Type@. +This works even if there's no explicit signature and the type or kind is inferred. +-} +reifyType :: Name -> Q Type +reifyType = qReifyType +#endif + +-- | Like 'reifyTypeWithLocals_maybe', but throws an exception upon failure, +-- warning the user about separating splices. +reifyTypeWithLocals :: DsMonad q => Name -> q Type +reifyTypeWithLocals name = do + m_info <- reifyTypeWithLocals_maybe name + case m_info of + Nothing -> reifyFail name + Just i -> return i + +-- | Like 'reifyWithLocals_maybe' but for types and kinds. Note that a return +-- value of @Nothing@ might mean that the name is not in scope, or it might +-- mean that the full type of the name cannot be determined. (Use +-- 'reifyWithLocals_maybe' if you really need to tell the difference.) +reifyTypeWithLocals_maybe :: DsMonad q => Name -> q (Maybe Type) +reifyTypeWithLocals_maybe name = do +#if __GLASGOW_HASKELL__ >= 809 + cusks <- qIsExtEnabled CUSKs +#else + -- On earlier GHCs, the behavior of -XCUSKs was the norm. + let cusks = True +#endif + qRecover (return . reifyTypeInDecs cusks name =<< localDeclarations) + (Just `fmap` qReifyType name) + +-- | Look through a list of declarations and return its full type, if +-- available. +reifyTypeInDecs :: Bool -> Name -> [Dec] -> Maybe Type +reifyTypeInDecs cusks name decs = + (reifyInDecs name decs >>= infoType) <|> findKind cusks name decs + +-- Extract the type information (if any) contained in an Info. +infoType :: Info -> Maybe Type +infoType info = + case info of + ClassOpI _ t _ +#if __GLASGOW_HASKELL__ < 800 + _ +#endif + -> Just t + DataConI _ t _ +#if __GLASGOW_HASKELL__ < 800 + _ +#endif + -> Just t + VarI _ t _ +#if __GLASGOW_HASKELL__ < 800 + _ +#endif + -> Just t + TyVarI _ t -> Just t +#if __GLASGOW_HASKELL__ >= 802 + PatSynI _ t -> Just t +#endif + _ -> Nothing + +-- Like findType, but instead searching for kind signatures. +-- This mostly searches through `KiSigD`s, but if the -XCUSKs extension is +-- enabled, this also retrieves kinds for declarations with CUSKs. +findKind :: Bool -- Is -XCUSKs enabled? + -> Name -> [Dec] -> Maybe Kind +findKind cusks name decls = + firstMatch (match_kind_sig name decls) decls + <|> whenAlt cusks (firstMatch (match_cusk name) decls) + +-- Look for a declaration's kind by searching for its standalone kind +-- signature, if available. +match_kind_sig :: Name -> [Dec] -> Dec -> Maybe Kind +match_kind_sig n decs (ClassD _ n' tvbs _ sub_decs) + -- If a class has a standalone kind signature, then we can determine the + -- full kind of its associated types in 99% of cases. + -- See Note [The limitations of standalone kind signatures] for what + -- happens in the other 1% of cases. + | Just ki <- firstMatch (find_kind_sig n') decs + , let (arg_kis, _res_ki) = unravelType ki + mb_vis_arg_kis = map vis_arg_kind_maybe $ filterVisFunArgs arg_kis + cls_tvb_kind_map = + Map.fromList [ (tvName tvb, tvb_kind) + | (tvb, mb_vis_arg_ki) <- zip tvbs mb_vis_arg_kis + , Just tvb_kind <- [mb_vis_arg_ki <|> tvb_kind_maybe tvb] + ] + = firstMatch (find_assoc_type_kind n cls_tvb_kind_map) sub_decs +match_kind_sig n _ dec = find_kind_sig n dec + +find_kind_sig :: Name -> Dec -> Maybe Kind +#if __GLASGOW_HASKELL__ >= 809 +find_kind_sig n (KiSigD n' ki) + | n `nameMatches` n' = Just ki +#endif +find_kind_sig _ _ = Nothing + +-- Compute a declaration's kind by retrieving its CUSK, if it has one. +-- This is only done when -XCUSKs is enabled, or on older GHCs where +-- CUSKs were the only means of specifying this information. +match_cusk :: Name -> Dec -> Maybe Kind +#if __GLASGOW_HASKELL__ >= 800 +match_cusk n (DataD _ n' tvbs m_ki _ _) + | n `nameMatches` n' + = datatype_kind tvbs m_ki +match_cusk n (NewtypeD _ n' tvbs m_ki _ _) + | n `nameMatches` n' + = datatype_kind tvbs m_ki +match_cusk n (DataFamilyD n' tvbs m_ki) + | n `nameMatches` n' + = open_ty_fam_kind tvbs m_ki +match_cusk n (OpenTypeFamilyD (TypeFamilyHead n' tvbs res_sig _)) + | n `nameMatches` n' + = open_ty_fam_kind tvbs (res_sig_to_kind res_sig) +match_cusk n (ClosedTypeFamilyD (TypeFamilyHead n' tvbs res_sig _) _) + | n `nameMatches` n' + = closed_ty_fam_kind tvbs (res_sig_to_kind res_sig) +#else +match_cusk n (DataD _ n' tvbs _ _) + | n `nameMatches` n' + = datatype_kind tvbs Nothing +match_cusk n (NewtypeD _ n' tvbs _ _) + | n `nameMatches` n' + = datatype_kind tvbs Nothing +match_cusk n (FamilyD _ n' tvbs m_ki) + | n `nameMatches` n' + = open_ty_fam_kind tvbs m_ki +match_cusk n (ClosedTypeFamilyD n' tvbs m_ki _) + | n `nameMatches` n' + = closed_ty_fam_kind tvbs m_ki +#endif +match_cusk n (TySynD n' tvbs rhs) + | n `nameMatches` n' + = ty_syn_kind tvbs rhs +match_cusk n (ClassD _ n' tvbs _ sub_decs) + | n `nameMatches` n' + = class_kind tvbs + | -- An associated type family can only have a CUSK if its parent class + -- also has a CUSK. + all tvb_is_kinded tvbs + , let cls_tvb_kind_map = Map.fromList [ (tvName tvb, tvb_kind) + | tvb <- tvbs + , Just tvb_kind <- [tvb_kind_maybe tvb] + ] + = firstMatch (find_assoc_type_kind n cls_tvb_kind_map) sub_decs +match_cusk _ _ = Nothing + +-- Uncover the kind of an associated type family. There is an invariant +-- that this function should only ever be called when the kind of the +-- parent class is known (i.e., if it has a standalone kind signature or a +-- CUSK). Despite this, it is possible for this function to return Nothing. +-- See Note [The limitations of standalone kind signatures]. +find_assoc_type_kind :: Name -> Map Name Kind -> Dec -> Maybe Kind +find_assoc_type_kind n cls_tvb_kind_map sub_dec = + case sub_dec of +#if __GLASGOW_HASKELL__ >= 800 + DataFamilyD n' tf_tvbs m_ki + | n `nameMatches` n' + -> build_kind (map ascribe_tf_tvb_kind tf_tvbs) (default_res_ki m_ki) + OpenTypeFamilyD (TypeFamilyHead n' tf_tvbs res_sig _) + | n `nameMatches` n' + -> build_kind (map ascribe_tf_tvb_kind tf_tvbs) + (default_res_ki $ res_sig_to_kind res_sig) +#else + FamilyD _ n' tf_tvbs m_ki + | n `nameMatches` n' + -> build_kind (map ascribe_tf_tvb_kind tf_tvbs) (default_res_ki m_ki) +#endif + _ -> Nothing + where + ascribe_tf_tvb_kind :: TyVarBndr -> TyVarBndr + ascribe_tf_tvb_kind tvb = + case tvb of + KindedTV{} -> tvb + PlainTV tvn -> KindedTV tvn $ fromMaybe StarT $ Map.lookup tvn cls_tvb_kind_map + +-- Data types have CUSKs when: +-- +-- 1. All of their type variables have explicit kinds. +-- 2. All kind variables in the result kind are explicitly quantified. +datatype_kind :: [TyVarBndr] -> Maybe Kind -> Maybe Kind +datatype_kind tvbs m_ki = + whenAlt (all tvb_is_kinded tvbs && ki_fvs_are_bound) $ + build_kind tvbs (default_res_ki m_ki) + where + ki_fvs_are_bound :: Bool + ki_fvs_are_bound = + let ki_fvs = Set.fromList $ foldMap freeVariables m_ki + tvb_vars = Set.fromList $ freeVariables $ map tvbToTypeWithSig tvbs + in ki_fvs `Set.isSubsetOf` tvb_vars + +-- Classes have CUSKs when all of their type variables have explicit kinds. +class_kind :: [TyVarBndr] -> Maybe Kind +class_kind tvbs = whenAlt (all tvb_is_kinded tvbs) $ + build_kind tvbs ConstraintT + +-- Open type families and data families always have CUSKs. Type variables +-- without explicit kinds default to Type, as does the return kind if it +-- is not specified. +open_ty_fam_kind :: [TyVarBndr] -> Maybe Kind -> Maybe Kind +open_ty_fam_kind tvbs m_ki = + build_kind (map default_tvb tvbs) (default_res_ki m_ki) + +-- Closed type families have CUSKs when: +-- +-- 1. All of their type variables have explicit kinds. +-- 2. An explicit return kind is supplied. +closed_ty_fam_kind :: [TyVarBndr] -> Maybe Kind -> Maybe Kind +closed_ty_fam_kind tvbs m_ki = + case m_ki of + Just ki -> whenAlt (all tvb_is_kinded tvbs) $ + build_kind tvbs ki + Nothing -> Nothing + +-- Type synonyms have CUSKs when: +-- +-- 1. All of their type variables have explicit kinds. +-- 2. The right-hand-side type is annotated with an explicit kind. +ty_syn_kind :: [TyVarBndr] -> Type -> Maybe Kind +ty_syn_kind tvbs rhs = + case rhs of + SigT _ ki -> whenAlt (all tvb_is_kinded tvbs) $ + build_kind tvbs ki + _ -> Nothing + +-- Attempt to construct the full kind of a type-level declaration from its +-- type variable binders and return kind. Do note that the result type of +-- this function is `Maybe Kind` because there are situations where even +-- this amount of information is not sufficient to determine the full kind. +-- See Note [The limitations of standalone kind signatures]. +build_kind :: [TyVarBndr] -> Kind -> Maybe Kind +build_kind arg_kinds res_kind = + fmap quantifyType $ fst $ + foldr go (Just res_kind, Set.fromList (freeVariables res_kind)) arg_kinds + where + go :: TyVarBndr -> (Maybe Kind, Set Name) -> (Maybe Kind, Set Name) + go tvb (res, res_fvs) = + case tvb of + PlainTV n + -> ( if n `Set.member` res_fvs + then forall_vis tvb res + else Nothing -- We have a type variable binder without an + -- explicit kind that is not used dependently, so + -- we cannot build a kind from it. This is the + -- only case where we return Nothing. + , res_fvs + ) + KindedTV n k + -> ( if n `Set.member` res_fvs + then forall_vis tvb res + else fmap (ArrowT `AppT` k `AppT`) res + , Set.fromList (freeVariables k) `Set.union` res_fvs + ) + + forall_vis :: TyVarBndr -> Maybe Kind -> Maybe Kind +#if __GLASGOW_HASKELL__ >= 809 + forall_vis tvb m_ki = fmap (ForallVisT [tvb]) m_ki + -- One downside of this approach is that we generate kinds like this: + -- + -- forall a -> forall b -> forall c -> (a, b, c) + -- + -- Instead of this more compact kind: + -- + -- forall a b c -> (a, b, c) + -- + -- Thankfully, the difference is only cosmetic. +#else + forall_vis _ _ = Nothing +#endif + +tvb_is_kinded :: TyVarBndr -> Bool +tvb_is_kinded = isJust . tvb_kind_maybe + +tvb_kind_maybe :: TyVarBndr -> Maybe Kind +tvb_kind_maybe PlainTV{} = Nothing +tvb_kind_maybe (KindedTV _ k) = Just k + +vis_arg_kind_maybe :: VisFunArg -> Maybe Kind +vis_arg_kind_maybe (VisFADep tvb) = tvb_kind_maybe tvb +vis_arg_kind_maybe (VisFAAnon k) = Just k + +default_tvb :: TyVarBndr -> TyVarBndr +default_tvb (PlainTV n) = KindedTV n StarT +default_tvb tvb@KindedTV{} = tvb + +default_res_ki :: Maybe Kind -> Kind +default_res_ki = fromMaybe StarT + +#if __GLASGOW_HASKELL__ >= 800 +res_sig_to_kind :: FamilyResultSig -> Maybe Kind +res_sig_to_kind NoSig = Nothing +res_sig_to_kind (KindSig k) = Just k +res_sig_to_kind (TyVarSig tvb) = tvb_kind_maybe tvb +#endif + +whenAlt :: Alternative f => Bool -> f a -> f a +whenAlt b fa = if b then fa else empty + +{- +Note [The limitations of standalone kind signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A current limitation of StandaloneKindSignatures is that they cannot be applied +to associated type families. This can have some surprising consequences. +Consider the following code, taken from +https://gitlab.haskell.org/ghc/ghc/issues/17072#note_221324: + + type C :: forall a -> a -> Constraint + class C a b where + type T a :: Type + +The parent class C has a standalone kind signature, so GHC treats its +associated types as if they had CUSKs. Can th-desugar figure out the kind +that GHC gives to T? + +Unfortunately, the answer is "not easily". This is because `type T a` says +nothing about the kind of `a`, so th-desugar's only other option is to inspect +the kind signature for C. Even this is for naught, as the `forall a -> ...` +part doesn't state the kind of `a` either! The only way to know that the kind +of `a` should be Type is to infer that from the rest of the kind +(`a -> Constraint`), but this gets perilously close to requiring full kind +inference, which is rather unwieldy in Template Haskell. + +In cases like T, we simply give up and return Nothing when trying to reify +its kind. It's not ideal, but them's the breaks when you try to extract kinds +from syntax. There is a rather simple workaround available: just write +`type C :: forall (a :: Type) -> a -> Constraint` instead. +-} + +-------------------------------------- +-- Looking up name value and type names -------------------------------------- -- | Like 'lookupValueName' from Template Haskell, but looks also in 'Names' of diff --git a/Language/Haskell/TH/Desugar/Subst.hs b/Language/Haskell/TH/Desugar/Subst.hs --- a/Language/Haskell/TH/Desugar/Subst.hs +++ b/Language/Haskell/TH/Desugar/Subst.hs @@ -40,11 +40,12 @@ -- | Capture-avoiding substitution on types substTy :: Quasi q => DSubst -> DType -> q DType -substTy vars (DForallT tvbs cxt ty) = +substTy vars (DForallT fvf tvbs ty) = substTyVarBndrs vars tvbs $ \vars' tvbs' -> do - cxt' <- mapM (substTy vars') cxt ty' <- substTy vars' ty - return $ DForallT tvbs' cxt' ty' + return $ DForallT fvf tvbs' ty' +substTy vars (DConstrainedT cxt ty) = + DConstrainedT <$> mapM (substTy vars) cxt <*> substTy vars ty substTy vars (DAppT t1 t2) = DAppT <$> substTy vars t1 <*> substTy vars t2 substTy vars (DAppKindT t k) = diff --git a/Language/Haskell/TH/Desugar/Sweeten.hs b/Language/Haskell/TH/Desugar/Sweeten.hs --- a/Language/Haskell/TH/Desugar/Sweeten.hs +++ b/Language/Haskell/TH/Desugar/Sweeten.hs @@ -104,6 +104,8 @@ [NewtypeD (cxtToTH cxt) n (map tvbToTH tvbs) (conToTH con) (map derivingToTH derivings)] #endif +decToTH (DDataD Newtype _cxt _n _tvbs _mk _cons _derivings) = + error "Newtype declaration without exactly 1 constructor." decToTH (DTySynD n tvbs ty) = [TySynD n (map tvbToTH tvbs) (typeToTH ty)] decToTH (DClassD cxt n tvbs fds decs) = [ClassD (cxtToTH cxt) n (map tvbToTH tvbs) fds (decsToTH decs)] @@ -114,7 +116,7 @@ Nothing -> (_cxt, _ty) Just _tvbs -> #if __GLASGOW_HASKELL__ < 800 || __GLASGOW_HASKELL__ >= 802 - ([], DForallT _tvbs _cxt _ty) + ([], DForallT ForallInvis _tvbs $ DConstrainedT _cxt _ty) #else -- See #117 error $ "Explicit foralls in instance declarations " @@ -164,7 +166,7 @@ Nothing -> (_cxt, _ty) Just _tvbs -> #if __GLASGOW_HASKELL__ < 710 || __GLASGOW_HASKELL__ >= 802 - ([], DForallT _tvbs _cxt _ty) + ([], DForallT ForallInvis _tvbs $ DConstrainedT _cxt _ty) #else -- See #117 error $ "Explicit foralls in standalone deriving declarations " @@ -180,14 +182,21 @@ decToTH (DPatSynD n args dir pat) = [PatSynD n args (patSynDirToTH dir) (patToTH pat)] decToTH (DPatSynSigD n ty) = [PatSynSigD n (typeToTH ty)] #else -decToTH dec - | DPatSynD{} <- dec = patSynErr - | DPatSynSigD{} <- dec = patSynErr - where - patSynErr = error "Pattern synonyms supported only in GHC 8.2+" +decToTH DPatSynD{} = patSynErr +decToTH DPatSynSigD{} = patSynErr #endif -decToTH _ = error "Newtype declaration without exactly 1 constructor." +#if __GLASGOW_HASKELL__ >= 809 +decToTH (DKiSigD n ki) = [KiSigD n (typeToTH ki)] +#else +decToTH (DKiSigD {}) = + error "Standalone kind signatures supported only in GHC 8.10+" +#endif +#if __GLASGOW_HASKELL__ < 801 +patSynErr :: a +patSynErr = error "Pattern synonyms supported only in GHC 8.2+" +#endif + -- | Indicates whether something is a newtype or data type, bundling its -- constructor(s) along with it. data DNewOrDataCons @@ -320,9 +329,10 @@ go DArrowT = 0 go (DLitT {}) = 0 -- These won't show up on pre-8.0 GHCs - go (DForallT {}) = error "`forall` type used in GADT return type" - go DWildCardT = 0 - go (DAppKindT {}) = 0 + go (DForallT {}) = error "`forall` type used in GADT return type" + go (DConstrainedT {}) = error "Constrained type used in GADT return type" + go DWildCardT = 0 + go (DAppKindT {}) = 0 con' :: Con con' = conToTH $ DCon [] [] n fields rty @@ -404,7 +414,24 @@ clauseToTH (DClause pats exp) = Clause (map patToTH pats) (NormalB (expToTH exp)) [] typeToTH :: DType -> Type -typeToTH (DForallT tvbs cxt ty) = ForallT (map tvbToTH tvbs) (map predToTH cxt) (typeToTH ty) +-- We need a special case for DForallT ForallInvis followed by DConstrainedT +-- so that we may collapse them into a single ForallT when sweetening. +-- See Note [Desugaring and sweetening ForallT] in L.H.T.Desugar.Core. +typeToTH (DForallT ForallInvis tvbs (DConstrainedT ctxt ty)) = + ForallT (map tvbToTH tvbs) (map predToTH ctxt) (typeToTH ty) +typeToTH (DForallT fvf tvbs ty) = + case fvf of + ForallInvis -> ForallT tvbs' [] ty' + ForallVis -> +#if __GLASGOW_HASKELL__ >= 809 + ForallVisT tvbs' ty' +#else + error "Visible dependent quantification supported only in GHC 8.10+" +#endif + where + tvbs' = map tvbToTH tvbs + ty' = typeToTH ty +typeToTH (DConstrainedT cxt ty) = ForallT [] (map predToTH cxt) (typeToTH ty) typeToTH (DAppT t1 t2) = AppT (typeToTH t1) (typeToTH t2) typeToTH (DSigT ty ki) = SigT (typeToTH ty) (typeToTH ki) typeToTH (DVarT n) = VarT n @@ -480,6 +507,8 @@ = error "Wildcards supported only in GHC 8.0+" go _ (DForallT {}) = error "Quantified constraints supported only in GHC 8.6+" + go _ (DConstrainedT {}) + = error "Quantified constraints supported only in GHC 8.6+" go _ DArrowT = error "(->) spotted at head of a constraint" go _ (DLitT {}) @@ -497,10 +526,22 @@ predToTH DWildCardT = error "Wildcards supported only in GHC 8.0+" #endif #if __GLASGOW_HASKELL__ >= 805 -predToTH (DForallT tvbs cxt p) = - ForallT (map tvbToTH tvbs) (map predToTH cxt) (predToTH p) +-- We need a special case for DForallT ForallInvis followed by DConstrainedT +-- so that we may collapse them into a single ForallT when sweetening. +-- See Note [Desugaring and sweetening ForallT] in L.H.T.Desugar.Core. +predToTH (DForallT ForallInvis tvbs (DConstrainedT ctxt p)) = + ForallT (map tvbToTH tvbs) (map predToTH ctxt) (predToTH p) +predToTH (DForallT fvf tvbs p) = + case fvf of + ForallInvis -> ForallT tvbs' [] p' + ForallVis -> error "Visible dependent quantifier spotted at head of a constraint" + where + tvbs' = map tvbToTH tvbs + p' = predToTH p +predToTH (DConstrainedT cxt p) = ForallT [] (map predToTH cxt) (predToTH p) #else -predToTH (DForallT {}) = error "Quantified constraints supported only in GHC 8.6+" +predToTH (DForallT {}) = error "Quantified constraints supported only in GHC 8.6+" +predToTH (DConstrainedT {}) = error "Quantified constraints supported only in GHC 8.6+" #endif #if __GLASGOW_HASKELL__ >= 807 predToTH (DAppKindT p k) = AppKindT (predToTH p) (typeToTH k) diff --git a/Language/Haskell/TH/Desugar/Util.hs b/Language/Haskell/TH/Desugar/Util.hs --- a/Language/Haskell/TH/Desugar/Util.hs +++ b/Language/Haskell/TH/Desugar/Util.hs @@ -24,14 +24,15 @@ thirdOf3, splitAtList, extractBoundNamesDec, extractBoundNamesPat, tvbToType, tvbToTypeWithSig, tvbToTANormalWithSig, - nameMatches, thdOf3, firstMatch, + nameMatches, thdOf3, liftFst, liftSnd, firstMatch, unboxedSumDegree_maybe, unboxedSumNameDegree_maybe, tupleDegree_maybe, tupleNameDegree_maybe, unboxedTupleDegree_maybe, unboxedTupleNameDegree_maybe, splitTuple_maybe, topEverywhereM, isInfixDataCon, isTypeKindName, typeKindName, - mkExtraKindBindersGeneric, unravelType, unSigType, unfoldType, - TypeArg(..), applyType, filterTANormals, unSigTypeArg, probablyWrongUnTypeArg + unSigType, unfoldType, ForallVisFlag(..), FunArgs(..), VisFunArg(..), + filterVisFunArgs, ravelType, unravelType, + TypeArg(..), applyType, filterTANormals, probablyWrongUnTypeArg #if __GLASGOW_HASKELL__ >= 800 , bindIP #endif @@ -45,7 +46,6 @@ import Language.Haskell.TH.Desugar.OSet (OSet) import Language.Haskell.TH.Syntax -import Control.Monad ( replicateM ) import qualified Control.Monad.Fail as Fail import Data.Foldable import Data.Generics hiding ( Fixity ) @@ -206,28 +206,87 @@ = Just args go _ _ = Nothing --- | Like 'mkExtraDKindBinders', but parameterized to allow working over both --- 'Kind'/'TyVarBndr' and 'DKind'/'DTyVarBndr'. -mkExtraKindBindersGeneric - :: Quasi q - => (kind -> ([tyVarBndr], [pred], [kind], kind)) - -> (Name -> kind -> tyVarBndr) - -> kind -> q [tyVarBndr] -mkExtraKindBindersGeneric unravel mkKindedTV k = do - let (_, _, args, _) = unravel k - names <- replicateM (length args) (qNewName "a") - return (zipWith mkKindedTV names args) +-- | Is a @forall@ invisible (e.g., @forall a b. {...}@, with a dot) or visible +-- (e.g., @forall a b -> {...}@, with an arrow)? +data ForallVisFlag + = ForallVis -- ^ A visible @forall@ (with an arrow) + | ForallInvis -- ^ An invisible @forall@ (with a dot) + deriving (Eq, Show, Typeable, Data) --- | Decompose a function 'Type' into its type variables, its context, its --- argument types, and its result type. -unravelType :: Type -> ([TyVarBndr], [Pred], [Type], Type) +-- | The list of arguments in a function 'Type'. +data FunArgs + = FANil + -- ^ No more arguments. + | FAForalls ForallVisFlag [TyVarBndr] FunArgs + -- ^ A series of @forall@ed type variables followed by a dot (if + -- 'ForallInvis') or an arrow (if 'ForallVis'). For example, + -- the type variables @a1 ... an@ in @forall a1 ... an. r@. + | FACxt Cxt FunArgs + -- ^ A series of constraint arguments followed by @=>@. For example, + -- the @(c1, ..., cn)@ in @(c1, ..., cn) => r@. + | FAAnon Type FunArgs + -- ^ An anonymous argument followed by an arrow. For example, the @a@ + -- in @a -> r@. + deriving (Eq, Show, Typeable, Data) + +-- | A /visible/ function argument type (i.e., one that must be supplied +-- explicitly in the source code). This is in contrast to /invisible/ +-- arguments (e.g., the @c@ in @c => r@), which are instantiated without +-- the need for explicit user input. +data VisFunArg + = VisFADep TyVarBndr + -- ^ A visible @forall@ (e.g., @forall a -> a@). + | VisFAAnon Type + -- ^ An anonymous argument followed by an arrow (e.g., @a -> r@). + deriving (Eq, Show, Typeable, Data) + +-- | Filter the visible function arguments from a list of 'FunArgs'. +filterVisFunArgs :: FunArgs -> [VisFunArg] +filterVisFunArgs FANil = [] +filterVisFunArgs (FAForalls fvf tvbs args) = + case fvf of + ForallVis -> map VisFADep tvbs ++ args' + ForallInvis -> args' + where + args' = filterVisFunArgs args +filterVisFunArgs (FACxt _ args) = + filterVisFunArgs args +filterVisFunArgs (FAAnon t args) = + VisFAAnon t:filterVisFunArgs args + +-- | Reconstruct an arrow 'Type' from its argument and result types. +ravelType :: FunArgs -> Type -> Type +ravelType FANil res = res +-- We need a special case for FAForalls ForallInvis followed by FACxt so that we may +-- collapse them into a single ForallT when raveling. +-- See Note [Desugaring and sweetening ForallT] in L.H.T.Desugar.Core. +ravelType (FAForalls ForallInvis tvbs (FACxt p args)) res = + ForallT tvbs p (ravelType args res) +ravelType (FAForalls ForallInvis tvbs args) res = ForallT tvbs [] (ravelType args res) +ravelType (FAForalls ForallVis _tvbs _args) _res = +#if __GLASGOW_HASKELL__ >= 809 + ForallVisT _tvbs (ravelType _args _res) +#else + error "Visible dependent quantification supported only on GHC 8.10+" +#endif +ravelType (FACxt cxt args) res = ForallT [] cxt (ravelType args res) +ravelType (FAAnon t args) res = AppT (AppT ArrowT t) (ravelType args res) + +-- | Decompose a function 'Type' into its arguments (the 'FunArgs') and its +-- result type (the 'Type). +unravelType :: Type -> (FunArgs, Type) unravelType (ForallT tvbs cxt ty) = - let (tvbs', cxt', tys, res) = unravelType ty in - (tvbs ++ tvbs', cxt ++ cxt', tys, res) + let (args, res) = unravelType ty in + (FAForalls ForallInvis tvbs (FACxt cxt args), res) unravelType (AppT (AppT ArrowT t1) t2) = - let (tvbs, cxt, tys, res) = unravelType t2 in - (tvbs, cxt, t1 : tys, res) -unravelType t = ([], [], [], t) + let (args, res) = unravelType t2 in + (FAAnon t1 args, res) +#if __GLASGOW_HASKELL__ >= 809 +unravelType (ForallVisT tvbs ty) = + let (args, res) = unravelType ty in + (FAForalls ForallVis tvbs args, res) +#endif +unravelType t = (FANil, t) -- | Remove all of the explicit kind signatures from a 'Type'. unSigType :: Type -> Type @@ -314,11 +373,6 @@ getTANormal (TANormal t) = Just t getTANormal (TyArg {}) = Nothing --- | Remove all of the explicit kind signatures from a 'TypeArg'. -unSigTypeArg :: TypeArg -> TypeArg -unSigTypeArg (TANormal t) = TANormal (unSigType t) -unSigTypeArg (TyArg k) = TyArg (unSigType k) - -- | Extract the underlying 'Type' or 'Kind' from a 'TypeArg'. This forgets -- information about whether a type is a normal argument or not, so use with -- caution. @@ -406,6 +460,12 @@ thdOf3 :: (a,b,c) -> c thdOf3 (_,_,c) = c + +liftFst :: (a -> b) -> (a, c) -> (b, c) +liftFst f (a,c) = (f a, c) + +liftSnd :: (a -> b) -> (c, a) -> (c, b) +liftSnd f (c,a) = (c, f a) thirdOf3 :: (a -> b) -> (c, d, a) -> (c, d, b) thirdOf3 f (c, d, a) = (c, d, f a) diff --git a/Test/Dec.hs b/Test/Dec.hs --- a/Test/Dec.hs +++ b/Test/Dec.hs @@ -52,6 +52,10 @@ $(S.dectest17) #endif +#if __GLASGOW_HASKELL__ >= 809 +$(S.dectest18) +#endif + $(fmap unqualify S.instance_test) $(fmap unqualify S.imp_inst_test1) diff --git a/Test/DsDec.hs b/Test/DsDec.hs --- a/Test/DsDec.hs +++ b/Test/DsDec.hs @@ -77,6 +77,10 @@ $(return $ decsToTH [S.ds_dectest17]) #endif +#if __GLASGOW_HASKELL__ >= 809 +$(dsDecSplice S.dectest18) +#endif + $(do decs <- S.rec_sel_test withLocalDeclarations decs $ do [DDataD nd [] name [DPlainTV tvbName] k cons []] <- dsDecs decs diff --git a/Test/ReifyTypeCUSKs.hs b/Test/ReifyTypeCUSKs.hs new file mode 100644 --- /dev/null +++ b/Test/ReifyTypeCUSKs.hs @@ -0,0 +1,136 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +#if __GLASGOW_HASKELL__ >= 800 +{-# LANGUAGE TypeInType #-} +#endif +#if __GLASGOW_HASKELL__ >= 806 +{-# LANGUAGE StarIsType #-} +#endif +#if __GLASGOW_HASKELL__ >= 809 +{-# LANGUAGE CUSKs #-} +#endif +-- This is kept in a separate module from ReifyTypeSigs to isolate the use of +-- the -XCUSKs language extension. +module ReifyTypeCUSKs where + +#if __GLASGOW_HASKELL__ >= 800 && __GLASGOW_HASKELL__ < 806 +import Data.Kind (type (*)) +#endif +#if __GLASGOW_HASKELL__ < 710 +import Data.Traversable (traverse) +#endif +import GHC.Exts (Constraint) +import Language.Haskell.TH.Desugar +import Language.Haskell.TH.Syntax +import Splices (eqTH) + +test_reify_type_cusks, test_reify_type_no_cusks :: [Bool] +(test_reify_type_cusks, test_reify_type_no_cusks) = + $(do cusk_decls <- + [d| data A1 (a :: *) + type A2 (a :: *) = (a :: *) + type family A3 a + data family A4 a + type family A5 (a :: *) :: * where + A5 a = a + class A6 (a :: *) where + type A7 a b + +#if __GLASGOW_HASKELL__ >= 800 + data A8 (a :: k) :: k -> * +#endif +#if __GLASGOW_HASKELL__ >= 804 + data A9 (a :: j) :: forall k. k -> * +#endif +#if __GLASGOW_HASKELL__ >= 809 + data A10 (k :: Type) (a :: k) + data A11 :: forall k -> k -> * +#endif + |] + + no_cusk_decls <- + [d| data B1 a + type B2 (a :: *) = a + type B3 a = (a :: *) + type family B4 (a :: *) where + B4 a = a + type family B5 a :: * where + B5 a = a + class B6 a where + type B7 (a :: *) (b :: *) :: * + +#if __GLASGOW_HASKELL__ >= 800 + data B8 :: k -> * +#endif +#if __GLASGOW_HASKELL__ >= 804 + data B9 :: forall j. j -> k -> * +#endif + |] + + let test_reify_kind :: DsMonad q + => String -> (Int, Maybe DKind) -> q Bool + test_reify_kind prefix (i, expected_kind) = do + actual_kind <- dsReifyType $ mkName $ prefix ++ show i + return $ expected_kind `eqTH` actual_kind + + typeKind :: DKind + typeKind = DConT typeKindName + + type_to_type :: DKind + type_to_type = DArrowT `DAppT` typeKind `DAppT` typeKind + + cusk_decl_bools <- + withLocalDeclarations cusk_decls $ + traverse (\(i, k) -> test_reify_kind "A" (i, Just k)) $ + [ (1, type_to_type) + , (2, type_to_type) + , (3, type_to_type) + , (4, type_to_type) + , (5, type_to_type) + , (6, DArrowT `DAppT` typeKind `DAppT` DConT ''Constraint) + , (7, DArrowT `DAppT` typeKind `DAppT` type_to_type) + ] +#if __GLASGOW_HASKELL__ >= 800 + ++ + [ (8, let k = mkName "k" in + DForallT ForallInvis [DPlainTV k] $ + DArrowT `DAppT` DVarT k `DAppT` + (DArrowT `DAppT` DVarT k `DAppT` typeKind)) + ] +#endif +#if __GLASGOW_HASKELL__ >= 804 + ++ + [ (9, let j = mkName "j" + k = mkName "k" in + DForallT ForallInvis [DPlainTV j] $ + DArrowT `DAppT` DVarT j `DAppT` + (DForallT ForallInvis [DPlainTV k] $ + DArrowT `DAppT` DVarT k `DAppT` typeKind)) + ] +#endif +#if __GLASGOW_HASKELL__ >= 809 + ++ + [ (10, let k = mkName "k" in + DForallT ForallVis [DKindedTV k typeKind] $ + DArrowT `DAppT` DVarT k `DAppT` typeKind) + , (11, let k = mkName "k" in + DForallT ForallVis [DPlainTV k] $ + DArrowT `DAppT` DVarT k `DAppT` typeKind) + ] +#endif + + no_cusk_decl_bools <- + withLocalDeclarations no_cusk_decls $ + traverse (test_reify_kind "B") $ + map (, Nothing) $ + [1..7] +#if __GLASGOW_HASKELL__ >= 800 + ++ [8] +#endif +#if __GLASGOW_HASKELL__ >= 804 + ++ [9] +#endif + lift (cusk_decl_bools, no_cusk_decl_bools)) diff --git a/Test/ReifyTypeSigs.hs b/Test/ReifyTypeSigs.hs new file mode 100644 --- /dev/null +++ b/Test/ReifyTypeSigs.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +#if __GLASGOW_HASKELL__ >= 809 +{-# LANGUAGE StandaloneKindSignatures #-} +#endif +module ReifyTypeSigs where + +#if __GLASGOW_HASKELL__ >= 809 +import Data.Kind +import Data.Proxy +#endif +#if __GLASGOW_HASKELL__ < 710 +import Data.Traversable (traverse) +#endif +import Language.Haskell.TH.Desugar +import Language.Haskell.TH.Syntax hiding (Type) +import Splices (eqTH) + +test_reify_kind_sigs :: [Bool] +test_reify_kind_sigs = + $(do kind_sig_decls <- + [d| +#if __GLASGOW_HASKELL__ >= 809 + type A1 :: forall k. k -> Type + data A1 a + + type A2 :: k -> Type + type A2 a = a + + type A3 :: forall k. k -> Type + type family A3 + + type A4 :: forall k. k -> Type + data family A4 a + + type A5 :: k -> Type + type family A5 a where + A5 a = a + + type A6 :: forall (k :: Bool) -> Proxy k -> Constraint + class A6 a b where + type A7 a c +#endif + |] + + let test_reify_kind :: DsMonad q + => (Int, DKind) -> q Bool + test_reify_kind (i, expected_kind) = do + actual_kind <- dsReifyType $ mkName $ "A" ++ show i + return $ Just expected_kind `eqTH` actual_kind + + kind_sig_decl_bools <- + withLocalDeclarations kind_sig_decls $ + traverse test_reify_kind $ + [] +#if __GLASGOW_HASKELL__ >= 809 + ++ + let k = mkName "k" + typeKind = DConT typeKindName + boolKind = DConT ''Bool + k_to_type = DArrowT `DAppT` DVarT k `DAppT` typeKind + forall_k_invis_k_to_type = DForallT ForallInvis [DPlainTV k] k_to_type in + [ (1, forall_k_invis_k_to_type) + , (2, k_to_type) + , (3, forall_k_invis_k_to_type) + , (4, forall_k_invis_k_to_type) + , (5, k_to_type) + , (6, DForallT ForallVis [DKindedTV k boolKind] $ + DArrowT `DAppT` (DConT ''Proxy `DAppT` DVarT k) + `DAppT` DConT ''Constraint) + , (7, DArrowT `DAppT` boolKind `DAppT` + (DArrowT `DAppT` typeKind `DAppT` typeKind)) + ] +#endif + + lift kind_sig_decl_bools) diff --git a/Test/Run.hs b/Test/Run.hs --- a/Test/Run.hs +++ b/Test/Run.hs @@ -26,6 +26,10 @@ {-# LANGUAGE QuantifiedConstraints #-} #endif +#if __GLASGOW_HASKELL__ >= 809 +{-# LANGUAGE StandaloneKindSignatures #-} +#endif + module Main where import Prelude hiding ( exp ) @@ -38,6 +42,8 @@ import qualified DsDec import qualified Dec import Dec ( RecordSel ) +import ReifyTypeCUSKs +import ReifyTypeSigs import Language.Haskell.TH.Desugar import qualified Language.Haskell.TH.Desugar.OSet as OS import Language.Haskell.TH.Desugar.Expand ( expandUnsoundly ) @@ -49,7 +55,6 @@ import Control.Applicative #endif -import Data.Function ( on ) import qualified Data.Map as M import Data.Proxy @@ -294,17 +299,17 @@ test_t92 = $(do a <- newName "a" f <- newName "f" - let t = DForallT [DPlainTV f] [] (DVarT f `DAppT` DVarT a) + let t = DForallT ForallInvis [DPlainTV f] (DVarT f `DAppT` DVarT a) toposortTyVarsOf [t] `eqTHSplice` [DPlainTV a]) test_t97 :: Bool test_t97 = $(do a <- newName "a" k <- newName "k" - let orig_ty = DForallT + let orig_ty = DForallT ForallInvis [DKindedTV a (DConT ''Constant `DAppT` DConT ''Int `DAppT` DVarT k)] - [] (DVarT a) - expected_ty = DForallT [DKindedTV a (DVarT k)] [] (DVarT a) + (DVarT a) + expected_ty = DForallT ForallInvis [DKindedTV a (DVarT k)] (DVarT a) expanded_ty <- expandType orig_ty expected_ty `eqTHSplice` expanded_ty) @@ -325,6 +330,27 @@ True -- DataD didn't have the ability to store kind signatures prior to GHC 8.0 #endif +test_t100 :: Bool +test_t100 = +#if __GLASGOW_HASKELL__ >= 800 + $(do decs <- [d| data T b where + MkT :: forall a. { unT :: a } -> T a |] + info <- withLocalDeclarations decs (dsReify (mkName "unT")) + let -- forall a. T a -> a + exp_ty = DForallT ForallInvis [DPlainTV (mkName "a")] $ + DArrowT `DAppT` (DConT (mkName "T") `DAppT` DVarT (mkName "a")) + `DAppT` DVarT (mkName "a") + case info of + Just (DVarI _ actual_ty _) -> exp_ty `eqTHSplice` actual_ty + _ -> [| False |]) +#else + True -- RecGadtC didn't exist prior to GHC 8.0, do the quote above will + -- normalize to `data T b = MkT { unT :: b }`. This defeats the point of + -- this test, and to make things worse, this will cause `dsReify` to + -- return a different type for unT (forall b. T b -> b). Let's just not + -- bother testing this on pre-8.0 GHCs. +#endif + test_t102 :: Bool test_t102 = $(do decs <- [d| data Foo x where MkFoo :: forall a. { unFoo :: a } -> Foo a |] @@ -354,9 +380,12 @@ test_t112 = $(do a <- newName "a" b <- newName "b" - let [aVar, bVar] = map DVarT [a, b] - [aTvb, bTvb] = map DPlainTV [a, b] - let fvsABExpected = [aTvb, bTvb] + let aVar = DVarT a + bVar = DVarT b + aTvb = DPlainTV a + bTvb = DPlainTV b + + fvsABExpected = [aTvb, bTvb] fvsABActual = toposortTyVarsOf [aVar, bVar] fvsBAExpected = [bTvb, aTvb] @@ -366,16 +395,37 @@ eqBA = fvsBAExpected `eqTH` fvsBAActual [| [eqAB, eqBA] |]) +test_t132 :: Bool +test_t132 = + $(do let c = mkName "C" + m = mkName "m" + a = mkName "a" + fixity = Fixity 5 InfixR + -- Defines a class with a fixity declaration inside, i.e., + -- + -- class C a where + -- infixr 5 `m` + -- m :: a + -- + -- We define this by hand to avoid GHC#17608 on pre-8.12 GHCs. + decs = sweeten [ DClassD [] c [DPlainTV a] [] + [ DLetDec (DInfixD fixity m) + , DLetDec (DSigD m (DVarT a)) + ] + ] + expected = Just fixity + actual <- withLocalDeclarations decs (reifyFixityWithLocals m) + expected `eqTHSplice` actual) + -- Unit tests for functions that compute free variables (e.g., fvDType) test_fvs :: [Bool] test_fvs = $(do a <- newName "a" let -- (Show a => Show (Maybe a)) => String - ty1 = DForallT - [] - [DForallT [] [DConT ''Show `DAppT` DVarT a] - (DConT ''Show `DAppT` (DConT ''Maybe `DAppT` DVarT a))] + ty1 = DConstrainedT + [DConstrainedT [DConT ''Show `DAppT` DVarT a] + (DConT ''Show `DAppT` (DConT ''Maybe `DAppT` DVarT a))] (DConT ''String) b1 = fvDType ty1 `eqTH` OS.singleton a -- #93 @@ -392,15 +442,16 @@ -- (Nothing :: Maybe a) ty1 = DSigT (DConT 'Nothing) (DConT ''Maybe `DAppT` DVarT a) -- forall (c :: a). c - ty2 = DForallT [DKindedTV c (DVarT a)] [] (DVarT c) + ty2 = DForallT ForallInvis [DKindedTV c (DVarT a)] (DVarT c) -- forall a (c :: a). c - ty3 = DForallT [DPlainTV a, DKindedTV c (DVarT a)] [] (DVarT c) + ty3 = DForallT ForallInvis [DPlainTV a, DKindedTV c (DVarT a)] (DVarT c) -- forall (a :: k) k (b :: k). Proxy b -> Proxy a - ty4 = DForallT [ DKindedTV a (DVarT k) + ty4 = DForallT ForallInvis + [ DKindedTV a (DVarT k) , DPlainTV k , DKindedTV b (DVarT k) - ] [] (DArrowT `DAppT` (DConT ''Proxy `DAppT` DVarT b) - `DAppT` (DConT ''Proxy `DAppT` DVarT a)) + ] (DArrowT `DAppT` (DConT ''Proxy `DAppT` DVarT b) + `DAppT` (DConT ''Proxy `DAppT` DVarT a)) substTy1 <- substTy subst ty1 substTy2 <- substTy subst ty2 @@ -486,33 +537,29 @@ test_matchTy :: [Bool] test_matchTy = - [ matchTy NoIgnore (DVarT a) (DConT ''Bool) `eq` Just (M.singleton a (DConT ''Bool)) - , matchTy NoIgnore (DVarT a) (DVarT a) `eq` Just (M.singleton a (DVarT a)) - , matchTy NoIgnore (DVarT a) (DVarT b) `eq` Just (M.singleton a (DVarT b)) + [ matchTy NoIgnore (DVarT a) (DConT ''Bool) == Just (M.singleton a (DConT ''Bool)) + , matchTy NoIgnore (DVarT a) (DVarT a) == Just (M.singleton a (DVarT a)) + , matchTy NoIgnore (DVarT a) (DVarT b) == Just (M.singleton a (DVarT b)) , matchTy NoIgnore (DConT ''Either `DAppT` DVarT a `DAppT` DVarT b) (DConT ''Either `DAppT` DConT ''Int `DAppT` DConT ''Bool) - `eq` Just (M.fromList [(a, DConT ''Int), (b, DConT ''Bool)]) + == Just (M.fromList [(a, DConT ''Int), (b, DConT ''Bool)]) , matchTy NoIgnore (DConT ''Either `DAppT` DVarT a `DAppT` DVarT a) (DConT ''Either `DAppT` DConT ''Int `DAppT` DConT ''Int) - `eq` Just (M.singleton a (DConT ''Int)) + == Just (M.singleton a (DConT ''Int)) , matchTy NoIgnore (DConT ''Either `DAppT` DVarT a `DAppT` DVarT a) (DConT ''Either `DAppT` DConT ''Int `DAppT` DConT ''Bool) - `eq` Nothing - , matchTy NoIgnore (DConT ''Int) (DConT ''Bool) `eq` Nothing - , matchTy NoIgnore (DConT ''Int) (DConT ''Int) `eq` Just M.empty - , matchTy NoIgnore (DConT ''Int) (DVarT a) `eq` Nothing - , matchTy NoIgnore (DVarT a `DSigT` DConT ''Bool) (DConT ''Int) `eq` Nothing + == Nothing + , matchTy NoIgnore (DConT ''Int) (DConT ''Bool) == Nothing + , matchTy NoIgnore (DConT ''Int) (DConT ''Int) == Just M.empty + , matchTy NoIgnore (DConT ''Int) (DVarT a) == Nothing + , matchTy NoIgnore (DVarT a `DSigT` DConT ''Bool) (DConT ''Int) == Nothing , matchTy YesIgnore (DVarT a `DSigT` DConT ''Bool) (DConT ''Int) - `eq` Just (M.singleton a (DConT ''Int)) + == Just (M.singleton a (DConT ''Int)) ] where a = mkName "a" b = mkName "b" - -- GHC 7.6 uses containers-0.5.0.0 which doesn't have a good Data instance - -- for Map. So we have to convert to lists before comparing. - eq = (==) `on` fmap M.toList - -- Test that type synonym expansion is efficient test_t123 :: () test_t123 = @@ -555,6 +602,8 @@ it "expands type synonyms in type variable binders" $ test_t97 + it "reifies GADT record selectors correctly" $ test_t100 + it "collects GADT record selectors correctly" $ test_t102 it "quantifies kind variables in desugared ADT constructors" $ test_t103 @@ -564,6 +613,8 @@ zipWithM (\b n -> it ("toposorts free variables deterministically " ++ show n) b) test_t112 [1..] + it "reifies fixity declarations inside of classes" $ test_t132 + zipWithM (\b n -> it ("computes free variables correctly " ++ show n) b) test_fvs [1..] @@ -589,5 +640,14 @@ zipWithM (\b n -> it ("matches types " ++ show n) b) test_matchTy [1..] + + zipWithM (\b n -> it ("reifies kinds of declarations with CUSKs " ++ show n) b) + test_reify_type_cusks [1..] + + zipWithM (\b n -> it ("reifies kinds of declarations without CUSKs " ++ show n) b) + test_reify_type_no_cusks [1..] + + zipWithM (\b n -> it ("reifies the kinds of declarations with signatures " ++ show n) b) + test_reify_kind_sigs [1..] fromHUnitTest tests diff --git a/Test/Splices.hs b/Test/Splices.hs --- a/Test/Splices.hs +++ b/Test/Splices.hs @@ -10,7 +10,7 @@ DataKinds, PolyKinds, GADTs, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, StandaloneDeriving, DefaultSignatures, ConstraintKinds, GADTs, ViewPatterns, - TupleSections #-} + TupleSections, NoMonomorphismRestriction #-} #if __GLASGOW_HASKELL__ >= 711 {-# LANGUAGE TypeApplications #-} @@ -36,6 +36,10 @@ {-# LANGUAGE ImplicitParams #-} #endif +#if __GLASGOW_HASKELL__ >= 809 +{-# LANGUAGE StandaloneKindSignatures #-} +#endif + {-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-type-defaults -fno-warn-name-shadowing #-} @@ -188,8 +192,8 @@ f = return in [f 1, f 2] :: [Maybe Int] |] -test34_let_as = [| let a@(Just x) = Just 5 in - show x ++ show a |] +test34_let_as = [| let a@(x, y) = (5, 6) in + show x ++ show y ++ show a |] type Pair a = (a, a) test35_expand = [| let f :: Pair a -> a @@ -307,6 +311,9 @@ f 'x' = () in f |] +#if __GLASGOW_HASKELL__ >= 809 +type PolyTF :: forall k. k -> * +#endif type family PolyTF (x :: k) :: * where PolyTF (x :: *) = Bool @@ -428,6 +435,11 @@ (ConT ''ExData2 `AppT` VarT (mkName "a")))) ] #endif +#if __GLASGOW_HASKELL__ >= 809 +dectest18 = [d| data Dec18 :: forall k -> k -> * where + MkDec18 :: forall k (a :: k). Dec18 k a |] +#endif + instance_test = [d| instance (Show a, Show b) => Show (a -> b) where show _ = "function" |] @@ -504,6 +516,11 @@ class R2 a b where r3 :: a -> b -> c -> a type R4 b a :: * +#if __GLASGOW_HASKELL__ >= 800 + -- Only define this on GHC 8.0 or later, since TH had trouble quoting + -- associated type family defaults before then. + type R4 b a = Either a b +#endif data R5 a :: * data R6 a = R7 { r8 :: a -> a, r9 :: Bool } @@ -594,6 +611,14 @@ class R30 a where r31 :: a -> b -> a + +#if __GLASGOW_HASKELL__ >= 809 + type R32 :: forall k -> k -> * + type family R32 :: forall k -> k -> * where +#endif + + data R33 a where + R34 :: { r35 :: Int } -> R33 Int |] reifyDecsNames :: [Name] @@ -610,6 +635,10 @@ , "R25", "r26", "R28", "r29" #endif , "R30", "r31" +#if __GLASGOW_HASKELL__ >= 809 + , "R32" +#endif + , "R33", "R34", "r35" ] simplCaseTests :: [Q Exp] diff --git a/th-desugar.cabal b/th-desugar.cabal --- a/th-desugar.cabal +++ b/th-desugar.cabal @@ -1,5 +1,5 @@ name: th-desugar -version: 1.10 +version: 1.11 cabal-version: >= 1.10 synopsis: Functions to desugar Template Haskell homepage: https://github.com/goldfirere/th-desugar @@ -18,7 +18,8 @@ , GHC == 8.2.2 , GHC == 8.4.4 , GHC == 8.6.5 - , GHC == 8.8.1 + , GHC == 8.8.3 + , GHC == 8.10.1 description: This package provides the Language.Haskell.TH.Desugar module, which desugars Template Haskell's rich encoding of Haskell syntax into a simpler encoding. @@ -44,7 +45,7 @@ build-depends: base >= 4.7 && < 5, ghc-prim, - template-haskell >= 2.9 && < 2.16, + template-haskell >= 2.9 && < 2.17, containers >= 0.5, fail == 4.9.*, mtl >= 2.1, @@ -81,7 +82,11 @@ default-extensions: TemplateHaskell hs-source-dirs: Test main-is: Run.hs - other-modules: Splices, Dec, DsDec + other-modules: Dec + DsDec + ReifyTypeCUSKs + ReifyTypeSigs + Splices build-depends: base >= 4 && < 5, @@ -93,5 +98,4 @@ hspec >= 1.3, th-desugar, th-lift >= 0.6.1, - th-orphans >= 0.9.1, - th-expand-syns >= 0.3.0.6 + th-orphans >= 0.13.9