singletons-th 3.4 → 3.5.1
raw patch · 23 files changed
Files
- CHANGES.md +49/−0
- README.md +1/−1
- singletons-th.cabal +8/−7
- src/Data/Singletons/TH.hs +1/−1
- src/Data/Singletons/TH/CustomStar.hs +1/−1
- src/Data/Singletons/TH/Deriving/Enum.hs +1/−1
- src/Data/Singletons/TH/Deriving/Foldable.hs +2/−2
- src/Data/Singletons/TH/Deriving/Functor.hs +3/−3
- src/Data/Singletons/TH/Deriving/Show.hs +1/−1
- src/Data/Singletons/TH/Deriving/Traversable.hs +1/−1
- src/Data/Singletons/TH/Deriving/Util.hs +16/−2
- src/Data/Singletons/TH/Partition.hs +2/−2
- src/Data/Singletons/TH/Promote.hs +509/−189
- src/Data/Singletons/TH/Promote/Defun.hs +138/−100
- src/Data/Singletons/TH/Promote/Monad.hs +178/−10
- src/Data/Singletons/TH/Single.hs +56/−233
- src/Data/Singletons/TH/Single/Data.hs +11/−222
- src/Data/Singletons/TH/Single/Decide.hs +22/−21
- src/Data/Singletons/TH/Single/Fixity.hs +48/−28
- src/Data/Singletons/TH/Single/Type.hs +42/−70
- src/Data/Singletons/TH/Syntax.hs +43/−16
- src/Data/Singletons/TH/Syntax/LocalVar.hs +252/−0
- src/Data/Singletons/TH/Util.hs +21/−56
CHANGES.md view
@@ -1,6 +1,55 @@ Changelog for the `singletons-th` project ========================================= +3.5.1 [2026.01.10]+------------------+* Require building with GHC 9.14.++3.5 [2024.12.11]+----------------+* Require building with GHC 9.12.+* Require building with `th-desugar-1.18` or later. Notably, `th-desugar-1.18`+ now desugars all lambda, `case`, and `\case` expressions to `\cases`+ expressions, and the same principle applies to the code that `singletons-th`+ generates.++ Generally speaking, most code should continue to work after this change. Note+ that singled code might now generate `-Wunused-matches` warnings where it+ didn't before. For example, previous versions of `singletons-th` would not+ warn that the `x` in `map (\x -> ())` is unused after singling it, but this+ `singletons-th` will now generate an `-Wunused-matches` warning for the+ singled version of `x`.+* Add support for promoting and singling type variables that scope over the+ bodies of class method defaults and instance methods.+* `singletons-th` can now generate more precise types for singled data+ constructors whose parent data types have standalone kind signatures. For+ instance, consider this data type:++ ```hs+ $(singletons [d|+ type D :: forall k. k -> Type+ data D a = MkD+ |])+ ```++ Previously, `singletons-th` would generate the following type for `SMkD` (the+ singled counterpart to `MkD`):++ ```hs+ data SD :: forall k. k -> Type where+ SMkD :: forall a. SD (MkD :: D a)+ ```++ This was not as precise as it could have been, as the type of `SMkD` did not+ make the kind variable `k` eligible for visible type application (as is the+ case in `MkD :: forall k (a :: k). D a`). `singletons-th` now accomplishes+ this by generating the following code instead:++ ```hs+ data SD :: forall k. k -> Type where+ SMkD :: forall k (a :: k). SD (MkD :: D a)+ ```+ 3.4 [2024.05.12] ---------------- * Require building with GHC 9.10.
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.10). For more information,+of GHC (currently GHC 9.14). 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.4+version: 3.5.1 cabal-version: 1.24 synopsis: A framework for generating singleton types homepage: http://www.github.com/goldfirere/singletons@@ -8,7 +8,7 @@ maintainer: Ryan Scott <ryan.gl.scott@gmail.com> bug-reports: https://github.com/goldfirere/singletons/issues stability: experimental-tested-with: GHC == 9.10.1+tested-with: GHC == 9.14.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.10). For more information,+ of GHC (currently GHC 9.14). For more information, consult the @singletons@ @<https://github.com/goldfirere/singletons/blob/master/README.md README>@. .@@ -52,17 +52,17 @@ library hs-source-dirs: src- build-depends: base >= 4.20 && < 4.21,+ build-depends: base >= 4.22 && < 4.23, containers >= 0.5, mtl >= 2.2.1 && < 2.4, ghc-boot-th, singletons == 3.0.*, syb >= 0.4,- template-haskell >= 2.22 && < 2.23,- th-desugar >= 1.17 && < 1.18,+ template-haskell >= 2.24 && < 2.25,+ th-desugar >= 1.19 && < 1.20, th-orphans >= 0.13.11 && < 0.14, transformers >= 0.5.2- default-language: GHC2021+ default-language: GHC2024 other-extensions: TemplateHaskellQuotes exposed-modules: Data.Singletons.TH Data.Singletons.TH.CustomStar@@ -94,6 +94,7 @@ Data.Singletons.TH.Single.Ord Data.Singletons.TH.Single.Type Data.Singletons.TH.Syntax+ Data.Singletons.TH.Syntax.LocalVar Data.Singletons.TH.Util -- singletons re-exports
src/Data/Singletons/TH.hs view
@@ -165,7 +165,7 @@ -> m Exp -- body -> m DExp buildCases ctor_infos expq bodyq =- DCaseE <$> (dsExp =<< expq) <*>+ dCaseE <$> (dsExp =<< expq) <*> mapM (\con -> DMatch (conToPat con) <$> (dsExp =<< bodyq)) ctor_infos where conToPat :: (Name, Int) -> DPat
src/Data/Singletons/TH/CustomStar.hs view
@@ -66,7 +66,7 @@ -- > SNat :: Sing Nat -- > SBool :: Sing Bool -- > SMaybe :: Sing a -> Sing (Maybe a)--- > type instance Sing = SRep+-- > type instance Sing @(*) = SRep -- -- The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@, -- @Bool@, and @Maybe@, not just promoted data constructors.
src/Data/Singletons/TH/Deriving/Enum.hs view
@@ -44,7 +44,7 @@ let to_enum = UFunction [DClause [DVarP n] (to_enum_rhs cons [0..])] to_enum_rhs [] _ = DVarE errorName `DAppE` DLitE (StringL "toEnum: bad argument") to_enum_rhs (DCon _ _ name _ _ : rest) (num:nums) =- DCaseE (DVarE equalsName `DAppE` DVarE n `DAppE` DLitE (IntegerL num))+ dCaseE (DVarE equalsName `DAppE` DVarE n `DAppE` DLitE (IntegerL num)) [ DMatch (DConP trueName [] []) (DConE name) , DMatch (DConP falseName [] []) (to_enum_rhs rest nums) ] to_enum_rhs _ _ = error "Internal error: exhausted infinite list in to_enum_rhs"
src/Data/Singletons/TH/Deriving/Foldable.hs view
@@ -25,7 +25,7 @@ f <- newUniqueName "_f" z <- newUniqueName "_z" let ft_foldMap :: FFoldType (q DExp)- ft_foldMap = FT { ft_triv = mkSimpleLam $ \_ -> pure $ DVarE memptyName+ ft_foldMap = FT { ft_triv = mkSimpleWildLam $ pure $ DVarE memptyName -- foldMap f = \x -> mempty , ft_var = pure $ DVarE f -- foldMap f = f@@ -36,7 +36,7 @@ } ft_foldr :: FFoldType (q DExp)- ft_foldr = FT { ft_triv = mkSimpleLam2 $ \_ z' -> pure z'+ ft_foldr = FT { ft_triv = mkSimpleWildLam2 pure -- foldr f = \x z -> z , ft_var = pure $ DVarE f -- foldr f = f
src/Data/Singletons/TH/Deriving/Functor.hs view
@@ -39,7 +39,7 @@ ft_replace :: FFoldType (q Replacer) ft_replace = FT { ft_triv = fmap Nested $ mkSimpleLam pure -- (p <$) = \x -> x- , ft_var = fmap Immediate $ mkSimpleLam $ \_ -> pure $ DVarE z+ , ft_var = fmap Immediate $ mkSimpleWildLam $ pure $ DVarE z -- (p <$) = const p , ft_ty_app = \_ gm -> do g <- gm@@ -69,13 +69,13 @@ mk_fmap :: q [DClause] mk_fmap = case cons of [] -> do v <- newUniqueName "v"- pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])]+ pure [DClause [DWildP, DVarP v] (dCaseE (DVarE v) [])] _ -> traverse mk_fmap_clause cons mk_replace :: q [DClause] mk_replace = case cons of [] -> do v <- newUniqueName "v"- pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])]+ pure [DClause [DWildP, DVarP v] (dCaseE (DVarE v) [])] _ -> traverse mk_replace_clause cons fmap_clauses <- mk_fmap
src/Data/Singletons/TH/Deriving/Show.hs view
@@ -43,7 +43,7 @@ p <- newUniqueName "p" -- The precedence argument (not always used) if null cons then do v <- newUniqueName "v"- pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])]+ pure [DClause [DWildP, DVarP v] (dCaseE (DVarE v) [])] else mapM (mk_showsPrec_clause p) cons mk_showsPrec_clause :: forall q. DsMonad q
src/Data/Singletons/TH/Deriving/Traversable.hs view
@@ -55,7 +55,7 @@ mk_trav = case cons of [] -> do v <- newUniqueName "v" pure [DClause [DWildP, DVarP v]- (DVarE pureName `DAppE` DCaseE (DVarE v) [])]+ (DVarE pureName `DAppE` dCaseE (DVarE v) [])] _ -> traverse mk_trav_clause cons trav_clauses <- mk_trav
src/Data/Singletons/TH/Deriving/Util.hs view
@@ -258,15 +258,29 @@ mkSimpleLam lam = do n <- newUniqueName "n" body <- lam (DVarE n)- return $ DLamE [n] body+ return $ dLamE [DVarP n] body +-- Make a 'DLamE' using a wildcard pattern.+mkSimpleWildLam :: Quasi q => q DExp -> q DExp+mkSimpleWildLam lam = do+ body <- lam+ return $ dLamE [DWildP] body+ -- Make a 'DLamE' using two fresh variables. mkSimpleLam2 :: Quasi q => (DExp -> DExp -> q DExp) -> q DExp mkSimpleLam2 lam = do n1 <- newUniqueName "n1" n2 <- newUniqueName "n2" body <- lam (DVarE n1) (DVarE n2)- return $ DLamE [n1, n2] body+ return $ dLamE [DVarP n1, DVarP n2] body++-- Make a 'DLamE' where the first argument is a wildcard pattern and the second+-- argument is a fresh variable.+mkSimpleWildLam2 :: Quasi q => (DExp -> q DExp) -> q DExp+mkSimpleWildLam2 lam = do+ n <- newUniqueName "n"+ body <- lam (DVarE n)+ return $ dLamE [DWildP, DVarP n] body -- "Con a1 a2 a3 -> fold [x1 a1, x2 a2, x3 a3]" --
src/Data/Singletons/TH/Partition.hs view
@@ -163,8 +163,8 @@ pure (valueBinding name (UValue exp), mempty) partitionClassDec (DLetDec (DFunD name clauses)) = pure (valueBinding name (UFunction clauses), mempty)-partitionClassDec (DLetDec (DInfixD fixity _ name)) =- pure (infixDecl fixity name, mempty)+partitionClassDec (DLetDec (DInfixD fixity ns name)) =+ pure (infixDecl fixity ns name, mempty) partitionClassDec (DLetDec (DPragmaD {})) = pure (mempty, mempty) partitionClassDec (DOpenTypeFamilyD tf_head) =
src/Data/Singletons/TH/Promote.hs view
@@ -15,6 +15,8 @@ import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap import Language.Haskell.TH.Desugar.OMap.Strict (OMap) import qualified Language.Haskell.TH.Desugar.OSet as OSet+import Language.Haskell.TH.Desugar.OSet (OSet)+import qualified Language.Haskell.TH.Desugar.Subst.Capturing as SC import Data.Singletons.TH.Deriving.Bounded import Data.Singletons.TH.Deriving.Enum import Data.Singletons.TH.Deriving.Eq@@ -35,7 +37,8 @@ import Control.Monad import Control.Monad.Trans.Maybe import Control.Monad.Writer-import Data.List (nub)+import Data.Function (on)+import Data.List (deleteFirstsBy, nub) import qualified Data.Map.Strict as Map import Data.Map.Strict ( Map ) import Data.Maybe@@ -159,10 +162,11 @@ promoteInstance mk_inst class_name name = do (df, tvbs, cons) <- getDataD ("I cannot make an instance of " ++ class_name ++ " for it.") name- tvbs' <- mapM dsTvbVis tvbs- let data_ty = foldTypeTvbs (DConT name) tvbs'- cons' <- concatMapM (dsCon tvbs' data_ty) cons- let data_decl = DataDecl df name tvbs' cons'+ dtvbs <- mapM dsTvbVis tvbs+ let data_ty = foldTypeTvbs (DConT name) dtvbs+ dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs+ cons' <- concatMapM (dsCon dtvbSpecs data_ty) cons+ let data_decl = DataDecl df name dtvbs cons' raw_inst <- mk_inst Nothing data_ty data_decl decs <- promoteM_ [] $ void $ promoteInstanceDec OMap.empty Map.empty raw_inst@@ -208,13 +212,20 @@ opts <- getOptions let_dec_env <- buildLetDecEnv decls all_locals <- allLocals- let binds = [ (name, foldType (DConT sym) (map DVarT all_locals))- | (name, _) <- OMap.assocs $ lde_defns let_dec_env- , let proName = promotedValueName opts name mb_let_uniq- sym = defunctionalizedName opts proName (length all_locals) ]+ let let_dec_proms :: [(Name, LetDecProm)]+ let_dec_proms =+ [ (name, (pro_name, all_locals))+ | (name, _) <- OMap.assocs $ lde_defns let_dec_env+ , let pro_name = promotedValueName opts name mb_let_uniq ]++ binds :: [LetBind]+ binds =+ [ (name, foldTypeLocalVars (DConT sym) locals)+ | (name, (pro_name, locals)) <- let_dec_proms+ , let sym = defunctionalizedName0 opts pro_name ] (decs, let_dec_env') <- letBind binds $ promoteLetDecEnv mb_let_uniq let_dec_env emitDecs decs- return (binds, let_dec_env' { lde_proms = OMap.fromList binds })+ return (binds, let_dec_env' { lde_proms = OMap.fromList let_dec_proms }) promoteDataDecs :: [DataDecl] -> PrM [DLetDec] promoteDataDecs = concatMapM promoteDataDec@@ -256,7 +267,7 @@ promoteClassDec :: UClassDecl -> PrM AClassDecl promoteClassDec decl@(ClassDecl { cd_name = cls_name- , cd_tvbs = tvbs+ , cd_tvbs = orig_cls_tvbs , cd_fds = fundeps , cd_atfs = atfs , cd_lde = lde@LetDecEnv@@ -270,17 +281,34 @@ defaults_list = OMap.assocs defaults defaults_names = map fst defaults_list mb_cls_sak <- dsReifyType cls_name- sig_decs <- mapM (uncurry promote_sig) meth_sigs_list++ -- If the class has a standalone kind signature, we take the original,+ -- user-written class binders (`orig_cls_tvbs`) and fill them out using+ -- `dMatchUpSAKWithDecl` to produce the "full" binders, as described in+ -- Note [Propagating kind information from class standalone kind signatures].+ mb_full_cls_tvbs <-+ traverse (\cls_sak -> dMatchUpSAKWithDecl cls_sak orig_cls_tvbs) mb_cls_sak+ let mb_full_cls_tvbs_spec = dtvbForAllTyFlagsToSpecs <$> mb_full_cls_tvbs+ -- The class binders, converted to `DTyVarBndrSpec`s. If the parent class+ -- has a standalone kind signature, we compute these `DTyVarBndrSpec`s+ -- from the full class binders, which likely have richer kind information.+ -- Otherwise, we compute these from the original, user-written class+ -- binders.+ cls_tvbs_spec = fromMaybe+ (changeDTVFlags SpecifiedSpec orig_cls_tvbs)+ mb_full_cls_tvbs_spec++ sig_decs <- mapM (uncurry (promote_sig mb_full_cls_tvbs_spec)) meth_sigs_list (default_decs, ann_rhss, prom_rhss)- <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs) defaults_list- defunAssociatedTypeFamilies tvbs atfs+ <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvbs_spec) defaults_list+ defunAssociatedTypeFamilies orig_cls_tvbs atfs - infix_decls' <- mapMaybeM (uncurry (promoteInfixDecl Nothing)) $+ infix_decls' <- mapMaybeM (\(n, (f, ns)) -> promoteInfixDecl Nothing n f ns) $ OMap.assocs infix_decls cls_infix_decls <- promoteReifiedInfixDecls $ cls_name:meth_names -- no need to do anything to the fundeps. They work as is!- let pro_cls_dec = DClassD [] pClsName tvbs fundeps+ let pro_cls_dec = DClassD [] pClsName orig_cls_tvbs fundeps (sig_decs ++ default_decs ++ infix_decls') mb_pro_cls_sak = fmap (DKiSigD pClsName) mb_cls_sak emitDecs $ maybeToList mb_pro_cls_sak ++ pro_cls_dec:cls_infix_decls@@ -289,27 +317,65 @@ return (decl { cd_lde = lde { lde_defns = OMap.fromList defaults_list' , lde_proms = OMap.fromList proms } }) where- promote_sig :: Name -> DType -> PrM DDec- promote_sig name ty = do+ -- Promote a class method's type signature to an associated type family.+ promote_sig ::+ Maybe [DTyVarBndrSpec]+ -- ^ If the parent class has a standalone kind signature, then this+ -- will be @'Just' full_bndrs@, where @full_bndrs@ are the full type+ -- variable binders described in @Note [Propagating kind information+ -- from class standalone kind signatures]@. Otherwise, this will be+ -- 'Nothing'.+ -> Name+ -- ^ The class method's name.+ -> DType+ -- ^ The class method's type.+ -> PrM DDec+ -- ^ The associated type family for the promoted class method.+ promote_sig mb_full_cls_tvbs_spec name meth_ty = do opts <- getOptions let proName = promotedTopLevelValueName opts name- -- When computing the kind to use for the defunctionalization symbols,- -- /don't/ use the type variable binders from the method's type...- (_, argKs, resK) <- promoteUnraveled ty- args <- mapM (const $ qNewName "arg") argKs- let proTvbs = zipWith (`DKindedTV` BndrReq) args argKs- -- ...instead, compute the type variable binders in a left-to-right order,- -- since that is the same order that the promoted method's kind will use.- -- See Note [Promoted class methods and kind variable ordering]- meth_sak_tvbs = changeDTVFlags SpecifiedSpec $- toposortTyVarsOf $ argKs ++ [resK]- meth_sak = ravelVanillaDType meth_sak_tvbs [] argKs resK+ (_, meth_arg_kis, meth_res_ki) <- promoteUnraveled meth_ty+ args <- mapM (const $ qNewName "arg") meth_arg_kis+ let pro_meth_args = zipWith (`DKindedTV` BndrReq) args meth_arg_kis+ -- Binders for all of the type variables mentioned in the argument and+ -- result kinds of the promoted class method. This includes both class+ -- variables and variables that only scope over the method itself.+ --+ -- This quantifies the variables in a simple left-to-right order,+ -- which may not be the same order in which the original method's type+ -- quantifies them. This is a known limitation: see+ -- Note [Promoted class methods and kind variable ordering].+ meth_tvbs = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf $ meth_arg_kis ++ [meth_res_ki]+ -- The type variable binders to use in the standalone kind signatures+ -- for the promoted class method's defunctionalization symbols.+ meth_sak_tvbs =+ case mb_full_cls_tvbs_spec of+ -- If the parent class has a standalone kind signature, then+ -- propagate as much of the kind information as possible by+ -- incorporating the full class binders. See Note [Propagating+ -- kind information from class standalone kind signatures].+ Just full_cls_tvbs_spec ->+ -- `meth_tvbs` can include class binder names, so make sure to+ -- delete type variables from `meth_tvbs` whose names are also+ -- bound by the full class binders.+ let meth_tvbs_without_cls_tvbs =+ deleteFirstsBy+ ((==) `on` extractTvbName)+ meth_tvbs+ full_cls_tvbs_spec in+ full_cls_tvbs_spec ++ meth_tvbs_without_cls_tvbs+ -- If the parent class lacks a standalone kind signature, then we+ -- simply return `meth_tvbs`.+ Nothing ->+ meth_tvbs+ meth_sak = ravelVanillaDType meth_sak_tvbs [] meth_arg_kis meth_res_ki m_fixity <- reifyFixityWithLocals name emitDecsM $ defunctionalize proName m_fixity $ DefunSAK meth_sak return $ DOpenTypeFamilyD (DTypeFamilyHead proName- proTvbs- (DKindSig resK)+ pro_meth_args+ (DKindSig meth_res_ki) Nothing) {-@@ -344,17 +410,131 @@ type MSym0 :: forall a b. a ~> b ~> a type MSym1 :: forall a b. a -> b ~> a -There is one potential hack we could use to rectify this:+In the past, we have considered different ways to rectify this, but none of+the approaches that we have tried are quite satisfactory: - type FlipConst x y = y- class PC (b :: Type) where- type M (x :: FlipConst '(b, a) a) (y :: b) :: a+* We could hackily specify the order of kind variables using a type synonym+ like `FlipConst`: -Using `FlipConst` would cause `b` to be mentioned before `a`, which would give-`M` the kind `forall b a. FlipConst '(b, a) a -> b -> a`. While the order of-type variables would be preserved, the downside is that the ugly `FlipConst`-type synonym leaks into the kind. I'm not particularly fond of this, so I have-decided not to use this hack unless someone specifically requests it.+ type FlipConst x y = y+ class PC (b :: Type) where+ type M (x :: FlipConst '(b, a) a) (y :: b) :: a++ Using `FlipConst` would cause `b` to be mentioned before `a`, which would give+ `M` the kind `forall b a. FlipConst '(b, a) a -> b -> a`. While the order of+ type variables would be preserved, the downside is that the ugly `FlipConst`+ type synonym leaks into the kind. I'm not particularly fond of this, so I have+ decided not to use this hack unless someone specifically requests it.++* We could specify the order of kind variables using the TypeAbstractions+ language extension:++ class PC (b :: Type) where+ type M @(b :: Type) @a (x :: a) (y :: b) :: a++ This is much nicer to look at than the `FlipConst` hack above. However, this+ approach has its own drawbacks. For one thing, GHC only permits using+ TypeAbstractions in an associated type family declaration if its parent class+ also has a standalone kind signature. As such, this trick would only work some+ of the time.++ Even if we /did/ give the parent class a standalone kind signature, however,+ it is still not guaranteed that the promoted method would kind-check. Consider+ what would happen if you promoted this class:++ type Traversable :: (Type -> Type) -> Constraint+ class (Functor t, Foldable t) => Traversable t where+ traverse :: Applicative f => (a -> f b) -> t a -> t (f b)++ This would be promoted to:++ type PTraversable :: (Type -> Type) -> Constraint+ class PTraversable t where+ type PTraverse @(t :: Type -> Type) @f @a @b+ (x :: a ~> f b) (y :: t a) :: t (f b)++ There is a subtle problem with this definition: because the `@f` binder lacks+ an explicit kind signature, GHC defaults its kind to `Type`. This is very bad,+ however, because `f`'s kind must be `Type -> Type`, not `Type`! Nor would it+ be straightforward to generate `@(f :: Type -> Type)`, as nothing in the+ original definition of `traverse` explicitly indicates that `f` has the kind+ `Type -> Type`.++ In theory, we could implement kind inference inside of Template Haskell to+ infer that `f :: Type -> Type`, but this is a tall order. Best to keep things+ simple and not do this.++Note [Propagating kind information from class standalone kind signatures]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Consider what happens when you promote this example:++ type Alternative :: (Type -> Type) -> Constraint+ class Applicative f => Alternative f where+ empty :: f a+ ...++We want the promoted `Empty` type family, as well as the `EmptySym0`+defunctionalization symbol, to have the kind+`forall (f :: Type -> Type) a. f a`. Giving `Empty` the appropriate kind is+easy enough, as we can simply copy over `Alternative`'s standalone kind+signature to `PAltenative`, its promoted counterpart:++ type PAlternative :: (Type -> Type) -> Constraint+ class PAlternative f where+ type Empty :: f a+ ...++Giving `EmptySym0` the appropriate kind is trickier, however. A naïve approach+would be to generate this:++ type EmptySym0 :: f a+ type family EmptySym0 where+ EmptySym0 = Empty++This would give EmptySym0 a more general kind than what we want, however, as+GHC will generalize this to:++ EmptySym0 :: forall {k} (f :: k -> Type) (a :: k). f a++This is undesirable, as now `EmptySym0` can be called on kinds that cannot have+`PAlternative` instances. What's more, if GHC proposal #425 were fully+implemented (see+https://github.com/ghc-proposals/ghc-proposals/blob/8443acc903437cef1a7fbb56de79b6dce77b1a09/proposals/0425-decl-invis-binders.rst#proposed-change-specification-instances),+then this code would simply not kind-check, as the left-hand side of the+`EmptySym0 = Empty` would be too general for its right-hand side.++Instead, we strive to generate this code for `EmptySym0` instead:++ type EmptySym0 :: forall (f :: Type -> Type) a. f a+ type family EmptySym0 where+ EmptySym0 = Empty++This is very doable because the user gave `Alternative` a standalone kind+signature, so it should be possible to match up the `Type -> Type` part of the+standalone kind signature with `f`. And that is exactly what we do:++* In `promoteClassDec`, we use the `dMatchUpSAKWithDecl` function to take the+ original class type variable binders and the class standalone kind signature+ as input and produce a new set of class binders as output, where the new+ binders have been annotated with kinds taken from the standalone kind+ signature. We will call these new class type variable binders the /full/+ binders.++* When generating a defunctionalization symbol for a promoted class method, we+ always quantify the defunctionalization symbol's kind using an explicit+ `forall`, where the `forall` looks like:++ forall <full class type variable binders> <method type variable binders>. ...++ This ensures that the kind information from the full class binders is+ propagated through to the defunctionalization symbol. (Note that we do not+ make any guarantees about the /order/ of these type variables, however. See+ Note [Promoted class methods and kind variable ordering].)++If the parent class lacks a standalone kind signature, then we skip all of this+and simply quantify the the defunctionalization symbols' kind variables in a+left-to-right order. Again, the order of these kind variables in unspecified, so+we are free to choose a simpler implementation that makes our lives easier. -} -- returns (unpromoted method name, ALetDecRHS) pairs@@ -376,8 +556,9 @@ cls_tvb_names = map extractTvbName cls_tvbs subst = Map.fromList $ zip cls_tvb_names inst_kis meth_impl = InstanceMethods inst_sigs subst+ inst_ki_kvbs = changeDTVFlags SpecifiedSpec $ toposortTyVarsOf inst_kis (meths', ann_rhss, _)- <- mapAndUnzip3M (promoteMethod meth_impl orig_meth_sigs) meths+ <- mapAndUnzip3M (promoteMethod meth_impl orig_meth_sigs inst_ki_kvbs) meths emitDecs [DInstanceD Nothing Nothing [] (foldType (DConT pClsName) inst_kis) meths'] return (decl { id_meths = zip (map fst meths) ann_rhss })@@ -459,16 +640,39 @@ promoteMethod :: MethodSort -> OMap Name DType -- method types+ -> [DTyVarBndrSpec] -- The type variables bound by the class+ -- header (e.g., the @a b@ in+ -- @class C a b where ...@). -> (Name, ULetDecRHS)- -> PrM (DDec, ALetDecRHS, DType)+ -> PrM (DDec, ALetDecRHS, LetDecProm) -- returns (type instance, ALetDecRHS, promoted RHS)-promoteMethod meth_sort orig_sigs_map (meth_name, meth_rhs) = do+promoteMethod meth_sort orig_sigs_map cls_tvbs (meth_name, meth_rhs) = do opts <- getOptions- (meth_arg_kis, meth_res_ki) <- promote_meth_ty+ (meth_scoped_tvs, meth_tvbs, meth_arg_kis, meth_res_ki) <- promote_meth_ty+ -- If ScopedTypeVariables is enabled, bring type variables into scope over the+ -- RHS. These type variables can come from the class/instance header, the+ -- method type signature/instance signature, or both, depending on how the+ -- class or instance declaration is written. See+ -- Note [Scoped type variables and class methods] in D.S.TH.Promote.Monad.+ -- See also (Wrinkle: Partial scoping) from that Note for a scenario in which+ -- we bring class/instance header type variables into scope but /not/+ -- type variables from the class method/instance signature.+ scoped_tvs_ext <- qIsExtEnabled LangExt.ScopedTypeVariables+ let all_meth_scoped_tvs+ | scoped_tvs_ext+ = OSet.fromList (map tvbToLocalVar cls_tvbs) `OSet.union` meth_scoped_tvs+ | otherwise+ = OSet.empty meth_arg_tvs <- replicateM (length meth_arg_kis) (qNewName "a") let proName = promotedTopLevelValueName opts meth_name+ -- The name of the "helper" type family which defines the promoted version+ -- of a class method default or instance method. If the method's name is+ -- alphanumeric, we reuse the method's name for the helper type family's+ -- name. Otherwise, we use the name "TFHelper". (Note that+ -- promoteLetDecRHS expects a value-level name, so we pass it "tFHelper",+ -- which later gets promoted to TFHelper.) helperNameBase = case nameBase proName of- first:_ | not (isHsLetter first) -> "TFHelper"+ first:_ | not (isHsLetter first) -> "tFHelper" alpha -> alpha -- family_args are the type variables in a promoted class's@@ -485,18 +689,44 @@ -- strictly necessary, as kind inference can figure them out just as well. family_args = map DVarT meth_arg_tvs helperName <- newUniqueName helperNameBase- let helperDefunName = defunctionalizedName0 opts helperName- (pro_decs, defun_decs, ann_rhs)- <- promoteLetDecRHS (ClassMethodRHS meth_arg_kis meth_res_ki)+ let proHelperName = promotedValueName opts helperName Nothing+ -- If a promoted method's kind lacks an outermost `forall`, then we need+ -- to compute the list of kind variable binders manually. The order of+ -- these binders doesn't matter, as the user will never invoke a helper+ -- type family directly, so we simply quantify the binders in+ -- left-to-right order.+ full_meth_tvbs+ | null meth_tvbs+ = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf (meth_arg_kis ++ [meth_res_ki])+ | otherwise+ = meth_tvbs+ -- Make sure not to re-quantify any kind variable binders that are already+ -- bound by the class or instance head.+ full_meth_tvbs_without_cls_tvbs =+ deleteFirstsBy ((==) `on` extractTvbName) full_meth_tvbs cls_tvbs+ -- All of the kind variable binders, including both (1) those bound by the+ -- class or instance head, and (2) those bound by the promoted method's+ -- kind. This will be used in an outermost `forall` in the helper type+ -- family's standalone kind signature to specify the kinds of kind+ -- variables (when possible).+ all_meth_tvbs = cls_tvbs ++ full_meth_tvbs_without_cls_tvbs++ -- Promote the right-hand side of the helper. Note that we never partially+ -- apply the helper type family, and users will never invoke the helper+ -- directly. As such, there is no need to emit defunctionalization symbols for+ -- the helper type family.+ (pro_decs, _defun_decs, ann_rhs)+ <- promoteLetDecRHS (ClassMethodRHS all_meth_scoped_tvs all_meth_tvbs meth_arg_kis meth_res_ki) OMap.empty OMap.empty Nothing helperName meth_rhs- emitDecs (pro_decs ++ defun_decs)+ emitDecs pro_decs return ( DTySynInstD (DTySynEqn Nothing (foldType (DConT proName) family_args)- (foldApply (DConT helperDefunName) (map DVarT meth_arg_tvs)))+ (foldType (DConT proHelperName) family_args)) , ann_rhs- , DConT helperDefunName )+ , (proHelperName, []) ) where -- Promote the type of a class method. For a default method, "the type" is -- simply the type of the original method. For an instance method,@@ -504,7 +734,43 @@ -- the types in the instance head. (e.g., if you have `class C a` and -- `instance C T`, then the substitution [a |-> T] must be applied to the -- original method's type.)- promote_meth_ty :: PrM ([DKind], DKind)+ --+ -- This returns four things in a tuple:+ --+ -- 1. The set of scoped type variables from the class method signature or+ -- instance signature. If an instance method lacks an instance signature,+ -- this will be an empty set. These type variables will be brought into+ -- scope over the RHS of the method: see Note [Scoped type variables and+ -- class methods] in D.S.TH.Promote.Monad.+ --+ -- 2. The list of kind variable binders that are explicitly quantified by an+ -- outermost `forall` in the promoted type. If there is no such outermost+ -- `forall`, then this will be the empty list.+ --+ -- 3. The promoted argument kinds.+ --+ -- 4. The promoted result kind.+ --+ -- Note that:+ --+ -- * Ultimately, this information is used to compute a standalone kind+ -- signature for a "helper" type family which defines the promoted version+ -- of a class method default or instance method. Because users never+ -- invoke helper type families directly, it is not important to get the+ -- order of kind variables exactly right. As such, the list of kind+ -- variable binders can be in an unspecified order.+ --+ -- * The kind variable binders only include kind variables that are+ -- quantified by the /method/, not by the class or instance head. The+ -- variables bound by the class or instance head are added separately+ -- (see `all_meth_tvbs` above).+ --+ -- * The set of scoped type variable names will always be a subset of the+ -- names in the list of kind variable binders. We are using the kind+ -- variable binders primarily as a way to annotate the kinds of each+ -- variable, so it is possible for the helper type family to bind a kind+ -- variable in a `forall` without it scoping over the body.+ promote_meth_ty :: PrM (OSet LocalVar, [DTyVarBndrSpec], [DKind], DKind) promote_meth_ty = case meth_sort of DefaultMethods ->@@ -518,28 +784,33 @@ -- We have an InstanceSig. These are easy: we can just use the -- instance signature's type directly, and no substitution for -- class variables is required.- (_tvbs, arg_kis, res_ki) <- promoteUnraveled ty- pure (arg_kis, res_ki)+ (kvbs, arg_kis, res_ki) <- promoteUnraveled ty+ pure (OSet.fromList (map tvbToLocalVar kvbs), kvbs, arg_kis, res_ki) Nothing -> do -- We don't have an InstanceSig, so we must compute the kind to use -- ourselves.- (arg_kis, res_ki) <- lookup_meth_ty+ (_, kvbs, arg_kis, res_ki) <- lookup_meth_ty -- Substitute for the class variables in the method's type. -- See Note [Promoted class method kinds]- let arg_kis' = map (substKind cls_subst) arg_kis- res_ki' = substKind cls_subst res_ki- pure (arg_kis', res_ki')+ let kvbs' = mapDTVKind (SC.substTy cls_subst) <$> kvbs+ arg_kis' = map (SC.substTy cls_subst) arg_kis+ res_ki' = SC.substTy cls_subst res_ki+ -- If there is no instance signature, then there are no additional+ -- type variables to bring into scope, so return an empty set of+ -- scoped type variables. We will reuse the list of kind variable+ -- binders in case they have useful kind information.+ pure (OSet.empty, kvbs', arg_kis', res_ki') -- Attempt to look up a class method's original type.- lookup_meth_ty :: PrM ([DKind], DKind)+ lookup_meth_ty :: PrM (OSet LocalVar, [DTyVarBndrSpec], [DKind], DKind) lookup_meth_ty = do opts <- getOptions let proName = promotedTopLevelValueName opts meth_name case OMap.lookup meth_name orig_sigs_map of Just ty -> do -- The type of the method is in scope, so promote that.- (_tvbs, arg_kis, res_ki) <- promoteUnraveled ty- pure (arg_kis, res_ki)+ (kvbs, arg_kis, res_ki) <- promoteUnraveled ty+ pure (OSet.fromList (map tvbToLocalVar kvbs), kvbs, arg_kis, res_ki) Nothing -> do -- If the type of the method is not in scope, the only other option -- is to try reifying the promoted method name.@@ -549,7 +820,14 @@ Just (DTyConI (DOpenTypeFamilyD (DTypeFamilyHead _ tvbs mb_res_ki _)) _) -> let arg_kis = map (defaultMaybeToTypeKind . extractTvbKind) tvbs res_ki = defaultMaybeToTypeKind (resultSigToMaybeKind mb_res_ki)- in pure (arg_kis, res_ki)+ -- If there is no instance signature, then there are no+ -- additional type variables to bring into scope, so return an+ -- empty set of scoped type variables. Moreover, we do not+ -- have a list of kind variable binders readily available, so+ -- we return an empty list. This is OK, as we will compute+ -- the kind variable binders for the helper type family+ -- elsewhere (see `full_meth_tvbs` above).+ in pure (OSet.empty, [], arg_kis, res_ki) _ -> fail $ "Cannot find type annotation for " ++ show proName {-@@ -591,14 +869,14 @@ promoteLetDecEnv mb_let_uniq (LetDecEnv { lde_defns = value_env , lde_types = type_env , lde_infix = fix_env }) = do- infix_decls <- mapMaybeM (uncurry (promoteInfixDecl mb_let_uniq)) $+ infix_decls <- mapMaybeM (\(n, (f, ns)) -> promoteInfixDecl mb_let_uniq n f ns) $ OMap.assocs fix_env -- promote all the declarations, producing annotated declarations let (names, rhss) = unzip $ OMap.assocs value_env (pro_decs, defun_decss, ann_rhss) <- fmap unzip3 $- zipWithM (promoteLetDecRHS LetBindingRHS type_env fix_env mb_let_uniq)+ zipWithM (promoteLetDecRHS LetBindingRHS type_env (fmap fst fix_env) mb_let_uniq) names rhss emitDecs $ concat defun_decss@@ -615,8 +893,15 @@ -- Promote a fixity declaration. promoteInfixDecl :: forall q. OptionsMonad q- => Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)-promoteInfixDecl mb_let_uniq name fixity = do+ => Maybe Uniq -> Name -> Fixity+ -> NamespaceSpecifier+ -- The namespace specifier for the fixity declaration. We+ -- only pass this for the sake of checking if we need to+ -- avoid promoting a fixity declaration (see `promote_val`+ -- below). The actual namespace used in the promoted fixity+ -- declaration will always be `type`.+ -> q (Maybe DDec)+promoteInfixDecl mb_let_uniq name fixity ns = do opts <- getOptions fld_sels <- qIsExtEnabled LangExt.FieldSelectors mb_ns <- reifyNameSpace name@@ -635,9 +920,10 @@ -> finish $ promotedClassName opts name _ -> never_mind where- -- Produce the fixity declaration.+ -- Produce the fixity declaration. Promoted names always inhabit the `type`+ -- namespace (i.e., `TypeNamespaceSpecifier`). finish :: Name -> q (Maybe DDec)- finish = pure . Just . DLetDec . DInfixD fixity NoNamespaceSpecifier+ finish = pure . Just . DLetDec . DInfixD fixity TypeNamespaceSpecifier -- Don't produce a fixity declaration at all. This can happen in the -- following circumstances:@@ -653,16 +939,23 @@ never_mind = pure Nothing -- Certain value names do not change when promoted (e.g., infix names).- -- Therefore, don't bother promoting their fixity declarations if- -- 'genQuotedDecs' is set to 'True', since that will run the risk of- -- generating duplicate fixity declarations.+ -- Therefore, don't bother promoting their fixity declarations if the+ -- following hold:+ --+ -- - 'genQuotedDecs' is set to 'True'.+ --+ -- - The name lacks an explicit namespace specifier.+ --+ -- Doing so will run the risk of generating duplicate fixity declarations. -- See Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1. promote_val :: q (Maybe DDec) promote_val = do opts <- getOptions let promoted_name :: Name promoted_name = promotedValueName opts name mb_let_uniq- if nameBase name == nameBase promoted_name && genQuotedDecs opts+ if nameBase name == nameBase promoted_name+ && genQuotedDecs opts+ && ns == NoNamespaceSpecifier then never_mind else finish promoted_name @@ -679,7 +972,15 @@ mFixity <- qReifyFixity name case mFixity of Nothing -> pure Nothing- Just fixity -> promoteInfixDecl Nothing name fixity+ -- NB: We don't have a NamespaceSpecifier in hand here. We could try+ -- to look one up, but it doesn't actually matter which namespace we+ -- pass here. If we reach this point in the code, we know we have a+ -- non-quoted Name (as reification would failed earlier if the Name+ -- were quoted). As such, the special case described in+ -- [singletons-th and fixity declarations] in D.S.TH.Single.Fixity,+ -- wrinkle 1 won't apply, and we only pass a namespace specifier for+ -- the sake of checking this special case.+ Just fixity -> promoteInfixDecl Nothing name fixity NoNamespaceSpecifier -- Which sort of let-bound declaration's right-hand side is being promoted? data LetDecRHSSort@@ -688,8 +989,19 @@ -- The right-hand side of a class method (either a default method or a -- method in an instance declaration). | ClassMethodRHS- [DKind] DKind- -- The RHS's promoted argument and result types. Needed to fix #136.+ (OSet LocalVar)+ -- The scoped type variables to bring into scope over+ -- the RHS of the class method. See+ -- Note [Scoped type variables and class methods]+ -- in D.S.TH.Promote.Monad.+ [DTyVarBndrSpec]+ -- The RHS's kind variable binders. Note that we do not+ -- guarantee a particular order for these binders (see+ -- Note [Promoted class methods and kind variable ordering]),+ -- as we are mainly using kind variable binders for the sake+ -- of annotating variables with their kinds.+ [DKind] -- The RHS's promoted argument kinds. Needed to fix #136.+ DKind -- The RHS's promoted result kind. Needed to fix #136. deriving Show -- This function is used both to promote class method defaults and normal@@ -724,7 +1036,7 @@ UFunction clauses -> promote_function_rhs all_locals clauses where -- Promote the RHS of a UFunction (or a UValue with a function type).- promote_function_rhs :: [Name]+ promote_function_rhs :: [LocalVar] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS) promote_function_rhs all_locals clauses = do numArgs <- count_args clauses@@ -742,7 +1054,7 @@ -- -- * For UFunctions, `prom_a` is [DTySynEqn] and `a` is [DClause]. promote_let_dec_rhs- :: [Name] -- Local variables bound in this scope+ :: [LocalVar] -- Local variables bound in this scope -> Maybe LetDecRHSKindInfo -- Information about the promoted kind (if present) -> Int -- The number of promoted function arguments -> PrM (prom_a, a) -- Promote the RHS@@ -754,7 +1066,6 @@ opts <- getOptions tyvarNames <- replicateM ty_num_args (qNewName "a") let proName = promotedValueName opts name mb_let_uniq- local_tvbs = map (`DPlainTV` BndrReq) all_locals m_fixity = OMap.lookup name fix_env mk_tf_head :: [DTyVarBndrVis] -> DFamilyResultSig -> DTypeFamilyHead@@ -769,19 +1080,18 @@ let arg_tvbs = map (`DPlainTV` BndrReq) tyvarNames in ( OSet.empty , Nothing- , DefunNoSAK (local_tvbs ++ arg_tvbs) Nothing+ , DefunNoSAK all_locals arg_tvbs Nothing , mk_tf_head arg_tvbs DNoSig ) -- 2. We have some kind information in the form of a LetDecRHSKindInfo.- Just (LDRKI m_sak tvbs argKs resK) ->- let arg_tvbs = zipWith (`DKindedTV` BndrReq) tyvarNames argKs- lde_kvs_to_bind' = OSet.fromList (map extractTvbName tvbs) in+ Just (LDRKI m_sak lde_kvs_to_bind' tvbs argKs resK) ->+ let arg_tvbs = zipWith (`DKindedTV` BndrReq) tyvarNames argKs in case m_sak of -- 2(a). We do not have a standalone kind signature. Nothing -> ( lde_kvs_to_bind' , Nothing- , DefunNoSAK (local_tvbs ++ arg_tvbs) (Just resK)+ , DefunNoSAK all_locals arg_tvbs (Just resK) , mk_tf_head arg_tvbs (DKindSig resK) ) -- 2(b). We have a standalone kind signature.@@ -794,7 +1104,7 @@ toposortTyVarsOf (argKs ++ [resK]) | otherwise = tvbs- arg_tvbs' = tvbSpecsToBndrVis tvbs' ++ arg_tvbs in+ arg_tvbs' = dtvbSpecsToBndrVis tvbs' ++ arg_tvbs in ( lde_kvs_to_bind' , Just $ DKiSigD proName sak , DefunSAK sak@@ -813,7 +1123,8 @@ , defun_decs , mk_alet_dec_rhs thing ) - promote_let_dec_ty :: [Name] -- The local variables that the let-dec closes+ promote_let_dec_ty :: [LocalVar]+ -- The local variables that the let-dec closes -- over. If this is non-empty, we cannot -- produce a standalone kind signature. -- See Note [No SAKs for let-decs with local variables]@@ -833,15 +1144,9 @@ -- will default to the earlier Int argument. promote_let_dec_ty all_locals default_num_args = case rhs_sort of- ClassMethodRHS arg_kis res_ki- -> -- For class method RHS helper functions, don't bother quantifying- -- any type variables in their SAKS. We could certainly try, but- -- given that these functions are only used internally, there's no- -- point in trying to get the order of type variables correct,- -- since we don't apply these functions with visible kind- -- applications.- let sak = ravelVanillaDType [] [] arg_kis res_ki in- return (Just (LDRKI (Just sak) [] arg_kis res_ki), length arg_kis)+ ClassMethodRHS scoped_tvs tvbs arg_kis res_ki+ -> let sak = ravelVanillaDType tvbs [] arg_kis res_ki in+ return (Just (LDRKI (Just sak) scoped_tvs tvbs arg_kis res_ki), length arg_kis) LetBindingRHS | Just ty <- OMap.lookup name type_env -> do@@ -853,8 +1158,15 @@ -- don't give it a SAK. -- See Note [No SAKs for let-decs with local variables] | otherwise = Nothing+ -- If ScopedTypeVariables is enabled, bring all of the type variables+ -- from the outermost forall into scope over the RHS.+ scoped_tvs_ext <- qIsExtEnabled LangExt.ScopedTypeVariables+ let scoped_tvs | scoped_tvs_ext+ = OSet.fromList (map tvbToLocalVar tvbs)+ | otherwise+ = OSet.empty -- invariant: count_args ty == length argKs- return (Just (LDRKI m_sak tvbs argKs resultK), length argKs)+ return (Just (LDRKI m_sak scoped_tvs tvbs argKs resultK), length argKs) | otherwise -> return (Nothing, default_num_args)@@ -868,7 +1180,7 @@ return $ DClause (pats ++ newPats) (foldExp exp newArgs) | otherwise = do -- Eta-contract let (clausePats, lamPats) = splitAt ty_num_args pats- lamExp <- mkDLamEFromDPats lamPats exp+ lamExp = dLamE lamPats exp return $ DClause clausePats lamExp where n = ty_num_args - clause_num_args@@ -885,6 +1197,13 @@ -- This will be Nothing if the let-dec RHS has local -- variables that it closes over. -- See Note [No SAKs for let-decs with local variables]+ (OSet LocalVar) -- The scoped type variables to bring into scope over+ -- the RHS of the let-dec. This will be a subset of the+ -- type variables of the kind (see the field below),+ -- but not necessarily the same. See+ -- Note [Scoped type variables and class methods]+ -- (Wrinkle: Partial scoping) in D.S.TH.Promote.Monad+ -- for an example where this can be a proper subset. [DTyVarBndrSpec] -- The type variable binders of the kind. [DKind] -- The argument kinds. DKind -- The result kind.@@ -1014,7 +1333,7 @@ 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+Note that we do not bind @b here. The `dtvbSpecsToBndrVis` function is responsible for filtering out inferred type variable binders. -} @@ -1024,22 +1343,32 @@ -- ^ Name of the function being promoted -> Maybe LetDecRHSKindInfo -- ^ Information about the promoted kind (if present)- -> [Name]+ -> [LocalVar] -- ^ The local variables currently in scope -> DClause -> PrM (DTySynEqn, ADClause) promoteClause mb_let_uniq name m_ldrki all_locals (DClause pats exp) = do- -- promoting the patterns creates variable bindings. These are passed- -- to the function promoted the RHS- ((types, pats'), prom_pat_infos) <- evalForPair $ mapAndUnzipM promotePat pats+ -- First, check to see if we know the kinds of the patterns in the clause...+ let m_kinds = fmap (\(LDRKI _ _ _ kinds _) -> kinds) m_ldrki+ -- ...if so, use these kinds when promoting the patterns to the type level.+ -- Promoting patterns can create LocalVars, and these LocalVars are brought+ -- into scope when promoting the RHS of the clause. Recording the kinds of+ -- each LocalVar will make the lambda-lifted code more precise. (See+ -- Note [Local variables and kind information] in+ -- D.S.TH.Promote.Syntax.LocalVar.)+ ((types, pats'), prom_pat_infos) <- evalForPair $+ case m_kinds of+ Just kinds ->+ unzip <$> zipWithM (\kind -> promotePat (Just kind)) kinds pats+ Nothing ->+ mapAndUnzipM (promotePat Nothing) pats -- If the function has scoped type variables, then we annotate each argument -- in the promoted type family equation with its kind. -- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad for an -- explanation of why we do this.- scoped_tvs <- qIsExtEnabled LangExt.ScopedTypeVariables let types_w_kinds = case m_ldrki of- Just (LDRKI _ tvbs kinds _)- | not (null tvbs) && scoped_tvs+ Just (LDRKI _ scoped_tvs _ kinds _)+ | not (OSet.null scoped_tvs) -> zipWith DSigT types kinds _ -> types let PromDPatInfos { prom_dpat_vars = new_vars@@ -1051,35 +1380,29 @@ return ( DTySynEqn Nothing (foldType pro_clause_fun types_w_kinds) ty , ADClause new_vars pats' ann_exp ) -promoteMatch :: DType -- What to use as the LHS of the promoted type family- -- equation. This should consist of the promoted name of- -- the case expression to which the match belongs, applied- -- to any local arguments (e.g., `Case x y z`).- -> DMatch -> PrM (DTySynEqn, ADMatch)-promoteMatch pro_case_fun (DMatch pat exp) = do- -- promoting the patterns creates variable bindings. These are passed- -- to the function promoted the RHS- ((ty, pat'), prom_pat_infos) <- evalForPair $ promotePat pat- let PromDPatInfos { prom_dpat_vars = new_vars- , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos- (rhs, ann_exp) <- scopedBind sig_kvs $- lambdaBind new_vars $- promoteExp exp- return $ ( DTySynEqn Nothing (pro_case_fun `DAppT` ty) rhs- , ADMatch new_vars pat' ann_exp)---- promotes a term pattern into a type pattern, accumulating bound variable names-promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)-promotePat (DLitP lit) = (, ADLitP lit) <$> promoteLitPat lit-promotePat (DVarP name) = do+-- | Promote a term pattern into a type pattern, accumulating bound variable+-- names in 'PromDPatInfos'.+promotePat ::+ Maybe DKind+ -- ^ The kind of the pattern ('Just' if known, 'Nothing' if unknown). When+ -- the kind is known, we can record a 'LocalVar' for variable patterns (see+ -- the 'DVarP' case below) that includes more precise kind information. See+ -- @Note [Local variables and kind information] (Wrinkle: Binding positions+ -- versus argument positions)@ in+ -- "Data.Singletons.TH.Promote.Syntax.LocalVar" for more information.+ -> DPat+ -> QWithAux PromDPatInfos PrM (DType, ADPat)+promotePat _ (DLitP lit) = (, ADLitP lit) <$> promoteLitPat lit+promotePat m_ki (DVarP name) = do -- term vars can be symbols... type vars can't! tyName <- mkTyName name- tell $ PromDPatInfos [(name, tyName)] OSet.empty+ let lv = LocalVar { lvName = tyName, lvKind = m_ki }+ tell $ PromDPatInfos [(name, lv)] OSet.empty return (DVarT tyName, ADVarP name)-promotePat (DConP name tys pats) = do+promotePat _ (DConP name tys pats) = do opts <- getOptions kis <- traverse (promoteType_options conOptions) tys- (types, pats') <- mapAndUnzipM promotePat pats+ (types, pats') <- mapAndUnzipM (promotePat Nothing) pats let name' = promotedDataTypeOrConName opts name return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats') where@@ -1088,24 +1411,27 @@ -- will produce code that GHC will accept. conOptions :: PromoteTypeOptions conOptions = defaultPromoteTypeOptions{ptoAllowWildcards = True}-promotePat (DTildeP pat) = do+promotePat m_ki (DTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern in promotion"- second ADTildeP <$> promotePat pat-promotePat (DBangP pat) = do+ second ADTildeP <$> promotePat m_ki pat+promotePat m_ki (DBangP pat) = do qReportWarning "Strict pattern converted into regular pattern in promotion"- second ADBangP <$> promotePat pat-promotePat (DSigP pat ty) = do+ second ADBangP <$> promotePat m_ki pat+promotePat _ (DSigP pat ty) = do -- We must maintain the invariant that any promoted pattern signature must -- not have any wildcards in the underlying pattern. -- See Note [Singling pattern signatures]. wildless_pat <- removeWilds pat- (promoted, pat') <- promotePat wildless_pat ki <- promoteType ty- tell $ PromDPatInfos [] (fvDType ki)+ (promoted, pat') <- promotePat (Just ki) wildless_pat+ tell $ PromDPatInfos []+ $ OSet.fromList+ $ map tvbToLocalVar+ $ toposortTyVarsOf [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)+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@@ -1121,40 +1447,30 @@ promoteExp (DAppTypeE exp _) = do qReportWarning "Visible type applications are ignored by `singletons-th`." promoteExp exp-promoteExp (DLamE names exp) = do+promoteExp (DLamCasesE clauses) = do opts <- getOptions- lambdaName <- newUniqueName "Lambda"- tyNames <- mapM mkTyName names- let var_proms = zip names tyNames- (rhs, ann_exp) <- lambdaBind var_proms $ promoteExp exp- all_locals <- allLocals- let tvbs = map (`DPlainTV` BndrReq) tyNames- all_args = all_locals ++ tyNames- all_tvbs = map (`DPlainTV` BndrReq) all_args- tfh = dTypeFamilyHead_with_locals lambdaName all_locals tvbs DNoSig- emitDecs [DClosedTypeFamilyD- tfh- [DTySynEqn Nothing- (foldType (DConT lambdaName) (map DVarT all_args))- rhs]]- emitDecsM $ defunctionalize lambdaName Nothing $ DefunNoSAK all_tvbs Nothing- let promLambda = foldApply (DConT (defunctionalizedName opts lambdaName 0))- (map DVarT all_locals)- return (promLambda, ADLamE tyNames promLambda names ann_exp)-promoteExp (DCaseE exp matches) = do- caseTFName <- newUniqueName "Case"+ lam_cases_tf_name <- newUniqueName "LamCases" all_locals <- allLocals- let prom_case = foldType (DConT caseTFName) (map DVarT all_locals)- (exp', ann_exp) <- promoteExp exp- (eqns, ann_matches) <- mapAndUnzipM (promoteMatch prom_case) matches- tyvarName <- qNewName "t"- let tvbs = [DPlainTV tyvarName BndrReq]- tfh = dTypeFamilyHead_with_locals caseTFName all_locals tvbs DNoSig+ (eqns, ann_clauses) <-+ mapAndUnzipM (promoteClause Nothing lam_cases_tf_name Nothing all_locals) clauses+ -- Per the Haddocks for DLamCasesE, an empty list of clauses indicates that+ -- the overall `\cases` expression takes one argument. Otherwise, we look at+ -- the first clause to see how many arguments the expression takes, as each+ -- clause is required to have the same number of patterns.+ let num_args =+ case clauses of+ [] -> 1+ DClause pats _ : _ -> length pats+ arg_tvb_names <- replicateM num_args (newUniqueName "a")+ let arg_tvbs = map (`DPlainTV` BndrReq) arg_tvb_names+ tfh = dTypeFamilyHead_with_locals lam_cases_tf_name all_locals arg_tvbs DNoSig emitDecs [DClosedTypeFamilyD tfh eqns]- -- See Note [Annotate case return type] in Single- let applied_case = prom_case `DAppT` exp'- return ( applied_case- , ADCaseE ann_exp ann_matches applied_case )+ emitDecsM $ defunctionalize lam_cases_tf_name Nothing $ DefunNoSAK all_locals arg_tvbs Nothing+ let prom_lam_cases =+ foldTypeLocalVars+ (DConT (defunctionalizedName opts lam_cases_tf_name 0))+ all_locals+ pure (prom_lam_cases, ADLamCasesE num_args prom_lam_cases ann_clauses) promoteExp (DLetE decs exp) = do unique <- qNewUnique (binds, ann_env) <- promoteLetDecs (Just unique) decs@@ -1164,10 +1480,12 @@ (exp', ann_exp) <- promoteExp exp ty' <- promoteType ty return (DSigT exp' ty', ADSigE exp' ann_exp ty')-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)+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)+promoteExp e@(DForallE {}) = fail ("Embedded `forall` expressions cannot be promoted: " ++ show e)+promoteExp e@(DConstrainedE {}) = fail ("Embedded constraint expressions cannot be promoted: " ++ show e) promoteLitExp :: OptionsMonad q => Lit -> q DType promoteLitExp (IntegerL n) = do@@ -1213,7 +1531,7 @@ -- ^ Name of the function being promoted -> Maybe LetDecRHSKindInfo -- ^ Information about the promoted kind (if present)- -> [Name]+ -> [LocalVar] -- ^ The local variables currently in scope -> PrM DType promoteLetDecName mb_let_uniq name m_ldrki all_locals = do@@ -1221,12 +1539,12 @@ let proName = promotedValueName opts name mb_let_uniq type_args = case m_ldrki of- Just (LDRKI m_sak tvbs _ _)+ 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. Convert the scoped type variables -- `tvbs` to invisible arguments, making sure to use- -- `tvbSpecsToBndrVis` to filter out any inferred type variable+ -- `dtvbSpecsToBndrVis` 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@@ -1240,10 +1558,10 @@ -- -- 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+ -> map dTyVarBndrVisToDTypeArg $ dtvbSpecsToBndrVis tvbs _ -> -- ...otherwise, return the local variables as explicit arguments -- using DTANormal.- map (DTANormal . DVarT) all_locals+ map localVarToTypeArg all_locals pure $ applyDType (DConT proName) type_args -- Construct a 'DTypeFamilyHead' that closes over some local variables. We@@ -1252,30 +1570,32 @@ dTypeFamilyHead_with_locals :: Name -- ^ Name of type family- -> [Name]+ -> [LocalVar] -- ^ Local variables -> [DTyVarBndrVis] -- ^ Variables for type family arguments -> DFamilyResultSig -- ^ Type family result -> DTypeFamilyHead-dTypeFamilyHead_with_locals tf_nm local_nms arg_tvbs res_sig =+dTypeFamilyHead_with_locals tf_nm local_vars arg_tvbs res_sig = DTypeFamilyHead tf_nm- (map (`DPlainTV` BndrReq) local_nms' ++ arg_tvbs')+ (map (localVarToTvb BndrReq) local_vars' ++ arg_tvbs') res_sig' Nothing where- -- We take care to only apply `noExactName` to the local variables and not+ -- We take care to only apply `noExactTyVars` to the local variables and not -- to any of the argument/result types. The latter are much more likely to- -- show up in the Haddocks, and `noExactName` produces incredibly long Names- -- that are much harder to read in the rendered Haddocks.- local_nms' = map noExactName local_nms+ -- show up in the Haddocks, and `noExactTyVars` produces incredibly long+ -- Names that are much harder to read in the rendered Haddocks.+ local_vars' = noExactTyVars local_vars -- Ensure that all references to local_nms are substituted away. subst1 = Map.fromList $- zipWith (\local_nm local_nm' -> (local_nm, DVarT local_nm'))- local_nms- local_nms'- (subst2, arg_tvbs') = substTvbs subst1 arg_tvbs+ zipWith+ (\(LocalVar { lvName = local_nm }) (LocalVar { lvName = local_nm' }) ->+ (local_nm, DVarT local_nm'))+ local_vars+ local_vars'+ (subst2, arg_tvbs') = SC.substTyVarBndrs subst1 arg_tvbs (_subst3, res_sig') = substFamilyResultSig subst2 res_sig
src/Data/Singletons/TH/Promote/Defun.hs view
@@ -172,7 +172,7 @@ let defun = defunctionalize name m_fixity case m_sak of Just sak -> defun $ DefunSAK sak- Nothing -> defun $ DefunNoSAK tvbs m_res_kind+ Nothing -> defun $ DefunNoSAK [] tvbs m_res_kind -- Generate symbol data types, Apply instances, and other declarations required -- for defunctionalization.@@ -190,13 +190,13 @@ -- If the kind isn't vanilla, use the fallback approach. -- See Note [Defunctionalization game plan], -- Wrinkle 2: Non-vanilla kinds.- Left _ -> defun_fallback [] (Just sak)+ Left _ -> defun_fallback [] [] (Just sak) -- Otherwise, proceed with defun_vanilla_sak. Right (sak_tvbs, _sak_cxt, sak_arg_kis, sak_res_ki) -> defun_vanilla_sak sak_tvbs sak_arg_kis sak_res_ki -- If a declaration lacks a SAK, it likely has a partial kind. -- See Note [Defunctionalization game plan], Wrinkle 1: Partial kinds.- DefunNoSAK tvbs m_res -> defun_fallback tvbs m_res+ DefunNoSAK locals tvbs m_res -> defun_fallback locals tvbs m_res where -- Generate defunctionalization symbols for things with vanilla SAKs. -- The symbols themselves will also be given SAKs.@@ -275,12 +275,15 @@ 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- tyfun = buildTyFunArrow (snd res_nk) res_ki+ let (tyfun_res_ki, decs) = go (n+1) (arg_nks ++ [res_nk]) res_nks+ tyfun_arg_ki = snd res_nk+ tyfun = buildTyFunArrow tyfun_arg_ki tyfun_res_ki defun_sak_dec = mk_sak_dec tyfun defun_other_decs = mk_defun_decs opts n sak_arg_n arg_tvbs (fst res_nk)- extra_name (Just tyfun)+ (Just tyfun_arg_ki)+ (Just tyfun_res_ki)+ extra_name in (tyfun, defun_sak_dec:defun_other_decs ++ decs) pure $ snd $ go 0 [] $ zip arg_names sak_arg_kis@@ -291,12 +294,13 @@ -- (see Note [Defunctionalization game plan], Wrinkle 1: Partial kinds) -- or a non-vanilla kind -- (see Note [Defunctionalization game plan], Wrinkle 2: Non-vanilla kinds).- defun_fallback :: [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]- defun_fallback tvbs' m_res' = do+ defun_fallback :: [LocalVar] -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]+ defun_fallback locals tvbs' m_res' = do opts <- getOptions extra_name <- qNewName "arg" -- Use noExactTyVars below to avoid GHC#11812. -- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util.+ let locals' = noExactTyVars locals (tvbs, m_res) <- eta_expand (noExactTyVars tvbs') (noExactTyVars m_res') let tvbs_n = length tvbs@@ -323,17 +327,20 @@ -- the result kind is not always fully known. go :: Int -> [DTyVarBndrVis] -> [DTyVarBndrVis] -> (Maybe DKind, [DDec]) go n arg_tvbs res_tvbss =+ let all_tvbs = map (localVarToTvb BndrReq) locals' ++ arg_tvbs in case res_tvbss of [] ->- let sat_decs = mk_sat_decs opts n [] arg_tvbs m_res+ let sat_decs = mk_sat_decs opts n [] all_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- m_tyfun = buildTyFunArrow_maybe (extractTvbKind res_tvb)- m_res_ki- defun_decs' = mk_defun_decs opts n tvbs_n arg_tvbs- (extractTvbName res_tvb)- extra_name m_tyfun+ let (m_tyfun_res_ki, decs) = go (n+1) (arg_tvbs ++ [res_tvb]) res_tvbs+ m_tyfun_arg_ki = extractTvbKind res_tvb+ m_tyfun = buildTyFunArrow_maybe m_tyfun_arg_ki+ m_tyfun_res_ki+ defun_decs' = mk_defun_decs opts n tvbs_n all_tvbs+ (extractTvbName res_tvb)+ m_tyfun_arg_ki m_tyfun_res_ki+ extra_name in (m_tyfun, defun_decs' ++ decs) pure $ snd $ go 0 [] tvbs@@ -343,10 +350,11 @@ -> Int -> [DTyVarBndrVis] -> Name- -> Name -> Maybe DKind+ -> Maybe DKind+ -> Name -> [DDec]- mk_defun_decs opts n fully_sat_n arg_tvbs tyfun_name extra_name m_tyfun =+ mk_defun_decs opts n fully_sat_n arg_tvbs tyfun_name m_tyfun_arg_ki m_tyfun_res_ki extra_name = let data_name = defunctionalizedName opts name n next_name = defunctionalizedName opts name (n+1) con_name = prefixName "" ":" $ suffixName "KindInference" "###" data_name@@ -360,12 +368,23 @@ (foldTypeTvbs (DConT data_name) params) data_decl = DDataD Data [] data_name args m_tyfun [con_decl] [] where+ m_tyfun = buildTyFunArrow_maybe m_tyfun_arg_ki m_tyfun_res_ki+ args | isJust m_tyfun = arg_tvbs | otherwise = params app_data_ty = foldTypeTvbs (DConT data_name) arg_tvbs app_eqn = DTySynEqn Nothing- (DConT applyName `DAppT` app_data_ty- `DAppT` DVarT tyfun_name)+ (DConT applyName+ -- If possible, specify kind arguments to+ -- Apply using explicit kind applications,+ -- falling back on type wildcards when the+ -- kinds are not known. See+ -- Note [Defunctionalization game plan],+ -- Wrinkle 2: Non-vanilla kinds.+ `DAppKindT` fromMaybe DWildCardT m_tyfun_arg_ki+ `DAppKindT` fromMaybe DWildCardT m_tyfun_res_ki+ `DAppT` app_data_ty+ `DAppT` DVarT tyfun_name) (foldTypeTvbs (DConT app_eqn_rhs_name) params) -- If the next defunctionalization symbol is fully saturated, then -- use the original declaration name instead.@@ -406,7 +425,7 @@ let sat_name = defunctionalizedName opts name n sat_dec = DClosedTypeFamilyD (DTypeFamilyHead sat_name- (tvbSpecsToBndrVis sat_tvbs ++ sat_args)+ (dtvbSpecsToBndrVis sat_tvbs ++ sat_args) (maybeKindToResultSig m_sat_res) Nothing) [DTySynEqn Nothing (foldTypeTvbs (DConT sat_name) sat_args)@@ -443,7 +462,7 @@ (noExactName <$> qNewName "e") mk_fix_decl :: Name -> Fixity -> DDec- mk_fix_decl n f = DLetDec $ DInfixD f NoNamespaceSpecifier n+ mk_fix_decl n f = DLetDec $ DInfixD f TypeNamespaceSpecifier n -- Indicates whether the type being defunctionalized has a standalone kind -- signature. If it does, DefunSAK contains the kind. If not, DefunNoSAK@@ -452,8 +471,15 @@ -- See Note [Defunctionalization game plan] for details on how this -- information is used. data DefunKindInfo- = DefunSAK DKind- | DefunNoSAK [DTyVarBndrVis] (Maybe DKind)+ = -- The thing being defunctionalized has a standalone kind signature.+ DefunSAK DKind+ -- The thing being defunctionalized does not have a standalone kind+ -- signature. See Note [Defunctionalization game plan] (Wrinkle 1: Partial+ -- kinds) for examples.+ | DefunNoSAK+ [LocalVar] -- The local variables currently in scope+ [DTyVarBndrVis] -- The arguments, along with their kinds (if known)+ (Maybe DKind) -- The result kind (if known) -- Shorthand for building (k1 ~> k2) buildTyFunArrow :: DKind -> DKind -> DKind@@ -520,10 +546,10 @@ to as "fully saturated" defunctionalization symbols. See Note [Fully saturated defunctionalization symbols]. -* If Foo had a fixity declaration (e.g., infixl 4 `Foo`), then we would also- generate fixity declarations for each defunctionalization symbol (e.g.,- infixl 4 `FooSym0`).- See Note [Fixity declarations for defunctionalization symbols].+* If Foo had a fixity declaration (e.g., infixl 4 type `Foo`), then we would+ also generate fixity declarations for each defunctionalization symbol (e.g.,+ infixl 4 type `FooSym0`). See Note [Fixity declarations for+ defunctionalization symbols]. * Foo has a vanilla kind signature. (See Note [Vanilla-type validity checking during promotion] in D.S.TH.Promote.Type@@ -604,6 +630,46 @@ data BarSym2 x (y :: Nat) :: Nat ~> Nat where ... type family BarSym3 x (y :: Nat) (z :: Nat) :: Nat where ... +A variation on this theme is local definitions, such as `x` in this definition:++ $(singletons+ [d| f :: forall a b c. a -> Either a (b, c)+ f x = let g y = Left y :: Either a (b, c)+ in g x+ |])++Because `a`, `b`, and `c` scope over the right-hand side of `f`, they must be in+scope in the definition of `g`. As such, we will promote `g` to the following+type family:++ type LetG a b c x y where+ LetG a b c x y = Left y :: Either a (b, c)++How should we defunctionalize LetG? It's tempting to do this:++ data LetGSym0 f+ data LetGSym1 a f+ data LetGSym2 a b f+ data LetGSym3 a b c f+ data LetGSym4 a b c x f+ type family LetGSym5 a b c x y where ...++Doing so would be somewhat wasteful, however. This is because `a`, `b`, `c`,+and `x` are local variables, and as such, we will /always/ fully apply them to+LetG's defunctionalization symbols. That is to say: there is never a situation+where we will need to partially apply LetG at 0, 1, 2, or 3 arguments. This+means that we can get away with a much simpler approach:++ data LetGSym0 a b c x f+ type family LetGSym1 a b c x y where ...++Now there are only two defunctionalization-related definitions instead of a+whopping six. This means that the <N> in LetGSym<N> only refers to the number+of direct arguments to `g` in the original code, not including any local+variables currently in scope.++All of these cases are captured by the DefunNoSAK constructor of DefunKindInfo.+ ----- -- Wrinkle 2: Non-vanilla kinds -----@@ -676,10 +742,36 @@ type family QuuxSym2 (k :: Type) (x :: k) :: Type where ... The catch is that the kind of QuuxSym0, `forall k. Type ~> k ~> Type`, is-slightly more general than it ought to be. In practice, however, this is-unlikely to be a problem as long as you apply QuuxSym0 to arguments of the-right kinds.+slightly more general than it ought to be. In practice, however, this is not a+problem as long as we apply QuuxSym0 to arguments of the right kinds. In+particular, we must be careful when generating an `Apply` instance for+`QuuxSym0`. In particular, we do /not/ want to generate this instance: + type instance Apply QuuxSym0 k = QuuxSym1 k++When GHC kind-checks this instance, it will determine what the kind of the+right-hand side should be by only looking at the left-hand side. As a result,+GHC will conclude that the instance should have this shape:++ type instance Apply @Type @(k1 ~> Type) PSym0 k =+ QuuxSym1 k :: k1 ~> Type++Where `k1` is distinct from `k`. This is wrong, because `QuuxSym1 k` has kind+`k1 ~> Type`, not `k ~> Type`! As such, GHC would reject this instance.++The tricky part is that `QuuxSym0`'s kind does not require its second argument+to have the same kind as its first argument, so `Apply PSym0 k :: k1 ~> Type`+is the most general kind it can have. We want to prevent GHC from doing this+sort of kind generalization, so we instead generate this Apply instance:++ type instance Apply @Type @(k ~> Type) QuuxSym0 k = QuuxSym1 k++Now the right-hand side is required to have kind `k ~> Type`, and all is well.++Of course, not all Apply instances that we generate will know what kinds to use.+If we don't know what kinds to use, we generate `type instance Apply @_ @_ ...`+instead, using type wildcards to let GHC infer the kinds.+ Note [Fully saturated defunctionalization symbols] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When generating defunctionalization symbols, most of the symbols are data@@ -724,77 +816,23 @@ type ConstSym2 :: a -> b -> a type ConstSym2 x y = Const x y -This approach has various downsides which make it impractical:--* Type synonyms are often not expanded in the output of GHCi's :kind! command.- As issue #445 chronicles, this can significantly impact the readability of- even simple :kind! queries. It can be the difference between this:-- λ> :kind! Map IdSym0 '[1,2,3]- Map IdSym0 '[1,2,3] :: [Nat]- = 1 :@#@$$$ '[2, 3]-- And this:-- λ> :kind! Map IdSym0 '[1,2,3]- Map IdSym0 '[1,2,3] :: [Nat]- = '[1, 2, 3]-- Making fully saturated defunctionalization symbols like (:@#@$$$) type- families makes this issue moot, since :kind! always expands type families.-* There are a handful of corner cases where using type synonyms can actually- make fully saturated defunctionalization symbols fail to typecheck.- Here is one such corner case:-- $(promote [d|- class Applicative f where- pure :: a -> f a- ...- (*>) :: f a -> f b -> f b- |])-- ==>-- class PApplicative f where- type Pure (x :: a) :: f a- type (*>) (x :: f a) (y :: f b) :: f b-- What would happen if we were to defunctionalize the promoted version of (*>)?- We'd end up with the following defunctionalization symbols:-- type (*>@#@$) :: f a ~> f b ~> f b- data (*>@#@$) f where ...-- type (*>@#@$$) :: f a -> f b ~> f b- data (*>@#@$$) x f where ...-- type (*>@#@$$$) :: f a -> f b -> f b- type (*>@#@$$$) x y = (*>) x y+This approach has a downside which makes it impractical: type synonyms are+often not expanded in the output of GHCi's :kind! command. As issue #445+chronicles, this can significantly impact the readability of even simple :kind!+queries. It can be the difference between this: - It turns out, however, that (*>@#@$$$) will not kind-check. Because (*>@#@$$$)- has a standalone kind signature, it is kind-generalized *before* kind-checking- the actual definition itself. Therefore, the full kind is:+ λ> :kind! Map IdSym0 '[1,2,3]+ Map IdSym0 '[1,2,3] :: [Nat]+ = 1 :@#@$$$ '[2, 3] - type (*>@#@$$$) :: forall {k} (f :: k -> Type) (a :: k) (b :: k).- f a -> f b -> f b- type (*>@#@$$$) x y = (*>) x y+And this: - However, the kind of (*>) is- `forall (f :: Type -> Type) (a :: Type) (b :: Type). f a -> f b -> f b`.- This is not general enough for (*>@#@$$$), which expects kind-polymorphic `f`,- `a`, and `b`, leading to a kind error. You might think that we could somehow- infer this information, but note the quoted definition of Applicative (and- PApplicative, as a consequence) omits the kinds of `f`, `a`, and `b` entirely.- Unless we were to implement full-blown kind inference inside of Template- Haskell (which is a tall order), the kind `f a -> f b -> f b` is about as good- as we can get.+ λ> :kind! Map IdSym0 '[1,2,3]+ Map IdSym0 '[1,2,3] :: [Nat]+ = '[1, 2, 3] - Making (*>@#@$$$) a type family rather than a type synonym avoids this issue- since type family equations are allowed to match on kind arguments. In this- example, (*>@#@$$$) would have kind-polymorphic `f`, `a`, and `b` in its kind- signature, but its equation would implicitly equate `k` with `Type`. Note- that (*>@#@$) and (*>@#@$$), which are GADTs, also use a similar trick by- equating `k` with `Type` in their GADT constructors.+Making fully saturated defunctionalization symbols like (:@#@$$$) type families+makes this issue moot, since :kind! always expands type families. ----- -- Wrinkle: avoiding reduction stack overflows@@ -834,7 +872,7 @@ (.) :: (b -> c) -> (a -> b) -> (a -> c) (f . g) x = f (g x)- infixr 9 .+ infixr 9 data . One often writes (f . g . h) at the value level, but because (.) is promoted to a type family with three arguments, this doesn't directly translate to the@@ -843,6 +881,6 @@ f .@#@$$$ g .@#@$$$ h But in order to ensure that this associates to the right as expected, one must-generate an `infixr 9 .@#@#$$$` declaration. This is why defunctionalize accepts-a Maybe Fixity argument.+generate an `infixr 9 type .@#@#$$$` declaration. This is why defunctionalize+accepts a Maybe Fixity argument. -}
src/Data/Singletons/TH/Promote/Monad.hs view
@@ -30,10 +30,10 @@ -- environment during promotion data PrEnv = PrEnv { pr_options :: Options- , pr_scoped_vars :: OSet Name+ , pr_scoped_vars :: OSet LocalVar -- ^ The set of scoped type variables currently in scope. -- See @Note [Scoped type variables]@.- , pr_lambda_vars :: OMap Name Name+ , pr_lambda_vars :: OMap Name LocalVar -- ^ Map from term-level 'Name's of variables bound in lambdas and -- function clauses to their type-level counterparts. -- See @Note [Tracking local variables]@.@@ -65,7 +65,7 @@ getOptions = asks pr_options -- return *type-level* names-allLocals :: MonadReader PrEnv m => m [Name]+allLocals :: MonadReader PrEnv m => m [LocalVar] allLocals = do scoped <- asks (F.toList . pr_scoped_vars) lambdas <- asks (OMap.assocs . pr_lambda_vars)@@ -79,10 +79,10 @@ decs <- action emitDecs decs --- ^ Bring a list of type variables into scope for the duration the supplied+-- ^ Bring a set of type variables into scope for the duration the supplied -- computation. See @Note [Tracking local variables]@ and -- @Note [Scoped type variables]@.-scopedBind :: OSet Name -> PrM a -> PrM a+scopedBind :: OSet LocalVar -> PrM a -> PrM a scopedBind binds = local (\env@(PrEnv { pr_scoped_vars = scoped }) -> env { pr_scoped_vars = binds `OSet.union` scoped })@@ -95,13 +95,15 @@ , pr_local_vars = locals }) = -- Per Note [Tracking local variables], these will be added to both -- `pr_lambda_vars` and `pr_local_vars`.- let new_locals = OMap.fromList [ (tmN, DVarT tyN) | (tmN, tyN) <- binds ] in- env { pr_lambda_vars = OMap.fromList binds `OMap.union` lambdas- , pr_local_vars = new_locals `OMap.union` locals }+ let new_lambdas = OMap.fromList binds+ new_locals = fmap localVarToType new_lambdas in+ env { pr_lambda_vars = new_lambdas `OMap.union` lambdas+ , pr_local_vars = new_locals `OMap.union` locals } -- ^ A pair consisting of a term-level 'Name' of a variable, bound in a @let@--- binding or @where@ clause, and its type-level counterpart.--- See @Note [Tracking local variables]@.+-- binding or @where@ clause, and its type-level counterpart. The type will+-- always be a defunctionalization symbol so that it can be partially applied if+-- necessary. See @Note [Tracking local variables]@. type LetBind = (Name, DType) -- ^ Bring a list of 'LetBind's into scope for the duration the supplied@@ -432,4 +434,170 @@ type LetY x :: Maybe b where LetY x :: Maybe b = Nothing :: Maybe b++Note [Scoped type variables and class methods]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Implementing support for scoped type variables (see Note [Scoped type variables]+as a primer) in the type signatures of class methods is surprisingly tricky.+First, let's consider a small but illustrative example:++ class C a where+ m :: forall b. a -> b -> (a, b)+ m x y = (x, y) :: (a, b)++In the default implementation of `m`, there are /two/ levels of scoped type+variables:++* The `a` type variable from the `class C a` header.+* The `b` type variable from the method signature `forall b. a -> b -> (a, b)`++This means that in order to promote `m` to an associated type family, we need+to ensure that both `a` and `b` are brought into scope. Roughly speaking, we+promote `C` and `m` like so:++ class PC a where+ type M (x :: a) (y :: b) :: (a, b)+ type M x y = MDefault x y++ type MDefault :: forall a b. a -> b -> (a, b)+ type family MDefault x y where+ MDefault @a @b x y = '(x, y) :: (a, b)++The most subtle part is defining MDefault, as we need to give it a standalone+kind signature in order to bind `@a` and `@b` in the definition of `MDefault`.+Note that it's not enough to promote the method signature, as that doesn't+quantify `a`. Instead, we simply collect the free variables of the argument and+result types (`a -> b -> a`) and quantify those, giving us `forall a b. a -> b+-> a`. Note that the exact order of type variables doesn't matter, as the user+doesn't invoke MDefault directly. We mainly use the `forall` to ensure /some/+predictable ordering for the type variables so that we can match the order in+the invisible arguments in the type family equation.++A similar process applies to class instances. For example:++ instance C [a] where+ m :: forall b. [a] -> b -> ([a], b)+ m x y = (reverse x, y) :: ([a], b)++In this example, there are also two levels of scoped type variables: the `a`+from the instance head, and the `b` in the instance signature. We would promote+this instance similarly:++ instance PC [a] where+ type M x y = MImpl x y++ type MImpl :: forall a b. [a] -> b -> ([a], b)+ type family MImpl x y where+ MImpl @a @b x y = '(Reverse x, y) :: ([a], b)++-----+-- Wrinkle: Partial scoping+-----++Although the examples above use two levels of scoped type variables, it is not+necessarily the case that you /have/ to use both levels. Consider, for example:++ instance C (Maybe a) where+ m :: Maybe a -> b -> (Maybe a, b)+ m x y = (fmap (\xx -> (xx :: a)) x, y)++Note that the `a` scopes over the body of `m`'s implementation, but /not/ `b`,+as `m`'s instance signature does not have an outermost `forall`. A more extreme+version of this example is:++ instance C (Maybe a) where+ m x y = (fmap (\xx -> (xx :: a)) x, y)++Here, `m` does not have an instance signature at all, so there is no `b` in+sight.++In both examples, we are presented with a challenge: how do we ensure that `a`+(and only `a`) scopes? Note that singletons-th's approach to promoting class+methods means that we will promote this instance to code that looks like:++ instance PC (Maybe a) where+ type M x y = MImpl x y++ type MImpl :: forall a b. Maybe a -> b -> (Maybe a, b)+ type family MImpl x y where+ ...++We need to give `MImpl` a standalone kind signature we ensure that we can bring+`a` into scope over the right-hand side of `MImpl`'s type family equation. What+does this mean for `b`? One idea is that we could bring `b` into scope over the+right-hand side of the equation as well. This would give rise to this+definition:++ type MImpl :: forall a b. Maybe a -> b -> (Maybe a, b)+ type family MImpl x y where+ M @a @b x y = (Fmap (LambdaSym1 a b x y) x, y)++ data LambdaSym1 a b x y xx+ type instance Apply (LambdaSym1 a b x y) xx = Lambda a b x y xx++ type family Lambda a b x y xx where+ Lambda a b x y xx = xx :: a++Note that Lambda (the lambda-lifted version of the `\xx -> (xx :: a)`+expression) includes both `a` and `b` as local variables. Somewhat+surprisingly, this ends up being a problem when /singling/ the instance. To see+why, consider the singled code for the extreme version of the instance:++ instance SC (Maybe a) where+ sM (sX :: Sing x) (sY :: Sing y) =+ ( sFmap (singFun1 @(LambdaSym1 a b x y)+ (\(sXX :: Sing xx) -> (sXX :: Sing (xx :: a)))+ , sY+ )++GHC will reject this code, as `b` is not in scope in the subexpression+`singFun1 @(LambdaSym1 a b x y)`. And indeed, the original code doesn't bring+`b` into scope, so it makes sense that `b` wouldn't be in scope in the singled+code. We could try to infer an instance signature for `sM` that quantifies `b`+in an outermost `forall`, but doing so is fraught with peril (see #590).++Luckily, there is a relatively simple way to make this work. The reason that+LambdaSym1 includes `b` as an argument is because we typically call+`scopedBind` (see Note [Scoped type variables]) on all of the type variables+bound in the outermost `forall` to bring them into scope in the right-hand+side. For class methods, however, we need not call `scopedBind` on /every/ type+variable in the outermost `forall`. Instead, we can only call `scopedBind` on+the type variables that actually interact with ScopedTypeVariables, and we can+leave all other type variables alone. Concretely, this means that we would+generate the following code for `MImpl`:++ type MImpl :: forall a b. Maybe a -> b -> (Maybe a, b)+ type family MImpl x y where+ M @a @b x y =+ -- NB: Call `scopedBind [a]` here, not `scopedBind [a, b]`+ (Fmap (LambdaSym1 a x y) x, y)++ data LambdaSym1 a x y xx+ type instance Apply (LambdaSym1 a x y) xx = Lambda a x y xx++ type family Lambda a x y xx where+ Lambda a x y xx = xx :: a++Note that we still bind `@b` in an invisible argument, but we no longer pass it+along to LambdaSym1. This means that when we generate `singFun1 @(LambdaSym1 a+x y)` in the singled instance, we no longer reference `b` at all, avoiding the+issue above. (Note that we don't need to bind `@b` in an invisible argument+anymore, but it would require more work to special-case class methods in+`promoteClause` to avoid this, and it doesn't hurt anything to leave `@b` in+place).++The `OSet LocalVar` field of `ClassMethodRHS` dictates which type variables to+bring into scope via `scopedBind`. There are multiple places in the code which+determine which type variables get put into the `OSet`:++* For class declarations, the scoped type variables from the class header+ (e.g., the `a` in `class C a`) are determined in `promoteClassDec`.+* For instance declarations, the scoped type variables from the instance head+ (e.g., the `a` in `instance C (Maybe a)`) are determined in+ `promoteInstanceDec`.+* The scoped type variables from class method signatures and instance signatures+ are determined in `promoteMethod.promote_meth_ty`.++Each of these functions have references to this Note near the particular lines+of relevant code. -}
src/Data/Singletons/TH/Single.hs view
@@ -148,8 +148,9 @@ singDecideInstance name = do (_df, tvbs, cons) <- getDataD ("I cannot make an instance of SDecide for it.") name dtvbs <- mapM dsTvbVis tvbs- let data_ty = foldTypeTvbs (DConT name) dtvbs- dcons <- concatMapM (dsCon dtvbs data_ty) cons+ let data_ty = foldTypeTvbs (DConT name) dtvbs+ dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs+ dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons (scons, _) <- singM [] $ mapM (singCtor name) dcons sDecideInstance <- mkDecideInstance Nothing data_ty dcons scons eqInstance <- mkEqInstanceForSingleton data_ty name@@ -200,8 +201,9 @@ showSingInstance name = do (df, tvbs, cons) <- getDataD ("I cannot make an instance of Show for it.") name dtvbs <- mapM dsTvbVis tvbs- let data_ty = foldTypeTvbs (DConT name) dtvbs- dcons <- concatMapM (dsCon dtvbs data_ty) cons+ let data_ty = foldTypeTvbs (DConT name) dtvbs+ dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs+ dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons let tyvars = map (DVarT . extractTvbName) dtvbs kind = foldType (DConT name) tyvars data_decl = DataDecl df name dtvbs dcons@@ -263,7 +265,7 @@ [DLetDec $ DFunD singMethName [DClause [] $ wrapSingFun 1 DWildCardT $- DLamE [x] $+ dLamE [DVarP x] $ DVarE withSingIName `DAppE` DVarE x `DAppE` DVarE singMethName]] @@ -272,8 +274,9 @@ (df, tvbs, cons) <- getDataD ("I cannot make an instance of " ++ inst_name ++ " for it.") name dtvbs <- mapM dsTvbVis tvbs- let data_ty = foldTypeTvbs (DConT name) dtvbs- dcons <- concatMapM (dsCon dtvbs data_ty) cons+ let data_ty = foldTypeTvbs (DConT name) dtvbs+ dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs+ dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons let data_decl = DataDecl df name dtvbs dcons raw_inst <- mk_inst Nothing data_ty data_decl (a_inst, decs) <- promoteM [] $@@ -390,18 +393,20 @@ mb_cls_sak <- dsReifyType cls_name let sing_cls_name = singledClassName opts cls_name mb_sing_cls_sak = fmap (DKiSigD sing_cls_name) mb_cls_sak+ pro_meth_names_and_locals =+ map (\meth_name -> (promotedValueName opts meth_name Nothing, []))+ meth_names cls_infix_decls <- singReifiedInfixDecls $ cls_name:meth_names (sing_sigs, _, tyvar_names, cxts, res_kis, singIDefunss) <- unzip6 <$> zipWithM (singTySig no_meth_defns meth_sigs)- meth_names- (map (DConT . defunctionalizedName0 opts) meth_names)+ meth_names pro_meth_names_and_locals emitDecs $ maybeToList mb_sing_cls_sak ++ cls_infix_decls ++ concat singIDefunss let default_sigs = catMaybes $ zipWith4 (mk_default_sig opts) meth_names sing_sigs tyvar_names res_kis sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList cxts))) (OMap.assocs default_defns)- fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs fixities+ fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs $ fmap fst fixities cls_cxt' <- mapM singPred cls_cxt return $ DClassD cls_cxt' sing_cls_name@@ -427,7 +432,10 @@ pure $ DSigT sty' ski add_constraints opts meth_name sty bound_kvs res_ki = do (tvbs, cxt, args, res) <- unravelVanillaDType sty- prom_dflt <- OMap.lookup meth_name promoted_defaults+ -- Class defaults always occur at the top level, and as such, they are+ -- guaranteed never to close over any local names.+ (prom_dflt_name, _prom_deflt_locals) <-+ OMap.lookup meth_name promoted_defaults -- Filter out explicitly bound kind variables. Otherwise, if you had -- the following class (#312):@@ -446,13 +454,13 @@ -- Which applies Bar/BarDefault to b, which shouldn't happen. let tvs = map tvbToType $ filter (\tvb -> extractTvbName tvb `Set.member` bound_kv_set) tvbs- prom_meth = DConT $ defunctionalizedName0 opts meth_name+ prom_meth = DConT $ promotedValueName opts meth_name Nothing default_pred = foldType (DConT equalityName) -- NB: Need the res_ki here to prevent ambiguous -- kinds in result-inferred default methods. -- See #175- [ foldApply prom_meth tvs `DSigT` res_ki- , foldApply prom_dflt tvs ]+ [ foldType prom_meth tvs `DSigT` res_ki+ , foldType (DConT prom_dflt_name) tvs ] return $ ravelVanillaDType tvbs (default_pred : cxt) args res where bound_kv_set = Set.fromList bound_kvs@@ -476,48 +484,21 @@ sing_meth :: Name -> ALetDecRHS -> SgM [DDec] sing_meth name rhs = do opts <- getOptions- mb_s_info <- dsReify (singledValueName opts name)- inst_kis <- mapM promoteType inst_tys- let mk_subst cls_tvbs = Map.fromList $ zip (map extractTvbName vis_cls_tvbs) inst_kis- where- -- This is a half-hearted attempt to address the underlying problem- -- in #358, where we can sometimes have more class type variables- -- (due to implicit kind arguments) than class arguments. This just- -- ensures that the explicit type variables are properly mapped- -- to the class arguments, leaving the implicit kind variables- -- unmapped. That could potentially cause *other* problems, but- -- those are perhaps best avoided by using InstanceSigs. At the- -- very least, this workaround will make error messages slightly- -- less confusing.- vis_cls_tvbs = drop (length cls_tvbs - length inst_kis) cls_tvbs-- sing_meth_ty :: DType -> SgM DType+ let sing_meth_ty :: DType -> SgM DType sing_meth_ty inner_ty = do -- Make sure to expand through type synonyms here! Not doing so -- resulted in #167. raw_ty <- expand inner_ty (s_ty, _num_args, _tyvar_names, _ctxt, _arg_kis, _res_ki)- <- singType (DConT $ defunctionalizedName0 opts name) raw_ty+ <- singType (DConT $ promotedValueName opts name Nothing) raw_ty pure s_ty - s_ty <- case OMap.lookup name inst_sigs of- Just inst_sig ->- -- We have an InstanceSig, so just single that type.- sing_meth_ty inst_sig- Nothing -> case mb_s_info of- -- We don't have an InstanceSig, so we must compute the type to use- -- in the singled instance ourselves through reification.- Just (DVarI _ (DForallT (DForallInvis cls_tvbs) (DConstrainedT _cls_pred s_ty)) _) ->- pure $ substType (mk_subst cls_tvbs) s_ty- _ -> do- mb_info <- dsReify name- case mb_info of- Just (DVarI _ (DForallT (DForallInvis cls_tvbs)- (DConstrainedT _cls_pred inner_ty)) _) -> do- s_ty <- sing_meth_ty inner_ty- pure $ substType (mk_subst cls_tvbs) s_ty- _ -> fail $ "Cannot find type of method " ++ show name-+ -- If an instance signature exists, single it. Otherwise, leave it out.+ -- Unlike most other places, we don't actually *need* explicit type+ -- signatures for instance methods, as GHC can figure out the types of+ -- the instance methods on its own. As such, any GADT pattern matching in+ -- the singled instance method code will work as expected.+ mb_s_ty <- traverse sing_meth_ty $ OMap.lookup name inst_sigs meth' <- singLetDecRHS Map.empty -- Because we are singling an instance declaration, -- we aren't generating defunctionalization symbols@@ -525,7 +506,9 @@ -- generating any SingI instances. Therefore, we -- don't need to include anything in this Map. name rhs- return $ map DLetDec [DSigD (singledValueName opts name) s_ty, meth']+ return $ map DLetDec+ $ maybeToList (DSigD (singledValueName opts name) <$> mb_s_ty)+ ++ [meth'] singLetDecEnv :: ALetDecEnv -> SgM a@@ -544,7 +527,7 @@ let prom_list = OMap.assocs proms (typeSigs, letBinds, _tyvarNames, cxts, _res_kis, singIDefunss) <- unzip6 <$> mapM (uncurry (singTySig defns types)) prom_list- infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs infix_decls+ infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs $ fmap fst infix_decls bindLets letBinds $ do let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList cxts))) (OMap.assocs defns)@@ -553,7 +536,7 @@ singTySig :: OMap Name ALetDecRHS -- definitions -> OMap Name DType -- type signatures- -> Name -> DType -- the type is the promoted type, not the type sig!+ -> Name -> LetDecProm -- the LetDecProm is the promoted type, not the type sig! -> SgM ( DLetDec -- the new type signature , (Name, DExp) -- the let-bind entry , [Name] -- the scoped tyvar names in the tysig@@ -561,9 +544,11 @@ , Maybe DKind -- the result kind in the tysig , [DDec] -- SingI instances for defun symbols )-singTySig defns types name prom_ty = do+singTySig defns types name (prom_name, prom_locals) = do opts <- getOptions let sName = singledValueName opts name+ prom_defun_name = defunctionalizedName0 opts prom_name+ prom_defun_ty = foldTypeLocalVars (DConT prom_defun_name) prom_locals case OMap.lookup name types of Nothing -> do num_args <- guess_num_args@@ -571,7 +556,7 @@ singIDefuns <- singDefuns name VarName [] (map (const Nothing) tyvar_names) Nothing return ( DSigD sName sty- , (name, wrapSingFun num_args prom_ty (DVarE sName))+ , (name, wrapSingFun num_args prom_defun_ty (DVarE sName)) , tyvar_names , (name, []) , Nothing@@ -583,12 +568,15 @@ singIDefuns <- singDefuns name VarName (bound_cxt ++ ctxt) (map Just arg_kis) (Just res_ki) return ( DSigD sName sty- , (name, wrapSingFun num_args prom_ty (DVarE sName))+ , (name, wrapSingFun num_args prom_defun_ty (DVarE sName)) , tyvar_names , (name, ctxt) , Just res_ki , singIDefuns ) where+ prom_ty :: DType+ prom_ty = foldTypeLocalVars (DConT prom_name) prom_locals+ guess_num_args :: SgM Int guess_num_args = case OMap.lookup name defns of@@ -609,7 +597,7 @@ [] (map (\nm -> singFamily `DAppT` DVarT nm) arg_names) (sing_w_wildcard `DAppT`- (foldApply prom_ty (map DVarT arg_names)))+ (foldType prom_ty (map DVarT arg_names))) , arg_names ) {-@@ -655,10 +643,8 @@ This is too general, since `sX` will only typecheck if the return kind of `LetX` is `MyProxy a`, not `MyProxy a1`. In order to avoid this problem, we need to avoid kind generalization when kind-checking the type of `sX`.-To accomplish this, we borrow a trick from-Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization]-and use TypeApplications plus a wildcard type. That is, we generate this code-for `sF`:+To accomplish this, we use TypeApplications plus a wildcard type. That is, we+generate this code for `sF`: sF :: forall a (t :: MyProxy a). Sing t -> Sing (F t :: MyProxy a) sF SMyProxy =@@ -729,7 +715,7 @@ sBody <- bindLambdas lambda_binds $ singExp exp return $ DClause sPats $ mkSigPaCaseE sigPaExpsSigs sBody -singPat :: Map Name Name -- from term-level names to type-level names+singPat :: Map Name LocalVar -- from term-level names to type-level names -> ADPat -> QWithAux SingDSigPaInfos SgM DPat singPat var_proms = go@@ -742,7 +728,7 @@ tyname <- case Map.lookup name var_proms of Nothing -> fail "Internal error: unknown variable when singling pattern"- Just tyname -> return tyname+ Just (LocalVar { lvName = tyname }) -> return tyname pure $ DVarP (singledValueName opts name) `DSigP` (singFamily `DAppT` DVarT tyname) go (ADConP name tys pats) = do@@ -769,42 +755,10 @@ -- that brings singleton equality constraints into scope via pattern-matching. -- See @Note [Singling pattern signatures]@. mkSigPaCaseE :: SingDSigPaInfos -> DExp -> DExp-mkSigPaCaseE exps_with_sigs exp- | null exps_with_sigs = exp- | otherwise =- let (exps, sigs) = unzip exps_with_sigs- scrutinee = mkTupleDExp exps- pats = map (DSigP DWildP . DAppT (DConT singFamilyName)) sigs- in DCaseE scrutinee [DMatch (mkTupleDPat pats) exp]---- Note [Annotate case return type]--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~------ We're straining GHC's type inference here. One particular trouble area--- is determining the return type of a GADT pattern match. In general, GHC--- cannot infer return types of GADT pattern matches because the return type--- becomes "untouchable" in the case matches. See the OutsideIn paper. But,--- during singletonization, we *know* the return type. So, just add a type--- annotation. See #54.------ In particular, we add a type annotation in a somewhat unorthodox fashion.--- Instead of the usual `(x :: t)`, we use `id @t x`. See--- Note [The id hack; or, how singletons-th learned to stop worrying and avoid--- kind generalization] for an explanation of why we do this.---- Note [Why error is so special]--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~--- Some of the transformations that happen before this point produce impossible--- case matches. We must be careful when processing these so as not to make--- an error GHC will complain about. When binding the case-match variables, we--- normally include an equality constraint saying that the scrutinee is equal--- to the matched pattern. But, we can't do this in inaccessible matches, because--- equality is bogus, and GHC (rightly) complains. However, we then have another--- problem, because GHC doesn't have enough information when type-checking the--- RHS of the inaccessible match to deem it type-safe. The solution: treat error--- as super-special, so that GHC doesn't look too hard at singletonized error--- calls. Specifically, DON'T do the applySing stuff. Just use sError, which--- has a custom type (Sing x -> a) anyway.+mkSigPaCaseE exps_with_sigs exp =+ let (exps, sigs) = unzip exps_with_sigs+ pats = map (DSigP DWildP . DAppT (DConT singFamilyName)) sigs+ in multiCase exps pats exp -- Note [Singling pattern signatures] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~@@ -883,41 +837,16 @@ -- And now everything is hunky-dory. singExp :: ADExp -> SgM DExp- -- See Note [Why error is so special]-singExp (ADVarE err `ADAppE` arg)- | err == errorName = do opts <- getOptions- DAppE (DVarE (singledValueName opts err)) <$>- singExp arg singExp (ADVarE name) = lookupVarE name singExp (ADConE name) = lookupConE name singExp (ADLitE lit) = singLit lit singExp (ADAppE e1 e2) = do e1' <- singExp e1 e2' <- singExp e2- -- `applySing undefined x` kills type inference, because GHC can't figure- -- out the type of `undefined`. So we don't emit `applySing` there.- if isException e1'- then return $ e1' `DAppE` e2'- else return $ (DVarE applySingName) `DAppE` e1' `DAppE` e2'-singExp (ADLamE ty_names prom_lam names exp) = do- opts <- getOptions- let sNames = map (singledValueName opts) names- exp' <- bindLambdas (zip names sNames) $ singExp exp- -- we need to bind the type variables... but DLamE doesn't allow SigT patterns.- -- So: build a case- let caseExp = DCaseE (mkTupleDExp (map DVarE sNames))- [DMatch (mkTupleDPat- (map ((DWildP `DSigP`) .- (singFamily `DAppT`) .- DVarT) ty_names)) exp']- return $ wrapSingFun (length names) prom_lam $ DLamE sNames caseExp-singExp (ADCaseE exp matches ret_ty) =- -- See Note [Annotate case return type] and- -- Note [The id hack; or, how singletons-th learned to stop worrying and- -- avoid kind generalization]- DAppE (DAppTypeE (DVarE 'id)- (singFamily `DAppT` ret_ty))- <$> (DCaseE <$> singExp exp <*> mapM singMatch matches)+ pure $ DVarE applySingName `DAppE` e1' `DAppE` e2'+singExp (ADLamCasesE num_args prom_lam_cases clauses) = do+ clauses' <- traverse singClause clauses+ pure $ wrapSingFun num_args prom_lam_cases $ DLamCasesE clauses' singExp (ADLetE env exp) = do -- We intentionally discard the SingI instances for exp's defunctionalization -- symbols, as we also do not generate the declarations for the@@ -989,30 +918,6 @@ (DConT showName `DAppT` (DConT sty_tycon `DAppT` DSigT (DVarT z) ki)) pure [show_inst] -isException :: DExp -> Bool-isException (DVarE n) = nameBase n == "sUndefined"-isException (DConE {}) = False-isException (DLitE {}) = False-isException (DAppE (DVarE fun) _) | nameBase fun == "sError" = True-isException (DAppE fun _) = isException fun-isException (DAppTypeE e _) = isException e-isException (DLamE _ _) = False-isException (DCaseE e _) = isException e-isException (DLetE _ e) = isException e-isException (DSigE e _) = isException e-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- opts <- getOptions- (sPat, sigPaExpsSigs) <- evalForPair $ singPat (Map.fromList var_proms) pat- let lambda_binds = map (\(n,_) -> (n, singledValueName opts n)) var_proms- sExp <- bindLambdas lambda_binds $ singExp exp- return $ DMatch sPat $ mkSigPaCaseE sigPaExpsSigs sExp- singLit :: Lit -> SgM DExp singLit (IntegerL n) = do opts <- getOptions@@ -1035,85 +940,3 @@ return $ DVarE singMethName `DSigE` (singFamily `DAppT` DLitT (CharTyLit c)) singLit lit = fail ("Only string, natural number, and character literals can be singled: " ++ show lit)--{--Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-GHC 8.8 was a time of great change. In particular, 8.8 debuted a fix for-Trac #15141 (decideKindGeneralisationPlan is too complicated). To fix this, a-wily GHC developer—who shall remain unnamed, but whose username rhymes with-schmoldfire—decided to make decideKindGeneralisationPlan less complicated by,-well, removing the whole thing. One consequence of this is that local-definitions are now kind-generalized (whereas they would not have been-previously).--While schmoldfire had the noblest of intentions when authoring his fix, he-unintentionally made life much harder for singletons-th. Why? Consider the-following program:-- class Foo a where- bar :: a -> (a -> b) -> b- baz :: a-- quux :: Foo a => a -> a- quux x = x `bar` \_ -> baz--When singled, this program will turn into something like this:-- type family Quux (x :: a) :: a where- Quux x = Bar x (LambdaSym1 x)-- sQuux :: forall a (x :: a). SFoo a => Sing x -> Sing (Quux x :: a)- sQuux (sX :: Sing x)- = sBar sX- ((singFun1 @(LambdaSym1 x))- (\ sArg- -> case sArg of {- (_ :: Sing arg)- -> (case sArg of { _ -> sBaz }) ::- Sing (Case x arg arg) }))-- type family Case x arg t where- Case x arg _ = Baz- type family Lambda x t where- Lambda x arg = Case x arg arg- data LambdaSym1 x t- type instance Apply (LambdaSym1 x) t = Lambda x t--The high-level bit is the explicit `Sing (Case x arg arg)` signature. Question:-what is the kind of `Case x arg arg`? The answer depends on whether local-definitions are kind-generalized or not!--1. If local definitions are *not* kind-generalized (i.e., the status quo before- GHC 8.8), then `Case x arg arg :: a`.-2. If local definitions *are* kind-generalized (i.e., the status quo in GHC 8.8- and later), then `Case x arg arg :: k` for some fresh kind variable `k`.--Unfortunately, the kind of `Case x arg arg` *must* be `a` in order for `sQuux`-to type-check. This means that the code above suddenly stopped working in GHC-8.8. What's more, we can't just remove these explicit signatures, as there is-code elsewhere in `singletons-th` that crucially relies on them to guide type-inference along (e.g., `sShowParen` in `Text.Show.Singletons`).--Luckily, there is an ingenious hack that lets us the benefits of explicit-signatures without the pain of kind generalization: our old friend, the `id`-function. The plan is as follows: instead of generating this code:-- (case sArg of ...) :: Sing (Case x arg arg)--We instead generate this code:-- id @(Sing (Case x arg arg)) (case sArg of ...)--That's it! This works because visible type arguments in terms do not get kind--generalized, unlike top-level or local signatures. Now `Case x arg arg`'s kind-is not generalized, and all is well. We dub this: the `id` hack.--One might wonder: will we need the `id` hack around forever? Perhaps not. While-GHC 8.8 removed the decideKindGeneralisationPlan function, there have been-rumblings that a future version of GHC may bring it back (in a limited form).-If this happens, it is possibly that GHC's attitude towards kind-generalizing-local definitions may change *again*, which could conceivably render the `id`-hack unnecessary. This is all speculation, of course, so all we can do now is-wait and revisit this design at a later date.--}
src/Data/Singletons/TH/Single/Data.hs view
@@ -13,10 +13,7 @@ import Language.Haskell.TH.Desugar as Desugar import Language.Haskell.TH.Syntax-import qualified Data.Map.Strict as Map-import Data.Map.Strict (Map) import Data.Maybe-import Data.Traversable (mapAccumL) import Data.Singletons.TH.Names import Data.Singletons.TH.Options import Data.Singletons.TH.Promote.Type@@ -151,13 +148,13 @@ mkEmptyFromSingClause = do x <- qNewName "x" pure $ DClause [DVarP x]- $ DCaseE (DVarE x) []+ $ dCaseE (DVarE x) [] mkEmptyToSingClause :: SgM DClause mkEmptyToSingClause = do x <- qNewName "x" pure $ DClause [DVarP x]- $ DConE someSingDataName `DAppE` DCaseE (DVarE x) []+ $ DConE someSingDataName `DAppE` dCaseE (DVarE x) [] -- Single a constructor. singCtor :: Name -> DCon -> SgM DCon@@ -234,7 +231,7 @@ (foldType pCon indices `DSigT` rty')) -- Make sure to include an explicit `rty'` kind annotation. -- See Note [Preserve the order of type variables during singling],- -- wrinkle 3, in D.S.TH.Single.Type.+ -- wrinkle 2, in D.S.TH.Single.Type. where mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness mk_source_unpackedness su = case su of@@ -270,26 +267,12 @@ -- type SD :: forall j l (a :: l) (b :: j). D @j @l (a :: l) b -> Type -- @ ----- Note that:------ * This function has a precondition that the length of @data_bndrs@ must--- always be equal to the number of visible quantifiers (i.e., the number of--- function arrows plus the number of visible @forall@–bound variables) in--- @sak@. @singletons-th@ maintains this invariant when constructing a--- 'DataDecl' (see the 'buildDataDTvbs' function).------ * The order of the invisible quantifiers is preserved, so both--- @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would--- expect it to.+-- Note that the order of the invisible quantifiers is preserved, so both+-- @D \@Bool \@Ordering@ and @SD \@Bool \@Ordering@ will work the way you would+-- expect it to. ----- * Whenever possible, this function reuses type variable names from the data--- type's user-written binders. This is why the standalone kind signature uses--- @forall j l@ instead of @forall j k@, since the @(a :: l)@ binder uses @l@--- instead of @k@. We could have just as well chose the other way around, but--- we chose to pick variable names from the data type binders since they scope--- over other parts of the data type declaration (e.g., in @deriving@--- clauses), so keeping these names avoids having to perform some--- alpha-renaming.+-- See also the Haddocks for 'dMatchUpSAKWithDecl' function, which also apply+-- here. singDataSAK :: MonadFail q => DKind@@ -301,204 +284,10 @@ -> q DKind -- ^ The standalone kind signature for the singled data type singDataSAK data_sak data_bndrs data_k = do- -- (1) First, explicitly quantify any free kind variables in `data_sak` using- -- an invisible @forall@. This is done to ensure that precondition (2) in- -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function).- let data_sak_free_tvbs =- changeDTVFlags SpecifiedSpec $ toposortTyVarsOf [data_sak]- data_sak' = DForallT (DForallInvis data_sak_free_tvbs) data_sak-- -- (2) Next, compute type variable binders for the singled data type's- -- standalone kind signature using `matchUpSigWithDecl`. Note that these can- -- be biased towards type variable names mention in `data_sak` over names- -- mentioned in `data_bndrs`, but we will fix that up in the next step.- let (data_sak_args, _) = unravelDType data_sak'- sing_sak_tvbs <- matchUpSigWithDecl data_sak_args data_bndrs-- -- (3) Swizzle the type variable names so that names in `data_bndrs` are- -- preferred over names in `data_sak`.- --- -- This is heavily inspired by similar code in GHC:- -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616- let invis_data_sak_args = filterInvisTvbArgs data_sak_args- invis_data_sak_arg_nms = map extractTvbName invis_data_sak_args-- invis_data_bndrs = toposortKindVarsOfTvbs data_bndrs- invis_data_bndr_nms = map extractTvbName invis_data_bndrs-- swizzle_env =- Map.fromList $ zip invis_data_sak_arg_nms invis_data_bndr_nms- (_, swizzled_sing_sak_tvbs) =- mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs-- -- (4) Finally, construct the kind of the singled data type.- pure $ DForallT (DForallInvis swizzled_sing_sak_tvbs)+ sing_sak_tvbs <- dMatchUpSAKWithDecl data_sak data_bndrs+ let sing_sak_tvbs' = dtvbForAllTyFlagsToSpecs sing_sak_tvbs+ pure $ DForallT (DForallInvis sing_sak_tvbs') $ DArrowT `DAppT` data_k `DAppT` DConT typeKindName---- Match the quantifiers in a data type's standalone kind signature with the--- binders in the data type declaration. This function assumes the following--- preconditions:------ 1. The number of required binders in the data type declaration is equal to--- the number of visible quantifiers (i.e., the number of function arrows--- plus the number of visible @forall@–bound variables) in the standalone--- kind signature.------ 2. The number of invisible \@-binders in the data type declaration is less--- than or equal to the number of invisible quantifiers (i.e., the number of--- invisible @forall@–bound variables) in the standalone kind signature.------ The implementation of this function is heavily based on a GHC function of--- the same name:--- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2645-2715-matchUpSigWithDecl ::- forall q.- MonadFail q- => DFunArgs- -- ^ The quantifiers in the data type's standalone kind signature- -> [DTyVarBndrVis]- -- ^ The user-written binders in the data type declaration- -> q [DTyVarBndrSpec]-matchUpSigWithDecl = go_fun_args Map.empty- where- go_fun_args ::- DSubst- -- ^ A substitution from the names of @forall@-bound variables in the- -- standalone kind signature to corresponding binder names in the- -- user-written binders. (See the Haddocks for `singDataSAK` for an- -- explanation of why we perform this substitution.) For example:- --- -- @- -- type T :: forall a. forall b -> Maybe (a, b) -> Type- -- data T @x y z- -- @- --- -- After matching up the @a@ in @forall a.@ with @x@ and- -- the @b@ in @forall b ->@ with @y@, this substitution will be- -- extended with @[a :-> x, b :-> y]@. This ensures that we will- -- produce @Maybe (x, y)@ instead of @Maybe (a, b)@ in- -- the kind for @z@.- -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec]- go_fun_args _ DFANil [] =- pure []- -- This should not happen, per the function's precondition- go_fun_args _ DFANil data_bndrs =- fail $ "matchUpSigWithDecl.go_fun_args: Too many binders: " ++ show data_bndrs- -- GHC now disallows kind-level constraints, per this GHC proposal:- -- https://github.com/ghc-proposals/ghc-proposals/blob/b0687d96ce8007294173b7f628042ac4260cc738/proposals/0547-no-kind-equalities.rst- go_fun_args _ (DFACxt{}) _ =- fail "matchUpSigWithDecl.go_fun_args: Unexpected kind-level constraint"- go_fun_args subst (DFAForalls (DForallInvis tvbs) sig_args) data_bndrs =- go_invis_tvbs subst tvbs sig_args data_bndrs- go_fun_args subst (DFAForalls (DForallVis tvbs) sig_args) data_bndrs =- go_vis_tvbs subst tvbs sig_args data_bndrs- go_fun_args subst (DFAAnon anon sig_args) (data_bndr:data_bndrs) = do- let data_bndr_name = extractTvbName data_bndr- mb_data_bndr_kind = extractTvbKind data_bndr- anon' = substType subst anon-- anon'' =- case mb_data_bndr_kind of- Nothing -> anon'- Just data_bndr_kind ->- let mb_match_subst = matchTy NoIgnore data_bndr_kind anon' in- maybe data_bndr_kind (`substType` data_bndr_kind) mb_match_subst- sig_args' <- go_fun_args subst sig_args data_bndrs- pure $ DKindedTV data_bndr_name SpecifiedSpec anon'' : sig_args'- -- This should not happen, per precondition (1).- go_fun_args _ _ [] =- fail "matchUpSigWithDecl.go_fun_args: Too few binders"-- go_invis_tvbs :: DSubst -> [DTyVarBndrSpec] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec]- go_invis_tvbs subst [] sig_args data_bndrs =- go_fun_args subst sig_args data_bndrs- -- This should not happen, per precondition (2).- go_invis_tvbs _ (_:_) _ [] =- fail $ "matchUpSigWithDecl.go_invis_tvbs: Too few binders"- go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args data_bndrss@(data_bndr:data_bndrs) =- case extractTvbFlag data_bndr of- -- If the next data_bndr is required, then we have a invisible forall in- -- the kind without a corresponding invisible @-binder, which is- -- allowed. In this case, we simply apply the substitution and recurse.- BndrReq -> do- let (subst', invis_tvb') = substTvb subst invis_tvb- sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args data_bndrss- pure $ invis_tvb' : sig_args'- -- If the next data_bndr is an invisible @-binder, then we must match it- -- against the invisible forall–bound variable in the kind.- BndrInvis -> do- let (subst', sig_tvb) = match_tvbs subst invis_tvb data_bndr- sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args data_bndrs- pure (sig_tvb : sig_args')-- go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndrSpec]- go_vis_tvbs subst [] sig_args data_bndrs =- go_fun_args subst sig_args data_bndrs- -- This should not happen, per precondition (1).- go_vis_tvbs _ (_:_) _ [] =- fail $ "matchUpSigWithDecl.go_vis_tvbs: Too few binders"- go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (data_bndr:data_bndrs) = do- case extractTvbFlag data_bndr of- -- If the next data_bndr is required, then we must match it against the- -- visible forall–bound variable in the kind.- BndrReq -> do- let (subst', sig_tvb) = match_tvbs subst vis_tvb data_bndr- sig_args' <- go_vis_tvbs subst' vis_tvbs sig_args data_bndrs- pure (sig_tvb : sig_args')- -- We have a visible forall in the kind, but an invisible @-binder as- -- the next data_bndr. This is ill kinded, so throw an error.- BndrInvis ->- fail $ "matchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: "- ++ show data_bndr-- -- @match_tvbs subst sig_tvb data_bndr@ will match the kind of @data_bndr@- -- against the kind of @sig_tvb@ to produce a new kind. This function- -- produces two values as output:- --- -- 1. A new @subst@ that has been extended such that the name of @sig_tvb@- -- maps to the name of @data_bndr@. (See the Haddocks for the 'DSubst'- -- argument to @go_fun_args@ for an explanation of why we do this.)- --- -- 2. A 'DTyVarBndrSpec' that has the name of @data_bndr@, but with the new- -- kind resulting from matching.- match_tvbs :: DSubst -> DTyVarBndr flag -> DTyVarBndrVis -> (DSubst, DTyVarBndrSpec)- match_tvbs subst sig_tvb data_bndr =- let data_bndr_name = extractTvbName data_bndr- mb_data_bndr_kind = extractTvbKind data_bndr-- sig_tvb_name = extractTvbName sig_tvb- mb_sig_tvb_kind = substType subst <$> extractTvbKind sig_tvb-- mb_kind :: Maybe DKind- mb_kind =- case (mb_data_bndr_kind, mb_sig_tvb_kind) of- (Nothing, Nothing) -> Nothing- (Just data_bndr_kind, Nothing) -> Just data_bndr_kind- (Nothing, Just sig_tvb_kind) -> Just sig_tvb_kind- (Just data_bndr_kind, Just sig_tvb_kind) -> do- match_subst <- matchTy NoIgnore data_bndr_kind sig_tvb_kind- Just $ substType match_subst data_bndr_kind-- subst' = Map.insert sig_tvb_name (DVarT data_bndr_name) subst- sig_tvb' = case mb_kind of- Nothing -> DPlainTV data_bndr_name SpecifiedSpec- Just kind -> DKindedTV data_bndr_name SpecifiedSpec kind in-- (subst', sig_tvb')---- This is heavily inspired by the `swizzleTcb` function in GHC:--- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2741-2755-swizzleTvb :: Map Name Name -> DSubst -> DTyVarBndrSpec -> (DSubst, DTyVarBndrSpec)-swizzleTvb swizzle_env subst tvb =- (subst', tvb2)- where- subst' = Map.insert tvb_name (DVarT (extractTvbName tvb2)) subst- tvb_name = extractTvbName tvb- tvb1 = mapDTVKind (substType subst) tvb- tvb2 =- case Map.lookup tvb_name swizzle_env of- Just user_name -> mapDTVName (const user_name) tvb1- Nothing -> tvb1 {- Note [singletons-th and record selectors]
src/Data/Singletons/TH/Single/Decide.hs view
@@ -96,32 +96,33 @@ rpats = map DVarP rnames lvars = map DVarE lnames rvars = map DVarE rnames- refl <- qNewName "refl" return $ DClause [DConP lname [] lpats, DConP rname [] rpats]- (DCaseE (mkTupleDExp $- zipWith (\l r -> foldExp (DVarE sDecideMethName) [l, r])- lvars rvars)- ((DMatch (mkTupleDPat (replicate lNumArgs- (DConP provedName [] [DConP reflName [] []])))- (DAppE (DConE provedName) (DConE reflName))) :- [DMatch (mkTupleDPat (replicate i DWildP ++- DConP disprovedName [] [DVarP contra] :- replicate (lNumArgs - i - 1) DWildP))- (DAppE (DConE disprovedName)- (DLamE [refl] $- DCaseE (DVarE refl)- [DMatch (DConP reflName [] []) $- (DAppE (DVarE contra)- (DConE reflName))]))- | i <- [0..lNumArgs-1] ]))+ (dCasesE+ (zipWith (\l r -> foldExp (DVarE sDecideMethName) [l, r])+ lvars rvars)+ ((DClause+ (replicate+ lNumArgs+ (DConP provedName [] [DConP reflName [] []]))+ (DAppE (DConE provedName) (DConE reflName))) :+ [ DClause+ (replicate i DWildP +++ DConP disprovedName [] [DVarP contra] :+ replicate (lNumArgs - i - 1) DWildP)+ (DAppE+ (DConE disprovedName)+ (dLamCaseE+ [DMatch (DConP reflName [] []) $+ (DAppE (DVarE contra)+ (DConE reflName))]))+ | i <- [0..lNumArgs-1] ])) - | otherwise = do- x <- qNewName "x"+ | otherwise = return $ DClause [DConP lname [] (replicate lNumArgs DWildP), DConP rname [] (replicate rNumArgs DWildP)]- (DAppE (DConE disprovedName) (DLamE [x] (DCaseE (DVarE x) [])))+ (DAppE (DConE disprovedName) (dLamCaseE [])) where (lname, lNumArgs) = extractNameArgs c1@@ -131,4 +132,4 @@ mkEmptyDecideMethClause = do x <- qNewName "x" pure $ DClause [DVarP x, DWildP]- $ DConE provedName `DAppE` DCaseE (DVarE x) []+ $ DConE provedName `DAppE` dCaseE (DVarE x) []
src/Data/Singletons/TH/Single/Fixity.hs view
@@ -17,24 +17,24 @@ case mb_ns of -- If we can't find the Name for some odd reason, -- fall back to singValName- Nothing -> finish $ singledValueName opts name- Just VarName -> finish $ singledValueName opts name+ Nothing -> finish DataNamespaceSpecifier $ singledValueName opts name+ Just VarName -> finish DataNamespaceSpecifier $ singledValueName opts name Just (FldName _)- | fld_sels -> finish $ singledValueName opts name+ | fld_sels -> finish DataNamespaceSpecifier $ singledValueName opts name | otherwise -> never_mind- Just DataName -> finish $ singledDataConName opts name+ Just DataName -> finish DataNamespaceSpecifier $ singledDataConName opts name Just TcClsName -> do mb_info <- dsReify name case mb_info of Just (DTyConI DClassD{} _)- -> finish $ singledClassName opts name+ -> finish TypeNamespaceSpecifier $ singledClassName opts name _ -> never_mind -- Don't produce anything for other type constructors (type synonyms, -- type families, data types, etc.). -- See [singletons-th and fixity declarations], wrinkle 1. where- finish :: Name -> q (Maybe DLetDec)- finish = pure . Just . DInfixD fixity NoNamespaceSpecifier+ finish :: NamespaceSpecifier -> Name -> q (Maybe DLetDec)+ finish ns n = pure $ Just $ DInfixD fixity ns n never_mind :: q (Maybe DLetDec) never_mind = pure Nothing@@ -68,15 +68,15 @@ singletons-th will produce promoted and singled versions of them: - infixl 5 `Foo`- infixl 5 `sFoo`+ infixl 5 type `Foo`+ infixl 5 data `sFoo` singletons-th will also produce fixity declarations for its defunctionalization symbols (see Note [Fixity declarations for defunctionalization symbols] in D.S.TH.Promote.Defun): - infixl 5 `FooSym0`- infixl 5 `FooSym1`+ infixl 5 type `FooSym0`+ infixl 5 type `FooSym1` ... -----@@ -94,14 +94,15 @@ - Type synonyms - Type families - Data constructors- - Infix values+ - Infix values (when their fixity declaration lack explicit namespaces) We exclude the first four because the promoted versions of these names are the same as the originals, so generating an extra fixity declaration for them would run the risk of having duplicates, which GHC would reject with an error. - We exclude infix value because while their promoted versions are different,- they share the same name base. In concrete terms, this:+ We exclude infix values when their fixity declarations lack explicit+ namespaces because while their promoted versions are different, they share+ the same name base. In concrete terms, this: $(promote [d| infixl 4 ###@@ -112,22 +113,41 @@ type family (###) (x :: a) (y :: a) :: a where ... - So giving the type-level (###) a fixity declaration would clash with the- existing one for the value-level (###).+ Note that the original `infixl 4 ###` declaration lacks an explicit+ namespace, which means that it applies to both the term-level *and*+ type-level (###) definitions. This means that giving the type-level (###) a+ fixity declaration would clash with the original fixity declaration. - There *is* a scenario where we should generate a fixity declaration for the- type-level (###), however. Imagine the above example used the `promoteOnly`- function instead of `promote`. Then the type-level (###) would lack a fixity- declaration altogether because the original fixity declaration was discarded- by `promoteOnly`! The same problem would arise if one had to choose between- the `singletons` and `singletonsOnly` functions.+ There *are* scenarios where we should generate a fixity declaration for the+ type-level (###), however: - The difference between `promote` and `promoteOnly` (as well as `singletons`- and `singletonsOnly`) is whether the `genQuotedDecs` option is set to `True`- or `False`, respectively. Therefore, if `genQuotedDecs` is set to `False`- when promoting the fixity declaration for an infix value, we opt to generate- a fixity declaration (with the same name base) so that the type-level version- of that value gets one.+ - Imagine if the fixity declaration had an explicit `data` namespace:++ $(promote [d|+ infixl 4 data ###+ (###) :: a -> a -> a+ |])++ Then it would be fine to give the promoted (###) definition this fixity+ declaration:++ infixl 4 type ###++ This is because the two fixity declarations would refer to distinct names+ in a different namespaces, so the two fixity declarations would not clash.++ - Imagine the above example used the `promoteOnly` function instead of+ `promote`. Then the type-level (###) would lack a fixity declaration+ altogether because the original fixity declaration was discarded by+ `promoteOnly`! The same problem would arise if one had to choose between+ the `singletons` and `singletonsOnly` functions.++ The difference between `promote` and `promoteOnly` (as well as `singletons`+ and `singletonsOnly`) is whether the `genQuotedDecs` option is set to+ `True` or `False`, respectively. Therefore, if `genQuotedDecs` is set to+ `False` when promoting the fixity declaration for an infix value, we opt to+ generate a fixity declaration (with the same name base) so that the+ type-level version of that value gets one. * During singling, the following things will not have their fixity declarations singled:
src/Data/Singletons/TH/Single/Type.hs view
@@ -33,10 +33,10 @@ prom_args <- mapM promoteType_NC args prom_res <- promoteType_NC res let args' = map (\n -> singFamily `DAppT` (DVarT n)) arg_names- res' = singFamily `DAppT` (foldApply prom (map DVarT arg_names) `DSigT` prom_res)+ res' = singFamily `DAppT` (foldType prom (map DVarT arg_names) `DSigT` prom_res) -- Make sure to include an explicit `prom_res` kind annotation. -- See Note [Preserve the order of type variables during singling],- -- wrinkle 3.+ -- wrinkle 2. arg_tvbs = zipWith (`DKindedTV` SpecifiedSpec) arg_names prom_args -- If the original type signature lacks an explicit `forall`, then do not -- give the singled type signature an outermost `forall`. Instead, give it@@ -204,56 +204,7 @@ SMkT :: forall a (x :: a). Sing x -> ST (MkT x) -------- Wrinkle 2: The TH reification swamp--------There is another issue with type signatures that lack explicit `forall`s, one-which the current design of Template Haskell does not make simple to fix.-If we single code that is wrapped in TH quotes, such as in the following example:-- {-# LANGUAGE PolyKinds, ... #-}- $(singletons [d|- data Proxy a = MkProxy- |])--Then our job is made much easier when singling MkProxy, since we know that the-only type variable that must be quantified is `a`, as that is the only one-specified by the user. This results in the following type signature for-MkProxy:-- MkProxy :: forall a. Proxy a--However, this is not the only possible way to single MkProxy. One can-alternatively use $(genSingletons [''Proxy]), which uses TH reification to-infer the type of MkProxy. There is perilous, however, because this is how-TH reifies Proxy:-- DataD- [] ''Proxy [KindedTV a () (VarT k)] Nothing- [NormalC 'MkProxy []]- []--We must then construct a type signature for MkProxy using nothing but the type-variables from the data type header. But notice that `KindedTV a () (VarT k)`-gives no indication of whether `k` is specified or inferred! As a result, we-conservatively assume that `k` is specified, resulting the following type-signature for MkProxy:-- MkProxy :: forall k (a :: k). Proxy a--Contrast this with `MkProxy :: Proxy a`, where `k` is inferred. In other words,-if you single MkProxy using genSingletons, then `Proxy @True` will typecheck-but `SMkProxy @True` will /not/ typecheck—you'd have to use-`SMkProxy @_ @True` instead. Urk!--At present, Template Haskell does not have a way to distinguish among the-specificities bound by a data type header. Without this knowledge, it is-unclear how one could work around this issue. Thankfully, this issue is-only likely to surface in very limited circumstances, so the damage is somewhat-minimal.---------- Wrinkle 3: Where to put explicit kind annotations+-- Wrinkle 2: Where to put explicit kind annotations ----- Type variable binders are only part of the story—we must also determine what@@ -304,28 +255,49 @@ SNothing :: forall a. SMaybe (Nothing @a) This does work for many cases, but there are also some corner cases where this-approach fails. Recall the `MkProxy` example from Wrinkle 2 above:+approach fails. Suppose that `Nothing` was declared like so: - {-# LANGUAGE PolyKinds, ... #-}- data Proxy a = MkProxy- $(genSingletons [''Proxy])+ Nothing :: forall {a}. Maybe a -Due to the design of Template Haskell (discussed in Wrinkle 2), `MkProxy` will-be reified with the type of `forall k (a :: k). Proxy a`. This means that-if we used visible kind applications in the result type, we would end up with-this:+Then we couldn't write `Nothing @a`, as `a` wouldn't be eligible for visible+kind application. (GHC Core would let you write `Nothing @{a}`, but this isn't+possible in source Haskell.) As such, the only way to fix the type of `a` in+`Maybe a` would be to write `Nothing :: Maybe a`. - SMkProxy :: forall k (a :: k). SProxy (MkProxy @k @a)+An even more obscure corner case is when a type quantifies a type variable+without mentioning it at all in the rest of the type, e.g., -This will not kind-check because MkProxy only accepts /one/ visible kind argument,-whereas this supplies it with two. To avoid this issue, we instead use the type-`forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/-technically wrong due to the fact that it explicitly quantifies `k`, but at the-very least it typechecks. If Template Haskell gained the ability to distinguish-among the specificities of type variables bound by a data type header-(perhaps by way of a language feature akin to-https://github.com/ghc-proposals/ghc-proposals/pull/326), then we could revisit-this design choice.+ C :: forall a. D++At present, singletons-th does not handle this type of corner case at all. It+wouldn't suffice to single `C` to the following:++ SC :: forall a. SD (C :: D)++This is because the `a` argument to `C` is left ambiguous in the type `C :: D`,+as the return kind `D` doesn't indicate what `a` should be. In theory, we+/could/ write `C @a :: D` instead, which would solve that particular problem.+But there would still be trouble on the horizon, as there are other types of+code that singletons-th generates which exhibit similar sorts of ambiguity. For+example, here is the defunctionalization symbol that singletons-th would+generate for `C`:++ type CSym0 :: forall a. D+ type family CSym0 @a :: D where+ CSym0 = C++GHC will reject this type family equation, also for ambiguity-related reasons:++ error: [GHC-16220]+ • Uninferrable type variables k0, (a0 :: k0) in+ the type family equation right-hand side: C @{k0} @a0+ • In the type family declaration for ‘CSym0’++This is fixable, but we would need to audit all potential sources of type+variable-related ambiguity in singletons-th–generated code and make sure that+we have covered our bases. Given that types such as `forall a. D` are rare in+practice, I'm inclined not to worry about this unless someone specifically asks+for this featurette. Finally, note that we need only write `Sing x_1 -> ... -> Sing x_p`, and not `Sing (x_1 :: PT_1) -> ... Sing (x_p :: PT_p)`. This is simply because we
src/Data/Singletons/TH/Syntax.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {- Data/Singletons/TH/Syntax.hs@@ -10,7 +9,10 @@ and contains various other AST definitions. -} -module Data.Singletons.TH.Syntax where+module Data.Singletons.TH.Syntax+ ( module Data.Singletons.TH.Syntax+ , module Data.Singletons.TH.Syntax.LocalVar+ ) where import Prelude hiding ( exp ) import Data.Kind (Constraint, Type)@@ -20,13 +22,17 @@ import Language.Haskell.TH.Desugar.OMap.Strict (OMap) import Language.Haskell.TH.Desugar.OSet (OSet) -type VarPromotions = [(Name, Name)] -- from term-level name to type-level name+import Data.Singletons.TH.Syntax.LocalVar +-- | Pairs of term-level variable 'Name's and their corresponding type-level+-- names (encoded as 'LocalVar's).+type VarPromotions = [(Name, LocalVar)]+ -- Information that is accumulated when promoting patterns. data PromDPatInfos = PromDPatInfos { prom_dpat_vars :: VarPromotions -- Maps term-level pattern variables to their promoted, type-level counterparts.- , prom_dpat_sig_kvs :: OSet Name+ , prom_dpat_sig_kvs :: OSet LocalVar -- Kind variables bound by DSigPas. -- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad. }@@ -101,11 +107,16 @@ | ADConE Name | ADLitE Lit | ADAppE ADExp ADExp- | ADLamE [Name] -- type-level names corresponding to term-level ones- DType -- the promoted lambda- [Name] ADExp- | ADCaseE ADExp [ADMatch] DType- -- the type is the return type+ | ADLamCasesE+ Int+ -- ^ The number of arguments in each clause. Although this can be+ -- computed from the list of ADClauses, this information is used+ -- multiple times during promotion and singling, so we cache this+ -- number here as a convenience.+ DType+ -- ^ The promoted lambda.+ [ADClause]+ -- ^ The list of clauses in the @\\cases@ expression. | ADLetE ALetDecEnv ADExp | ADSigE DType -- the promoted expression ADExp DType@@ -121,7 +132,6 @@ ADPat DType | ADWildP -data ADMatch = ADMatch VarPromotions ADPat ADExp data ADClause = ADClause VarPromotions [ADPat] ADExp @@ -155,11 +165,28 @@ type ALetDecRHS = LetDecRHS Annotated type ULetDecRHS = LetDecRHS Unannotated +-- | A @let@-bound, term-level name that is promoted to the type level. The+-- first element of the pair (of type 'Name') is the promoted counterpart to the+-- term-level name, and the second element of the pair (of type @[Name]@) is the+-- list of local variables that this definition closes over after being+-- lambda-lifted. (See @Note [Tracking local variables]@ in+-- "Data.Singletons.TH.Promote.Monad".)+--+-- Note that the promoted Name in the first element of the pair is /not/ a+-- defunctionalization symbol, unlike 'LetBind' in+-- "Data.Singletons.TH.Promote.Monad". This is because it is sometimes+-- convenient to fully apply the promoted name to all of its arguments (e.g.,+-- when singling type signatures), in which case we can avoid needing to involve+-- defunctionalization symbols at all.+type LetDecProm = (Name, [LocalVar])+ data LetDecEnv ann = LetDecEnv { lde_defns :: OMap Name (LetDecRHS ann) , lde_types :: OMap Name DType -- type signatures- , lde_infix :: OMap Name Fixity -- infix declarations- , lde_proms :: IfAnn ann (OMap Name DType) () -- possibly, promotions+ , lde_infix :: OMap Name (Fixity, NamespaceSpecifier) -- infix declarations+ , lde_proms :: IfAnn ann (OMap Name LetDecProm) ()+ -- ^ If annotated, this maps let-bound term 'Name's to+ -- their promoted counterparts. } type ALetDecEnv = LetDecEnv Annotated type ULetDecEnv = LetDecEnv Unannotated@@ -177,8 +204,8 @@ typeBinding :: Name -> DType -> ULetDecEnv typeBinding n t = emptyLetDecEnv { lde_types = OMap.singleton n t } -infixDecl :: Fixity -> Name -> ULetDecEnv-infixDecl f n = emptyLetDecEnv { lde_infix = OMap.singleton n f }+infixDecl :: Fixity -> NamespaceSpecifier -> Name -> ULetDecEnv+infixDecl f ns n = emptyLetDecEnv { lde_infix = OMap.singleton n (f, ns) } emptyLetDecEnv :: ULetDecEnv emptyLetDecEnv = mempty@@ -196,8 +223,8 @@ go acc (flattened ++ rest) go acc (DSigD name ty : rest) = go (typeBinding name ty <> acc) rest- go acc (DInfixD f _ n : rest) =- go (infixDecl f n <> acc) rest+ go acc (DInfixD f ns n : rest) =+ go (infixDecl f ns n <> acc) rest go acc (DPragmaD{} : rest) = go acc rest -- See Note [DerivedDecl]
+ src/Data/Singletons/TH/Syntax/LocalVar.hs view
@@ -0,0 +1,252 @@+module Data.Singletons.TH.Syntax.LocalVar+ ( LocalVar(..)+ , foldTypeLocalVars+ , localVarToTvb+ , localVarToType+ , localVarToTypeArg+ , tvbToLocalVar+ ) where++import Data.Data (Data)+import Data.Function (on)+import Language.Haskell.TH.Desugar+import Language.Haskell.TH.Syntax++-- | A local variable that is captured in a lambda-lifted type family. (See+-- @Note [Tracking local variables]@ in "Data.Singletons.TH.Promote.Monad" for+-- an explanation of how lambda lifting works.) A 'LocalVar' consists of:+--+-- * An @'lvName' :: 'Name'@ that corresponds to the promoted, type-level+-- version of a term-level variable name.+--+-- * An optional @'lvKind' :: 'Maybe' 'DKind'@. When the kind of a local+-- variable is known, we can use it to generate code with more precise kind+-- information. See @Note [Local variables and kind information]@.+--+-- We maintain the invariant that if two 'LocalVar' values share the same+-- 'lvName', then they should both have the same 'lvKind' value.+--+-- A 'LocalVar' is very close in design to a 'DTyVarBndrUnit', as both contain+-- 'Name's and optional 'DKind's. We use a separate 'LocalVar' type to represent+-- local variables because 'LocalVar's can occur both in binding and argument+-- positions in generated code (see @Note [Local variables and kind information]+-- (Wrinkle: Binding positions versus argument positions)@), and using+-- 'DTyVarBndrUnit's to represent type arguments feels somewhat awkward.+data LocalVar = LocalVar+ { lvName :: Name+ , lvKind :: Maybe DKind+ } deriving (Data, Show)++-- Because of the invariant described in the Haddocks for 'LocalVar', it+-- suffices to only check the 'lvName's when checking 'LocalVar's for equality.+instance Eq LocalVar where+ (==) = (==) `on` lvName++-- Because of the invariant described in the Haddocks for 'LocalVar', it+-- suffices to only compare the 'lvName's when comparing 'LocalVar's.+instance Ord LocalVar where+ compare = compare `on` lvName++-- | Apply a 'DType' to a list of 'LocalVar' arguments. Because these+-- 'LocalVar's occur in argument positions, they will not contain any kind+-- information. See @Note [Local variables and kind information] (Wrinkle:+-- Binding positions versus argument positions)@.+foldTypeLocalVars :: DType -> [LocalVar] -> DType+foldTypeLocalVars ty = applyDType ty . map localVarToTypeArg++-- | Convert a 'LocalVar' used in a binding position to a 'DTyVarBndr' using the+-- supplied @flag@. Because this is used in a binding position, we include kind+-- information (if available) in the 'DTyVarBndr'. See @Note [Local variables+-- and kind information] (Wrinkle: Binding positions versus argument+-- positions)@.+localVarToTvb :: flag -> LocalVar -> DTyVarBndr flag+localVarToTvb flag (LocalVar { lvName = nm, lvKind = mbKind }) =+ case mbKind of+ Nothing -> DPlainTV nm flag+ Just kind -> DKindedTV nm flag kind++-- | Convert a 'LocalVar' used in an argument position to a 'DType'. Because+-- this is used in an argument positions, it will not kind any kind information.+-- See @Note [Local variables and kind information] (Wrinkle: Binding positions+-- versus argument positions)@.+localVarToType :: LocalVar -> DType+localVarToType (LocalVar { lvName = local_nm }) = DVarT local_nm++-- | Convert a 'LocalVar' used in an argument position to a 'DTypeArg'. Because+-- this is used in an argument positions, it will not kind any kind information.+-- See @Note [Local variables and kind information] (Wrinkle: Binding positions+-- versus argument positions)@.+localVarToTypeArg :: LocalVar -> DTypeArg+localVarToTypeArg = DTANormal . localVarToType++-- | Convert a 'DTyVarBndr' to a 'LocalVar'.+tvbToLocalVar :: DTyVarBndr flag -> LocalVar+tvbToLocalVar (DPlainTV nm _) =+ LocalVar { lvName = nm, lvKind = Nothing }+tvbToLocalVar (DKindedTV nm _ kind) =+ LocalVar { lvName = nm, lvKind = Just kind }++{-+Note [Local variables and kind information]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Consider the following function, which we want to promote to the type level:++ f :: forall a. a -> a+ f x = y+ where+ y = y++Per Note [Tracking local variables]@ in Data.Singletons.TH.Promote.Monad, we+observe that `y` closes over two local variables, `a` and `x`. A naïve attempt+at promoting this code would result in generate code that looks something like+this:++ type F :: forall a. a -> a+ type family F x where+ F @a x = LetY a x++ type family LetY a x where+ LetY a x = x++In today's GHC, this kind-checks. However, the generated code is somewhat+unsatisfying, as GHC infers a kind for LetY that is way more general than it+should be:++ LetY :: forall k1 k2. k1 -> k2 -> k2++Note that this inferred kind says nothing about the relationship between the+first and second visible arguments. In today's GHC, this works because the body+of LetY requires the kind of the second visible argument to be equal to the+first visible argument in order to match. It would be as if you had written+this code:++ type LetY :: forall k1 k2. k1 -> k2 -> k2+ type family LetY a x where+ LetY @Type @a (a :: Type) (x :: a) = x++This sort of thing will cause problems once+https://gitlab.haskell.org/ghc/ghc/-/issues/23515 is implemented. As such, we+should strive to do better.++Fortunately, there is a relatively easy fix that works well here. We observe+that we know what the kind of `x` just by looking at the syntax of `f`'s+definition, as we can pair up the `x` argument with the `a` argument type in+`f`'s type. As such, we can remember that `x :: a` and instead generate:++ type family LetY a (x :: a) where+ LetY a x = x++Now GHC infers exactly the kind we'd want for LetY:++ LetY :: forall a -> a -> a++On the implementation side, we achive this by tracking optional kind+information in each LocalVar (in the form of a `Maybe DKind` field). A key+place in the code where kind information is propagated through to LocalVars is+the `promotePat` function in Data.Singletons.TH.Promote, which takes a `Maybe+DKind` field that describes the kind of the pattern being promoted (if it is+known). This allows recording the types of DSigP patterns (e.g., the `y :: b`+pattern in `g (y :: b) = Nothing :: Maybe b`), as well as recording the kinds+of variable patterns whose types are described by top-level top signatures+(e.g., the `x` pattern in the `f x = y` example above).++This approach has its limitations. Consider this slightly more complicated+example:++ f' :: forall a. [a] -> Maybe (a, [a])+ f' [] = Nothing+ f' (x:xs) = y+ where+ y = Just (x, xs)++Note that the patterns for the arguments to `f'` aren't bare variables this+time, but rather constructor patterns. As such, we don't know the types of `x`+and `xs` just by looking at the syntax of `f'`. Instead, we'd have to do some+more clever analysis to conclude that `x :: a` and `xs :: [a]`. This is perhaps+doable, but it would require something akin to implementing type inference in+Template Haskell, which is a direction of travel that I am reluctant to go+down.++As such, we do not record the types of the `x` or `xs` variables in this+example, meaning that we promote `f'` to the following:++ type F' :: forall a. [a] -> Maybe (a, [a])+ type family F' l where+ F' @a '[] = Nothing+ F' @a (x:xs) = LetY a x xs++ type family LetY a x xs where+ LetY a x xs = Just '(x, xs)++And GHC will infer an overly polymorphic kind for LetY:++ LetY :: k1 -> k2 -> k3 -> Maybe (k2, k3)++If this proves to be troublesome in the future, we could consider refining this+approach. It is also worth nothing that in the event that singletons-th+generates a local definition with an overly polymorphic kind, one can always+constrain the kind by inserting more pattern signatures. For instance, if you+redefine `f'` to be the following:++ f' :: forall a. [a] -> Maybe (a, [a])+ f' [] = Nothing+ f' ((x :: a) : (xs :: [a])) = y -- This line now has pattern signatures+ where+ y = Just (x, xs)++Then singletons-th will now realize what the kinds of `x` and `xs` are, and it+will generate code for `LetY` that uses these kinds.++-----+-- Wrinkle: Binding positions versus argument positions+-----++Although we track the kinds of local variables throughout promotion, we don't+want to necessarily generate code involving the kind in all circumstances.+Consider this example:++fNoScope :: a -> a+fNoScope x = y+ where+ y = x++`fNoScope` is like `f` above, except that `a` does not scope over the body of+the function due to the lack of an outermost `forall` in the type signature. On+the other hand, `x` /does/ scope over the body, so we close over `x` when+lambda lifting `y`. Moreover, we know that the type of `x` is `a`. However, we+must be careful not to promote `fNoScope` to the following:++ type FNoScope :: a -> a+ type family FNoScope x where+ FNoScope x = LetY (x :: a)++ type family LetY (x :: a) where+ LetY (x :: a) = x++The problem with this code lies here:++ FNoScope x = LetY (x :: a)++Note that `a` is not in scope in this line! Even though we know that `x :: a`,+that doesn't mean that we can unconditionally generate the code `x :: a` in all+places, since `a` may not be in scope in all places. Of course, we /do/ want to+generate `x :: a` in this line:++ type family LetY (x :: a) where++The distinction between the two lines is one of binding positions versus+argument positions. In the former case, `x` occurs as an argument to a `LetY`+application, whereas in the latter case, `x` occurs as a type variable binder+when defining `LetY`. In binding positions such as these, `x :: a` will+implicitly quantify `a`, so it is fine to unconditionally use `x :: a` in these+positions. Implicit quantification does not occur in argument positions,+however, so we leave out the `:: a` kind signature in these positions. (This is+perfectly fine to do, since `x` will be bound somewhere else, and that binder+will include the `a` kind information.)++Implementation-wise, the difference between these two positions is embodied in+the `localVarToTvb` function (for converting `LocalVar`s to binding positions)+and the `localVarToType` function (for converting `LocalVar`s to argument+positions). Note that the derived functions `localVarToTypeArg` and+`foldTypeLocalVars` also treat `LocalVar`s as argument positions.+-}
src/Data/Singletons/TH/Util.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE LambdaCase #-}- {- Data/Singletons/TH/Util.hs (c) Richard Eisenberg 2013@@ -15,6 +13,7 @@ import Language.Haskell.TH ( pprint ) import Language.Haskell.TH.Syntax hiding ( lift ) import Language.Haskell.TH.Desugar+import qualified Language.Haskell.TH.Desugar.Subst.Capturing as SC import Data.Char import Control.Monad ( liftM, unless, when ) import Control.Monad.Except ( ExceptT, runExceptT, MonadError(..) )@@ -24,13 +23,14 @@ import Control.Monad.Writer ( MonadWriter(..), WriterT(..), execWriterT ) import qualified Data.Map as Map import Data.Map ( Map )-import Data.Bifunctor (second) import Data.Foldable import Data.Functor.Identity import Data.Traversable import Data.Generics import Data.Maybe +import Data.Singletons.TH.Syntax.LocalVar+ -- like reportWarning, but generalized to any Quasi qReportWarning :: Quasi q => String -> q () qReportWarning = qReport False@@ -209,16 +209,6 @@ extractTvbFlag (DPlainTV _ f) = f extractTvbFlag (DKindedTV _ f _) = f --- Map over the 'Name' of a 'DTyVarBndr'.-mapDTVName :: (Name -> Name) -> DTyVarBndr flag -> DTyVarBndr flag-mapDTVName f (DPlainTV name flag) = DPlainTV (f name) flag-mapDTVName f (DKindedTV name flag kind) = DKindedTV (f name) flag kind---- Map over the 'DKind' of a 'DTyVarBndr'.-mapDTVKind :: (DKind -> DKind) -> DTyVarBndr flag -> DTyVarBndr flag-mapDTVKind _ tvb@(DPlainTV{}) = tvb-mapDTVKind f (DKindedTV name flag kind) = DKindedTV name flag (f kind)- tvbToType :: DTyVarBndr flag -> DType tvbToType = DVarT . extractTvbName @@ -267,8 +257,16 @@ -- @ -- -- Note that note of @b@, @d@, or @e@ appear in the list.-tvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]-tvbSpecsToBndrVis = mapMaybe (traverse specificityToBndrVis)+--+-- See also 'dtvbForAllTyFlagsToBndrVis', which takes a list of @'DTyVarBndr'+-- 'ForAllTyFlag'@ as arguments instead of a list of 'DTyVarBndrSpec's. Note+-- that @'dtvbSpecsToBndrVis' . 'dtvbForAllTyFlagsToSpecs'@ is /not/ the same+-- thing as 'dtvbForAllTyFlagsToBndrVis'. This is because 'dtvbSpecsToBndrVis'+-- only produces 'BndrInvis' binders as output, whereas+-- 'dtvbForAllTyFlagsToBndrVis' can produce both 'BndrReq' and 'BndrInvis'+-- binders.+dtvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]+dtvbSpecsToBndrVis = mapMaybe (traverse specificityToBndrVis) where specificityToBndrVis :: Specificity -> Maybe BndrVis specificityToBndrVis SpecifiedSpec = Just BndrInvis@@ -430,6 +428,7 @@ `extT` fix_tvb @BndrVis `extT` fix_ty `extT` fix_inj_ann+ `extT` fix_local_var fix_tvb :: Typeable flag => DTyVarBndr flag -> DTyVarBndr flag fix_tvb (DPlainTV n f) = DPlainTV (noExactName n) f@@ -441,6 +440,10 @@ fix_inj_ann (InjectivityAnn lhs rhs) = InjectivityAnn (noExactName lhs) (map noExactName rhs) + fix_local_var :: LocalVar -> LocalVar+ fix_local_var (LocalVar { lvName = n, lvKind = mbKind })+ = LocalVar { lvName = noExactName n, lvKind = mbKind }+ -- Changes a unique Name with a NameU or NameL namespace to a non-unique Name. -- See Note [Pitfalls of NameU/NameL] for why this is useful. noExactName :: Name -> Name@@ -528,47 +531,10 @@ locations where we must apply this workaround. -} -substKind :: Map Name DKind -> DKind -> DKind-substKind = substType---- | Non–capture-avoiding substitution. (If you want capture-avoiding--- substitution, use @substTy@ from "Language.Haskell.TH.Desugar.Subst".-substType :: Map Name DType -> DType -> DType-substType subst ty | Map.null subst = ty-substType subst (DForallT tele inner_ty)- = DForallT tele' inner_ty'- where- (subst', tele') = subst_tele subst tele- inner_ty' = substType subst' inner_ty-substType subst (DConstrainedT cxt inner_ty) =- DConstrainedT (map (substType subst) cxt) (substType subst inner_ty)-substType subst (DAppT ty1 ty2) = substType subst ty1 `DAppT` substType subst ty2-substType subst (DAppKindT ty ki) = substType subst ty `DAppKindT` substType subst ki-substType subst (DSigT ty ki) = substType subst ty `DSigT` substType subst ki-substType subst (DVarT n) =- case Map.lookup n subst of- Just ki -> ki- Nothing -> DVarT n-substType _ ty@(DConT {}) = ty-substType _ ty@(DArrowT) = ty-substType _ ty@(DLitT {}) = ty-substType _ ty@DWildCardT = ty--subst_tele :: Map Name DKind -> DForallTelescope -> (Map Name DKind, DForallTelescope)-subst_tele s (DForallInvis tvbs) = second DForallInvis $ substTvbs s tvbs-subst_tele s (DForallVis tvbs) = second DForallVis $ substTvbs s tvbs--substTvbs :: Map Name DKind -> [DTyVarBndr flag] -> (Map Name DKind, [DTyVarBndr flag])-substTvbs = mapAccumL substTvb--substTvb :: Map Name DKind -> DTyVarBndr flag -> (Map Name DKind, DTyVarBndr flag)-substTvb s tvb@(DPlainTV n _) = (Map.delete n s, tvb)-substTvb s (DKindedTV n f k) = (Map.delete n s, DKindedTV n f (substKind s k))- substFamilyResultSig :: Map Name DKind -> DFamilyResultSig -> (Map Name DKind, DFamilyResultSig) substFamilyResultSig s frs@DNoSig = (s, frs)-substFamilyResultSig s (DKindSig k) = (s, DKindSig (substKind s k))-substFamilyResultSig s (DTyVarSig tvb) = let (s', tvb') = substTvb s tvb in+substFamilyResultSig s (DKindSig k) = (s, DKindSig (SC.substTy s k))+substFamilyResultSig s (DTyVarSig tvb) = let (s', tvb') = SC.substTyVarBndr s tvb in (s', DTyVarSig tvb') dropTvbKind :: DTyVarBndr flag -> DTyVarBndr flag@@ -605,8 +571,7 @@ -- build a pattern match over several expressions, each with only one pattern multiCase :: [DExp] -> [DPat] -> DExp -> DExp multiCase [] [] body = body-multiCase scruts pats body =- DCaseE (mkTupleDExp scruts) [DMatch (mkTupleDPat pats) body]+multiCase scruts pats body = dCasesE scruts [DClause pats body] -- a monad transformer for writing a monoid alongside returning a Q newtype QWithAux m q a = QWA { runQWA :: WriterT m q a }