singletons-th 3.1.1 → 3.5.1
raw patch · 31 files changed
Files
- CHANGES.md +102/−0
- README.md +1/−1
- singletons-th.cabal +11/−9
- src/Data/Singletons/TH.hs +54/−5
- src/Data/Singletons/TH/CustomStar.hs +2/−2
- src/Data/Singletons/TH/Deriving/Bounded.hs +14/−6
- src/Data/Singletons/TH/Deriving/Enum.hs +2/−2
- src/Data/Singletons/TH/Deriving/Eq.hs +1/−1
- src/Data/Singletons/TH/Deriving/Foldable.hs +3/−3
- src/Data/Singletons/TH/Deriving/Functor.hs +4/−4
- src/Data/Singletons/TH/Deriving/Ord.hs +2/−2
- src/Data/Singletons/TH/Deriving/Show.hs +2/−2
- src/Data/Singletons/TH/Deriving/Traversable.hs +2/−2
- src/Data/Singletons/TH/Deriving/Util.hs +17/−3
- src/Data/Singletons/TH/Names.hs +9/−5
- src/Data/Singletons/TH/Options.hs +1/−1
- src/Data/Singletons/TH/Partition.hs +17/−10
- src/Data/Singletons/TH/Promote.hs +1583/−1152
- src/Data/Singletons/TH/Promote/Defun.hs +193/−130
- src/Data/Singletons/TH/Promote/Monad.hs +500/−89
- src/Data/Singletons/TH/Single.hs +178/−390
- src/Data/Singletons/TH/Single/Data.hs +88/−43
- src/Data/Singletons/TH/Single/Decide.hs +55/−29
- src/Data/Singletons/TH/Single/Defun.hs +0/−1
- src/Data/Singletons/TH/Single/Fixity.hs +58/−30
- src/Data/Singletons/TH/Single/Monad.hs +37/−27
- src/Data/Singletons/TH/Single/Ord.hs +43/−0
- src/Data/Singletons/TH/Single/Type.hs +116/−120
- src/Data/Singletons/TH/Syntax.hs +68/−38
- src/Data/Singletons/TH/Syntax/LocalVar.hs +252/−0
- src/Data/Singletons/TH/Util.hs +171/−60
CHANGES.md view
@@ -1,6 +1,108 @@ 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.+* GHC 9.10 removes arity inference when kind-checking type families with+ standalone kind signatures, persuant to [this GHC+ proposal](https://github.com/ghc-proposals/ghc-proposals/blob/10290a668608d608c3f6c6010be265cf7a02e1fc/proposals/0425-decl-invis-binders.rst#breakage-2-arity-inference).+ In order to promote functions to type families with correct arities,+ `singletons-th` uses `TypeAbstractions` to bind type variable binders in the+ headers of promoted type families. As such, it is quite likely that you will+ need to enable `TypeAbstractions` in order to make GHC accept code that+ `singletons-th` generates.+* Fix a bug causing definitions with type signatures using inferred type+ variable binders (e.g., `forall a {b}. a -> b -> a`) to fail to promote.++3.3 [2023.10.13]+----------------+* Require building with GHC 9.8.+* Singled data types with derived `Eq` or `Ord` instances now generate `Eq` or+ `Ord` instances for the singleton type itself, e.g.,++ ```hs+ instance Eq (SExample a) where+ _ == _ = True++ instance Ord (SExample a) where+ compare _ _ = EQ+ ```+* `singletons-th` now makes an effort to promote definitions that use scoped+ type variables. See the "Scoped type variables" section of the `README` for+ more information about what `singletons-th` can (and can't) do.+* `singletons-th` now supports singling type-level definitions that use+ `TypeAbstractions`.+* Fix a bug in which data types using visible dependent quantification would+ generate ill-scoped code when singled.+* Fix a bug in which singling a local variable that shadows a top-level+ definition would fail to typecheck in some circumstances.+* Fix a bug in which `singletons-th` would incorrectly promote/single records+ to top-level field selectors when `NoFieldSelectors` was active.++3.2 [2023.03.12]+----------------+* Require building with GHC 9.6.+* Derived `POrd` and `SOrd` instances (arising from a use of `deriving Ord`)+ now use `(<>) @Ordering` in their implementations instead of the custom+ `thenCmp :: Ordering -> Ordering -> Ordering` function. While most code will+ likely continue to work after this change, this may break code that attempts+ to prove properties about the implementation of a derived `POrd`/`SOrd`+ instance.+* Fix a bug in which the `singDecideInstances` and `showSingInstances`, as well+ as `deriving Show` declarations, would not respect custom+ `promotedDataTypeOrConName` options.+* Allow building with `mtl-2.3.*`.+ 3.1.1 [2022.08.23] ------------------ * Require building with GHC 9.4.
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.4). 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.1.1+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.4.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.4). 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>@. .@@ -42,7 +42,7 @@ type: git location: https://github.com/goldfirere/singletons.git subdir: singletons-th- tag: v3.1.1+ tag: v3.1.2 source-repository head type: git@@ -52,17 +52,17 @@ library hs-source-dirs: src- build-depends: base >= 4.17 && < 4.18,+ build-depends: base >= 4.22 && < 4.23, containers >= 0.5,- mtl >= 2.2.1,+ mtl >= 2.2.1 && < 2.4, ghc-boot-th, singletons == 3.0.*, syb >= 0.4,- template-haskell >= 2.19 && < 2.20,- th-desugar >= 1.14 && < 1.15,+ 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@@ -91,8 +91,10 @@ Data.Singletons.TH.Single.Defun Data.Singletons.TH.Single.Fixity Data.Singletons.TH.Single.Monad+ 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
@@ -71,8 +71,54 @@ -- is identical. This may be useful if the type-checker requires knowledge of which -- constructor is used to satisfy equality or type-class constraints, but where -- each constructor is treated the same.+--+-- Here is a simple example to illustrate where 'cases' can be useful. Suppose+-- you use @singletons-th@ to single this code:+--+-- @+-- $('singletons' [d|+-- foo :: Bool -> ()+-- foo True = ()+-- foo False = ()+-- |])+-- @+--+-- And that you want to write a function of this type:+--+-- @+-- bar :: SBool b -> STuple0 (Foo b)+-- @+--+-- How would you do this? You might be tempted to write the following:+--+-- @+-- bar _ = STuple0+-- @+--+-- However, this won't typecheck, as Foo b won't reduce to @'()@ unless GHC+-- knows @b@ is either 'True' or 'False'. In order to convince GHC of this, you+-- must explicitly match on each of the data constructors of @SBool@:+--+-- @+-- bar :: SBool b -> STuple0 (Foo b)+-- bar b = case b of+-- STrue -> STuple0+-- SFalse -> STuple0+-- @+--+-- This is doable, but it is somewhat tedious. After all, the right-hand side+-- of each case alternative is exactly the same! This only becomes more tedious+-- when you deal with data types with lots of lots of data constructors. For+-- this reason, @singletons-th@ offers the 'cases' function to generate this+-- boilerplate code for you. The following is equivalent to the implementation+-- of @bar@ above:+--+-- @+-- bar :: SBool b -> STuple0 (Foo b)+-- bar b = $(cases ''SBool [| b |] [| STuple0 |])+-- @ cases :: DsMonad q- => Name -- ^ The head of the type of the scrutinee. (Like @''Maybe@ or @''Bool@.)+ => Name -- ^ The head of the type of the scrutinee. (e.g., @''SBool@) -> q Exp -- ^ The scrutinee, in a Template Haskell quote -> q Exp -- ^ The body, in a Template Haskell quote -> q Exp@@ -89,9 +135,12 @@ -- | The function 'sCases' generates a case expression where each right-hand side -- is identical. This may be useful if the type-checker requires knowledge of which -- constructor is used to satisfy equality or type-class constraints, but where--- each constructor is treated the same. For 'sCases', unlike 'cases', the--- scrutinee is a singleton. But make sure to pass in the name of the /original/--- datatype, preferring @''Maybe@ over @''SMaybe@.+-- each constructor is treated the same.+--+-- For 'sCases', unlike 'cases', the scrutinee is a singleton. But make sure to+-- pass in the name of the /original/ datatype, preferring @''Maybe@ over+-- @''SMaybe@. In other words, @sCases ''Maybe@ is equivalent to+-- @'cases' ''SMaybe@. sCases :: OptionsMonad q => Name -- ^ The head of the type the scrutinee's type is based on. -- (Like @''Maybe@ or @''Bool@.)@@ -116,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.@@ -81,7 +81,7 @@ let repDecl = DDataD Data [] repName [] (Just (DConT typeKindName)) ctors [DDerivClause Nothing (map DConT [''Eq, ''Ord, ''Read, ''Show])] fakeCtors <- zipWithM (mkCtor False) names kinds- let dataDecl = DataDecl repName [] fakeCtors+ let dataDecl = DataDecl Data repName [] fakeCtors -- Why do we need withLocalDeclarations here? It's because we end up -- expanding type synonyms when deriving instances for Rep, which requires -- reifying Rep itself. Since Rep hasn't been spliced in yet, we must put it
src/Data/Singletons/TH/Deriving/Bounded.hs view
@@ -25,20 +25,28 @@ -- monadic only for failure and parallelism with other functions -- that make instances mkBoundedInstance :: DsMonad q => DerivDesc q-mkBoundedInstance mb_ctxt ty (DataDecl _ _ cons) = do+mkBoundedInstance mb_ctxt ty (DataDecl _ _ _ cons) = do -- We can derive instance of Bounded if datatype is an enumeration (all -- constructors must be nullary) or has only one constructor. See Section 11 -- of Haskell 2010 Language Report. -- Note that order of conditions below is important.- when (null cons- || (any (\(DCon _ _ _ f _) -> not . null . tysOfConFields $ f) cons- && (not . null . tail $ cons))) $+ let illegal_bounded_inst =+ case cons of+ [] -> True+ _:cons' ->+ any (\(DCon _ _ _ f _) -> not . null . tysOfConFields $ f) cons+ && not (null cons')+ when illegal_bounded_inst $ fail ("Can't derive Bounded instance for " ++ pprint (typeToTH ty) ++ ".") -- at this point we know that either we have a datatype that has only one -- constructor or a datatype where each constructor is nullary- let (DCon _ _ minName fields _) = head cons- (DCon _ _ maxName _ _) = last cons+ let internal_err = fail "Internal error (mkBoundedInstance): non-empty list of constructors"+ DCon _ _ minName fields _ <-+ case cons of+ (c:_) -> pure c+ [] -> internal_err+ let (_, DCon _ _ maxName _ _) = snocView cons fieldsCount = length $ tysOfConFields fields (minRHS, maxRHS) = case fieldsCount of 0 -> (DConE minName, DConE maxName)
src/Data/Singletons/TH/Deriving/Enum.hs view
@@ -25,7 +25,7 @@ -- monadic for failure only mkEnumInstance :: DsMonad q => DerivDesc q-mkEnumInstance mb_ctxt ty (DataDecl _ _ cons) = do+mkEnumInstance mb_ctxt ty (DataDecl _ _ _ cons) = do -- GHC only allows deriving Enum instances for enumeration types (i.e., those -- data types whose constructors all lack fields). We perform the same -- validity check here.@@ -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/Eq.hs view
@@ -22,7 +22,7 @@ import Language.Haskell.TH.Syntax mkEqInstance :: DsMonad q => DerivDesc q-mkEqInstance mb_ctxt ty (DataDecl _ _ cons) = do+mkEqInstance mb_ctxt ty (DataDecl _ _ _ cons) = do let con_pairs = [ (c1, c2) | c1 <- cons, c2 <- cons ] constraints <- inferConstraintsDef mb_ctxt (DConT eqName) ty cons clauses <- if null cons
src/Data/Singletons/TH/Deriving/Foldable.hs view
@@ -20,12 +20,12 @@ import Language.Haskell.TH.Desugar mkFoldableInstance :: forall q. DsMonad q => DerivDesc q-mkFoldableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do+mkFoldableInstance mb_ctxt ty dd@(DataDecl _ _ _ cons) = do functorLikeValidityChecks False dd 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
@@ -21,7 +21,7 @@ import Language.Haskell.TH.Desugar mkFunctorInstance :: forall q. DsMonad q => DerivDesc q-mkFunctorInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do+mkFunctorInstance mb_ctxt ty dd@(DataDecl _ _ _ cons) = do functorLikeValidityChecks False dd f <- newUniqueName "_f" z <- newUniqueName "_z"@@ -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/Ord.hs view
@@ -23,7 +23,7 @@ -- | Make a *non-singleton* Ord instance mkOrdInstance :: DsMonad q => DerivDesc q-mkOrdInstance mb_ctxt ty (DataDecl _ _ cons) = do+mkOrdInstance mb_ctxt ty (DataDecl _ _ _ cons) = do constraints <- inferConstraintsDef mb_ctxt (DConT ordName) ty cons compare_eq_clauses <- mapM mk_equal_clause cons let compare_noneq_clauses = map (uncurry mk_nonequal_clause)@@ -48,7 +48,7 @@ let pat1 = DConP name [] (map DVarP a_names) pat2 = DConP name [] (map DVarP b_names) return $ DClause [pat1, pat2] (DVarE foldlName `DAppE`- DVarE thenCmpName `DAppE`+ DVarE sappendName `DAppE` DConE cmpEQName `DAppE` mkListE (zipWith (\a b -> DVarE compareName `DAppE` DVarE a
src/Data/Singletons/TH/Deriving/Show.hs view
@@ -29,7 +29,7 @@ import GHC.Show (appPrec, appPrec1) mkShowInstance :: OptionsMonad q => DerivDesc q-mkShowInstance mb_ctxt ty (DataDecl _ _ cons) = do+mkShowInstance mb_ctxt ty (DataDecl _ _ _ cons) = do clauses <- mk_showsPrec cons constraints <- inferConstraintsDef mb_ctxt (DConT showName) ty cons return $ InstDecl { id_cxt = constraints@@ -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
@@ -20,7 +20,7 @@ import Language.Haskell.TH.Desugar mkTraversableInstance :: forall q. DsMonad q => DerivDesc q-mkTraversableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do+mkTraversableInstance mb_ctxt ty dd@(DataDecl _ _ _ cons) = do functorLikeValidityChecks False dd f <- newUniqueName "_f" let ft_trav :: FFoldType (q DExp)@@ -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
@@ -174,7 +174,7 @@ -- deal with a more complex error message when the generate code fails to -- typecheck. functorLikeValidityChecks :: forall q. DsMonad q => Bool -> DataDecl -> q ()-functorLikeValidityChecks allowConstrainedLastTyVar (DataDecl n data_tvbs cons)+functorLikeValidityChecks allowConstrainedLastTyVar (DataDecl _df n data_tvbs cons) | null data_tvbs -- (1) = fail $ "Data type " ++ nameBase n ++ " must have some type parameters" | otherwise@@ -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/Names.hs view
@@ -23,7 +23,6 @@ import Data.String (fromString) import Data.Type.Equality ( TestEquality(..) ) import Data.Type.Coercion ( TestCoercion(..) )-import Control.Applicative {- Note [Wired-in Names]@@ -70,14 +69,14 @@ testCoercionClassName, testCoercionMethName, decideCoercionName, provedName, disprovedName, reflName, toSingName, fromSingName, equalityName, applySingName, suppressClassName, suppressMethodName,- thenCmpName, sameKindName, fromIntegerName, negateName,+ sameKindName, fromIntegerName, negateName, errorName, foldlName, cmpEQName, cmpLTName, cmpGTName, toEnumName, fromEnumName, enumName, equalsName, constraintName, showName, showSName, showCharName, showCommaSpaceName, showParenName, showsPrecName, showSpaceName, showStringName, showSingName, composeName, gtName, fromStringName,- foldableName, foldMapName, memptyName, mappendName, foldrName,+ foldableName, foldMapName, memptyName, mappendName, sappendName, foldrName, functorName, fmapName, replaceName, traversableName, traverseName, pureName, apName, liftA2Name :: Name boolName = ''Bool@@ -128,7 +127,6 @@ applySingName = 'applySing suppressClassName = ''SuppressUnusedWarnings suppressMethodName = 'suppressUnusedWarnings-thenCmpName = 'thenCmp sameKindName = ''SameKind fromIntegerName = 'fromInteger negateName = 'negate@@ -158,6 +156,7 @@ foldMapName = 'foldMap memptyName = 'mempty mappendName = 'mappend+sappendName = '(<>) foldrName = 'foldr functorName = ''Functor fmapName = 'fmap@@ -168,10 +167,15 @@ apName = '(<*>) liftA2Name = 'liftA2 +-- | Return a fresh alphanumeric 'Name'. In particular, if the supplied 'Name'+-- is symbolic (e.g., (%%)), then return a fresh 'Name' with the 'OccName' @ty@.+-- Otherwise, return a fresh 'Name' with the same 'OccName' as the supplied+-- 'Name'. See @Note [Tracking local variables]@ in+-- "Data.Singletons.TH.Promote.Monad" for why we do this. mkTyName :: Quasi q => Name -> q Name mkTyName tmName = do let nameStr = nameBase tmName- symbolic = not (isHsLetter (head nameStr))+ symbolic = not (isHsLetter (headNameStr nameStr)) qNewName (if symbolic then "ty" else nameStr) mkTyConName :: Int -> Name
src/Data/Singletons/TH/Options.hs view
@@ -248,7 +248,7 @@ default_case :: Name -> Name default_case name' = let capped = toUpcaseStr noPrefix name' in- if isHsLetter (head capped)+ if isHsLetter (headNameStr capped) then mkName (capped ++ "Sym" ++ (show sat)) else mkName (capped ++ "@#@" -- See Note [Defunctionalization symbol suffixes] ++ (replicate (sat + 1) '$'))
src/Data/Singletons/TH/Partition.hs view
@@ -48,17 +48,18 @@ , pd_open_type_family_decs :: [OpenTypeFamilyDecl] , pd_closed_type_family_decs :: [ClosedTypeFamilyDecl] , pd_derived_eq_decs :: [DerivedEqDecl]+ , pd_derived_ord_decs :: [DerivedOrdDecl] , pd_derived_show_decs :: [DerivedShowDecl] } instance Semigroup PartitionedDecs where- PDecs a1 b1 c1 d1 e1 f1 g1 h1 i1 <> PDecs a2 b2 c2 d2 e2 f2 g2 h2 i2 =+ PDecs a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 <> PDecs a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 = PDecs (a1 <> a2) (b1 <> b2) (c1 <> c2) (d1 <> d2) (e1 <> e2)- (f1 <> f2) (g1 <> g2) (h1 <> h2) (i1 <> i2)+ (f1 <> f2) (g1 <> g2) (h1 <> h2) (i1 <> i2) (j1 <> j2) instance Monoid PartitionedDecs where mempty = PDecs mempty mempty mempty mempty mempty- mempty mempty mempty mempty+ mempty mempty mempty mempty mempty -- | Split up a @[DDec]@ into its pieces, extracting 'Ord' instances -- from deriving clauses@@ -69,9 +70,9 @@ partitionDec (DLetDec (DPragmaD {})) = return mempty partitionDec (DLetDec letdec) = return $ mempty { pd_let_decs = [letdec] } -partitionDec (DDataD _nd _cxt name tvbs mk cons derivings) = do+partitionDec (DDataD df _cxt name tvbs mk cons derivings) = do all_tvbs <- buildDataDTvbs tvbs mk- let data_decl = DataDecl name all_tvbs cons+ let data_decl = DataDecl df name all_tvbs cons derived_dec = mempty { pd_data_decs = [data_decl] } derived_decs <- mapM (\(strat, deriv_pred) ->@@ -143,9 +144,9 @@ -> do let cls_pred = foldType cls_pred_ty cls_arg_tys dinfo <- dsReify data_tycon case dinfo of- Just (DTyConI (DDataD _ _ dn dtvbs dk dcons _) _) -> do+ Just (DTyConI (DDataD df _ dn dtvbs dk dcons _) _) -> do all_tvbs <- buildDataDTvbs dtvbs dk- let data_decl = DataDecl dn all_tvbs dcons+ let data_decl = DataDecl df dn all_tvbs dcons partitionDeriving mb_strat cls_pred (Just ctxt) data_ty data_decl Just _ -> fail $ "Standalone derived instance for something other than a datatype: "@@ -162,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) =@@ -287,10 +288,16 @@ -- See Note [DerivedDecl] in Data.Singletons.TH.Syntax , ( eqName, do -- These will become PEq/SEq instances... inst_for_promotion <- mk_instance mkEqInstance- -- ...and these will become SDecide/TestEquality/TestCoercion instances.+ -- ...and these will become SDecide/Eq/TestEquality/TestCoercion instances. let inst_for_decide = derived_decl return $ mempty { pd_instance_decs = [inst_for_promotion] , pd_derived_eq_decs = [inst_for_decide] } )+ , ( ordName, do -- These will become POrd/SOrd instances...+ inst_for_promotion <- mk_instance mkOrdInstance+ -- ...and this will become an Ord instance.+ let inst_for_ord = derived_decl+ pure $ mempty { pd_instance_decs = [inst_for_promotion]+ , pd_derived_ord_decs = [inst_for_ord] } ) , ( showName, do -- These will become PShow/SShow instances... inst_for_promotion <- mk_instance mkShowInstance -- ...and this will become a Show instance.
src/Data/Singletons/TH/Promote.hs view
@@ -16,1155 +16,1586 @@ 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 Data.Singletons.TH.Deriving.Bounded-import Data.Singletons.TH.Deriving.Enum-import Data.Singletons.TH.Deriving.Eq-import Data.Singletons.TH.Deriving.Ord-import Data.Singletons.TH.Deriving.Show-import Data.Singletons.TH.Deriving.Util-import Data.Singletons.TH.Names-import Data.Singletons.TH.Options-import Data.Singletons.TH.Partition-import Data.Singletons.TH.Promote.Defun-import Data.Singletons.TH.Promote.Monad-import Data.Singletons.TH.Promote.Type-import Data.Singletons.TH.Syntax-import Data.Singletons.TH.Util-import Prelude hiding (exp)-import Control.Applicative (Alternative(..))-import Control.Arrow (second)-import Control.Monad-import Control.Monad.Trans.Maybe-import Control.Monad.Writer-import Data.List (nub)-import qualified Data.Map.Strict as Map-import Data.Map.Strict ( Map )-import Data.Maybe-import qualified GHC.LanguageExtensions.Type as LangExt--{--Note [Disable genQuotedDecs in genPromotions and genSingletons]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-Somewhat curiously, the genPromotions and genSingletons functions set the-genQuotedDecs option to False, despite neither function accepting quoted-declarations as arguments in the first place. There is a good reason for doing-this, however. Imagine this code:-- class C a where- infixl 9 <%%>- (<%%>) :: a -> a -> a- $(genPromotions [''C])--If genQuotedDecs is set to True, then the (<%%>) type family will not receive-a fixity declaration (see-Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1 for-more details on this point). Therefore, we set genQuotedDecs to False to avoid-this problem.--}---- | Generate promoted definitions for each of the provided type-level--- declaration 'Name's. This is generally only useful with classes.-genPromotions :: OptionsMonad q => [Name] -> q [Dec]-genPromotions names = do- opts <- getOptions- -- See Note [Disable genQuotedDecs in genPromotions and genSingletons]- withOptions opts{genQuotedDecs = False} $ do- checkForRep names- infos <- mapM reifyWithLocals names- dinfos <- mapM dsInfo infos- ddecs <- promoteM_ [] $ mapM_ promoteInfo dinfos- return $ decsToTH ddecs---- | Promote every declaration given to the type level, retaining the originals.--- See the--- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@--- for further explanation.-promote :: OptionsMonad q => q [Dec] -> q [Dec]-promote qdecs = do- opts <- getOptions- withOptions opts{genQuotedDecs = True} $ promote' $ lift qdecs---- | Promote each declaration, discarding the originals. Note that a promoted--- datatype uses the same definition as an original datatype, so this will--- not work with datatypes. Classes, instances, and functions are all fine.-promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]-promoteOnly qdecs = do- opts <- getOptions- withOptions opts{genQuotedDecs = False} $ promote' $ lift qdecs---- The workhorse for 'promote' and 'promoteOnly'. The difference between the--- two functions is whether 'genQuotedDecs' is set to 'True' or 'False'.-promote' :: OptionsMonad q => q [Dec] -> q [Dec]-promote' qdecs = do- opts <- getOptions- decs <- qdecs- ddecs <- withLocalDeclarations decs $ dsDecs decs- promDecs <- promoteM_ decs $ promoteDecs ddecs- let origDecs | genQuotedDecs opts = decs- | otherwise = []- return $ origDecs ++ decsToTH promDecs---- | Generate defunctionalization symbols for each of the provided type-level--- declaration 'Name's. See the "Promotion and partial application" section of--- the @singletons@--- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@--- for further explanation.-genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]-genDefunSymbols names = do- checkForRep names- infos <- mapM (dsInfo <=< reifyWithLocals) names- decs <- promoteMDecs [] $ concatMapM defunInfo infos- return $ decsToTH decs---- | Produce instances for @PEq@ from the given types-promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]-promoteEqInstances = concatMapM promoteEqInstance---- | Produce an instance for @PEq@ from the given type-promoteEqInstance :: OptionsMonad q => Name -> q [Dec]-promoteEqInstance = promoteInstance mkEqInstance "Eq"---- | Produce instances for 'POrd' from the given types-promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]-promoteOrdInstances = concatMapM promoteOrdInstance---- | Produce an instance for 'POrd' from the given type-promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]-promoteOrdInstance = promoteInstance mkOrdInstance "Ord"---- | Produce instances for 'PBounded' from the given types-promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]-promoteBoundedInstances = concatMapM promoteBoundedInstance---- | Produce an instance for 'PBounded' from the given type-promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]-promoteBoundedInstance = promoteInstance mkBoundedInstance "Bounded"---- | Produce instances for 'PEnum' from the given types-promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]-promoteEnumInstances = concatMapM promoteEnumInstance---- | Produce an instance for 'PEnum' from the given type-promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]-promoteEnumInstance = promoteInstance mkEnumInstance "Enum"---- | Produce instances for 'PShow' from the given types-promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]-promoteShowInstances = concatMapM promoteShowInstance---- | Produce an instance for 'PShow' from the given type-promoteShowInstance :: OptionsMonad q => Name -> q [Dec]-promoteShowInstance = promoteInstance mkShowInstance "Show"--promoteInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec]-promoteInstance mk_inst class_name name = do- (tvbs, cons) <- getDataD ("I cannot make an instance of " ++ class_name- ++ " for it.") name- tvbs' <- mapM dsTvbUnit tvbs- let data_ty = foldTypeTvbs (DConT name) tvbs'- cons' <- concatMapM (dsCon tvbs' data_ty) cons- let data_decl = DataDecl name tvbs' cons'- raw_inst <- mk_inst Nothing data_ty data_decl- decs <- promoteM_ [] $ void $- promoteInstanceDec OMap.empty Map.empty raw_inst- return $ decsToTH decs--promoteInfo :: DInfo -> PrM ()-promoteInfo (DTyConI dec _instances) = promoteDecs [dec]-promoteInfo (DPrimTyConI _name _numArgs _unlifted) =- fail "Promotion of primitive type constructors not supported"-promoteInfo (DVarI _name _ty _mdec) =- fail "Promotion of individual values not supported"-promoteInfo (DTyVarI _name _ty) =- fail "Promotion of individual type variables not supported"-promoteInfo (DPatSynI {}) =- fail "Promotion of pattern synonyms not supported"---- Note [Promoting declarations in two stages]--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~------ It is necessary to know the types of things when promoting. So,--- we promote in two stages: first, we build a LetDecEnv, which allows--- for easy lookup. Then, we go through the actual elements of the LetDecEnv,--- performing the promotion.------ Why do we need the types? For kind annotations on the type family. We also--- need to have both the types and the actual function definition at the same--- time, because the function definition tells us how many patterns are--- matched. Note that an eta-contracted function needs to return a TyFun,--- not a proper type-level function.------ Consider this example:------ foo :: Nat -> Bool -> Bool--- foo Zero = id--- foo _ = not------ Here the first parameter to foo is non-uniform, because it is--- inspected in a pattern and can be different in each defining--- equation of foo. The second parameter to foo, specified in the type--- signature as Bool, is a uniform parameter - it is not inspected and--- each defining equation of foo uses it the same way. The foo--- function will be promoted to a type familty Foo like this:------ type family Foo (n :: Nat) :: Bool ~> Bool where--- Foo Zero = Id--- Foo a = Not------ To generate type signature for Foo type family we must first learn--- what is the actual number of patterns used in defining cequations--- of foo. In this case there is only one so we declare Foo to take--- one argument and have return type of Bool -> Bool.---- Promote a list of top-level declarations.-promoteDecs :: [DDec] -> PrM ()-promoteDecs raw_decls = do- decls <- expand raw_decls -- expand type synonyms- checkForRepInDecls decls- PDecs { pd_let_decs = let_decs- , pd_class_decs = classes- , pd_instance_decs = insts- , pd_data_decs = datas- , pd_ty_syn_decs = ty_syns- , pd_open_type_family_decs = o_tyfams- , pd_closed_type_family_decs = c_tyfams } <- partitionDecs decls-- defunTopLevelTypeDecls ty_syns c_tyfams o_tyfams- rec_sel_let_decs <- promoteDataDecs datas- -- promoteLetDecs returns LetBinds, which we don't need at top level- _ <- promoteLetDecs Nothing $ rec_sel_let_decs ++ let_decs- mapM_ promoteClassDec classes- let orig_meth_sigs = foldMap (lde_types . cd_lde) classes- cls_tvbs_map = Map.fromList $ map (\cd -> (cd_name cd, cd_tvbs cd)) classes- mapM_ (promoteInstanceDec orig_meth_sigs cls_tvbs_map) insts---- curious about ALetDecEnv? See the LetDecEnv module for an explanation.-promoteLetDecs :: Maybe Uniq -- let-binding unique (if locally bound)- -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)- -- See Note [Promoting declarations in two stages]-promoteLetDecs mb_let_uniq decls = do- 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) ]- (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 })--promoteDataDecs :: [DataDecl] -> PrM [DLetDec]-promoteDataDecs = concatMapM promoteDataDec---- "Promotes" a data type, much like D.S.TH.Single.Data.singDataD singles a data--- type. Promoting a data type is much easier than singling it, however, since--- DataKinds automatically promotes data types and kinds and data constructors--- to types. That means that promoteDataDec only has to do three things:------ 1. Emit defunctionalization symbols for each data constructor,------ 2. Emit promoted fixity declarations for each data constructor and promoted--- record selector (assuming the originals have fixity declarations), and------ 3. Assemble a top-level function that mimics the behavior of its record--- selectors. Note that promoteDataDec does not actually promote this record--- selector function—it merely returns its DLetDecs. Later, the promoteDecs--- function takes these DLetDecs and promotes them (using promoteLetDecs).--- This greatly simplifies the plumbing, since this allows all DLetDecs to--- be promoted in a single location.--- See Note [singletons-th and record selectors] in D.S.TH.Single.Data.-promoteDataDec :: DataDecl -> PrM [DLetDec]-promoteDataDec (DataDecl _ _ ctors) = do- let rec_sel_names = nub $ concatMap extractRecSelNames ctors- -- Note the use of nub: the same record selector name can- -- be used in multiple constructors!- rec_sel_let_decs <- getRecordSelectors ctors- ctorSyms <- buildDefunSymsDataD ctors- infix_decs <- promoteReifiedInfixDecls rec_sel_names- emitDecs $ ctorSyms ++ infix_decs- pure rec_sel_let_decs--promoteClassDec :: UClassDecl -> PrM AClassDecl-promoteClassDec decl@(ClassDecl { cd_name = cls_name- , cd_tvbs = tvbs- , cd_fds = fundeps- , cd_atfs = atfs- , cd_lde = lde@LetDecEnv- { lde_defns = defaults- , lde_types = meth_sigs- , lde_infix = infix_decls } }) = do- opts <- getOptions- let pClsName = promotedClassName opts cls_name- forallBind cls_kvs_to_bind $ do- let meth_sigs_list = OMap.assocs meth_sigs- meth_names = map fst meth_sigs_list- 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- (default_decs, ann_rhss, prom_rhss)- <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs) defaults_list- defunAssociatedTypeFamilies tvbs atfs-- infix_decls' <- mapMaybeM (uncurry (promoteInfixDecl Nothing)) $- 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- (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- let defaults_list' = zip defaults_names ann_rhss- proms = zip defaults_names prom_rhss- cls_kvs_to_bind' = cls_kvs_to_bind <$ meth_sigs- return (decl { cd_lde = lde { lde_defns = OMap.fromList defaults_list'- , lde_proms = OMap.fromList proms- , lde_bound_kvs = cls_kvs_to_bind' } })- where- cls_kvb_names, cls_tvb_names, cls_kvs_to_bind :: OSet Name- cls_kvb_names = foldMap (foldMap fvDType . extractTvbKind) tvbs- cls_tvb_names = OSet.fromList $ map extractTvbName tvbs- cls_kvs_to_bind = cls_kvb_names `OSet.union` cls_tvb_names-- promote_sig :: Name -> DType -> PrM DDec- promote_sig name 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` ()) 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- m_fixity <- reifyFixityWithLocals name- emitDecsM $ defunctionalize proName m_fixity $ DefunSAK meth_sak-- return $ DOpenTypeFamilyD (DTypeFamilyHead proName- proTvbs- (DKindSig resK)- Nothing)--{--Note [Promoted class methods and kind variable ordering]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-In general, we make an effort to preserve the order of type variables when-promoting type signatures, but there is an annoying corner case where this is-difficult: class methods. When promoting class methods, the order of kind-variables in their kinds will often "just work" by happy coincidence, but-there are some situations where this does not happen. Consider the following-class:-- class C (b :: Type) where- m :: forall a. a -> b -> a--The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds-`b` before `a`. This order is preserved when singling `m`, but *not* when-promoting `m`. This is because the `C` class is promoted as follows:-- class PC (b :: Type) where- type M (x :: a) (y :: b) :: a--Due to the way GHC kind-checks associated type families, the kind of `M` is-`forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the-`StandaloneKindSignatures` extension does not provide a way to explicitly-declare the full kind of an associated type family, so this limitation is-not easy to work around.--The defunctionalization symbols for `M` will also follow a similar-order of type variables:-- 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:-- 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.--}---- returns (unpromoted method name, ALetDecRHS) pairs-promoteInstanceDec :: OMap Name DType- -- Class method type signatures- -> Map Name [DTyVarBndrUnit]- -- Class header type variable (e.g., if `class C a b` is- -- quoted, then this will have an entry for {C |-> [a, b]})- -> UInstDecl -> PrM AInstDecl-promoteInstanceDec orig_meth_sigs cls_tvbs_map- decl@(InstDecl { id_name = cls_name- , id_arg_tys = inst_tys- , id_sigs = inst_sigs- , id_meths = meths }) = do- opts <- getOptions- cls_tvbs <- lookup_cls_tvbs- inst_kis <- mapM promoteType inst_tys- let pClsName = promotedClassName opts cls_name- cls_tvb_names = map extractTvbName cls_tvbs- kvs_to_bind = foldMap fvDType inst_kis- forallBind kvs_to_bind $ do- let subst = Map.fromList $ zip cls_tvb_names inst_kis- meth_impl = InstanceMethods inst_sigs subst- (meths', ann_rhss, _)- <- mapAndUnzip3M (promoteMethod meth_impl orig_meth_sigs) meths- emitDecs [DInstanceD Nothing Nothing [] (foldType (DConT pClsName)- inst_kis) meths']- return (decl { id_meths = zip (map fst meths) ann_rhss })- where- lookup_cls_tvbs :: PrM [DTyVarBndrUnit]- lookup_cls_tvbs =- -- First, try consulting the map of class names to their type variables.- -- It is important to do this first to ensure that we consider locally- -- declared classes before imported ones. See #410 for what happens if- -- you don't.- case Map.lookup cls_name cls_tvbs_map of- Just tvbs -> pure tvbs- Nothing -> reify_cls_tvbs- -- If the class isn't present in this map, we try reifying the class- -- as a last resort.-- reify_cls_tvbs :: PrM [DTyVarBndrUnit]- reify_cls_tvbs = do- opts <- getOptions- let pClsName = promotedClassName opts cls_name- mk_tvbs = extract_tvbs (dsReifyTypeNameInfo pClsName)- <|> extract_tvbs (dsReifyTypeNameInfo cls_name)- -- See Note [Using dsReifyTypeNameInfo when promoting instances]- mb_tvbs <- runMaybeT mk_tvbs- case mb_tvbs of- Just tvbs -> pure tvbs- Nothing -> fail $ "Cannot find class declaration annotation for " ++ show cls_name-- extract_tvbs :: PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndrUnit]- extract_tvbs reify_info = do- mb_info <- lift reify_info- case mb_info of- Just (DTyConI (DClassD _ _ tvbs _ _) _) -> pure tvbs- _ -> empty--{--Note [Using dsReifyTypeNameInfo when promoting instances]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-During the promotion of a class instance, it becomes necessary to reify the-original promoted class's info to learn various things. It's tempting to think-that just calling dsReify on the class name will be sufficient, but it's not.-Consider this class and its promotion:-- class Eq a where- (==) :: a -> a -> Bool-- class PEq a where- type (==) (x :: a) (y :: a) :: Bool--Notice how both of these classes have an identifier named (==), one at the-value level, and one at the type level. Now imagine what happens when you-attempt to promote this Template Haskell declaration:-- [d| f :: Bool- f = () == () |]--When promoting ==, singletons-th will come up with its promoted equivalent (which also-happens to be ==). However, this promoted name is a raw Name, since it is created-with mkName. This becomes an issue when we call dsReify the raw "==" Name, as-Template Haskell has to arbitrarily choose between reifying the info for the-value-level (==) and the type-level (==), and in this case, it happens to pick the-value-level (==) info. We want the type-level (==) info, however, because we care-about the promoted version of (==).--Fortunately, there's a serviceable workaround. Instead of dsReify, we can use-dsReifyTypeNameInfo, which first calls lookupTypeName (to ensure we can find a Name-that's in the type namespace) and _then_ reifies it.--}---- Which sort of class methods are being promoted?-data MethodSort- -- The method defaults in class declarations.- = DefaultMethods- -- The methods in instance declarations.- | InstanceMethods (OMap Name DType) -- ^ InstanceSigs- (Map Name DKind) -- ^ Instantiations for class tyvars- -- See Note [Promoted class method kinds]- deriving Show--promoteMethod :: MethodSort- -> OMap Name DType -- method types- -> (Name, ULetDecRHS)- -> PrM (DDec, ALetDecRHS, DType)- -- returns (type instance, ALetDecRHS, promoted RHS)-promoteMethod meth_sort orig_sigs_map (meth_name, meth_rhs) = do- opts <- getOptions- (meth_tvbs, meth_arg_kis, meth_res_ki) <- promote_meth_ty- meth_arg_tvs <- replicateM (length meth_arg_kis) (qNewName "a")- let proName = promotedTopLevelValueName opts meth_name- helperNameBase = case nameBase proName of- first:_ | not (isHsLetter first) -> "TFHelper"- alpha -> alpha-- -- family_args are the type variables in a promoted class's- -- associated type family instance (or default implementation), e.g.,- --- -- class C k where- -- type T (a :: k) (b :: Bool)- -- type T a b = THelper1 a b -- family_args = [a, b]- --- -- instance C Bool where- -- type T a b = THelper2 a b -- family_args = [a, b]- --- -- We could annotate these variables with explicit kinds, but it's not- -- 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_tvbs meth_arg_kis meth_res_ki)- OMap.empty OMap.empty- Nothing helperName meth_rhs- emitDecs (pro_decs ++ defun_decs)- return ( DTySynInstD- (DTySynEqn Nothing- (foldType (DConT proName) family_args)- (foldApply (DConT helperDefunName) (map DVarT meth_arg_tvs)))- , ann_rhs- , DConT helperDefunName )- 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,- -- "the type" is like the type of the original method, but substituted for- -- 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 ([DTyVarBndrSpec], [DKind], DKind)- promote_meth_ty =- case meth_sort of- DefaultMethods ->- -- No substitution for class variables is required for default- -- method type signatures, as they share type variables with the- -- class they inhabit.- lookup_meth_ty- InstanceMethods inst_sigs_map cls_subst ->- case OMap.lookup meth_name inst_sigs_map of- Just ty -> do- -- 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.- promoteUnraveled ty- Nothing -> do- -- We don't have an InstanceSig, so we must compute the kind to use- -- ourselves.- (_, 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- -- 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]- tvbs' = changeDTVFlags SpecifiedSpec $- toposortTyVarsOf (arg_kis' ++ [res_ki'])- pure (tvbs', arg_kis', res_ki')-- -- Attempt to look up a class method's original type.- lookup_meth_ty :: PrM ([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.- promoteUnraveled ty- Nothing -> do- -- If the type of the method is not in scope, the only other option- -- is to try reifying the promoted method name.- mb_info <- dsReifyTypeNameInfo proName- -- See Note [Using dsReifyTypeNameInfo when promoting instances]- case mb_info of- Just (DTyConI (DOpenTypeFamilyD (DTypeFamilyHead _ tvbs mb_res_ki _)) _)- -> let arg_kis = map (defaultMaybeToTypeKind . extractTvbKind) tvbs- res_ki = defaultMaybeToTypeKind (resultSigToMaybeKind mb_res_ki)- -- 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]- tvbs' = changeDTVFlags SpecifiedSpec $- toposortTyVarsOf (arg_kis ++ [res_ki])- in pure (tvbs', arg_kis, res_ki)- _ -> fail $ "Cannot find type annotation for " ++ show proName--{--Note [Promoted class method kinds]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-Consider this example of a type class (and instance):-- class C a where- m :: a -> Bool -> Bool- m _ x = x-- instance C [a] where- m l _ = null l--The promoted version of these declarations would be:-- class PC a where- type M (x :: a) (y :: Bool) :: Bool- type M x y = MHelper1 x y-- instance PC [a] where- type M x y = MHelper2 x y-- type MHelper1 :: a -> Bool -> Bool- type family MHelper1 x y where ...-- type MHelper2 :: [a] -> Bool -> Bool- type family MHelper2 x y where ...--Getting the kind signature for MHelper1 (the promoted default implementation of-M) is quite simple, as it corresponds exactly to the kind of M. We might even-choose to make that the kind of MHelper2, but then it would be overly general-(and more difficult to find in -ddump-splices output). For this reason, we-substitute in the kinds of the instance itself to determine the kinds of-promoted method implementations like MHelper2.--}--promoteLetDecEnv :: Maybe Uniq -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)-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)) $- 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)- names rhss-- emitDecs $ concat defun_decss- bound_kvs <- allBoundKindVars- let decs = concat pro_decs ++ infix_decls-- -- build the ALetDecEnv- let let_dec_env' = LetDecEnv { lde_defns = OMap.fromList $ zip names ann_rhss- , lde_types = type_env- , lde_infix = fix_env- , lde_proms = OMap.empty -- filled in promoteLetDecs- , lde_bound_kvs = OMap.fromList $ map (, bound_kvs) names }-- return (decs, let_dec_env')---- Promote a fixity declaration.-promoteInfixDecl :: forall q. OptionsMonad q- => Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)-promoteInfixDecl mb_let_uniq name fixity = do- opts <- getOptions- mb_ns <- reifyNameSpace name- case mb_ns of- -- If we can't find the Name for some odd reason, fall back to promote_val- Nothing -> promote_val- Just VarName -> promote_val- Just DataName -> never_mind- Just TcClsName -> do- mb_info <- dsReify name- case mb_info of- Just (DTyConI DClassD{} _)- -> finish $ promotedClassName opts name- _ -> never_mind- where- -- Produce the fixity declaration.- finish :: Name -> q (Maybe DDec)- finish = pure . Just . DLetDec . DInfixD fixity-- -- Don't produce a fixity declaration at all. This happens when promoting a- -- fixity declaration for a name whose promoted counterpart is the same as- -- the original name.- -- See Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1.- never_mind :: q (Maybe DDec)- 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.- -- 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- then never_mind- else finish promoted_name---- Try producing promoted fixity declarations for Names by reifying them--- /without/ consulting quoted declarations. If reification fails, recover and--- return the empty list.--- See [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 2.-promoteReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec]-promoteReifiedInfixDecls = mapMaybeM tryPromoteFixityDeclaration- where- tryPromoteFixityDeclaration :: Name -> q (Maybe DDec)- tryPromoteFixityDeclaration name =- qRecover (return Nothing) $ do- mFixity <- qReifyFixity name- case mFixity of- Nothing -> pure Nothing- Just fixity -> promoteInfixDecl Nothing name fixity---- Which sort of let-bound declaration's right-hand side is being promoted?-data LetDecRHSSort- -- An ordinary (i.e., non-class-related) let-bound declaration.- = LetBindingRHS- -- The right-hand side of a class method (either a default method or a- -- method in an instance declaration).- | ClassMethodRHS- [DTyVarBndrSpec] [DKind] DKind- -- The RHS's promoted type variable binders, argument types, and- -- result type. Needed to fix #136.- deriving Show---- This function is used both to promote class method defaults and normal--- let bindings. Thus, it can't quite do all the work locally and returns--- an intermediate structure. Perhaps a better design is available.-promoteLetDecRHS :: LetDecRHSSort- -> OMap Name DType -- local type env't- -> OMap Name Fixity -- local fixity env't- -> Maybe Uniq -- let-binding unique (if locally bound)- -> Name -- name of the thing being promoted- -> ULetDecRHS -- body of the thing- -> PrM ( [DDec] -- promoted type family dec, plus the- -- SAK dec (if one exists)- , [DDec] -- defunctionalization- , ALetDecRHS ) -- annotated RHS-promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do- opts <- getOptions- all_locals <- allLocals- case let_dec_rhs of- UValue exp -> do- (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals 0- if ty_num_args == 0- then- let proName = promotedValueName opts name mb_let_uniq- prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals in- promote_let_dec_rhs all_locals m_ldrki 0 (promoteExp exp)- (\exp' -> [DTySynEqn Nothing prom_fun_lhs exp'])- AValue- else- -- If we have a UValue with a function type, process it as though it- -- were a UFunction. promote_function_rhs will take care of- -- eta-expanding arguments as necessary.- promote_function_rhs all_locals [DClause [] exp]- 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]- -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)- promote_function_rhs all_locals clauses = do- opts <- getOptions- numArgs <- count_args clauses- let proName = promotedValueName opts name mb_let_uniq- prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals- (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals numArgs- expClauses <- mapM (etaContractOrExpand ty_num_args numArgs) clauses- promote_let_dec_rhs all_locals m_ldrki ty_num_args- (mapAndUnzipM (promoteClause prom_fun_lhs) expClauses)- id AFunction-- -- Promote a UValue or a UFunction.- -- Notes about type variables:- --- -- * For UValues, `prom_a` is DType and `a` is Exp.- --- -- * For UFunctions, `prom_a` is [DTySynEqn] and `a` is [DClause].- promote_let_dec_rhs- :: [Name] -- 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- -> (prom_a -> [DTySynEqn]) -- Turn the promoted RHS into type family equations- -> (DType -> Int -> a -> ALetDecRHS) -- Build an ALetDecRHS- -> PrM ([DDec], [DDec], ALetDecRHS)- promote_let_dec_rhs all_locals m_ldrki ty_num_args- promote_thing mk_prom_eqns mk_alet_dec_rhs = do- opts <- getOptions- tyvarNames <- replicateM ty_num_args (qNewName "a")- let proName = promotedValueName opts name mb_let_uniq- local_tvbs = map (`DPlainTV` ()) all_locals- m_fixity = OMap.lookup name fix_env-- mk_tf_head :: [DTyVarBndrUnit] -> DFamilyResultSig -> DTypeFamilyHead- mk_tf_head tvbs res_sig = DTypeFamilyHead proName tvbs res_sig Nothing-- (lde_kvs_to_bind, m_sak_dec, defun_ki, tf_head) =- -- There are three possible cases:- case m_ldrki of- -- 1. We have no kind information whatsoever.- Nothing ->- let all_args = local_tvbs ++ map (`DPlainTV` ()) tyvarNames in- ( OSet.empty- , Nothing- , DefunNoSAK all_args Nothing- , mk_tf_head all_args DNoSig- )- -- 2. We have some kind information in the form of a LetDecRHSKindInfo.- Just (LDRKI m_sak tvbs argKs resK) ->- let all_args = local_tvbs ++ zipWith (`DKindedTV` ()) tyvarNames argKs- lde_kvs_to_bind' = OSet.fromList (map extractTvbName tvbs) in- case m_sak of- -- 2(a). We do not have a standalone kind signature.- Nothing ->- ( lde_kvs_to_bind'- , Nothing- , DefunNoSAK all_args (Just resK)- , mk_tf_head all_args (DKindSig resK)- )- -- 2(b). We have a standalone kind signature.- Just sak ->- ( lde_kvs_to_bind'- , Just $ DKiSigD proName sak- , DefunSAK sak- -- We opt to annotate the argument and result kinds in- -- the body of the type family declaration even if it is- -- given a standalone kind signature.- -- See Note [Keep redundant kind information for Haddocks].- , mk_tf_head all_args (DKindSig resK)- )-- defun_decs <- defunctionalize proName m_fixity defun_ki- (prom_thing, thing) <- forallBind lde_kvs_to_bind promote_thing- prom_fun_rhs <- lookupVarE name- return ( catMaybes [ m_sak_dec- , Just $ DClosedTypeFamilyD tf_head (mk_prom_eqns prom_thing)- ]- , defun_decs- , mk_alet_dec_rhs prom_fun_rhs ty_num_args thing )-- promote_let_dec_ty :: [Name] -- 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]- -> Int -- The number of arguments to default to if the- -- type cannot be inferred. This is 0 for UValues- -- and the number of arguments in a single clause- -- for UFunctions.- -> PrM (Maybe LetDecRHSKindInfo, Int)- -- Returns two things in a pair:- --- -- 1. Information about the promoted kind,- -- if available.- --- -- 2. The number of arguments the let-dec has.- -- If no kind information is available from- -- which to infer this number, then this- -- will default to the earlier Int argument.- promote_let_dec_ty all_locals default_num_args =- case rhs_sort of- ClassMethodRHS tvbs 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) tvbs arg_kis res_ki), length arg_kis)- LetBindingRHS- | Just ty <- OMap.lookup name type_env- -> do- -- promoteType turns rank-1 uses of (->) into (~>). So, we unravel- -- first to avoid this behavior, and then ravel back.- (tvbs, argKs, resultK) <- promoteUnraveled ty- let m_sak | null all_locals = Just $ ravelVanillaDType tvbs [] argKs resultK- -- If this let-dec closes over local variables, then- -- don't give it a SAK.- -- See Note [No SAKs for let-decs with local variables]- | otherwise = Nothing- -- invariant: count_args ty == length argKs- return (Just (LDRKI m_sak tvbs argKs resultK), length argKs)-- | otherwise- -> return (Nothing, default_num_args)-- etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause- etaContractOrExpand ty_num_args clause_num_args (DClause pats exp)- | n >= 0 = do -- Eta-expand- names <- replicateM n (newUniqueName "a")- let newPats = map DVarP names- newArgs = map DVarE names- return $ DClause (pats ++ newPats) (foldExp exp newArgs)- | otherwise = do -- Eta-contract- let (clausePats, lamPats) = splitAt ty_num_args pats- lamExp <- mkDLamEFromDPats lamPats exp- return $ DClause clausePats lamExp- where- n = ty_num_args - clause_num_args-- count_args :: [DClause] -> PrM Int- count_args (DClause pats _ : _) = return $ length pats- count_args _ = fail $ "Impossible! A function without clauses."---- An auxiliary data type used in promoteLetDecRHS that describes information--- related to the promoted kind of a class method default or normal--- let binding.-data LetDecRHSKindInfo =- LDRKI (Maybe DKind) -- The standalone kind signature, if applicable.- -- 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]- [DTyVarBndrSpec] -- The type variable binders of the kind.- [DKind] -- The argument kinds.- DKind -- The result kind.--{--Note [No SAKs for let-decs with local variables]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-Consider promoting this:-- f :: Bool- f = let x = True- g :: () -> Bool- g _ = x- in g ()--Clearly, the promoted `F` type family will have the following SAK:-- type F :: ()--What about `G`? At a passing glance, it appears that you could get away with-this:-- type G :: Bool -> ()--But this isn't quite right, since `g` closes over `x = True`. The body of `G`,-therefore, has to lift `x` to be an explicit argument:-- type family G x (u :: ()) :: Bool where- G x _ = x--At present, we don't keep track of the types of local variables like `x`, which-makes it difficult to create a SAK for things like `G`. Here are some possible-ideas, each followed by explanations for why they are infeasible:--* Use wildcards:-- type G :: _ -> () -> Bool-- Alas, GHC currently does not allow wildcards in SAKs. See GHC#17432.--* Use visible dependent quantification to avoid having to say what the kind- of `x` is:-- type G :: forall x -> () -> Bool-- A clever trick to be sure, but it doesn't quite do what we want, since- GHC will generalize that kind to become `forall (x :: k) -> () -> Bool`,- which is more general than we want.--In any case, it's probably not worth bothering with SAKs for local definitions-like `g` in the first place, so we avoid generating SAKs for anything that-closes over at least one local variable for now. If someone yells about this,-we'll reconsider this design.--Note [Keep redundant kind information for Haddocks]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-`singletons-th` generates explicit argument kinds and result kinds for-type-level declarations whenever possible, even if those kinds are technically-redundant. For example, `singletons-th` would promote this:-- id' :: a -> a--To this:-- type Id' :: a -> a- type family Id' (x :: a) :: a where ...--Strictly speaking, the argument and result kind of Id' are unnecessary, since-the same information is already present in the standalone kind signature.-However, due to a Haddock limitation-(https://github.com/haskell/haddock/issues/1178), Haddock will not render-standalone kind signatures at all, so if the argument and result kind of Id'-were omitted in the body, Haddock would render it like so:-- type family Id' x where ...--This is unfortunate for Haddock viewers, as this does not convey any kind-information whatsoever. Until the aformentioned Haddock issue is resolved, we-work around this limitation by generating the redundant argument and kind-information anyway. Thankfully, this is simple to accomplish, as we already-compute this information to begin with.--}--promoteClause :: DType -- What to use as the LHS of the promoted type family- -- equation. This should consist of the promoted name of- -- the function to which the clause belongs, applied to- -- any local arguments (e.g., `Go x y z`).- -> DClause -> PrM (DTySynEqn, ADClause)-promoteClause pro_clause_fun (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- let PromDPatInfos { prom_dpat_vars = new_vars- , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos- (ty, ann_exp) <- forallBind sig_kvs $- lambdaBind new_vars $- promoteExp exp- return ( DTySynEqn Nothing (foldType pro_clause_fun types) 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) <- forallBind 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- -- term vars can be symbols... type vars can't!- tyName <- mkTyName name- tell $ PromDPatInfos [(name, tyName)] OSet.empty- return (DVarT tyName, ADVarP name)-promotePat (DConP name tys pats) = do- opts <- getOptions- kis <- traverse (promoteType_options conOptions) tys- (types, pats') <- mapAndUnzipM promotePat pats- let name' = promotedDataTypeOrConName opts name- return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats')- where- -- Currently, visible type patterns of data constructors are the one place- -- in `singletons-th` where it makes sense to promote wildcard types, as it- -- will produce code that GHC will accept.- conOptions :: PromoteTypeOptions- conOptions = defaultPromoteTypeOptions{ptoAllowWildcards = True}-promotePat (DTildeP pat) = do- qReportWarning "Lazy pattern converted into regular pattern in promotion"- second ADTildeP <$> promotePat pat-promotePat (DBangP pat) = do- qReportWarning "Strict pattern converted into regular pattern in promotion"- second ADBangP <$> promotePat 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)- return (DSigT promoted ki, ADSigP promoted pat' ki)-promotePat DWildP = return (DWildCardT, ADWildP)--promoteExp :: DExp -> PrM (DType, ADExp)-promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name-promoteExp (DConE name) = do- opts <- getOptions- return (DConT $ defunctionalizedName0 opts name, ADConE name)-promoteExp (DLitE lit) = fmap (, ADLitE lit) $ promoteLitExp lit-promoteExp (DAppE exp1 exp2) = do- (exp1', ann_exp1) <- promoteExp exp1- (exp2', ann_exp2) <- promoteExp exp2- return (apply exp1' exp2', ADAppE ann_exp1 ann_exp2)--- Until we get visible kind applications, this is the best we can do.-promoteExp (DAppTypeE exp _) = do- qReportWarning "Visible type applications are ignored by `singletons-th`."- promoteExp exp-promoteExp (DLamE names exp) = 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 all_args = all_locals ++ tyNames- tvbs = map (`DPlainTV` ()) all_args- emitDecs [DClosedTypeFamilyD (DTypeFamilyHead- lambdaName- tvbs- DNoSig- Nothing)- [DTySynEqn Nothing- (foldType (DConT lambdaName) $- map DVarT all_args)- rhs]]- emitDecsM $ defunctionalize lambdaName Nothing $ DefunNoSAK tvbs Nothing- let promLambda = foldl apply (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"- 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 all_args = all_locals ++ [tyvarName]- tvbs = map (`DPlainTV` ()) all_args- emitDecs [DClosedTypeFamilyD (DTypeFamilyHead caseTFName tvbs DNoSig Nothing) 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 )-promoteExp (DLetE decs exp) = do- unique <- qNewUnique- (binds, ann_env) <- promoteLetDecs (Just unique) decs- (exp', ann_exp) <- letBind binds $ promoteExp exp- return (exp', ADLetE ann_env ann_exp)-promoteExp (DSigE exp ty) = do- (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)--promoteLitExp :: OptionsMonad q => Lit -> q DType-promoteLitExp (IntegerL n) = do- opts <- getOptions- let tyFromIntegerName = promotedValueName opts fromIntegerName Nothing- tyNegateName = promotedValueName opts negateName Nothing- if n >= 0- then return $ (DConT tyFromIntegerName `DAppT` DLitT (NumTyLit n))- else return $ (DConT tyNegateName `DAppT`- (DConT tyFromIntegerName `DAppT` DLitT (NumTyLit (-n))))-promoteLitExp (StringL str) = do- opts <- getOptions- let prom_str_lit = DLitT (StrTyLit str)- os_enabled <- qIsExtEnabled LangExt.OverloadedStrings- pure $ if os_enabled- then DConT (promotedValueName opts fromStringName Nothing) `DAppT` prom_str_lit- else prom_str_lit-promoteLitExp (CharL c) = return $ DLitT (CharTyLit c)-promoteLitExp lit =- fail ("Only string, natural number, and character literals can be promoted: " ++ show lit)--promoteLitPat :: MonadFail m => Lit -> m DType-promoteLitPat (IntegerL n)- | n >= 0 = return $ (DLitT (NumTyLit n))- | otherwise =- fail $ "Negative literal patterns are not allowed,\n" ++- "because literal patterns are promoted to natural numbers."-promoteLitPat (StringL str) = return $ DLitT (StrTyLit str)-promoteLitPat (CharL c) = return $ DLitT (CharTyLit c)-promoteLitPat lit =- fail ("Only string, natural number, and character literals can be promoted: " ++ show lit)+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+import Data.Singletons.TH.Deriving.Ord+import Data.Singletons.TH.Deriving.Show+import Data.Singletons.TH.Deriving.Util+import Data.Singletons.TH.Names+import Data.Singletons.TH.Options+import Data.Singletons.TH.Partition+import Data.Singletons.TH.Promote.Defun+import Data.Singletons.TH.Promote.Monad+import Data.Singletons.TH.Promote.Type+import Data.Singletons.TH.Syntax+import Data.Singletons.TH.Util+import Prelude hiding (exp)+import Control.Applicative (Alternative(..))+import Control.Arrow (second)+import Control.Monad+import Control.Monad.Trans.Maybe+import Control.Monad.Writer+import Data.Function (on)+import Data.List (deleteFirstsBy, nub)+import qualified Data.Map.Strict as Map+import Data.Map.Strict ( Map )+import Data.Maybe+import qualified GHC.LanguageExtensions.Type as LangExt++{-+Note [Disable genQuotedDecs in genPromotions and genSingletons]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Somewhat curiously, the genPromotions and genSingletons functions set the+genQuotedDecs option to False, despite neither function accepting quoted+declarations as arguments in the first place. There is a good reason for doing+this, however. Imagine this code:++ class C a where+ infixl 9 <%%>+ (<%%>) :: a -> a -> a+ $(genPromotions [''C])++If genQuotedDecs is set to True, then the (<%%>) type family will not receive+a fixity declaration (see+Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1 for+more details on this point). Therefore, we set genQuotedDecs to False to avoid+this problem.+-}++-- | Generate promoted definitions for each of the provided type-level+-- declaration 'Name's. This is generally only useful with classes.+genPromotions :: OptionsMonad q => [Name] -> q [Dec]+genPromotions names = do+ opts <- getOptions+ -- See Note [Disable genQuotedDecs in genPromotions and genSingletons]+ withOptions opts{genQuotedDecs = False} $ do+ checkForRep names+ infos <- mapM reifyWithLocals names+ dinfos <- mapM dsInfo infos+ ddecs <- promoteM_ [] $ mapM_ promoteInfo dinfos+ return $ decsToTH ddecs++-- | Promote every declaration given to the type level, retaining the originals.+-- See the+-- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@+-- for further explanation.+promote :: OptionsMonad q => q [Dec] -> q [Dec]+promote qdecs = do+ opts <- getOptions+ withOptions opts{genQuotedDecs = True} $ promote' $ lift qdecs++-- | Promote each declaration, discarding the originals. Note that a promoted+-- datatype uses the same definition as an original datatype, so this will+-- not work with datatypes. Classes, instances, and functions are all fine.+promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]+promoteOnly qdecs = do+ opts <- getOptions+ withOptions opts{genQuotedDecs = False} $ promote' $ lift qdecs++-- The workhorse for 'promote' and 'promoteOnly'. The difference between the+-- two functions is whether 'genQuotedDecs' is set to 'True' or 'False'.+promote' :: OptionsMonad q => q [Dec] -> q [Dec]+promote' qdecs = do+ opts <- getOptions+ decs <- qdecs+ ddecs <- withLocalDeclarations decs $ dsDecs decs+ promDecs <- promoteM_ decs $ promoteDecs ddecs+ let origDecs | genQuotedDecs opts = decs+ | otherwise = []+ return $ origDecs ++ decsToTH promDecs++-- | Generate defunctionalization symbols for each of the provided type-level+-- declaration 'Name's. See the "Promotion and partial application" section of+-- the @singletons@+-- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@+-- for further explanation.+genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]+genDefunSymbols names = do+ checkForRep names+ infos <- mapM (dsInfo <=< reifyWithLocals) names+ decs <- promoteMDecs [] $ concatMapM defunInfo infos+ return $ decsToTH decs++-- | Produce instances for @PEq@ from the given types+promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]+promoteEqInstances = concatMapM promoteEqInstance++-- | Produce an instance for @PEq@ from the given type+promoteEqInstance :: OptionsMonad q => Name -> q [Dec]+promoteEqInstance = promoteInstance mkEqInstance "Eq"++-- | Produce instances for 'POrd' from the given types+promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]+promoteOrdInstances = concatMapM promoteOrdInstance++-- | Produce an instance for 'POrd' from the given type+promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]+promoteOrdInstance = promoteInstance mkOrdInstance "Ord"++-- | Produce instances for 'PBounded' from the given types+promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]+promoteBoundedInstances = concatMapM promoteBoundedInstance++-- | Produce an instance for 'PBounded' from the given type+promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]+promoteBoundedInstance = promoteInstance mkBoundedInstance "Bounded"++-- | Produce instances for 'PEnum' from the given types+promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]+promoteEnumInstances = concatMapM promoteEnumInstance++-- | Produce an instance for 'PEnum' from the given type+promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]+promoteEnumInstance = promoteInstance mkEnumInstance "Enum"++-- | Produce instances for 'PShow' from the given types+promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]+promoteShowInstances = concatMapM promoteShowInstance++-- | Produce an instance for 'PShow' from the given type+promoteShowInstance :: OptionsMonad q => Name -> q [Dec]+promoteShowInstance = promoteInstance mkShowInstance "Show"++promoteInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec]+promoteInstance mk_inst class_name name = do+ (df, tvbs, cons) <- getDataD ("I cannot make an instance of " ++ class_name+ ++ " for it.") name+ 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+ return $ decsToTH decs++promoteInfo :: DInfo -> PrM ()+promoteInfo (DTyConI dec _instances) = promoteDecs [dec]+promoteInfo (DPrimTyConI _name _numArgs _unlifted) =+ fail "Promotion of primitive type constructors not supported"+promoteInfo (DVarI _name _ty _mdec) =+ fail "Promotion of individual values not supported"+promoteInfo (DTyVarI _name _ty) =+ fail "Promotion of individual type variables not supported"+promoteInfo (DPatSynI {}) =+ fail "Promotion of pattern synonyms not supported"++-- Promote a list of top-level declarations.+promoteDecs :: [DDec] -> PrM ()+promoteDecs raw_decls = do+ decls <- expand raw_decls -- expand type synonyms+ checkForRepInDecls decls+ PDecs { pd_let_decs = let_decs+ , pd_class_decs = classes+ , pd_instance_decs = insts+ , pd_data_decs = datas+ , pd_ty_syn_decs = ty_syns+ , pd_open_type_family_decs = o_tyfams+ , pd_closed_type_family_decs = c_tyfams } <- partitionDecs decls++ defunTopLevelTypeDecls ty_syns c_tyfams o_tyfams+ rec_sel_let_decs <- promoteDataDecs datas+ -- promoteLetDecs returns LetBinds, which we don't need at top level+ _ <- promoteLetDecs Nothing $ rec_sel_let_decs ++ let_decs+ mapM_ promoteClassDec classes+ let orig_meth_sigs = foldMap (lde_types . cd_lde) classes+ cls_tvbs_map = Map.fromList $ map (\cd -> (cd_name cd, cd_tvbs cd)) classes+ mapM_ (promoteInstanceDec orig_meth_sigs cls_tvbs_map) insts++-- curious about ALetDecEnv? See the LetDecEnv module for an explanation.+promoteLetDecs :: Maybe Uniq -- let-binding unique (if locally bound)+ -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)+promoteLetDecs mb_let_uniq decls = do+ opts <- getOptions+ let_dec_env <- buildLetDecEnv decls+ all_locals <- allLocals+ 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 let_dec_proms })++promoteDataDecs :: [DataDecl] -> PrM [DLetDec]+promoteDataDecs = concatMapM promoteDataDec++-- "Promotes" a data type, much like D.S.TH.Single.Data.singDataD singles a data+-- type. Promoting a data type is much easier than singling it, however, since+-- DataKinds automatically promotes data types and kinds and data constructors+-- to types. That means that promoteDataDec only has to do three things:+--+-- 1. Emit defunctionalization symbols for each data constructor,+--+-- 2. Emit promoted fixity declarations for each data constructor and promoted+-- record selector (assuming the originals have fixity declarations), and+--+-- 3. Assemble a top-level function that mimics the behavior of its record+-- selectors. Note that promoteDataDec does not actually promote this record+-- selector function—it merely returns its DLetDecs. Later, the promoteDecs+-- function takes these DLetDecs and promotes them (using promoteLetDecs).+-- This greatly simplifies the plumbing, since this allows all DLetDecs to+-- be promoted in a single location.+-- See Note [singletons-th and record selectors] in D.S.TH.Single.Data.+--+-- Note that if @NoFieldSelectors@ is active, then neither steps (2) nor (3)+-- will promote any records to top-level field selectors.+promoteDataDec :: DataDecl -> PrM [DLetDec]+promoteDataDec (DataDecl _ _ _ ctors) = do+ let rec_sel_names = nub $ concatMap extractRecSelNames ctors+ -- Note the use of nub: the same record selector name can+ -- be used in multiple constructors!+ fld_sels <- qIsExtEnabled LangExt.FieldSelectors+ rec_sel_let_decs <- if fld_sels then getRecordSelectors ctors else pure []+ ctorSyms <- buildDefunSymsDataD ctors+ -- NB: If NoFieldSelectors is active, then promoteReifiedInfixDecls will not+ -- promote any of `rec_sel_names` to field selectors, so there is no need to+ -- check for it here.+ infix_decs <- promoteReifiedInfixDecls rec_sel_names+ emitDecs $ ctorSyms ++ infix_decs+ pure rec_sel_let_decs++promoteClassDec :: UClassDecl -> PrM AClassDecl+promoteClassDec decl@(ClassDecl { cd_name = cls_name+ , cd_tvbs = orig_cls_tvbs+ , cd_fds = fundeps+ , cd_atfs = atfs+ , cd_lde = lde@LetDecEnv+ { lde_defns = defaults+ , lde_types = meth_sigs+ , lde_infix = infix_decls } }) = do+ opts <- getOptions+ let pClsName = promotedClassName opts cls_name+ meth_sigs_list = OMap.assocs meth_sigs+ meth_names = map fst meth_sigs_list+ defaults_list = OMap.assocs defaults+ defaults_names = map fst defaults_list+ mb_cls_sak <- dsReifyType cls_name++ -- 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 cls_tvbs_spec) defaults_list+ defunAssociatedTypeFamilies orig_cls_tvbs atfs++ 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 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+ let defaults_list' = zip defaults_names ann_rhss+ proms = zip defaults_names prom_rhss+ return (decl { cd_lde = lde { lde_defns = OMap.fromList defaults_list'+ , lde_proms = OMap.fromList proms } })+ where+ -- 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+ (_, 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+ pro_meth_args+ (DKindSig meth_res_ki)+ Nothing)++{-+Note [Promoted class methods and kind variable ordering]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+In general, we make an effort to preserve the order of type variables when+promoting type signatures, but there is an annoying corner case where this is+difficult: class methods. When promoting class methods, the order of kind+variables in their kinds will often "just work" by happy coincidence, but+there are some situations where this does not happen. Consider the following+class:++ class C (b :: Type) where+ m :: forall a. a -> b -> a++The full type of `m` is `forall b. C b => forall a. a -> b -> a`, which binds+`b` before `a`. This order is preserved when singling `m`, but *not* when+promoting `m`. This is because the `C` class is promoted as follows:++ class PC (b :: Type) where+ type M (x :: a) (y :: b) :: a++Due to the way GHC kind-checks associated type families, the kind of `M` is+`forall a b. a -> b -> a`, which binds `b` *after* `a`. Moreover, the+`StandaloneKindSignatures` extension does not provide a way to explicitly+declare the full kind of an associated type family, so this limitation is+not easy to work around.++The defunctionalization symbols for `M` will also follow a similar+order of type variables:++ type MSym0 :: forall a b. a ~> b ~> a+ type MSym1 :: forall a b. a -> b ~> a++In the past, we have considered different ways to rectify this, but none of+the approaches that we have tried are quite satisfactory:++* We could hackily specify the order of kind variables using a type synonym+ like `FlipConst`:++ 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+promoteInstanceDec :: OMap Name DType+ -- Class method type signatures+ -> Map Name [DTyVarBndrVis]+ -- Class header type variable (e.g., if `class C a b` is+ -- quoted, then this will have an entry for {C |-> [a, b]})+ -> UInstDecl -> PrM AInstDecl+promoteInstanceDec orig_meth_sigs cls_tvbs_map+ decl@(InstDecl { id_name = cls_name+ , id_arg_tys = inst_tys+ , id_sigs = inst_sigs+ , id_meths = meths }) = do+ opts <- getOptions+ cls_tvbs <- lookup_cls_tvbs+ inst_kis <- mapM promoteType inst_tys+ let pClsName = promotedClassName opts cls_name+ 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 inst_ki_kvbs) meths+ emitDecs [DInstanceD Nothing Nothing [] (foldType (DConT pClsName)+ inst_kis) meths']+ return (decl { id_meths = zip (map fst meths) ann_rhss })+ where+ lookup_cls_tvbs :: PrM [DTyVarBndrVis]+ lookup_cls_tvbs =+ -- First, try consulting the map of class names to their type variables.+ -- It is important to do this first to ensure that we consider locally+ -- declared classes before imported ones. See #410 for what happens if+ -- you don't.+ case Map.lookup cls_name cls_tvbs_map of+ Just tvbs -> pure tvbs+ Nothing -> reify_cls_tvbs+ -- If the class isn't present in this map, we try reifying the class+ -- as a last resort.++ reify_cls_tvbs :: PrM [DTyVarBndrVis]+ reify_cls_tvbs = do+ opts <- getOptions+ let pClsName = promotedClassName opts cls_name+ mk_tvbs = extract_tvbs (dsReifyTypeNameInfo pClsName)+ <|> extract_tvbs (dsReifyTypeNameInfo cls_name)+ -- See Note [Using dsReifyTypeNameInfo when promoting instances]+ mb_tvbs <- runMaybeT mk_tvbs+ case mb_tvbs of+ Just tvbs -> pure tvbs+ Nothing -> fail $ "Cannot find class declaration annotation for " ++ show cls_name++ extract_tvbs :: PrM (Maybe DInfo) -> MaybeT PrM [DTyVarBndrVis]+ extract_tvbs reify_info = do+ mb_info <- lift reify_info+ case mb_info of+ Just (DTyConI (DClassD _ _ tvbs _ _) _) -> pure tvbs+ _ -> empty++{-+Note [Using dsReifyTypeNameInfo when promoting instances]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+During the promotion of a class instance, it becomes necessary to reify the+original promoted class's info to learn various things. It's tempting to think+that just calling dsReify on the class name will be sufficient, but it's not.+Consider this class and its promotion:++ class Eq a where+ (==) :: a -> a -> Bool++ class PEq a where+ type (==) (x :: a) (y :: a) :: Bool++Notice how both of these classes have an identifier named (==), one at the+value level, and one at the type level. Now imagine what happens when you+attempt to promote this Template Haskell declaration:++ [d| f :: Bool+ f = () == () |]++When promoting ==, singletons-th will come up with its promoted equivalent (which also+happens to be ==). However, this promoted name is a raw Name, since it is created+with mkName. This becomes an issue when we call dsReify the raw "==" Name, as+Template Haskell has to arbitrarily choose between reifying the info for the+value-level (==) and the type-level (==), and in this case, it happens to pick the+value-level (==) info. We want the type-level (==) info, however, because we care+about the promoted version of (==).++Fortunately, there's a serviceable workaround. Instead of dsReify, we can use+dsReifyTypeNameInfo, which first calls lookupTypeName (to ensure we can find a Name+that's in the type namespace) and _then_ reifies it.+-}++-- Which sort of class methods are being promoted?+data MethodSort+ -- The method defaults in class declarations.+ = DefaultMethods+ -- The methods in instance declarations.+ | InstanceMethods (OMap Name DType) -- ^ InstanceSigs+ (Map Name DKind) -- ^ Instantiations for class tyvars+ -- See Note [Promoted class method kinds]+ deriving Show++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, LetDecProm)+ -- returns (type instance, ALetDecRHS, promoted RHS)+promoteMethod meth_sort orig_sigs_map cls_tvbs (meth_name, meth_rhs) = do+ opts <- getOptions+ (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"+ alpha -> alpha++ -- family_args are the type variables in a promoted class's+ -- associated type family instance (or default implementation), e.g.,+ --+ -- class C k where+ -- type T (a :: k) (b :: Bool)+ -- type T a b = THelper1 a b -- family_args = [a, b]+ --+ -- instance C Bool where+ -- type T a b = THelper2 a b -- family_args = [a, b]+ --+ -- We could annotate these variables with explicit kinds, but it's not+ -- strictly necessary, as kind inference can figure them out just as well.+ family_args = map DVarT meth_arg_tvs+ helperName <- newUniqueName helperNameBase+ 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+ return ( DTySynInstD+ (DTySynEqn Nothing+ (foldType (DConT proName) family_args)+ (foldType (DConT proHelperName) family_args))+ , ann_rhs+ , (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,+ -- "the type" is like the type of the original method, but substituted for+ -- 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.)+ --+ -- 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 ->+ -- No substitution for class variables is required for default+ -- method type signatures, as they share type variables with the+ -- class they inhabit.+ lookup_meth_ty+ InstanceMethods inst_sigs_map cls_subst ->+ case OMap.lookup meth_name inst_sigs_map of+ Just ty -> do+ -- 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.+ (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.+ (_, 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 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 (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.+ (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.+ mb_info <- dsReifyTypeNameInfo proName+ -- See Note [Using dsReifyTypeNameInfo when promoting instances]+ case mb_info of+ Just (DTyConI (DOpenTypeFamilyD (DTypeFamilyHead _ tvbs mb_res_ki _)) _)+ -> let arg_kis = map (defaultMaybeToTypeKind . extractTvbKind) tvbs+ res_ki = defaultMaybeToTypeKind (resultSigToMaybeKind mb_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++{-+Note [Promoted class method kinds]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Consider this example of a type class (and instance):++ class C a where+ m :: a -> Bool -> Bool+ m _ x = x++ instance C [a] where+ m l _ = null l++The promoted version of these declarations would be:++ class PC a where+ type M (x :: a) (y :: Bool) :: Bool+ type M x y = MHelper1 x y++ instance PC [a] where+ type M x y = MHelper2 x y++ type MHelper1 :: a -> Bool -> Bool+ type family MHelper1 x y where ...++ type MHelper2 :: [a] -> Bool -> Bool+ type family MHelper2 x y where ...++Getting the kind signature for MHelper1 (the promoted default implementation of+M) is quite simple, as it corresponds exactly to the kind of M. We might even+choose to make that the kind of MHelper2, but then it would be overly general+(and more difficult to find in -ddump-splices output). For this reason, we+substitute in the kinds of the instance itself to determine the kinds of+promoted method implementations like MHelper2.+-}++promoteLetDecEnv :: Maybe Uniq -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)+promoteLetDecEnv mb_let_uniq (LetDecEnv { lde_defns = value_env+ , lde_types = type_env+ , lde_infix = fix_env }) = do+ 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 (fmap fst fix_env) mb_let_uniq)+ names rhss++ emitDecs $ concat defun_decss+ let decs = concat pro_decs ++ infix_decls++ -- build the ALetDecEnv+ let let_dec_env' = LetDecEnv { lde_defns = OMap.fromList $ zip names ann_rhss+ , lde_types = type_env+ , lde_infix = fix_env+ , lde_proms = OMap.empty -- filled in promoteLetDecs+ }++ return (decs, let_dec_env')++-- Promote a fixity declaration.+promoteInfixDecl :: forall q. OptionsMonad q+ => 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+ case mb_ns of+ -- If we can't find the Name for some odd reason, fall back to promote_val+ Nothing -> promote_val+ Just VarName -> promote_val+ Just (FldName _)+ | fld_sels -> promote_val+ | otherwise -> never_mind+ Just DataName -> never_mind+ Just TcClsName -> do+ mb_info <- dsReify name+ case mb_info of+ Just (DTyConI DClassD{} _)+ -> finish $ promotedClassName opts name+ _ -> never_mind+ where+ -- 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 TypeNamespaceSpecifier++ -- Don't produce a fixity declaration at all. This can happen in the+ -- following circumstances:+ --+ -- - When promoting a fixity declaration for a name whose promoted+ -- counterpart is the same as the original name.+ -- See Note [singletons-th and fixity declarations] in+ -- D.S.TH.Single.Fixity, wrinkle 1.+ --+ -- - A fixity declaration contains the name of a record selector when+ -- NoFieldSelectors is active.+ never_mind :: q (Maybe DDec)+ 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 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+ && ns == NoNamespaceSpecifier+ then never_mind+ else finish promoted_name++-- Try producing promoted fixity declarations for Names by reifying them+-- /without/ consulting quoted declarations. If reification fails, recover and+-- return the empty list.+-- See [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 2.+promoteReifiedInfixDecls :: forall q. OptionsMonad q => [Name] -> q [DDec]+promoteReifiedInfixDecls = mapMaybeM tryPromoteFixityDeclaration+ where+ tryPromoteFixityDeclaration :: Name -> q (Maybe DDec)+ tryPromoteFixityDeclaration name =+ qRecover (return Nothing) $ do+ mFixity <- qReifyFixity name+ case mFixity of+ Nothing -> pure Nothing+ -- 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+ -- An ordinary (i.e., non-class-related) let-bound declaration.+ = LetBindingRHS+ -- The right-hand side of a class method (either a default method or a+ -- method in an instance declaration).+ | ClassMethodRHS+ (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+-- let bindings. Thus, it can't quite do all the work locally and returns+-- an intermediate structure. Perhaps a better design is available.+promoteLetDecRHS :: LetDecRHSSort+ -> OMap Name DType -- local type env't+ -> OMap Name Fixity -- local fixity env't+ -> Maybe Uniq -- let-binding unique (if locally bound)+ -> Name -- name of the thing being promoted+ -> ULetDecRHS -- body of the thing+ -> PrM ( [DDec] -- promoted type family dec, plus the+ -- SAK dec (if one exists)+ , [DDec] -- defunctionalization+ , ALetDecRHS ) -- annotated RHS+promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do+ all_locals <- allLocals+ case let_dec_rhs of+ UValue exp -> do+ (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals 0+ if ty_num_args == 0+ then do+ prom_fun_lhs <- promoteLetDecName mb_let_uniq name m_ldrki all_locals+ promote_let_dec_rhs all_locals m_ldrki 0 (promoteExp exp)+ (\exp' -> [DTySynEqn Nothing prom_fun_lhs exp'])+ AValue+ else+ -- If we have a UValue with a function type, process it as though it+ -- were a UFunction. promote_function_rhs will take care of+ -- eta-expanding arguments as necessary.+ promote_function_rhs all_locals [DClause [] exp]+ 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 :: [LocalVar]+ -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS)+ promote_function_rhs all_locals clauses = do+ numArgs <- count_args clauses+ (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals numArgs+ expClauses <- mapM (etaContractOrExpand ty_num_args numArgs) clauses+ let promote_clause = promoteClause mb_let_uniq name m_ldrki all_locals+ promote_let_dec_rhs all_locals m_ldrki ty_num_args+ (mapAndUnzipM promote_clause expClauses)+ id (AFunction ty_num_args)++ -- Promote a UValue or a UFunction.+ -- Notes about type variables:+ --+ -- * For UValues, `prom_a` is DType and `a` is Exp.+ --+ -- * For UFunctions, `prom_a` is [DTySynEqn] and `a` is [DClause].+ promote_let_dec_rhs+ :: [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+ -> (prom_a -> [DTySynEqn]) -- Turn the promoted RHS into type family equations+ -> (a -> ALetDecRHS) -- Build an ALetDecRHS+ -> PrM ([DDec], [DDec], ALetDecRHS)+ promote_let_dec_rhs all_locals m_ldrki ty_num_args+ promote_thing mk_prom_eqns mk_alet_dec_rhs = do+ opts <- getOptions+ tyvarNames <- replicateM ty_num_args (qNewName "a")+ let proName = promotedValueName opts name mb_let_uniq+ m_fixity = OMap.lookup name fix_env++ mk_tf_head :: [DTyVarBndrVis] -> DFamilyResultSig -> DTypeFamilyHead+ mk_tf_head arg_tvbs res_sig =+ dTypeFamilyHead_with_locals proName all_locals arg_tvbs res_sig++ (lde_kvs_to_bind, m_sak_dec, defun_ki, tf_head) =+ -- There are three possible cases:+ case m_ldrki of+ -- 1. We have no kind information whatsoever.+ Nothing ->+ let arg_tvbs = map (`DPlainTV` BndrReq) tyvarNames in+ ( OSet.empty+ , 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 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 all_locals arg_tvbs (Just resK)+ , mk_tf_head arg_tvbs (DKindSig resK)+ )+ -- 2(b). We have a standalone kind signature.+ Just sak ->+ -- Compute the type variable binders needed to give the type+ -- family the correct arity.+ -- See Note [Generating type families with the correct arity].+ let tvbs' | null tvbs+ = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf (argKs ++ [resK])+ | otherwise+ = tvbs+ arg_tvbs' = dtvbSpecsToBndrVis tvbs' ++ arg_tvbs in+ ( lde_kvs_to_bind'+ , Just $ DKiSigD proName sak+ , DefunSAK sak+ -- We opt to annotate the argument and result kinds in+ -- the body of the type family declaration even if it is+ -- given a standalone kind signature.+ -- See Note [Keep redundant kind information for Haddocks].+ , mk_tf_head arg_tvbs' (DKindSig resK)+ )++ defun_decs <- defunctionalize proName m_fixity defun_ki+ (prom_thing, thing) <- scopedBind lde_kvs_to_bind promote_thing+ return ( catMaybes [ m_sak_dec+ , Just $ DClosedTypeFamilyD tf_head (mk_prom_eqns prom_thing)+ ]+ , defun_decs+ , mk_alet_dec_rhs thing )++ 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]+ -> Int -- The number of arguments to default to if the+ -- type cannot be inferred. This is 0 for UValues+ -- and the number of arguments in a single clause+ -- for UFunctions.+ -> PrM (Maybe LetDecRHSKindInfo, Int)+ -- Returns two things in a pair:+ --+ -- 1. Information about the promoted kind,+ -- if available.+ --+ -- 2. The number of arguments the let-dec has.+ -- If no kind information is available from+ -- which to infer this number, then this+ -- will default to the earlier Int argument.+ promote_let_dec_ty all_locals default_num_args =+ case rhs_sort of+ 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+ -- promoteType turns rank-1 uses of (->) into (~>). So, we unravel+ -- first to avoid this behavior, and then ravel back.+ (tvbs, argKs, resultK) <- promoteUnraveled ty+ let m_sak | null all_locals = Just $ ravelVanillaDType tvbs [] argKs resultK+ -- If this let-dec closes over local variables, then+ -- 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 scoped_tvs tvbs argKs resultK), length argKs)++ | otherwise+ -> return (Nothing, default_num_args)++ etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause+ etaContractOrExpand ty_num_args clause_num_args (DClause pats exp)+ | n >= 0 = do -- Eta-expand+ names <- replicateM n (newUniqueName "a")+ let newPats = map DVarP names+ newArgs = map DVarE names+ return $ DClause (pats ++ newPats) (foldExp exp newArgs)+ | otherwise = do -- Eta-contract+ let (clausePats, lamPats) = splitAt ty_num_args pats+ lamExp = dLamE lamPats exp+ return $ DClause clausePats lamExp+ where+ n = ty_num_args - clause_num_args++ count_args :: [DClause] -> PrM Int+ count_args (DClause pats _ : _) = return $ length pats+ count_args _ = fail $ "Impossible! A function without clauses."++-- An auxiliary data type used in promoteLetDecRHS that describes information+-- related to the promoted kind of a class method default or normal+-- let binding.+data LetDecRHSKindInfo =+ LDRKI (Maybe DKind) -- The standalone kind signature, if applicable.+ -- 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.++{-+Note [No SAKs for let-decs with local variables]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Consider promoting this:++ f :: Bool+ f = let x = True+ g :: () -> Bool+ g _ = x+ in g ()++Clearly, the promoted `F` type family will have the following SAK:++ type F :: ()++What about `G`? At a passing glance, it appears that you could get away with+this:++ type G :: Bool -> ()++But this isn't quite right, since `g` closes over `x = True`. The body of `G`,+therefore, has to lift `x` to be an explicit argument:++ type family G x (u :: ()) :: Bool where+ G x _ = x++At present, we don't keep track of the types of local variables like `x`, which+makes it difficult to create a SAK for things like `G`. Here are some possible+ideas, each followed by explanations for why they are infeasible:++* Use wildcards:++ type G :: _ -> () -> Bool++ Alas, GHC currently does not allow wildcards in SAKs. See GHC#17432.++* Use visible dependent quantification to avoid having to say what the kind+ of `x` is:++ type G :: forall x -> () -> Bool++ A clever trick to be sure, but it doesn't quite do what we want, since+ GHC will generalize that kind to become `forall (x :: k) -> () -> Bool`,+ which is more general than we want.++In any case, it's probably not worth bothering with SAKs for local definitions+like `g` in the first place, so we avoid generating SAKs for anything that+closes over at least one local variable for now. If someone yells about this,+we'll reconsider this design.++Note [Keep redundant kind information for Haddocks]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+`singletons-th` generates explicit argument kinds and result kinds for+type-level declarations whenever possible, even if those kinds are technically+redundant. For example, `singletons-th` would promote this:++ id' :: a -> a++To this:++ type Id' :: a -> a+ type family Id' (x :: a) :: a where ...++Strictly speaking, the argument and result kind of Id' are unnecessary, since+the same information is already present in the standalone kind signature.+However, due to a Haddock limitation+(https://github.com/haskell/haddock/issues/1178), Haddock will not render+standalone kind signatures at all, so if the argument and result kind of Id'+were omitted in the body, Haddock would render it like so:++ type family Id' x where ...++This is unfortunate for Haddock viewers, as this does not convey any kind+information whatsoever. Until the aformentioned Haddock issue is resolved, we+work around this limitation by generating the redundant argument and kind+information anyway. Thankfully, this is simple to accomplish, as we already+compute this information to begin with.++Note [Generating type families with the correct arity]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+As of GHC 9.10, GHC no longer performs arity inference when kind-checking type+family declarations with standalone kind signatures. This is an important+consideration when promoting functions with top-level type signatures. For+example, we would not want to take this definition:++ f :: Either a Bool+ f = Right True++And promote it to this type family:++ type F :: Either a Bool+ type family F where+ F = Right True++GHC would reject this type family because it would expect F to have arity 0,+but its definition requires arity 1. This is because the definition of F is+tantamount to writing:++ F @a = Right @a @Bool True -- This takes 1 argument, hence arity 1++In order to make F kind-check, we need to generate a type family header that+explicitly declares it to have arity 1, not arity 0:++ type F :: Either a Bool+ type family F @a where+ F = Right True++Note the @a binder after F in the type family header.++If the standalone kind signature lacks an outermost forall, then we simply bind+the type variables in left-to-right order, preserving dependencies (using+`toposortTyVarsOf`). If the standalone kind signature does have an outermost+`forall`, then we bind the type variables according to the order in which it+appears in the `forall`, making sure to filter out any inferred type variable+binders. For example, we would want to take this definition (from #585):++ konst :: forall a {b}. a -> b -> a+ konst x _ = x++And promote it to this type family:++ type Konst :: forall a {b}. a -> b -> a+ type family Konst @a x y where+ Konst @a (x :: a) (_ :: b) = x++Note that we do not bind @b here. The `dtvbSpecsToBndrVis` function is+responsible for filtering out inferred type variable binders.+-}++promoteClause :: Maybe Uniq+ -- ^ Let-binding unique (if locally bound)+ -> Name+ -- ^ Name of the function being promoted+ -> Maybe LetDecRHSKindInfo+ -- ^ Information about the promoted kind (if present)+ -> [LocalVar]+ -- ^ The local variables currently in scope+ -> DClause -> PrM (DTySynEqn, ADClause)+promoteClause mb_let_uniq name m_ldrki all_locals (DClause pats exp) = do+ -- 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.+ let types_w_kinds =+ case m_ldrki of+ Just (LDRKI _ scoped_tvs _ kinds _)+ | not (OSet.null scoped_tvs)+ -> zipWith DSigT types kinds+ _ -> types+ let PromDPatInfos { prom_dpat_vars = new_vars+ , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos+ (ty, ann_exp) <- scopedBind sig_kvs $+ lambdaBind new_vars $+ promoteExp exp+ pro_clause_fun <- promoteLetDecName mb_let_uniq name m_ldrki all_locals+ return ( DTySynEqn Nothing (foldType pro_clause_fun types_w_kinds) ty+ , ADClause new_vars pats' ann_exp )++-- | 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+ 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+ opts <- getOptions+ kis <- traverse (promoteType_options conOptions) tys+ (types, pats') <- mapAndUnzipM (promotePat Nothing) pats+ let name' = promotedDataTypeOrConName opts name+ return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats')+ where+ -- Currently, visible type patterns of data constructors are the one place+ -- in `singletons-th` where it makes sense to promote wildcard types, as it+ -- will produce code that GHC will accept.+ conOptions :: PromoteTypeOptions+ conOptions = defaultPromoteTypeOptions{ptoAllowWildcards = True}+promotePat m_ki (DTildeP pat) = do+ qReportWarning "Lazy pattern converted into regular pattern in promotion"+ second ADTildeP <$> promotePat m_ki pat+promotePat m_ki (DBangP pat) = do+ qReportWarning "Strict pattern converted into regular pattern in promotion"+ 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+ ki <- promoteType ty+ (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)++promoteExp :: DExp -> PrM (DType, ADExp)+promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name+promoteExp (DConE name) = do+ opts <- getOptions+ return (DConT $ defunctionalizedName0 opts name, ADConE name)+promoteExp (DLitE lit) = fmap (, ADLitE lit) $ promoteLitExp lit+promoteExp (DAppE exp1 exp2) = do+ (exp1', ann_exp1) <- promoteExp exp1+ (exp2', ann_exp2) <- promoteExp exp2+ return (apply exp1' exp2', ADAppE ann_exp1 ann_exp2)+-- Until we get visible kind applications, this is the best we can do.+promoteExp (DAppTypeE exp _) = do+ qReportWarning "Visible type applications are ignored by `singletons-th`."+ promoteExp exp+promoteExp (DLamCasesE clauses) = do+ opts <- getOptions+ lam_cases_tf_name <- newUniqueName "LamCases"+ all_locals <- allLocals+ (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]+ 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+ (exp', ann_exp) <- letBind binds $ promoteExp exp+ return (exp', ADLetE ann_env ann_exp)+promoteExp (DSigE exp ty) = do+ (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@(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+ opts <- getOptions+ let tyFromIntegerName = promotedValueName opts fromIntegerName Nothing+ tyNegateName = promotedValueName opts negateName Nothing+ if n >= 0+ then return $ (DConT tyFromIntegerName `DAppT` DLitT (NumTyLit n))+ else return $ (DConT tyNegateName `DAppT`+ (DConT tyFromIntegerName `DAppT` DLitT (NumTyLit (-n))))+promoteLitExp (StringL str) = do+ opts <- getOptions+ let prom_str_lit = DLitT (StrTyLit str)+ os_enabled <- qIsExtEnabled LangExt.OverloadedStrings+ pure $ if os_enabled+ then DConT (promotedValueName opts fromStringName Nothing) `DAppT` prom_str_lit+ else prom_str_lit+promoteLitExp (CharL c) = return $ DLitT (CharTyLit c)+promoteLitExp lit =+ fail ("Only string, natural number, and character literals can be promoted: " ++ show lit)++promoteLitPat :: MonadFail m => Lit -> m DType+promoteLitPat (IntegerL n)+ | n >= 0 = return $ (DLitT (NumTyLit n))+ | otherwise =+ fail $ "Negative literal patterns are not allowed,\n" +++ "because literal patterns are promoted to natural numbers."+promoteLitPat (StringL str) = return $ DLitT (StrTyLit str)+promoteLitPat (CharL c) = return $ DLitT (CharTyLit c)+promoteLitPat lit =+ fail ("Only string, natural number, and character literals can be promoted: " ++ show lit)++-- Promote the name of a 'ULetDecRHS' to the type level. If the promoted+-- 'ULetDecRHS' has a standalone type signature and does not close over any+-- local variables, then this will include the scoped type variables from the+-- type signature as invisible arguments. (See Note [Scoped type variables] in+-- Data.Singletons.TH.Promote.Monad.) Otherwise, it will include any local+-- variables that it closes over as explicit arguments.+promoteLetDecName ::+ Maybe Uniq+ -- ^ Let-binding unique (if locally bound)+ -> Name+ -- ^ Name of the function being promoted+ -> Maybe LetDecRHSKindInfo+ -- ^ Information about the promoted kind (if present)+ -> [LocalVar]+ -- ^ The local variables currently in scope+ -> PrM DType+promoteLetDecName mb_let_uniq name m_ldrki all_locals = do+ opts <- getOptions+ let proName = promotedValueName opts name mb_let_uniq+ type_args =+ case m_ldrki of+ 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+ -- `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+ -- konst x _ = x+ --+ -- To this type family:+ --+ -- type Konst :: forall a {b}. a -> b -> a+ -- type family Konst @a x y where+ -- Konst @a (x :: a) (_ :: b) = x+ --+ -- Note that we apply `a` in `Konst @a` but _not_ `b`, as `b` is+ -- bound using an inferred type variable binder.+ -> map dTyVarBndrVisToDTypeArg $ dtvbSpecsToBndrVis tvbs+ _ -> -- ...otherwise, return the local variables as explicit arguments+ -- using DTANormal.+ map localVarToTypeArg all_locals+ pure $ applyDType (DConT proName) type_args++-- Construct a 'DTypeFamilyHead' that closes over some local variables. We+-- apply `noExactName` to each local variable to avoid GHC#11812.+-- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util.+dTypeFamilyHead_with_locals ::+ Name+ -- ^ Name of type family+ -> [LocalVar]+ -- ^ Local variables+ -> [DTyVarBndrVis]+ -- ^ Variables for type family arguments+ -> DFamilyResultSig+ -- ^ Type family result+ -> DTypeFamilyHead+dTypeFamilyHead_with_locals tf_nm local_vars arg_tvbs res_sig =+ DTypeFamilyHead+ tf_nm+ (map (localVarToTvb BndrReq) local_vars' ++ arg_tvbs')+ res_sig'+ Nothing+ where+ -- 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 `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+ (\(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
@@ -53,7 +53,7 @@ -- Defunctionalize all the type families associated with a type class. defunAssociatedTypeFamilies ::- [DTyVarBndrUnit] -- The type variables bound by the parent class+ [DTyVarBndrVis] -- The type variables bound by the parent class -> [OpenTypeFamilyDecl] -- The type families associated with the parent class -> PrM () defunAssociatedTypeFamilies cls_tvbs atfs = do@@ -85,11 +85,11 @@ -- -- Here, we know that `T :: Bool -> Type` because we can infer that the `a` -- in `type T a` should be of kind `Bool` from the class SAK.- ascribe_tf_tvb_kind :: DTyVarBndrUnit -> DTyVarBndrUnit+ ascribe_tf_tvb_kind :: DTyVarBndrVis -> DTyVarBndrVis ascribe_tf_tvb_kind tvb = case tvb of DKindedTV{} -> tvb- DPlainTV n _ -> maybe tvb (DKindedTV n ()) $ Map.lookup n cls_tvb_kind_map+ DPlainTV n _ -> maybe tvb (DKindedTV n BndrReq) $ Map.lookup n cls_tvb_kind_map buildDefunSyms :: DDec -> PrM [DDec] buildDefunSyms dec =@@ -121,8 +121,8 @@ buildDefunSymsTypeFamilyHead defaultTvbToTypeKind (Just . defaultMaybeToTypeKind) buildDefunSymsTypeFamilyHead- :: (DTyVarBndrUnit -> DTyVarBndrUnit) -- How to default each type variable binder- -> (Maybe DKind -> Maybe DKind) -- How to default the result kind+ :: (DTyVarBndrVis -> DTyVarBndrVis) -- How to default each type variable binder+ -> (Maybe DKind -> Maybe DKind) -- How to default the result kind -> DTypeFamilyHead -> PrM [DDec] buildDefunSymsTypeFamilyHead default_tvb default_kind (DTypeFamilyHead name tvbs result_sig _) = do@@ -130,7 +130,7 @@ res_kind = default_kind (resultSigToMaybeKind result_sig) defunReify name arg_tvbs res_kind -buildDefunSymsTySynD :: Name -> [DTyVarBndrUnit] -> DType -> PrM [DDec]+buildDefunSymsTySynD :: Name -> [DTyVarBndrVis] -> DType -> PrM [DDec] buildDefunSymsTySynD name tvbs rhs = defunReify name tvbs mb_res_kind where -- If a type synonym lacks a SAK, we can "infer" its result kind by@@ -160,11 +160,11 @@ -- (see Note [Fixity declarations for defunctionalization symbols]) -- and dsReifyType to determine whether defunctionalization should make use -- of SAKs or not (see Note [Defunctionalization game plan]).-defunReify :: Name -- Name of the declaration to be defunctionalized- -> [DTyVarBndrUnit] -- The declaration's type variable binders- -- (only used if the declaration lacks a SAK)- -> Maybe DKind -- The declaration's return kind, if it has one- -- (only used if the declaration lacks a SAK)+defunReify :: Name -- Name of the declaration to be defunctionalized+ -> [DTyVarBndrVis] -- The declaration's type variable binders+ -- (only used if the declaration lacks a SAK)+ -> Maybe DKind -- The declaration's return kind, if it has one+ -- (only used if the declaration lacks a SAK) -> PrM [DDec] defunReify name tvbs m_res_kind = do m_fixity <- reifyFixityWithLocals name@@ -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.@@ -206,6 +206,7 @@ extra_name <- qNewName "arg" let sak_arg_n = length sak_arg_kis -- Use noExactName below to avoid GHC#17537.+ -- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util. arg_names <- replicateM sak_arg_n (noExactName <$> qNewName "a") let -- The inner loop. @go n arg_nks res_nks@ returns @(res_k, decls)@.@@ -252,8 +253,8 @@ -- gets to be that large. go :: Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec]) go n arg_nks res_nkss =- let arg_tvbs :: [DTyVarBndrUnit]- arg_tvbs = map (\(na, ki) -> DKindedTV na () ki) arg_nks+ let arg_tvbs :: [DTyVarBndrVis]+ arg_tvbs = map (\(na, ki) -> DKindedTV na BndrReq ki) arg_nks mk_sak_dec :: DKind -> DDec mk_sak_dec res_ki =@@ -262,15 +263,27 @@ case res_nkss of [] -> let sat_sak_dec = mk_sak_dec sak_res_ki- sat_decs = mk_sat_decs opts n arg_tvbs (Just sak_res_ki)+ -- Compute the type variable binders needed to give the type+ -- family the correct arity.+ -- See Note [Generating type families with the correct arity]+ -- in D.S.TH.Promote.+ sak_tvbs' | null sak_tvbs+ = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf (sak_arg_kis ++ [sak_res_ki])+ | otherwise+ = sak_tvbs+ sat_decs = mk_sat_decs opts n sak_tvbs' arg_tvbs (Just sak_res_ki) in (sak_res_ki, sat_sak_dec:sat_decs) res_nk:res_nks ->- let (res_ki, decs) = go (n+1) (arg_nks ++ [res_nk]) res_nks- 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@@ -281,11 +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 :: [DTyVarBndrUnit] -> 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@@ -310,19 +325,22 @@ -- kinds are not always known. By a similar token, this function -- uses Maybe DKind, not DKind, as the type of @m_res_k@, since -- the result kind is not always fully known.- go :: Int -> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])+ 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@@ -330,33 +348,44 @@ mk_defun_decs :: Options -> Int -> Int- -> [DTyVarBndrUnit]- -> Name+ -> [DTyVarBndrVis] -> 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- arg_names = map extractTvbName arg_tvbs- params = arg_tvbs ++ [DPlainTV tyfun_name ()]+ params = arg_tvbs ++ [DPlainTV tyfun_name BndrReq] con_eq_ct = DConT sameKindName `DAppT` lhs `DAppT` rhs where- lhs = foldType (DConT data_name) (map DVarT arg_names) `apply` (DVarT extra_name)- rhs = foldType (DConT next_name) (map DVarT (arg_names ++ [extra_name]))+ lhs = app_data_ty `apply` DVarT extra_name+ rhs = foldTypeTvbs (DConT next_name)+ (arg_tvbs ++ [DPlainTV extra_name BndrReq]) con_decl = DCon [] [con_eq_ct] con_name (DNormalC False []) (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)- (foldTypeTvbs (DConT app_eqn_rhs_name)- (arg_tvbs ++ [DPlainTV 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. -- See Note [Fully saturated defunctionalization symbols]@@ -379,15 +408,28 @@ -- Generate a "fully saturated" defunction symbol, along with a fixity -- declaration (if needed). -- See Note [Fully saturated defunctionalization symbols].- mk_sat_decs :: Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]- mk_sat_decs opts n sat_tvbs m_sat_res =+ mk_sat_decs ::+ Options+ -> Int+ -> [DTyVarBndrSpec]+ -- ^ The invisible type variable binders to put in the type family+ -- head in order to give it the correct arity.+ -- See Note [Generating type families with the correct arity] in+ -- D.S.TH.Promote.+ -> [DTyVarBndrVis]+ -- ^ The visible kind arguments.+ -> Maybe DKind+ -- ^ The result kind (if known).+ -> [DDec]+ mk_sat_decs opts n sat_tvbs sat_args m_sat_res = let sat_name = defunctionalizedName opts name n sat_dec = DClosedTypeFamilyD- (DTypeFamilyHead sat_name sat_tvbs+ (DTypeFamilyHead sat_name+ (dtvbSpecsToBndrVis sat_tvbs ++ sat_args) (maybeKindToResultSig m_sat_res) Nothing) [DTySynEqn Nothing- (foldTypeTvbs (DConT sat_name) sat_tvbs)- (foldTypeTvbs (DConT name) sat_tvbs)]+ (foldTypeTvbs (DConT sat_name) sat_args)+ (foldTypeTvbs (DConT name) sat_args)] sat_fixity_dec = maybeToList $ fmap (mk_fix_decl sat_name) m_fixity in sat_dec : sat_fixity_dec @@ -399,7 +441,7 @@ -- -- >>> eta_expand [(x :: a), (y :: b)] Nothing -- ([(x :: a), (y :: b)], Nothing)- eta_expand :: [DTyVarBndrUnit] -> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)+ eta_expand :: [DTyVarBndrVis] -> Maybe DKind -> PrM ([DTyVarBndrVis], Maybe DKind) eta_expand m_arg_tvbs Nothing = pure (m_arg_tvbs, Nothing) eta_expand m_arg_tvbs (Just res_kind) = do let (arg_ks, result_k) = unravelDType res_kind@@ -409,16 +451,18 @@ -- Convert a DVisFunArg to a DTyVarBndr, generating a fresh type variable -- name if the DVisFunArg is an anonymous argument.- mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrUnit+ mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrVis mk_extra_tvb vfa = case vfa of- DVisFADep tvb -> pure tvb- DVisFAAnon k -> (\n -> DKindedTV n () k) <$>+ DVisFADep tvb -> pure (BndrReq <$ tvb)+ DVisFAAnon k -> (\n -> DKindedTV n BndrReq k) <$> -- Use noExactName below to avoid GHC#19743.+ -- See also Note [Pitfalls of NameU/NameL]+ -- in Data.Singletons.TH.Util. (noExactName <$> qNewName "e") mk_fix_decl :: Name -> Fixity -> DDec- mk_fix_decl n f = DLetDec $ DInfixD f n+ mk_fix_decl n f = DLetDec $ DInfixD f TypeNamespaceSpecifier n -- Indicates whether the type being defunctionalized has a standalone kind -- signature. If it does, DefunSAK contains the kind. If not, DefunNoSAK@@ -427,8 +471,15 @@ -- See Note [Defunctionalization game plan] for details on how this -- information is used. data DefunKindInfo- = DefunSAK DKind- | DefunNoSAK [DTyVarBndrUnit] (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@@ -495,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@@ -579,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 -----@@ -651,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@@ -699,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@@ -809,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@@ -818,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
@@ -12,11 +12,12 @@ module Data.Singletons.TH.Promote.Monad ( PrM, promoteM, promoteM_, promoteMDecs, VarPromotions, allLocals, emitDecs, emitDecsM,- lambdaBind, LetBind, letBind, lookupVarE, forallBind, allBoundKindVars+ scopedBind, lambdaBind, LetBind, letBind, lookupVarE ) where import Control.Monad.Reader import Control.Monad.Writer+import qualified Data.Foldable as F import Language.Haskell.TH.Syntax hiding ( lift ) import Language.Haskell.TH.Desugar import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap@@ -26,23 +27,30 @@ import Data.Singletons.TH.Options import Data.Singletons.TH.Syntax -type LetExpansions = OMap Name DType -- from **term-level** name- -- environment during promotion data PrEnv =- PrEnv { pr_options :: Options- , pr_lambda_bound :: OMap Name Name- , pr_let_bound :: LetExpansions- , pr_forall_bound :: OSet Name -- See Note [Explicitly binding kind variables]- , pr_local_decls :: [Dec]+ PrEnv { pr_options :: Options+ , pr_scoped_vars :: OSet LocalVar+ -- ^ The set of scoped type variables currently in scope.+ -- See @Note [Scoped type variables]@.+ , 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]@.+ , pr_local_vars :: OMap Name DType+ -- ^ Map from term-level 'Name's of local variables to their+ -- type-level counterparts. Note that scoped type variables are stored+ -- separately in 'pr_scoped_tvs'.+ -- See @Note [Tracking local variables]@.+ , pr_local_decls :: [Dec] } emptyPrEnv :: PrEnv-emptyPrEnv = PrEnv { pr_options = defaultOptions- , pr_lambda_bound = OMap.empty- , pr_let_bound = OMap.empty- , pr_forall_bound = OSet.empty- , pr_local_decls = [] }+emptyPrEnv = PrEnv { pr_options = defaultOptions+ , pr_scoped_vars = OSet.empty+ , pr_lambda_vars = OMap.empty+ , pr_local_vars = OMap.empty+ , pr_local_decls = [] } -- the promotion monad newtype PrM a = PrM (ReaderT PrEnv (WriterT [DDec] Q) a)@@ -57,16 +65,11 @@ getOptions = asks pr_options -- return *type-level* names-allLocals :: MonadReader PrEnv m => m [Name]+allLocals :: MonadReader PrEnv m => m [LocalVar] allLocals = do- lambdas <- asks (OMap.assocs . pr_lambda_bound)- lets <- asks pr_let_bound- -- filter out shadowed variables!- return [ typeName- | (termName, typeName) <- lambdas- , case OMap.lookup termName lets of- Just (DVarT typeName') | typeName' == typeName -> True- _ -> False ]+ scoped <- asks (F.toList . pr_scoped_vars)+ lambdas <- asks (OMap.assocs . pr_lambda_vars)+ return $ scoped ++ map snd lambdas emitDecs :: MonadWriter [DDec] m => [DDec] -> m () emitDecs = tell@@ -76,42 +79,51 @@ decs <- action emitDecs decs --- when lambda-binding variables, we still need to add the variables--- to the let-expansion, because of shadowing. ugh.+-- ^ 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 LocalVar -> PrM a -> PrM a+scopedBind binds =+ local (\env@(PrEnv { pr_scoped_vars = scoped }) ->+ env { pr_scoped_vars = binds `OSet.union` scoped })++-- ^ Bring a list of 'VarPromotions' into scope for the duration the supplied+-- computation. See @Note [Tracking local variables]@. lambdaBind :: VarPromotions -> PrM a -> PrM a lambdaBind binds = local add_binds- where add_binds env@(PrEnv { pr_lambda_bound = lambdas- , pr_let_bound = lets }) =- let new_lets = OMap.fromList [ (tmN, DVarT tyN) | (tmN, tyN) <- binds ] in- env { pr_lambda_bound = OMap.fromList binds `OMap.union` lambdas- , pr_let_bound = new_lets `OMap.union` lets }+ where add_binds env@(PrEnv { pr_lambda_vars = lambdas+ , pr_local_vars = locals }) =+ -- Per Note [Tracking local variables], these will be added to both+ -- `pr_lambda_vars` and `pr_local_vars`.+ 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. 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+-- computation. See @Note [Tracking local variables]@. letBind :: [LetBind] -> PrM a -> PrM a letBind binds = local add_binds- where add_binds env@(PrEnv { pr_let_bound = lets }) =- env { pr_let_bound = OMap.fromList binds `OMap.union` lets }+ where add_binds env@(PrEnv { pr_local_vars = locals }) =+ env { pr_local_vars = OMap.fromList binds `OMap.union` locals } +-- | Map a term-level 'Name' to its type-level counterpart. This function is+-- aware of any local variables that are currently in scope.+-- See @Note [Tracking local variables]@. lookupVarE :: Name -> PrM DType lookupVarE n = do opts <- getOptions- lets <- asks pr_let_bound- case OMap.lookup n lets of+ locals <- asks pr_local_vars+ case OMap.lookup n locals of Just ty -> return ty Nothing -> return $ DConT $ defunctionalizedName0 opts n --- Add to the set of bound kind variables currently in scope.--- See Note [Explicitly binding kind variables]-forallBind :: OSet Name -> PrM a -> PrM a-forallBind kvs1 =- local (\env@(PrEnv { pr_forall_bound = kvs2 }) ->- env { pr_forall_bound = kvs1 `OSet.union` kvs2 })---- Look up the set of bound kind variables currently in scope.--- See Note [Explicitly binding kind variables]-allBoundKindVars :: PrM (OSet Name)-allBoundKindVars = asks pr_forall_bound- promoteM :: OptionsMonad q => [Dec] -> PrM a -> q (a, [DDec]) promoteM locals (PrM rdr) = do opts <- getOptions@@ -133,60 +145,459 @@ return $ decs1 ++ decs2 {--Note [Explicitly binding kind variables]-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-We want to ensure that when we single type signatures for functions and data-constructors, we should explicitly quantify every kind variable bound by a-forall. For example, if we were to single the identity function:+Note [Tracking local variables]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Handling local variables in singletons-th requires some care. There are three+sorts of local variables that singletons-th tracks: - identity :: forall a. a -> a- identity x = x+1. Scoped type variables, e.g., -We want the final result to be:+ d :: forall a. Maybe a+ d = Nothing :: Maybe a - sIdentity :: forall a (x :: a). Sing x -> Sing (Identity x :: a)- sIdentity sX = sX+ e (x :: a) = Nothing :: Maybe a -Accomplishing this takes a bit of care during promotion. When promoting a-function, we determine what set of kind variables are currently bound at that-point and store them in an ALetDecEnv (as lde_bound_kvs), which in turn is-singled. Then, during singling, we extract every kind variable in a singled-type signature, subtract the lde_bound_kvs, and explicitly bind the variables-that remain.+ In both `d` and `e`, the variable `a` in `:: Maybe a` is scoped. -For a top-level function like identity, lde_bound_kvs is the empty set. But-consider this more complicated example:+2. Lambda-bound variables, e.g., - f :: forall a. a -> a- f = g- where- g :: a -> a- g x = x+ f = \x -> x+ g x = x -When singling, we would eventually end up in this spot:+ In both `f` and `g`, the variable `x` is considered lambda-bound. - sF :: forall a (x :: a). Sing a -> Sing (F a :: a)- sF = sG- where- sG :: _- sG x = x+3. Let-bound variables, e.g., -We must make sure /not/ to fill in the following type for _:+ h =+ let x = 42 in+ x + x - sF :: forall a (x :: a). Sing a -> Sing (F a :: a)- sF = sG- where- sG :: forall a (y :: a). Sing a -> Sing (G a :: a)- sG x = x+ i = x + x+ where+ x = 42 -This would be incorrect, as the `a` bound by sF /must/ be the same one used in-sG, as per the scoping of the original `f` function. Thus, we ensure that the-bound variables from `f` are put into lde_bound_kvs when promoting `g` so-that we subtract out `a` and are left with the correct result:+ In both `h` and `i`, the variable `x` is considered let-bound. - sF :: forall a (x :: a). Sing a -> Sing (F a :: a)- sF = sG- where- sG :: forall (y :: a). Sing a -> Sing (G a :: a)- sG x = x+Why does singletons-th need to track local variables? It's because they must+be promoted differently depending on whether they are local or not. Consider:++ j = ... x ...++When promoting the `j` function to a type family `J`, there are four possible+ways of promoting `x`:++* If `x` is a scoped type variable, then `x` must be promoted to the same+ name. This is because promoting a type variable to a kind variable is a+ no-op. For instance, we would promote this:++ j (z :: x) = (z :: x)++ Here, `(%%)`, `x`, and `y` are lambda-bound variables. But we cannot promote+ `j` to this type family:++ type family J arg where+ J (z :: x) = (z :: x)++* If `x` is a lambda-bound variable, then `x` must be promoted to a type+ variable. In general, we cannot promote `x` to the same name. Consider this+ example:++ j (%%) x y = x %% y++ Here, `(%%)`, `x`, and `y` are lambda-bound variables. But we cannot promote+ `j` to this type family:++ type family J (%%) x y where+ J (%%) x y = x %% y++ This is because type variable names cannot be symbolic like `(%%)` is. As a+ result, we create a fresh name `ty` and promote each occurrence of `(%%)` to+ `ty`:++ type family J ty x y where+ J ty x y = x `ty` y++ See `mkTyName` in Data.Singletons.TH.Names. In fact, `mkTyName` will also+ freshen alphanumeric names, so it would be more accurate to say that `j` will+ be promoted to this:++ type family J ty x_123 y_456 where+ J ty x_123 y_456 = x_123 `ty` y_456++ Where `x_123` and `y_456` are fresh names that are distinct from `x` and `y`.+ Freshening alphanumeric names like `x` and `y` is probably not strictly+ necessary, but `mkTyName` does it anyway (1) for consistency with symbolic+ names and (2) to make the type-level names easier to tell apart from the+ original term-level names.++* If `x` is a let-bound variable, then `x` must be promoted to something like+ `LetX`, where `LetX` is the lambda-lifted version of `x`. For instance, we+ would promote this:++ j = x+ where+ x = True++ To this:++ type family J where+ J = LetX+ type family LetX where+ LetX = True++* If `x` is not a local variable at all, then `x` must be promoted to something+ like `X`, which is assumed to be a top-level function. For instance, we would+ promote this:++ x = 42+ j = x++ To this:++ type family X where+ X = 42+ type family J where+ J = X++Being able to distinguish between all these sorts of variables requires+recording whether they are scoped, lambda-bound, or let-bound at their binding+sites during promotion and singling. This is primarily done in two places:++* During promotion, the `pr_local_vars` field of `PrEnv` tracks lambda- and+ let-bound variables.++* During singling, the `sg_local_vars` field of `SgEnv` tracks lambda- and+ let-bound variables.++Each of these fields are Maps from the original, term-level Names to the+promoted or singled versions of the Names. The `lookupVarE` functions (which+can be found in both Data.Singletons.TH.Promote.Monad and+Data.Singletons.TH.Single.Monad) are responsible for determining what a+term-level Name should be mapped to.++In addition to `pr_local_vars` and `sg_local_vars`, which include both lambda-+and let-bound variables, `PrEnv` also includes two additional fields for+tracking other sorts of local variables:++* The `pr_scoped_vars` field tracks which scoped type variables are currently+ in scope. As discussed above, promoting an occurrence of a scoped type+ variable is a no-op, and as such, we never need to use `lookupVarE` to figure+ out what a scoped type variable promotes to. As such, there is no need to put+ the scoped type variables in `pr_local_vars`.++ On the other hand, we /do/ need to track the scoped type variables for+ lambda-lifting purposes (see Note [Scoped type variables]), and this is the+ only reason why we bother maintaining the `pr_scoped_vars` field in the first+ place. See the `scopedBind` function, which is responsible for adding new+ scoped type variables to `pr_scoped_vars`.++* The `pr_lambda_vars` field only tracks lambda-bound variables, unlike+ `pr_local_vars`, which also includes let-bound variables. We must do this+ because lambda-bound variables are treated differently during lambda lifting.+ Lambda-lifted functions must close over any lambda-bound variables in scope,+ but /not/ any let-bound variables in scope, since the latter are+ lambda-lifted separately.++ A consequence of this is that when we lambda-bind a variable during promotion+ (see `lambdaBind`), we add the variable to both `pr_lambda_vars` and+ `pr_local_vars`. When we let-bind a variable during promotion (see+ `letBind`), we only add the variable to `pr_local_vars`. This means that+ `pr_lambda_vars` will always be a subset of `pr_local_vars`.++Because singling does not do anything akin to lambda lifting, `SgEnv` does not+have anything like `sg_scoped_vars` or `sg_lambda_vars`.++Note [Scoped type variables]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Scoped type variables are a particular form of local variable (see Note+[Tracking local variables]). They are arguably the trickiest form of local+variable to handle, and as noted in the singletons README, there are still some+forms of scoped type variables that singletons-th cannot handle during+promotion.++First, let's discuss how singletons-th promotes scoped type variables in+general:++* When promoting a function with a top-level type signature, we annotate each+ argument on the left-hand sides of type family equations with its kind. This+ is usually redundant, but it can sometimes be useful for bringing type+ variables into scope. For example, this:++ f :: forall a. a -> Maybe a+ f x = (Just x :: Maybe a)++ Will be promoted to something like this:++ type F :: forall a. a -> Maybe a+ type family F x where+ F (x :: a) = (Just x :: Maybe a)++ Note that we gave the `x` on the left-hand side of `F`'s equation an explicit+ `:: a` kind signature to ensure that the `a` on the right-hand side of the+ type family equation is in scope.++ The `promoteClause` function in Data.Singletons.TH.Promote is responsible for+ implementing this.++* Sometimes, there are no arguments available to bring type variables into+ scope. In these situations, we can sometimes use `@` in type family equations+ as an alternative. For example, this:++ g :: forall a. Maybe a+ g = (Nothing :: Maybe a)++ Will be promoted to this:++ type G :: forall a. Maybe a+ type family G where+ G @a = (Nothing :: Maybe a)++ Note the `@a` on `G`'s left-hand side. This relies on `G` having a standalone+ kind signature to work.++ The `promoteLetDecName` function in Data.Singletons.TH.Promote is responsible+ for implementing this.++* When lambda-lifting, singletons-th tracks the current set of scoped type+ variables and includes them as explicit arguments when promoting local+ definitions. For example, this:++ h :: forall a. a -> a+ h x = i+ where+ i = (x :: a)++ Will be promoted to this:++ type H :: forall a. a -> a+ type family H x where+ H @a (x :: a) = LetI a x++ type I a x where+ I a x = (x :: a)++ The `I` type family includes both `a` (a scoped type variable) and `x` (a+ lambda-bound variable) as explicit arguments to ensure that they are in scope+ on the right-hand side, which mentions both of them.++ singletons-th uses the `pr_scoped_vars` field of `PrM` to track scoped type+ variables. Whenever new scoped type variables are bound during promotion, the+ `scopedBind` function is used to add the variables to `pr_scoped_vars`.++These three tricks suffice to handle a substantial number of ways that scoped+type variables can be used. The approach is not perfect, however. Here are two+scenarios where singletons-th fails to promote scoped type variables:++* Funky pattern signatures like this one will not work:++ j :: forall a. a -> a+ j (x :: b) = b++ This is because singletons-th will attempt to promote `j` like so:++ type J :: forall a. a -> a+ type J x where+ J @a ((x :: b) :: a) = b++ But unlike in terms, GHC has no way to know that `a` and `b` are meant to+ refer to the same type variable. In order to make this work, we would need to+ substitute all occurrences of `a` with `b` in the type family equation (or+ vice versa), which seems challenging in the general case.++* Scoped type variables that are only mentioned in the return types of local+ definitions may not always work, such as in this example:++ k x = y+ where+ y :: forall b. Maybe b+ y = Nothing :: Maybe b++ singletons-th would promote `k` and `y` to the following type families:++ type K x where+ K x = LetY x++ type LetY x :: Maybe b where+ LetY x = Nothing :: Maybe b++ Note that because `LetY` closes over the `x` argument, it cannot easily be+ given a standalone kind signature, and this prevents us from writing+ `LetY @b x = ...`. Moreover, `LetY` does not have an argument that we can+ attach an explicit `:: b` signature to. (Attaching it to `x` would be+ incorrect, as that would give `LetY` a less general kind.)++ One possible way forward here would be to give type families the ability to+ write result signatures on their left-hand sides, similar to what GHC+ proposal #228+ (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0228-function-result-sigs.rst)+ offers:++ 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
@@ -33,14 +33,13 @@ import Data.Singletons.TH.Single.Defun import Data.Singletons.TH.Single.Fixity import Data.Singletons.TH.Single.Monad+import Data.Singletons.TH.Single.Ord import Data.Singletons.TH.Single.Type import Data.Singletons.TH.Syntax import Data.Singletons.TH.Util import Language.Haskell.TH.Desugar 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 Data.Map.Strict as Map import Data.Map.Strict ( Map ) import Data.Maybe@@ -138,26 +137,26 @@ singEqInstance :: OptionsMonad q => Name -> q [Dec] singEqInstance = singInstance mkEqInstance "Eq" --- | Create instances of 'SDecide', 'TestEquality', and 'TestCoercion' for each--- type in the list.+-- | Create instances of 'SDecide', 'Eq', 'TestEquality', and 'TestCoercion' for+-- each type in the list. singDecideInstances :: OptionsMonad q => [Name] -> q [Dec] singDecideInstances = concatMapM singDecideInstance --- | Create instances of 'SDecide', 'TestEquality', and 'TestCoercion' for the--- given type.+-- | Create instances of 'SDecide', 'Eq', 'TestEquality', and 'TestCoercion' for+-- the given type. singDecideInstance :: OptionsMonad q => Name -> q [Dec] singDecideInstance name = do- (tvbs, cons) <- getDataD ("I cannot make an instance of SDecide for it.") name- dtvbs <- mapM dsTvbUnit tvbs- let data_ty = foldTypeTvbs (DConT name) dtvbs- dcons <- concatMapM (dsCon dtvbs data_ty) cons- let tyvars = map (DVarT . extractTvbName) dtvbs- kind = foldType (DConT name) tyvars+ (_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+ dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs+ dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons (scons, _) <- singM [] $ mapM (singCtor name) dcons- sDecideInstance <- mkDecideInstance Nothing kind dcons scons- testInstances <- traverse (mkTestInstance Nothing kind name dcons)+ sDecideInstance <- mkDecideInstance Nothing data_ty dcons scons+ eqInstance <- mkEqInstanceForSingleton data_ty name+ testInstances <- traverse (mkTestInstance Nothing data_ty name dcons) [TestEquality, TestCoercion]- return $ decsToTH (sDecideInstance:testInstances)+ return $ decsToTH (sDecideInstance:eqInstance:testInstances) -- | Create instances of 'SOrd' for the given types singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]@@ -200,13 +199,14 @@ -- (Not to be confused with 'singShowInstance'.) showSingInstance :: OptionsMonad q => Name -> q [Dec] showSingInstance name = do- (tvbs, cons) <- getDataD ("I cannot make an instance of Show for it.") name- dtvbs <- mapM dsTvbUnit tvbs- let data_ty = foldTypeTvbs (DConT name) dtvbs- dcons <- concatMapM (dsCon dtvbs data_ty) cons+ (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+ 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 name dtvbs dcons+ data_decl = DataDecl df name dtvbs dcons deriv_show_decl = DerivedDecl { ded_mb_cxt = Nothing , ded_type = kind , ded_type_tycon = name@@ -265,18 +265,19 @@ [DLetDec $ DFunD singMethName [DClause [] $ wrapSingFun 1 DWildCardT $- DLamE [x] $+ dLamE [DVarP x] $ DVarE withSingIName `DAppE` DVarE x `DAppE` DVarE singMethName]] singInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec] singInstance mk_inst inst_name name = do- (tvbs, cons) <- getDataD ("I cannot make an instance of " ++ inst_name- ++ " for it.") name- dtvbs <- mapM dsTvbUnit tvbs- let data_ty = foldTypeTvbs (DConT name) dtvbs- dcons <- concatMapM (dsCon dtvbs data_ty) cons- let data_decl = DataDecl name dtvbs dcons+ (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+ 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 [] $ promoteInstanceDec OMap.empty Map.empty raw_inst@@ -306,6 +307,7 @@ , pd_open_type_family_decs = o_tyfams , pd_closed_type_family_decs = c_tyfams , pd_derived_eq_decs = derivedEqDecs+ , pd_derived_ord_decs = derivedOrdDecs , pd_derived_show_decs = derivedShowDecs } <- partitionDecs decls ((letDecEnv, classes', insts'), promDecls) <- promoteM locals $ do@@ -329,34 +331,43 @@ newClassDecls <- mapM singClassD classes' newInstDecls <- mapM singInstD insts' newDerivedEqDecs <- concatMapM singDerivedEqDecs derivedEqDecs+ newDerivedOrdDecs <- concatMapM singDerivedOrdDecs derivedOrdDecs newDerivedShowDecs <- concatMapM singDerivedShowDecs derivedShowDecs return $ newDataDecls ++ newClassDecls ++ newInstDecls ++ newDerivedEqDecs+ ++ newDerivedOrdDecs ++ newDerivedShowDecs return $ promDecls ++ (map DLetDec newLetDecls) ++ singIDefunDecls ++ newDecls -- see comment at top of file buildDataLets :: OptionsMonad q => DataDecl -> q [(Name, DExp)]-buildDataLets (DataDecl _name _tvbs cons) = do+buildDataLets (DataDecl _df _name _tvbs cons) = do opts <- getOptions- pure $ concatMap (con_num_args opts) cons+ fld_sels <- qIsExtEnabled LangExt.FieldSelectors+ pure $ concatMap (con_num_args opts fld_sels) cons where- con_num_args :: Options -> DCon -> [(Name, DExp)]- con_num_args opts (DCon _tvbs _cxt name fields _rty) =+ con_num_args :: Options -> Bool -> DCon -> [(Name, DExp)]+ con_num_args opts fld_sels (DCon _tvbs _cxt name fields _rty) = (name, wrapSingFun (length (tysOfConFields fields)) (DConT $ defunctionalizedName0 opts name) (DConE $ singledDataConName opts name))- : rec_selectors opts fields+ : rec_selectors opts fld_sels fields - rec_selectors :: Options -> DConFields -> [(Name, DExp)]- rec_selectors _ (DNormalC {}) = []- rec_selectors opts (DRecC fields) =- let names = map fstOf3 fields in- [ (name, wrapSingFun 1 (DConT $ defunctionalizedName0 opts name)- (DVarE $ singledValueName opts name))- | name <- names ]+ rec_selectors :: Options -> Bool -> DConFields -> [(Name, DExp)]+ rec_selectors opts fld_sels con+ | fld_sels+ = case con of+ DNormalC {} -> []+ DRecC fields ->+ let names = map fstOf3 fields in+ [ (name, wrapSingFun 1 (DConT $ defunctionalizedName0 opts name)+ (DVarE $ singledValueName opts name))+ | name <- names ] + | otherwise+ = []+ -- see comment at top of file buildMethLets :: OptionsMonad q => UClassDecl -> q [(Name, DExp)] buildMethLets (ClassDecl { cd_lde = LetDecEnv { lde_types = meth_sigs } }) = do@@ -373,32 +384,29 @@ , cd_name = cls_name , cd_tvbs = cls_tvbs , cd_fds = cls_fundeps- , cd_lde = LetDecEnv { lde_defns = default_defns- , lde_types = meth_sigs- , lde_infix = fixities- , lde_proms = promoted_defaults- , lde_bound_kvs = meth_bound_kvs } }) =+ , cd_lde = LetDecEnv { lde_defns = default_defns+ , lde_types = meth_sigs+ , lde_infix = fixities+ , lde_proms = promoted_defaults } }) = bindContext [foldTypeTvbs (DConT cls_name) cls_tvbs] $ do opts <- getOptions 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_bound_kvs)- meth_names- (map (DConT . defunctionalizedName0 opts) meth_names)+ <- unzip6 <$> zipWithM (singTySig no_meth_defns meth_sigs)+ 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- res_ki_map = Map.fromList (zip meth_names- (map (fromMaybe always_sig) res_kis))- sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList tyvar_names)- (Map.fromList cxts)- res_ki_map))+ 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@@ -407,16 +415,27 @@ (map DLetDec (sing_sigs ++ sing_meths ++ fixities') ++ default_sigs) where no_meth_defns = error "Internal error: can't find declared method type"- always_sig = error "Internal error: no signature for default method" meth_names = map fst $ OMap.assocs meth_sigs + mk_default_sig :: Options -> Name -> DLetDec -> [Name] -> Maybe DType -> Maybe DDec mk_default_sig opts meth_name (DSigD s_name sty) bound_kvs (Just res_ki) = DDefaultSigD s_name <$> add_constraints opts meth_name sty bound_kvs res_ki mk_default_sig _ _ _ _ _ = error "Internal error: a singled signature isn't a signature." - add_constraints opts meth_name sty (_, bound_kvs) res_ki = do -- Maybe monad+ add_constraints :: Options -> Name -> DType -> [Name] -> DType -> Maybe DType+ -- We must look through `... :: Type` kind annotations, which can be added+ -- when singling type signatures lacking explicit `forall`s.+ -- See Note [Preserve the order of type variables during singling]+ -- (wrinkle 1) in D.S.TH.Single.Type.+ add_constraints opts meth_name (DSigT sty ski) bound_kvs res_ki = do+ sty' <- add_constraints opts meth_name sty bound_kvs res_ki+ 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):@@ -435,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@@ -465,73 +484,31 @@ 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 :: OSet Name -> DType- -> SgM (DType, [Name], DCxt, DKind)- sing_meth_ty bound_kvs inner_ty = do+ 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 bound_kvs (DConT $ defunctionalizedName0 opts name) raw_ty- pure (s_ty, tyvar_names, ctxt, res_ki)-- (s_ty, tyvar_names, ctxt, m_res_ki) <- case OMap.lookup name inst_sigs of- Just inst_sig -> do- -- We have an InstanceSig, so just single that type. Take care to- -- avoid binding the variables bound by the instance head as well.- let inst_bound = foldMap fvDType (cxt ++ inst_kis)- (s_ty, tyvar_names, ctxt, res_ki) <- sing_meth_ty inst_bound inst_sig- pure (s_ty, tyvar_names, ctxt, Just res_ki)- 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)) _) -> do- (sing_tvbs, ctxt, _args, res_ty) <- unravelVanillaDType s_ty- let subst = mk_subst cls_tvbs- m_res_ki = case res_ty of- _sing `DAppT` (_prom_func `DSigT` res_ki) -> Just (substKind subst res_ki)- _ -> Nothing-- pure ( substType subst s_ty- , map extractTvbName sing_tvbs- , map (substType subst) ctxt- , m_res_ki )- _ -> do- mb_info <- dsReify name- case mb_info of- Just (DVarI _ (DForallT (DForallInvis cls_tvbs)- (DConstrainedT _cls_pred inner_ty)) _) -> do- let subst = mk_subst cls_tvbs- cls_kvb_names = foldMap (foldMap fvDType . extractTvbKind) cls_tvbs- cls_tvb_names = OSet.fromList $ map extractTvbName cls_tvbs- cls_bound = cls_kvb_names `OSet.union` cls_tvb_names- (s_ty, tyvar_names, ctxt, res_ki) <- sing_meth_ty cls_bound inner_ty- pure ( substType subst s_ty- , tyvar_names- , ctxt- , Just (substKind subst res_ki) )- _ -> fail $ "Cannot find type of method " ++ show name+ (s_ty, _num_args, _tyvar_names, _ctxt, _arg_kis, _res_ki)+ <- singType (DConT $ promotedValueName opts name Nothing) raw_ty+ pure s_ty - let kind_map = maybe Map.empty (Map.singleton name) m_res_ki- meth' <- singLetDecRHS (Map.singleton name tyvar_names)- (Map.singleton name ctxt)- kind_map name rhs- return $ map DLetDec [DSigD (singledValueName opts name) s_ty, meth']+ -- 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+ -- for the class methods, and hence we aren't+ -- generating any SingI instances. Therefore, we+ -- don't need to include anything in this Map.+ name rhs+ return $ map DLetDec+ $ maybeToList (DSigD (singledValueName opts name) <$> mb_s_ty)+ ++ [meth'] singLetDecEnv :: ALetDecEnv -> SgM a@@ -542,40 +519,36 @@ -- 2. SingI instances for any defunctionalization symbols -- (see Data.Singletons.TH.Single.Defun) -- 3. The result of running the `SgM a` action-singLetDecEnv (LetDecEnv { lde_defns = defns- , lde_types = types- , lde_infix = infix_decls- , lde_proms = proms- , lde_bound_kvs = bound_kvs })+singLetDecEnv (LetDecEnv { lde_defns = defns+ , lde_types = types+ , lde_infix = infix_decls+ , lde_proms = proms }) thing_inside = do let prom_list = OMap.assocs proms- (typeSigs, letBinds, tyvarNames, cxts, res_kis, singIDefunss)- <- unzip6 <$> mapM (uncurry (singTySig defns types bound_kvs)) prom_list- infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs infix_decls- let res_ki_map = Map.fromList [ (name, res_ki) | ((name, _), Just res_ki)- <- zip prom_list res_kis ]+ (typeSigs, letBinds, _tyvarNames, cxts, _res_kis, singIDefunss)+ <- unzip6 <$> mapM (uncurry (singTySig defns types)) prom_list+ infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs $ fmap fst infix_decls bindLets letBinds $ do- let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList tyvarNames)- (Map.fromList cxts)- res_ki_map))+ let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList cxts))) (OMap.assocs defns) thing <- thing_inside return (infix_decls' ++ typeSigs ++ let_decs, concat singIDefunss, thing) singTySig :: OMap Name ALetDecRHS -- definitions -> OMap Name DType -- type signatures- -> OMap Name (OSet Name) -- bound kind variables- -> Name -> DType -- the type is the promoted type, not the type sig!- -> SgM ( DLetDec -- the new type signature- , (Name, DExp) -- the let-bind entry- , (Name, [Name]) -- the scoped tyvar names in the tysig- , (Name, DCxt) -- the context of the type signature- , Maybe DKind -- the result kind in the tysig- , [DDec] -- SingI instances for defun symbols+ -> 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+ , (Name, DCxt) -- the context of the type signature+ , Maybe DKind -- the result kind in the tysig+ , [DDec] -- SingI instances for defun symbols )-singTySig defns types bound_kvs 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@@ -583,38 +556,33 @@ singIDefuns <- singDefuns name VarName [] (map (const Nothing) tyvar_names) Nothing return ( DSigD sName sty- , (name, wrapSingFun num_args prom_ty (DVarE sName))- , (name, tyvar_names)+ , (name, wrapSingFun num_args prom_defun_ty (DVarE sName))+ , tyvar_names , (name, []) , Nothing , singIDefuns ) Just ty -> do- all_bound_kvs <- lookup_bound_kvs (sty, num_args, tyvar_names, ctxt, arg_kis, res_ki)- <- singType all_bound_kvs prom_ty ty+ <- singType prom_ty ty bound_cxt <- askContext 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, tyvar_names)+ , (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 Nothing -> fail "Internal error: promotion known for something not let-bound."- Just (AValue _ n _) -> return n- Just (AFunction _ n _) -> return n-- lookup_bound_kvs :: SgM (OSet Name)- lookup_bound_kvs =- case OMap.lookup name bound_kvs of- Nothing -> fail $ "Internal error: " ++ nameBase name ++ " has no type variable "- ++ "bindings, despite having a type signature"- Just kvs -> pure kvs+ Just (AValue _) -> return 0+ Just (AFunction n _) -> return n -- create a Sing t1 -> Sing t2 -> ... type of a given arity and result type mk_sing_ty :: Int -> SgM (DType, [Name])@@ -629,7 +597,7 @@ [] (map (\nm -> singFamily `DAppT` DVarT nm) arg_names) (sing_w_wildcard `DAppT`- (foldl apply prom_ty (map DVarT arg_names)))+ (foldType prom_ty (map DVarT arg_names))) , arg_names ) {-@@ -675,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 =@@ -727,55 +693,29 @@ above. -} -singLetDecRHS :: Map Name [Name]- -> Map Name DCxt -- the context of the type signature+singLetDecRHS :: Map Name DCxt -- the context of the type signature -- (might not be known)- -> Map Name DKind -- result kind (might not be known) -> Name -> ALetDecRHS -> SgM DLetDec-singLetDecRHS bound_names cxts res_kis name ld_rhs = do+singLetDecRHS cxts name ld_rhs = do opts <- getOptions bindContext (Map.findWithDefault [] name cxts) $ case ld_rhs of- AValue prom num_arrows exp ->+ AValue exp -> DValD (DVarP (singledValueName opts name)) <$>- (wrapUnSingFun num_arrows prom <$> singExp exp (Map.lookup name res_kis))- AFunction prom_fun num_arrows clauses ->- let tyvar_names = case Map.lookup name bound_names of- Nothing -> []- Just ns -> ns- res_ki = Map.lookup name res_kis- in+ singExp exp+ AFunction _num_arrows clauses -> DFunD (singledValueName opts name) <$>- mapM (singClause prom_fun num_arrows tyvar_names res_ki) clauses--singClause :: DType -- the promoted function- -> Int -- the number of arrows in the type. If this is more- -- than the number of patterns, we need to eta-expand- -- with unSingFun.- -> [Name] -- the names of the forall'd vars in the type sig of this- -- function. This list should have at least the length as the- -- number of patterns in the clause- -> Maybe DKind -- result kind, if known- -> ADClause -> SgM DClause-singClause prom_fun num_arrows bound_names res_ki- (ADClause var_proms pats exp) = do-- -- Fix #166:- when (num_arrows - length pats < 0) $- fail $ "Function being promoted to " ++ (pprint (typeToTH prom_fun)) ++- " has too many arguments."+ mapM singClause clauses +singClause :: ADClause -> SgM DClause+singClause (ADClause var_proms pats exp) = do+ opts <- getOptions (sPats, sigPaExpsSigs) <- evalForPair $ mapM (singPat (Map.fromList var_proms)) pats- sBody <- singExp exp res_ki- -- when calling unSingFun, the promoted pats aren't in scope, so we use the- -- bound_names instead- let pattern_bound_names = zipWith const bound_names pats- -- this does eta-expansion. See comment at top of file.- sBody' = wrapUnSingFun (num_arrows - length pats)- (foldl apply prom_fun (map DVarT pattern_bound_names)) sBody- return $ DClause sPats $ mkSigPaCaseE sigPaExpsSigs sBody'+ let lambda_binds = map (\(n,_) -> (n, singledValueName opts n)) var_proms+ 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@@ -788,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@@ -815,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] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~@@ -928,51 +836,25 @@ -- -- And now everything is hunky-dory. -singExp :: ADExp -> Maybe DKind -- the kind of the expression, if known- -> SgM DExp- -- See Note [Why error is so special]-singExp (ADVarE err `ADAppE` arg) _res_ki- | err == errorName = do opts <- getOptions- DAppE (DVarE (singledValueName opts err)) <$>- singExp arg (Just (DConT symbolName))-singExp (ADVarE name) _res_ki = lookupVarE name-singExp (ADConE name) _res_ki = lookupConE name-singExp (ADLitE lit) _res_ki = singLit lit-singExp (ADAppE e1 e2) _res_ki = do- e1' <- singExp e1 Nothing- e2' <- singExp e2 Nothing- -- `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) _res_ki = do- opts <- getOptions- let sNames = map (singledValueName opts) names- exp' <- singExp exp Nothing- -- 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) res_ki =- -- 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 `maybeSigT` res_ki)))- <$> (DCaseE <$> singExp exp Nothing <*> mapM (singMatch res_ki) matches)-singExp (ADLetE env exp) res_ki = do+singExp :: ADExp -> SgM DExp+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+ 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 -- defunctionalization symbols in the first place during promotion.- (let_decs, _, exp') <- singLetDecEnv env $ singExp exp res_ki+ (let_decs, _, exp') <- singLetDecEnv env $ singExp exp pure $ DLetE let_decs exp'-singExp (ADSigE prom_exp exp ty) _ = do- exp' <- singExp exp (Just ty)+singExp (ADSigE prom_exp exp ty) = do+ exp' <- singExp exp pure $ DSigE exp' $ DConT singFamilyName `DAppT` DSigT prom_exp ty -- See Note [DerivedDecl] in Data.Singletons.TH.Syntax@@ -980,10 +862,9 @@ singDerivedEqDecs (DerivedDecl { ded_mb_cxt = mb_ctxt , ded_type = ty , ded_type_tycon = ty_tycon- , ded_decl = DataDecl _ _ cons }) = do+ , ded_decl = DataDecl _ _ _ cons }) = do (scons, _) <- singM [] $ mapM (singCtor ty_tycon) cons mb_sctxt <- mapM (mapM singPred) mb_ctxt- kind <- promoteType ty -- Beware! The user might have specified an instance context like this: -- -- deriving instance Eq a => Eq (T a Int)@@ -992,10 +873,11 @@ -- this for the SDecide instance! The simplest solution is to simply replace -- all occurrences of SEq with SDecide in the context. mb_sctxtDecide <- traverse (traverse sEqToSDecide) mb_sctxt- sDecideInst <- mkDecideInstance mb_sctxtDecide kind cons scons- testInsts <- traverse (mkTestInstance mb_sctxtDecide kind ty_tycon cons)+ sDecideInst <- mkDecideInstance mb_sctxtDecide ty cons scons+ eqInst <- mkEqInstanceForSingleton ty ty_tycon+ testInsts <- traverse (mkTestInstance mb_sctxtDecide ty ty_tycon cons) [TestEquality, TestCoercion]- return (sDecideInst:testInsts)+ return (sDecideInst:eqInst:testInsts) -- Walk a DPred, replacing all occurrences of SEq with SDecide. sEqToSDecide :: OptionsMonad q => DPred -> q DPred@@ -1007,11 +889,18 @@ else n) p -- See Note [DerivedDecl] in Data.Singletons.TH.Syntax+singDerivedOrdDecs :: DerivedOrdDecl -> SgM [DDec]+singDerivedOrdDecs (DerivedDecl { ded_type = ty+ , ded_type_tycon = ty_tycon }) = do+ ord_inst <- mkOrdInstanceForSingleton ty ty_tycon+ pure [ord_inst]++-- See Note [DerivedDecl] in Data.Singletons.TH.Syntax singDerivedShowDecs :: DerivedShowDecl -> SgM [DDec] singDerivedShowDecs (DerivedDecl { ded_mb_cxt = mb_cxt , ded_type = ty , ded_type_tycon = ty_tycon- , ded_decl = DataDecl _ _ cons }) = do+ , ded_decl = DataDecl _ _ _ cons }) = do opts <- getOptions z <- qNewName "z" -- Generate a Show instance for a singleton type, like this:@@ -1023,31 +912,12 @@ show_cxt <- inferConstraintsDef (fmap mkShowSingContext mb_cxt) (DConT showSingName) ty cons+ ki <- promoteType ty let sty_tycon = singledDataTypeName opts ty_tycon show_inst = DStandaloneDerivD Nothing Nothing show_cxt- (DConT showName `DAppT` (DConT sty_tycon `DAppT` DSigT (DVarT z) ty))+ (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--singMatch :: Maybe DKind -- ^ the result kind, if known- -> ADMatch -> SgM DMatch-singMatch res_ki (ADMatch var_proms pat exp) = do- (sPat, sigPaExpsSigs) <- evalForPair $ singPat (Map.fromList var_proms) pat- sExp <- singExp exp res_ki- return $ DMatch sPat $ mkSigPaCaseE sigPaExpsSigs sExp- singLit :: Lit -> SgM DExp singLit (IntegerL n) = do opts <- getOptions@@ -1070,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
@@ -6,9 +6,12 @@ Singletonizes constructors. -} -module Data.Singletons.TH.Single.Data where+module Data.Singletons.TH.Single.Data+ ( singDataD+ , singCtor+ ) where -import Language.Haskell.TH.Desugar+import Language.Haskell.TH.Desugar as Desugar import Language.Haskell.TH.Syntax import Data.Maybe import Data.Singletons.TH.Names@@ -17,7 +20,6 @@ import Data.Singletons.TH.Single.Defun import Data.Singletons.TH.Single.Fixity import Data.Singletons.TH.Single.Monad-import Data.Singletons.TH.Single.Type import Data.Singletons.TH.Syntax import Data.Singletons.TH.Util import Control.Monad@@ -25,12 +27,13 @@ -- We wish to consider the promotion of "Rep" to be * -- not a promoted data constructor. singDataD :: DataDecl -> SgM [DDec]-singDataD (DataDecl name tvbs ctors) = do+singDataD (DataDecl df name tvbs ctors) = do opts <- getOptions- let tvbNames = map extractTvbName tvbs+ let reqTvbNames = map extractTvbName $+ filter (\tvb -> extractTvbFlag tvb == BndrReq) tvbs ctor_names = map extractName ctors rec_sel_names = concatMap extractRecSelNames ctors- k <- promoteType (foldType (DConT name) (map DVarT tvbNames))+ k <- promoteType (foldTypeTvbs (DConT name) tvbs) mb_data_sak <- dsReifyType name ctors' <- mapM (singCtor name) ctors fixityDecs <- singReifiedInfixDecls $ ctor_names ++ rec_sel_names@@ -41,12 +44,12 @@ emptyToSingClause <- mkEmptyToSingClause let singKindInst = DInstanceD Nothing Nothing- (map (singKindConstraint . DVarT) tvbNames)+ (map (singKindConstraint . DVarT) reqTvbNames) (DAppT (DConT singKindClassName) k) [ DTySynInstD $ DTySynEqn Nothing (DConT demoteName `DAppT` k) (foldType (DConT name)- (map (DAppT demote . DVarT) tvbNames))+ (map (DAppT demote . DVarT) reqTvbNames)) , DLetDec $ DFunD fromSingName (fromSingClauses `orIfEmpty` [emptyFromSingClause]) , DLetDec $ DFunD toSingName@@ -67,41 +70,33 @@ mk_data_dec kind = DDataD Data [] singDataName [] (Just kind) ctors' [] - data_decs = case mb_data_sak of- -- No standalone kind signature. Try to figure out the order of kind- -- variables on a best-effort basis.- Nothing ->- let sing_tvbs = changeDTVFlags SpecifiedSpec $- toposortTyVarsOf $ map dTyVarBndrToDType tvbs- kinded_sing_ty = DForallT (DForallInvis sing_tvbs) $- DArrowT `DAppT` k `DAppT` DConT typeKindName in- [mk_data_dec kinded_sing_ty]+ data_decs <- case mb_data_sak of+ -- No standalone kind signature. Try to figure out the order of kind+ -- variables on a best-effort basis.+ Nothing -> do+ let sing_tvbs = changeDTVFlags SpecifiedSpec $+ toposortTyVarsOf $ map dTyVarBndrToDType tvbs+ kinded_sing_ty = DForallT (DForallInvis sing_tvbs) $+ DArrowT `DAppT` k `DAppT` DConT typeKindName+ pure [mk_data_dec kinded_sing_ty] - -- A standalone kind signature is provided, so use that to determine the- -- order of kind variables.- Just data_sak ->- let (args, _) = unravelDType data_sak- vis_args = filterDVisFunArgs args- vis_tvbs = changeDTVFlags SpecifiedSpec $- zipWith replaceTvbKind vis_args tvbs- invis_args = filterInvisTvbArgs args- -- If the standalone kind signature did not explicitly quantify its- -- kind variables, do so ourselves. This is very similar to what- -- D.S.TH.Single.Type.singTypeKVBs does.- invis_tvbs | null invis_args- = changeDTVFlags SpecifiedSpec $- toposortTyVarsOf [data_sak]- | otherwise- = invis_args- sing_data_sak = DForallT (DForallInvis (invis_tvbs ++ vis_tvbs)) $- DArrowT `DAppT` k `DAppT` DConT typeKindName in- [ DKiSigD singDataName sing_data_sak- , mk_data_dec sing_data_sak- ]+ -- A standalone kind signature is provided, so use that to determine the+ -- order of kind variables.+ Just data_sak -> do+ sing_data_sak <- singDataSAK data_sak tvbs k+ pure [ DKiSigD singDataName sing_data_sak+ , mk_data_dec sing_data_sak+ ] return $ data_decs ++ singSynInst :- [singKindInst | genSingKindInsts opts] +++ [ singKindInst | genSingKindInsts opts+ , -- `type data` data constructors only exist at the+ -- type level. As such, we cannot define SingKind+ -- instances for them, as they require term-level+ -- data constructors to implement.+ df /= Desugar.TypeData+ ] ++ fixityDecs where -- in the Rep case, the names of the constructors are in the wrong scope -- (they're types, not datacons), so we have to reinterpret them.@@ -153,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@@ -183,7 +178,19 @@ rty' <- promoteType_NC rty let indices = map DVarT indexNames kindedIndices = zipWith DSigT indices kinds- kvbs = singTypeKVBs con_tvbs kinds [] rty' mempty+ -- The approach we use for singling data constructor types differs+ -- slightly from the approach taken in D.S.TH.Single.Type.singType in that+ -- we always explicitly quantify all type variables in a singled data+ -- constructor, regardless of whether the original data constructor+ -- explicitly quantified them or not. This explains the use of+ -- toposortTyVarsOf below.+ -- See Note [Preserve the order of type variables during singling]+ -- (wrinkle 1) in D.S.TH.Single.Type.+ kvbs | null con_tvbs+ = changeDTVFlags SpecifiedSpec (toposortTyVarsOf (kinds ++ [rty'])) +++ con_tvbs+ | otherwise+ = con_tvbs all_tvbs = kvbs ++ zipWith (`DKindedTV` SpecifiedSpec) indexNames kinds -- @mb_SingI_dec k@ returns 'Just' an instance of @SingI<k>@ if @k@ is@@ -224,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@@ -243,6 +250,44 @@ mk_bang_type :: Bang -> DType -> SgM DBangType mk_bang_type b index = do b' <- mk_bang b pure (b', DAppT singFamily index)++-- @'singDataSAK' sak data_bndrs@ produces a standalone kind signature for a+-- singled data declaration, using the original data type's standalone kind+-- signature (@sak@) and its user-written binders (@data_bndrs@) as a template.+-- For this example:+--+-- @+-- type D :: forall j k. k -> j -> Type+-- data D @j @l (a :: l) b = ...+-- @+--+-- We would produce the following standalone kind signature:+--+-- @+-- type SD :: forall j l (a :: l) (b :: j). D @j @l (a :: l) b -> Type+-- @+--+-- 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.+--+-- See also the Haddocks for 'dMatchUpSAKWithDecl' function, which also apply+-- here.+singDataSAK ::+ MonadFail q+ => DKind+ -- ^ The standalone kind signature for the original data type+ -> [DTyVarBndrVis]+ -- ^ The user-written binders for the original data type+ -> DKind+ -- ^ The original data type, promoted to a kind+ -> q DKind+ -- ^ The standalone kind signature for the singled data type+singDataSAK data_sak data_bndrs data_k = do+ 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 {- Note [singletons-th and record selectors]
src/Data/Singletons/TH/Single/Decide.hs view
@@ -14,41 +14,66 @@ import Data.Singletons.TH.Deriving.Infer import Data.Singletons.TH.Names import Data.Singletons.TH.Options+import Data.Singletons.TH.Promote.Type import Data.Singletons.TH.Util import Control.Monad -- Make an instance of SDecide.-mkDecideInstance :: DsMonad q => Maybe DCxt -> DKind+mkDecideInstance :: OptionsMonad q => Maybe DCxt -> DType -> [DCon] -- ^ The /original/ constructors (for inferring the instance context) -> [DCon] -- ^ The /singletons/ constructors -> q DDec-mkDecideInstance mb_ctxt k ctors sctors = do+mkDecideInstance mb_ctxt data_ty ctors sctors = do let sctorPairs = [ (sc1, sc2) | sc1 <- sctors, sc2 <- sctors ] methClauses <- if null sctors then (:[]) <$> mkEmptyDecideMethClause else mapM mkDecideMethClause sctorPairs- constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) k ctors+ constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) data_ty ctors+ data_ki <- promoteType data_ty return $ DInstanceD Nothing Nothing constraints- (DAppT (DConT sDecideClassName) k)+ (DAppT (DConT sDecideClassName) data_ki) [DLetDec $ DFunD sDecideMethName methClauses] +-- Make a boilerplate Eq instance for a singleton type, e.g.,+--+-- @+-- instance Eq (SExample (z :: Example a)) where+-- _ == _ = True+-- @+mkEqInstanceForSingleton :: OptionsMonad q+ => DType+ -> Name+ -- ^ The name of the data type+ -> q DDec+mkEqInstanceForSingleton data_ty data_name = do+ opts <- getOptions+ z <- qNewName "z"+ data_ki <- promoteType data_ty+ let sdata_name = singledDataTypeName opts data_name+ pure $ DInstanceD Nothing Nothing []+ (DAppT (DConT eqName) (DConT sdata_name `DAppT` DSigT (DVarT z) data_ki))+ [DLetDec $+ DFunD equalsName+ [DClause [DWildP, DWildP] (DConE trueName)]]+ data TestInstance = TestEquality | TestCoercion -- Make an instance of TestEquality or TestCoercion by leveraging SDecide.-mkTestInstance :: OptionsMonad q => Maybe DCxt -> DKind+mkTestInstance :: OptionsMonad q => Maybe DCxt -> DType -> Name -- ^ The name of the data type -> [DCon] -- ^ The /original/ constructors (for inferring the instance context) -> TestInstance -> q DDec-mkTestInstance mb_ctxt k data_name ctors ti = do+mkTestInstance mb_ctxt data_ty data_name ctors ti = do opts <- getOptions- constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) k ctors+ constraints <- inferConstraintsDef mb_ctxt (DConT sDecideClassName) data_ty ctors+ data_ki <- promoteType data_ty pure $ DInstanceD Nothing Nothing constraints (DAppT (DConT tiClassName) (DConT (singledDataTypeName opts data_name)- `DSigT` (DArrowT `DAppT` k `DAppT` DConT typeKindName)))+ `DSigT` (DArrowT `DAppT` data_ki `DAppT` DConT typeKindName))) [DLetDec $ DFunD tiMethName [DClause [] (DVarE tiDefaultName)]] where@@ -71,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@@ -106,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/Defun.hs view
@@ -14,7 +14,6 @@ module Data.Singletons.TH.Single.Defun (singDefuns) where import Control.Monad-import Data.Foldable import Data.Singletons.TH.Names import Data.Singletons.TH.Options import Data.Singletons.TH.Promote.Defun
src/Data/Singletons/TH/Single/Fixity.hs view
@@ -6,31 +6,39 @@ import Data.Singletons.TH.Options import Data.Singletons.TH.Util import Language.Haskell.TH.Desugar+import qualified GHC.LanguageExtensions.Type as LangExt -- Single a fixity declaration. singInfixDecl :: forall q. OptionsMonad q => Name -> Fixity -> q (Maybe DLetDec) singInfixDecl name fixity = do- opts <- getOptions+ opts <- getOptions+ fld_sels <- qIsExtEnabled LangExt.FieldSelectors mb_ns <- reifyNameSpace name 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- Just DataName -> finish $ singledDataConName opts name- Just TcClsName -> do+ Nothing -> finish DataNamespaceSpecifier $ singledValueName opts name+ Just VarName -> finish DataNamespaceSpecifier $ singledValueName opts name+ Just (FldName _)+ | fld_sels -> finish DataNamespaceSpecifier $ singledValueName opts name+ | otherwise -> never_mind+ 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- _ -> pure Nothing+ -> 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+ finish :: NamespaceSpecifier -> Name -> q (Maybe DLetDec)+ finish ns n = pure $ Just $ DInfixD fixity ns n + never_mind :: q (Maybe DLetDec)+ never_mind = pure Nothing+ -- Try producing singled fixity declarations for Names by reifying them -- /without/ consulting quoted declarations. If reification fails, recover and -- return the empty list.@@ -60,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` ... -----@@ -86,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 ###@@ -104,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/Monad.hs view
@@ -11,8 +11,9 @@ -} module Data.Singletons.TH.Single.Monad (- SgM, bindLets, bindContext, askContext, lookupVarE, lookupConE,- wrapSingFun, wrapUnSingFun,+ SgM, bindLambdas, bindLets, bindContext,+ askContext, lookupVarE, lookupConE,+ wrapSingFun, singM, singDecsM, emitDecs, emitDecsM ) where@@ -26,21 +27,26 @@ import Data.Singletons.TH.Util import Language.Haskell.TH.Syntax hiding ( lift ) import Language.Haskell.TH.Desugar-import Control.Monad.Reader-import Control.Monad.Writer+import Control.Monad ( liftM2 )+import Control.Monad.IO.Class ( MonadIO )+import Control.Monad.Reader ( MonadReader(..), ReaderT(..), asks )+import Control.Monad.Writer ( MonadWriter, WriterT(..) ) import Control.Applicative -- environment during singling data SgEnv = SgEnv { sg_options :: Options- , sg_let_binds :: Map Name DExp -- from the *original* name+ , sg_local_vars :: Map Name DExp+ -- ^ Map from term-level 'Name's of local variables to their+ -- singled counterparts. See @Note [Tracking local variables]@ in+ -- "Data.Singletons.TH.Promote.Monad". , sg_context :: DCxt -- See Note [Tracking the current type signature context] , sg_local_decls :: [Dec] } emptySgEnv :: SgEnv emptySgEnv = SgEnv { sg_options = defaultOptions- , sg_let_binds = Map.empty+ , sg_local_vars = Map.empty , sg_context = [] , sg_local_decls = [] }@@ -57,10 +63,24 @@ instance OptionsMonad SgM where getOptions = asks sg_options +-- ^ Bring a list of lambda-bound names into scope for the duration the supplied+-- computation, where the first element of each pair is the original, term-level+-- name, and the second element of each pair is the singled counterpart.+-- See @Note [Tracking local variables]@ in "Data.Singletons.TH.Promote.Monad".+bindLambdas :: [(Name, Name)] -> SgM a -> SgM a+bindLambdas lambdas = local add_binds+ where add_binds env@(SgEnv { sg_local_vars = locals }) =+ let new_locals = Map.fromList [ (tmN, DVarE tyN) | (tmN, tyN) <- lambdas ] in+ env { sg_local_vars = new_locals `Map.union` locals }++-- ^ Bring a list of let-bound names into scope for the duration the supplied+-- computation, where the first element of each pair is the original, term-level+-- name, and the second element of each pair is the singled counterpart.+-- See @Note [Tracking local variables]@ in "Data.Singletons.TH.Promote.Monad". bindLets :: [(Name, DExp)] -> SgM a -> SgM a-bindLets lets1 =- local (\env@(SgEnv { sg_let_binds = lets2 }) ->- env { sg_let_binds = (Map.fromList lets1) `Map.union` lets2 })+bindLets lets =+ local (\env@(SgEnv { sg_local_vars = locals }) ->+ env { sg_local_vars = Map.fromList lets `Map.union` locals }) -- Add some constraints to the current type signature context. -- See Note [Tracking the current type signature context]@@ -74,12 +94,16 @@ askContext :: SgM DCxt askContext = asks sg_context +-- | Map a term-level 'Name' to its singled counterpart. This function is aware+-- of any local variables that are currently in scope.+-- See @Note [Tracking local variables]@ in "Data.Singletons.TH.Promote.Monad". lookupVarE :: Name -> SgM DExp lookupVarE name = do opts <- getOptions lookup_var_con (singledValueName opts) (DVarE . singledValueName opts) name +-- | Map a data constructor name to its singled counterpart. lookupConE :: Name -> SgM DExp lookupConE name = do opts <- getOptions@@ -89,9 +113,9 @@ lookup_var_con :: (Name -> Name) -> (Name -> DExp) -> Name -> SgM DExp lookup_var_con mk_sing_name mk_exp name = do opts <- getOptions- letExpansions <- asks sg_let_binds+ localExpansions <- asks sg_local_vars sName <- mkDataName (nameBase (mk_sing_name name)) -- we want *term* names!- case Map.lookup name letExpansions of+ case Map.lookup name localExpansions of Nothing -> do -- try to get it from the global context m_dinfo <- liftM2 (<|>) (dsReify sName) (dsReify name)@@ -119,21 +143,6 @@ in (wrap_fun `DAppTypeE` ty `DAppE`) -wrapUnSingFun :: Int -> DType -> DExp -> DExp-wrapUnSingFun 0 _ = id-wrapUnSingFun n ty =- let unwrap_fun = DVarE $ case n of- 1 -> 'unSingFun1- 2 -> 'unSingFun2- 3 -> 'unSingFun3- 4 -> 'unSingFun4- 5 -> 'unSingFun5- 6 -> 'unSingFun6- 7 -> 'unSingFun7- _ -> error "No support for functions of arity > 7."- in- (unwrap_fun `DAppTypeE` ty `DAppE`)- singM :: OptionsMonad q => [Dec] -> SgM a -> q (a, [DDec]) singM locals (SgM rdr) = do opts <- getOptions@@ -151,7 +160,8 @@ {- Note [Tracking the current type signature context] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-Much like we track the let-bound names in scope, we also track the current+Much like we track the locally-bound names in scope (see Note [Tracking local+variables] in Data.Singletons.TH.Promote.Monad), we also track the current context. For instance, in the following program: -- (1)
+ src/Data/Singletons/TH/Single/Ord.hs view
@@ -0,0 +1,43 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.TH.Single.Ord+-- Copyright : (C) 2023 Ryan Scott+-- License : BSD-style (see LICENSE)+-- Maintainer : Ryan Scott+-- Stability : experimental+-- Portability : non-portable+--+-- Defines a function to generate boilerplate Ord instances for singleton+-- types.+--+-----------------------------------------------------------------------------++module Data.Singletons.TH.Single.Ord (mkOrdInstanceForSingleton) where++import Language.Haskell.TH.Syntax+import Language.Haskell.TH.Desugar+import Data.Singletons.TH.Names+import Data.Singletons.TH.Options+import Data.Singletons.TH.Promote.Type++-- Make a boilerplate Ord instance for a singleton type, e.g.,+--+-- @+-- instance Ord (SExample (z :: Example a)) where+-- compare _ _ = EQ+-- @+mkOrdInstanceForSingleton :: OptionsMonad q+ => DType+ -> Name+ -- ^ The name of the data type+ -> q DDec+mkOrdInstanceForSingleton data_ty data_name = do+ opts <- getOptions+ z <- qNewName "z"+ data_ki <- promoteType data_ty+ let sdata_name = singledDataTypeName opts data_name+ pure $ DInstanceD Nothing Nothing []+ (DAppT (DConT ordName) (DConT sdata_name `DAppT` DSigT (DVarT z) data_ki))+ [DLetDec $+ DFunD compareName+ [DClause [DWildP, DWildP] (DConE cmpEQName)]]
src/Data/Singletons/TH/Single/Type.hs view
@@ -9,7 +9,6 @@ module Data.Singletons.TH.Single.Type where import Language.Haskell.TH.Desugar-import Language.Haskell.TH.Desugar.OSet (OSet) import Language.Haskell.TH.Syntax import Data.Singletons.TH.Names import Data.Singletons.TH.Options@@ -17,14 +16,8 @@ import Data.Singletons.TH.Single.Monad import Data.Singletons.TH.Util import Control.Monad-import Data.Foldable-import Data.Function-import Data.List (deleteFirstsBy) -singType :: OSet Name -- the set of bound kind variables in this scope- -- see Note [Explicitly binding kind variables]- -- in Data.Singletons.TH.Promote.Monad- -> DType -- the promoted version of the thing classified by...+singType :: DType -- the promoted version of the thing classified by... -> DType -- ... this type -> SgM ( DType -- the singletonized type , Int -- the number of arguments@@ -32,7 +25,7 @@ , DCxt -- the context of the singletonized type , [DKind] -- the kinds of the argument types , DKind ) -- the kind of the result type-singType bound_kvs prom ty = do+singType prom ty = do (orig_tvbs, cxt, args, res) <- unravelVanillaDType ty let num_args = length args cxt' <- mapM singPred_NC cxt@@ -40,43 +33,23 @@ prom_args <- mapM promoteType_NC args prom_res <- promoteType_NC res let args' = map (\n -> singFamily `DAppT` (DVarT n)) arg_names- res' = singFamily `DAppT` (foldl apply 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.- kvbs = singTypeKVBs orig_tvbs prom_args cxt' prom_res bound_kvs- all_tvbs = kvbs ++ zipWith (`DKindedTV` SpecifiedSpec) arg_names prom_args- ty' = ravelVanillaDType all_tvbs cxt' args' res'+ -- 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+ -- a `<singled-ty> :: Type` kind annotation and let GHC implicitly+ -- quantify any type variables that are free in `<singled-ty>`.+ -- See Note [Preserve the order of type variables during singling],+ -- wrinkle 1.+ ty' | null orig_tvbs+ = ravelVanillaDType arg_tvbs cxt' args' res' `DSigT` DConT typeKindName+ | otherwise+ = ravelVanillaDType (orig_tvbs ++ arg_tvbs) cxt' args' res' return (ty', num_args, arg_names, cxt, prom_args, prom_res) --- Compute the kind variable binders to use in the singled version of a type--- signature. This has two main call sites: singType and D.S.TH.Single.Data.singCtor.------ This implements the advice documented in--- Note [Preserve the order of type variables during singling], wrinkle 1.-singTypeKVBs ::- [DTyVarBndrSpec] -- ^ The bound type variables from the original type signature.- -> [DType] -- ^ The argument types of the signature (promoted).- -> DCxt -- ^ The context of the signature (singled).- -> DType -- ^ The result type of the signature (promoted).- -> OSet Name -- ^ The type variables previously bound in the current scope.- -> [DTyVarBndrSpec] -- ^ The kind variables for the singled type signature.-singTypeKVBs orig_tvbs prom_args sing_ctxt prom_res bound_tvbs- | null orig_tvbs- -- There are no explicitly `forall`ed type variable binders, so we must- -- infer them ourselves.- = changeDTVFlags SpecifiedSpec $- deleteFirstsBy- ((==) `on` extractTvbName)- (toposortTyVarsOf $ prom_args ++ sing_ctxt ++ [prom_res])- (map (`DPlainTV` ()) $ toList bound_tvbs)- -- Make sure to subtract out the bound variables currently in scope,- -- lest we accidentally shadow them in this type signature.- -- See Note [Explicitly binding kind variables] in D.S.TH.Promote.Monad.- | otherwise- -- There is an explicit `forall`, so this case is easy.- = orig_tvbs- -- Single a DPred, checking that it is a vanilla type in the process. -- See [Vanilla-type validity checking during promotion] -- in Data.Singletons.TH.Promote.Type.@@ -151,85 +124,87 @@ absurd v = case v of {} This time, the order of type variables vis-à-vis TypeApplications is determined-by their left-to-right order of appearance in the type signature. It's tempting-to think that since there is no explicit `forall` in the original type-signature, we could get away without an explicit `forall` in the singled type-signature. That is, one could write:+by their left-to-right order of appearance in the type signature. This order+dictates that `a` is quantified before `b`, so we must mirror this order in the+singled type signature. - sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b)+One way to accomplish this would be to compute the order in which the type+variables appear and then explicitly quantify them. In the `absurd` example+above, this would be tantamount to writing: -This would have the right type variable order, but unfortunately, this approach-does not play well with singletons-th's style of code generation. Consider the code-that would be generated for the body of sAbsurd:+ sAbsurd :: forall a b (v :: V a). Sing v -> Sing (Absurd v :: b)+ ^^^+ |||+ Explicitly quantified by singletons-th,+ not in the original type signature - sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b)- sAbsurd (sV :: Sing v) = id @(Case v v :: b) (case sV of {})+This is possible to do, and indeed, singletons-th used to do this. However, it+is a bit tiresome to implement. In order to know which type variables to+quantify, you must keep track of which type variables have been brought into+scope at all times. For the historical details on how this worked, see this+now-removed Note describing the old implementation:+https://github.com/goldfirere/singletons/blob/10ef27880d7ecc16241824c504ca83e2bb6ca787/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs#L135-L192 -Note the use of the type `Case v v :: b` in the right-hand side of sAbsurd.-However, because `b` was not bound by a top-level `forall`, it won't be in-scope here, resulting in an error!+A much more straightforward approach, which singletons-th currently uses, is to+let GHC do the hard work of implicitly quantifying the type variables. That is,+we will single `absurd` to something like this: -(Why do we generate the code `id @(Case v v :: b)` in the first place? See-Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization]-in D.S.TH.Single.)+ sAbsurd :: () => forall (v :: V a). Sing v -> Sing (Absurd v :: b) -The simplest approach is to just always generate singled type signatures with-explicit `forall`s. In the event that the original type signature lacks an-explicit `forall`, we infer the correct type variable ordering ourselves and-synthesize a `forall` with that order. The `singTypeKVBs` function implements-this logic.+This works because just like in the original type signature, `a` and `b` are+implicitly quantified, and more importantly, they are quantified in exactly the+same order as in the original type signature. --------- Wrinkle 2: The TH reification swamp------+Why do we need the `() => ...` part? If we had instead written the type+signature like this: -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:+ sAbsurd :: forall (v :: V a). Sing v -> Sing (Absurd v :: b) - {-# LANGUAGE PolyKinds, ... #-}- $(singletons [d|- data Proxy a = MkProxy- |])+Then GHC would reject `a` and `b` for being out of scope. This is because of+GHC's "forall-or-nothing" rule: if a type signature has an outermost forall,+then all type variable occurrences in the type signature must have explicit+binding sites. Using `() => forall (v :: V a). ...` prevents the `forall` from+being an outermost `forall`, which bypasses the forall-or-nothing rule. -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:+Some further complications: - MkProxy :: forall a. Proxy a+* Template Haskell doesn't actually allow you to splice in types of the form+ `() => ...` in practice.+ See https://gitlab.haskell.org/ghc/ghc/-/issues/16396. Luckily, this isn't a+ deal-breaker, as we can also avoid the forall-or-nothing rule by annotating+ the type signature with an explicit `... :: Type` annotation: -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:+ sAbsurd :: ((forall (v :: V a). Sing v -> Sing (Absurd v :: b)) :: Type) - DataD- [] ''Proxy [KindedTV a () (VarT k)] Nothing- [NormalC 'MkProxy []]- []+ This is the approach that singletons-th actually uses. Note that there is one+ spot in the code (in D.S.TH.Single.singInstD) that must be taught to look+ through these `... :: Type` annotations, but this approach is otherwise fairly+ non-invasive. -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:+* We cannot use this trick when singling the types of data constructors. That+ is, we cannot single this: - MkProxy :: forall k (a :: k). Proxy a+ data T a where+ MkT :: a -> T 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!+ To this: -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.+ data ST z where+ SMkT :: ((forall (x :: a). Sing x -> ST (MkT x)) :: Type) + This is because GADT syntax does not currently permit nested `forall`s of this+ sort. (It might permit them in the future if+ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst+ is implemented, but not currently.) As a result, we /always/ explicitly+ quantify all type variables in a data constructor's type, regardless of+ whether the original type implicitly quantified them or not. In the example+ above, that means that the singled version would be:++ data ST z where+ SMkT :: forall a (x :: a). Sing x -> ST (MkT x)+ -------- 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@@ -280,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,16 +22,19 @@ 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 [Explicitly binding kind variables] in- -- Data.Singletons.TH.Promote.Monad.+ -- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad. } instance Semigroup PromDPatInfos where@@ -46,10 +51,10 @@ type SingDSigPaInfos = [(DExp, DType)] -- The parts of data declarations that are relevant to singletons-th.-data DataDecl = DataDecl Name [DTyVarBndrUnit] [DCon]+data DataDecl = DataDecl DataFlavor Name [DTyVarBndrVis] [DCon] -- The parts of type synonyms that are relevant to singletons-th.-data TySynDecl = TySynDecl Name [DTyVarBndrUnit] DType+data TySynDecl = TySynDecl Name [DTyVarBndrVis] DType -- The parts of open type families that are relevant to singletons-th. type OpenTypeFamilyDecl = TypeFamilyDecl 'Open@@ -66,7 +71,7 @@ data ClassDecl ann = ClassDecl { cd_cxt :: DCxt , cd_name :: Name- , cd_tvbs :: [DTyVarBndrUnit]+ , cd_tvbs :: [DTyVarBndrVis] , cd_fds :: [FunDep] , cd_lde :: LetDecEnv ann , cd_atfs :: [OpenTypeFamilyDecl]@@ -102,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@@ -122,7 +132,6 @@ ADPat DType | ADWildP -data ADMatch = ADMatch VarPromotions ADPat ADExp data ADClause = ADClause VarPromotions [ADPat] ADExp @@ -138,37 +147,56 @@ data family LetDecRHS :: AnnotationFlag -> Type data instance LetDecRHS Annotated- = AFunction DType -- promote function (unapplied)- Int -- number of arrows in type- [ADClause]- | AValue DType -- promoted exp- Int -- number of arrows in type- ADExp+ = -- A function definition. Invariant: each ADClause contains at least one+ -- pattern.+ AFunction+ Int -- The number of arrows in the type. As a consequence of the invariant+ -- above, this is always a positive number.+ [ADClause]++ | -- A value whose definition is given by the DExp. Invariant: the value is+ -- not a function (i.e., there are no occurrences of (->) in the value's+ -- type).+ AValue+ ADExp data instance LetDecRHS Unannotated = UFunction [DClause] | UValue DExp 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_bound_kvs :: IfAnn ann (OMap Name (OSet Name)) ()- -- The set of bound variables in scope.- -- See Note [Explicitly binding kind variables]- -- in Data.Singletons.TH.Promote.Monad.+ , 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 instance Semigroup ULetDecEnv where- LetDecEnv defns1 types1 infx1 _ _ <> LetDecEnv defns2 types2 infx2 _ _ =- LetDecEnv (defns1 <> defns2) (types1 <> types2) (infx1 <> infx2) () ()+ LetDecEnv defns1 types1 infx1 _ <> LetDecEnv defns2 types2 infx2 _ =+ LetDecEnv (defns1 <> defns2) (types1 <> types2) (infx1 <> infx2) () instance Monoid ULetDecEnv where- mempty = LetDecEnv OMap.empty OMap.empty OMap.empty () ()+ mempty = LetDecEnv OMap.empty OMap.empty OMap.empty () valueBinding :: Name -> ULetDecRHS -> ULetDecEnv valueBinding n v = emptyLetDecEnv { lde_defns = OMap.singleton n v }@@ -176,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@@ -195,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]@@ -208,6 +236,7 @@ } type DerivedEqDecl = DerivedDecl Eq+type DerivedOrdDecl = DerivedDecl Ord type DerivedShowDecl = DerivedDecl Show {- Note [DerivedDecl]@@ -228,13 +257,14 @@ Why are these instances handled outside of partitionDecs? * Deriving Eq in singletons-th not only derives PEq/SEq instances, but it also- derives SDecide, TestEquality, and TestCoercion instances.- Data.Singletons.TH.Single (depending on the task at hand).+ derives SDecide, Eq, TestEquality, and TestCoercion instances.+* Deriving Ord in singletons-th not only derives POrd/SOrd instances, but it also+ derives Ord instances for the singleton types themselves. * Deriving Show in singletons-th not only derives PShow/SShow instances, but it- also derives Show instances for singletons-th types.+ also derives Show instances for the singleton types themselves. To make this work, we let partitionDecs handle the P{Eq,Show} and S{Eq,Show} instances, but we also stick the relevant info into a DerivedDecl value for later use in Data.Singletons.TH.Single, where we additionally generate-SDecide, TestEquality, TestCoercion and Show instances for singleton types.+SDecide, Eq, TestEquality, TestCoercion and Show instances for singleton types. -}
+ 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,20 +13,24 @@ 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 hiding ( mapM )-import Control.Monad.Except hiding ( mapM )-import Control.Monad.Reader hiding ( mapM )-import Control.Monad.Writer hiding ( mapM )+import Control.Monad ( liftM, unless, when )+import Control.Monad.Except ( ExceptT, runExceptT, MonadError(..) )+import Control.Monad.IO.Class ( MonadIO )+import Control.Monad.Reader ( MonadReader(..), Reader, ReaderT(..) )+import Control.Monad.Trans ( MonadTrans )+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@@ -84,7 +86,7 @@ -- | Is an identifier a legal data constructor name in Haskell? That is, is its -- first character an uppercase letter (prefix) or a colon (infix)? isDataConName :: Name -> Bool-isDataConName n = let first = head (nameBase n) in isUpper first || first == ':'+isDataConName n = let first = headNameStr (nameBase n) in isUpper first || first == ':' -- | Is an identifier uppercase? --@@ -93,7 +95,7 @@ -- If you want to check if a name is legal as a data constructor, use the -- 'isDataConName' function. isUpcase :: Name -> Bool-isUpcase n = let first = head (nameBase n) in isUpper first+isUpcase n = let first = headNameStr (nameBase n) in isUpper first -- Make an identifier uppercase. If the identifier is infix, this acts as the -- identity function.@@ -112,9 +114,9 @@ where str = nameBase n- first = head str+ first = headNameStr str - upcase_alpha = alpha ++ (toUpper first) : tail str+ upcase_alpha = alpha ++ (toUpper first) : tailNameStr str upcase_symb = symb ++ str noPrefix :: (String, String)@@ -136,7 +138,7 @@ prefixName :: String -> String -> Name -> Name prefixName pre tyPre n = let str = nameBase n- first = head str in+ first = headNameStr str in if isHsLetter first then mkName (pre ++ str) else mkName (tyPre ++ str)@@ -146,11 +148,27 @@ suffixName :: String -> String -> Name -> Name suffixName ident symb n = let str = nameBase n- first = head str in+ first = headNameStr str in if isHsLetter first then mkName (str ++ ident) else mkName (str ++ symb) +-- Return the first character in a Name's string (i.e., nameBase).+-- Precondition: the string is non-empty.+headNameStr :: String -> Char+headNameStr str =+ case str of+ (c:_) -> c+ [] -> error "headNameStr: Expected non-empty string"++-- Drop the first character in a Name's string (i.e., nameBase).+-- Precondition: the string is non-empty.+tailNameStr :: String -> String+tailNameStr str =+ case str of+ (_:cs) -> cs+ [] -> error "tailNameStr: Expected non-empty string"+ -- convert a number into both alphanumeric and symoblic forms uniquePrefixes :: String -- alphanumeric prefix -> String -- symbolic prefix@@ -186,6 +204,11 @@ extractTvbName (DPlainTV n _) = n extractTvbName (DKindedTV n _ _) = n +-- extract the flag from a TyVarBndr.+extractTvbFlag :: DTyVarBndr flag -> flag+extractTvbFlag (DPlainTV _ f) = f+extractTvbFlag (DKindedTV _ f _) = f+ tvbToType :: DTyVarBndr flag -> DType tvbToType = DVarT . extractTvbName @@ -217,6 +240,38 @@ maybeSigT ty Nothing = ty maybeSigT ty (Just ki) = ty `DSigT` ki +-- | Convert a list of 'DTyVarBndrSpec's to a list of 'DTyVarBndrVis'es. Type+-- variable binders with a 'SpecifiedSpec' are converted to 'BndrInvis', and+-- type variable binders with an 'InferredSpec' are dropped entirely.+--+-- As an example, if you have this list of 'DTyVarBndrSpec's:+--+-- @+-- forall a {b} c {d e} f. <...>+-- @+--+-- The corresponding list of 'DTyVarBndrVis'es would be:+--+-- @+-- \@a \@b \@f+-- @+--+-- Note that note of @b@, @d@, or @e@ appear in the list.+--+-- 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+ specificityToBndrVis InferredSpec = Nothing+ -- Reconstruct a vanilla function type from its individual type variable -- binders, constraints, argument types, and result type. (See -- Note [Vanilla-type validity checking during promotion] in@@ -361,20 +416,19 @@ DForallVis _ -> res DForallInvis tvbs' -> tvbs' ++ res --- Infer the kind of a DTyVarBndr by using information from a DVisFunArg.-replaceTvbKind :: DVisFunArg -> DTyVarBndrUnit -> DTyVarBndrUnit-replaceTvbKind (DVisFADep tvb) _ = tvb-replaceTvbKind (DVisFAAnon k) tvb = DKindedTV (extractTvbName tvb) () k---- changes all TyVars not to be NameU's. Workaround for GHC#11812/#17537/#19743+-- Change all unique Names with a NameU or NameL namespace to non-unique Names+-- by performing a syb-based traversal. See Note [Pitfalls of NameU/NameL] for+-- why this is useful. noExactTyVars :: Data a => a -> a noExactTyVars = everywhere go where go :: Data a => a -> a go = mkT (fix_tvb @Specificity) `extT` fix_tvb @()+ `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@@ -386,48 +440,103 @@ fix_inj_ann (InjectivityAnn lhs rhs) = InjectivityAnn (noExactName lhs) (map noExactName rhs) --- changes a Name not to be a NameU. Workaround for GHC#11812/#17537/#19743+ 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-noExactName (Name (OccName occ) (NameU unique)) = mkName (occ ++ show unique)-noExactName n = n+noExactName n@(Name (OccName occ) ns) =+ case ns of+ NameU unique -> mk_name unique+ NameL unique -> mk_name unique+ _ -> n+ where+ mk_name unique = mkName (occ ++ show unique) -substKind :: Map Name DKind -> DKind -> DKind-substKind = substType+{-+Note [Pitfalls of NameU/NameL]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+Most of the Names used in singletons-th come from reified or quoted Template+Haskell definitions. Because these definitions have passed through GHC's+renamer, they have unique Names with unique a NameU/NameL namespace. For the+sake of convenience, we often reuse these Names in the definitions that we+generate. For example, if singletons-th is given a declaration+`f :: forall a_123. a_123 -> a_123`, it will produce a standalone kind signature+`type F :: forall a_123. a_123 -> a_123`, reusing the unique Name `a_123`. --- | 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+While reusing unique Names is convenient, it does have a downside. In+particular, GHC can sometimes get confused when the same unique Name is reused+in distinct type variable scopes. In the best case, this can lead to confusing+type errors, but in the worst case, it can cause GHC to panic, as seen in the+following issues (all of which were first observed in singletons-th): -subst_tele :: Map Name DKind -> DForallTelescope -> (Map Name DKind, DForallTelescope)-subst_tele s (DForallInvis tvbs) = second DForallInvis $ subst_tvbs s tvbs-subst_tele s (DForallVis tvbs) = second DForallVis $ subst_tvbs s tvbs+* https://gitlab.haskell.org/ghc/ghc/-/issues/11812+* https://gitlab.haskell.org/ghc/ghc/-/issues/17537+* https://gitlab.haskell.org/ghc/ghc/-/issues/19743 -subst_tvbs :: Map Name DKind -> [DTyVarBndr flag] -> (Map Name DKind, [DTyVarBndr flag])-subst_tvbs = mapAccumL subst_tvb+This is pretty terrible. Arguably, we are abusing Template Haskell here, since+GHC likely assumes the invariant that each unique Name only has a single+binding site. On the other hand, rearchitecting singletons-th to uphold this+invariant would require a substantial amount of work. -subst_tvb :: Map Name DKind -> DTyVarBndr flag -> (Map Name DKind, DTyVarBndr flag)-subst_tvb s tvb@(DPlainTV n _) = (Map.delete n s, tvb)-subst_tvb s (DKindedTV n f k) = (Map.delete n s, DKindedTV n f (substKind s k))+A far easier solution is to identify any problematic areas where unique Names+are reused and work around the issue by changing unique Names to non-unique+Names. The issues above all have a common theme: they arise when unique Names+are reused in the type variable binders of a data type or type family+declaration. For instance, when promoting a function like this: + f :: forall a_123. a_123 -> a_123+ f x_456 = g+ where+ g = x_456++We must promote `f` and `g` to something like this:++ type F :: forall a_123. a_123 -> a_123+ type family F (arg :: a_123) :: a_123 where+ F x_456 = G x_456++ type family LetG x_456 where+ LetG x_456 = x_456++This looks sensible enough. But note that we are reusing the same unique Name+`x_456` in three different scopes: once in the equation for `F`, once in the+the equation for `G`, and once more in the type variable binder in+`type family LetG x_456`. The last of these scopes in particular is enough to+confuse GHC in some situations and trigger GHC#11812.++Our workaround is to apply the `noExactName` function to such names, which+converts any Names with NameU/NameL namespaces into non-unique Names with+longer OccNames. For instance, `noExactName x_456` will return a non-unique+Name with the OccName `x456`. We use `noExactName` when generating `LetG` so+that it will instead be:++ type family LetG x456 where+ LetG x_456 = x_456++Here, `x456` is a non-unique Name, and `x_456` is a Unique name. Thankfully,+this is sufficient to work around GHC#11812. There is still some amount of+risk, since we are reusing `x_456` in two different type family equations (one+for `LetG` and one for `F`), but GHC accepts this for now. We prefer to use the+`noExactName` in as few places as possible, as using longer OccNames makes the+Haddocks harder to read, so we will continue to reuse unique Names unless GHC+forces us to behave differently.++In addition to the type family example above, we also make use of `noExactName`+(as well as its cousin, `noExactTyVars`) when generating defunctionalization+symbols, as these also require reusing Unique names in several type family and+data type declarations. See references to this Note in the code for particular+locations where we must apply this workaround.+-}++substFamilyResultSig :: Map Name DKind -> DFamilyResultSig -> (Map Name DKind, DFamilyResultSig)+substFamilyResultSig s frs@DNoSig = (s, frs)+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 dropTvbKind tvb@(DPlainTV {}) = tvb dropTvbKind (DKindedTV n f _) = DPlainTV n f@@ -437,12 +546,15 @@ foldType = foldl DAppT -- apply a type to a list of type variable binders-foldTypeTvbs :: DType -> [DTyVarBndr flag] -> DType-foldTypeTvbs ty = foldType ty . map tvbToType+foldTypeTvbs :: DType -> [DTyVarBndrVis] -> DType+foldTypeTvbs ty = applyDType ty . map dTyVarBndrVisToDTypeArg -- Construct a data type's variable binders, possibly using fresh variables--- from the data type's kind signature.-buildDataDTvbs :: DsMonad q => [DTyVarBndrUnit] -> Maybe DKind -> q [DTyVarBndrUnit]+-- from the data type's kind signature. This function is used when constructing+-- a @DataDecl@ to ensure that it has a number of binders equal in length to the+-- number of visible quantifiers (i.e., the number of function arrows plus the+-- number of visible @forall@–bound variables) in the data type's kind.+buildDataDTvbs :: DsMonad q => [DTyVarBndrVis] -> Maybe DKind -> q [DTyVarBndrVis] buildDataDTvbs tvbs mk = do extra_tvbs <- mkExtraDKindBinders $ fromMaybe (DConT typeKindName) mk pure $ tvbs ++ extra_tvbs@@ -459,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 }