diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,97 @@ `th-desugar` release notes ========================== +Version 1.18 [2024.12.11] +------------------------- +* Support GHC 9.12. +* Add further support for embedded types in terms. The `DExp` type now has a + `DForallE` data constructor (mirroring `ForallE` and `ForallVisE` in + `template-haskell`) and a `DConstrainedE` data constructor (mirroring + `ConstrainedE` in `template-haskell`). +* The `DLamE` and `DCaseE` data constructors (as well as the related + `mkDLamEFromDPats` function) are now deprecated in favor of the new + `DLamCasesE` data constructor. `DLamE`, `DCaseE`, and `mkDLamEFromDPats` will + be removed in a future release of `th-desugar`, so users are encouraged to + migrate. For more details on how to migrate your code, see [this + document](https://github.com/goldfirere/th-desugar/blob/master/docs/LambdaCaseMigration.md). +* The type of the `dsMatches` function has changed: + + ```diff + -dsMatches :: DsMonad q => Name -> [Match] -> q [DMatch] + +dsMatches :: DsMonad q => MatchContext -> [Match] -> q [DMatch] + ``` + + In particular: + + * `dsMatches` function no longer includes a `Name` argument for the + variable being scrutinized, as the new approach that `th-desugar` uses to + desugar `Match`es no longer requires this. + * `dsMatches` now requires a `MatchContext` argument, which + determines what kind of "`Non-exhaustive patterns in ...`" error it raises + when reaching a fallthrough case for non-exhaustive matches. +* Add a `maybeDCasesE :: MatchContext -> [DExp] -> [DClause] -> DExp` function. + `maybeDCasesE` is similar to `maybeDCaseE` except that it matches on multiple + expressions (using `\\cases`) instead of matching on a single expression. +* Add support for desugaring higher-order uses of embedded type patterns (e.g., + `\(type a) (x :: a) -> x :: a`) and invisible type patterns (e.g., + `\ @a (x :: a) -> x :: a`). +* Add a `Quote` instance for `DsM`. +* Add `mapDTVName` and `mapDTVKind` functions, which allow mapping over the + `Name` and `DKind` of a `DTyVarBndr`, respectively. +* Export `substTyVarBndr` from `Language.Haskell.TH.Desugar.Subst`. +* Add a `Language.Haskell.TH.Desugar.Subst.Capturing` module. This exposes + mostly the same API as `Language.Haskell.TH.Desugar.Subst`, except that the + substitution functions in `Language.Haskell.TH.Desugar.Subst.Capturing` do + not avoid capture when subtituting into a @forall@ type. As a result, these + substitution functions are pure rather than monadic. +* Add `dMatchUpSAKWithDecl`, a function that matches up type variable binders + from a standalone kind signature to the corresponding type variable binders + in the type-level declaration's header: + + * The type signature for `dMatchUpSAKWithDecl` returns + `[DTyVarBndr ForAllTyFlag]`, where `ForAllTyFlag` is a new data type that + generalizes both `Specificity` and `BndrVis`. + * Add `dtvbForAllTyFlagsToSpecs` and `dtvbForAllTyFlagsToBndrVis` functions, + which allow converting the results of calling `dMatchUpSAKWithDecl` to + `[DTyVarBndrSpec]` or `[DTyVarBndrVis]`, respectively. + * Also add `matchUpSAKWithDecl`, `tvbForAllTyFlagsToSpecs`, and + `tvbForAllTyFlagsToBndrVis` functions, which work over `TyVarBndr` instead + of `DTyVarBndr`. +* Locally reifying the type of a data constructor or class method now yields + type signatures with more precise type variable information, as `th-desugar` + now incorporates information from the standalone kind signature (if any) for + the parent data type or class, respectively. For instance, consider the + following data type declaration: + + ```hs + type P :: forall {k}. k -> Type + data P (a :: k) = MkP + ``` + + In previous versions of `th-desugar`, locally reifying `MkP` would yield the + following type: + + ```hs + MkP :: forall k (a :: k). P a + ``` + + This was subtly wrong, as `k` is marked as specified (i.e., eligible for + visible type application), not inferred. In `th-desugar-1.18`, however, the + locally reified type will mark `k` as inferred, as expected: + + ```hs + MkP :: forall {k} (a :: k). P a + ``` + + Similarly, desugaring `MkP` from Template Haskell to `th-desugar` results + in a data constructor with the expected type above. + * As a result of these changes, the type of `dsCon` has changed slightly: + + ```diff + -dsCon :: DsMonad q => [DTyVarBndrUnit] -> DType -> Con -> q [DCon] + +dsCon :: DsMonad q => [DTyVarBndrSpec] -> DType -> Con -> q [DCon] + ``` + Version 1.17 [2024.05.12] ------------------------- * Support GHC 9.10. diff --git a/Language/Haskell/TH/Desugar.hs b/Language/Haskell/TH/Desugar.hs --- a/Language/Haskell/TH/Desugar.hs +++ b/Language/Haskell/TH/Desugar.hs @@ -24,7 +24,8 @@ module Language.Haskell.TH.Desugar ( -- * Desugared data types - DExp(..), DLetDec(..), NamespaceSpecifier(..), DPat(..), + DExp(..), pattern DLamE, pattern DCaseE, + DLetDec(..), NamespaceSpecifier(..), DPat(..), DType(..), DForallTelescope(..), DKind, DCxt, DPred, DTyVarBndr(..), DTyVarBndrSpec, DTyVarBndrUnit, Specificity(..), DTyVarBndrVis, @@ -57,6 +58,7 @@ -- ** Secondary desugaring functions PatM, dsPred, dsPat, dsDec, dsDataDec, dsDataInstDec, DerivingClause, dsDerivClause, dsLetDec, + MatchContext(..), LamCaseVariant(..), dsMatches, dsBody, dsGuards, dsDoStmts, dsComp, dsClauses, dsBangType, dsVarBangType, dsTypeFamilyHead, dsFamilyResultSig, @@ -99,12 +101,17 @@ getDataD, dataConNameToDataName, dataConNameToCon, nameOccursIn, allNamesIn, flattenDValD, getRecordSelectors, mkTypeName, mkDataName, newUniqueName, - mkTupleDExp, mkTupleDPat, maybeDLetE, maybeDCaseE, mkDLamEFromDPats, + mkTupleDExp, mkTupleDPat, maybeDLetE, maybeDCaseE, maybeDCasesE, + dCaseE, dCasesE, dLamE, dLamCaseE, mkDLamEFromDPats, tupleNameDegree_maybe, unboxedSumNameDegree_maybe, unboxedTupleNameDegree_maybe, isTypeKindName, typeKindName, bindIP, mkExtraDKindBinders, dTyVarBndrToDType, changeDTVFlags, + mapDTVName, mapDTVKind, toposortTyVarsOf, toposortKindVarsOfTvbs, + ForAllTyFlag(..), + tvbForAllTyFlagsToSpecs, tvbForAllTyFlagsToBndrVis, matchUpSAKWithDecl, + dtvbForAllTyFlagsToSpecs, dtvbForAllTyFlagsToBndrVis, dMatchUpSAKWithDecl, -- ** 'FunArgs' and 'VisFunArg' FunArgs(..), ForallTelescope(..), VisFunArg(..), @@ -233,7 +240,7 @@ y <- newUniqueName "y" let pat' = wildify name y pat match = DMatch pat' (DVarE y) - cas = DCaseE (DVarE x) [match] + cas = dCaseE (DVarE x) [match] return $ DValD (DVarP name) cas wildify name y p = diff --git a/Language/Haskell/TH/Desugar/AST.hs b/Language/Haskell/TH/Desugar/AST.hs --- a/Language/Haskell/TH/Desugar/AST.hs +++ b/Language/Haskell/TH/Desugar/AST.hs @@ -6,7 +6,7 @@ constructors are prefixed with a D. -} -{-# LANGUAGE CPP, DeriveDataTypeable, DeriveTraversable, DeriveGeneric, DeriveLift #-} +{-# LANGUAGE CPP, DeriveDataTypeable, DeriveTraversable, DeriveGeneric, DeriveLift, PatternSynonyms, ViewPatterns #-} module Language.Haskell.TH.Desugar.AST where @@ -30,17 +30,141 @@ | DLitE Lit | DAppE DExp DExp | DAppTypeE DExp DType - | DLamE [Name] DExp - | DCaseE DExp [DMatch] + -- | A @\\cases@ expression. In the spirit of making 'DExp' minimal, + -- @th-desugar@ will desugar lambda expressions, @case@ expressions, + -- @\\case@ expressions, and @\\cases@ expressions to 'DLamCasesE'. + -- (See also the 'dLamE', 'dCaseE', and 'dLamCaseE' functions for + -- constructing these expressions in terms of 'DLamCasesE'.) + -- + -- A 'DLamCasesE' value should obey the following invariants: + -- + -- * Each 'DClause' should have exactly the same number of visible + -- arguments in its list of 'DPat's. + -- + -- * If the list of 'DClause's is empty, then the overall expression + -- should have exactly one argument. Note that this is a + -- difference in behavior from how @\\cases@ expressions work, as + -- @\\cases@ is required to have at least one clause. For this + -- reason, @th-desugar@ will sweeten @DLamCasesE []@ to + -- @\\case{}@. + | DLamCasesE [DClause] | DLetE [DLetDec] DExp | DSigE DExp DType | DStaticE DExp | DTypedBracketE DExp | DTypedSpliceE DExp | DTypeE DType + | DForallE DForallTelescope DExp + | DConstrainedE [DExp] DExp deriving (Eq, Show, Data, Generic, Lift) +-- | A 'DLamCasesE' value with exactly one 'DClause' where all 'DPat's are +-- 'DVarP's. This pattern synonym is provided for backwards compatibility with +-- older versions of @th-desugar@ in which 'DLamE' was a data constructor of +-- 'DExp'. This pattern synonym is deprecated and will be removed in a future +-- release of @th-desugar@. +pattern DLamE :: [Name] -> DExp -> DExp +pattern DLamE vars rhs <- (dLamE_maybe -> Just (vars, rhs)) + where + DLamE vars rhs = DLamCasesE [DClause (map DVarP vars) rhs] +{-# DEPRECATED DLamE "Use `dLamE` or `DLamCasesE` instead." #-} +-- | Return @'Just' (pats, rhs)@ if the supplied 'DExp' is a 'DLamCasesE' value +-- with exactly one 'DClause' where all 'DPat's are 'DVarP's, where @pats@ is +-- the list of 'DVarP' 'Name's and @rhs@ is the expression on the right-hand +-- side of the 'DClause'. Otherwise, return 'Nothing'. +dLamE_maybe :: DExp -> Maybe ([Name], DExp) +dLamE_maybe (DLamCasesE [DClause pats rhs]) = do + vars <- traverse dVarP_maybe pats + Just (vars, rhs) +dLamE_maybe _ = Nothing + +-- | Return @'Just' var@ if the supplied 'DPat' is a 'DVarP' value, where @var@ +-- is the 'DVarP' 'Name'. Otherwise, return 'Nothing'. +dVarP_maybe :: DPat -> Maybe Name +dVarP_maybe (DVarP n) = Just n +dVarP_maybe _ = Nothing + +-- | An application of a 'DLamCasesE' to some argument, where each 'DClause' in +-- the 'DLamCasesE' value has exactly one 'DPat'. This pattern synonym is +-- provided for backwards compatibility with older versions of @th-desugar@ in +-- which 'DCaseE' was a data constructor of 'DExp'. This pattern synonym is +-- deprecated and will be removed in a future release of @th-desugar@. +pattern DCaseE :: DExp -> [DMatch] -> DExp +pattern DCaseE scrut matches <- (dCaseE_maybe -> Just (scrut, matches)) + where + DCaseE scrut matches = DAppE (dLamCaseE matches) scrut +{-# DEPRECATED DCaseE "Use `dCaseE` or `DLamCasesE` instead." #-} + +-- | Return @'Just' (scrut, matches)@ if the supplied 'DExp' is a 'DLamCasesE' +-- value applied to some argument, where each 'DClause' in the 'DLamCasesE' +-- value has exactly one 'DPat'. Otherwise, return 'Nothing'. +dCaseE_maybe :: DExp -> Maybe (DExp, [DMatch]) +dCaseE_maybe (DAppE (DLamCasesE clauses) scrut) = do + matches <- traverse dMatch_maybe clauses + Just (scrut, matches) +dCaseE_maybe _ = Nothing + +-- | Construct a 'DExp' value that is equivalent to writing a @case@ expression. +-- Under the hood, this uses @\\cases@ ('DLamCasesE'). For instance, given this +-- code: +-- +-- @ +-- case scrut of +-- pat_1 -> rhs_1 +-- ... +-- pat_n -> rhs_n +-- @ +-- +-- The following @\\cases@ expression will be created under the hood: +-- +-- @ +-- (\\cases +-- pat_1 -> rhs_1 +-- ... +-- pat_n -> rhs_n) scrut +-- @ +dCaseE :: DExp -> [DMatch] -> DExp +dCaseE scrut matches = DAppE (dLamCaseE matches) scrut + +-- | Construct a 'DExp' value that is equivalent to writing a lambda expression. +-- Under the hood, this uses @\\cases@ ('DLamCasesE'). For instance, given this +-- code: +-- +-- @ +-- \\var_1 ... var_n -> rhs +-- @ +-- +-- The following @\\cases@ expression will be created under the hood: +-- +-- @ +-- \\cases var_1 ... var_n -> rhs +-- @ +dLamE :: [DPat] -> DExp -> DExp +dLamE pats rhs = DLamCasesE [DClause pats rhs] + +-- | Construct a 'DExp' value that is equivalent to writing a @\\case@ +-- expression. Under the hood, this uses @\\cases@ ('DLamCasesE'). For instance, +-- given this code: +-- +-- @ +-- \\case +-- pat_1 -> rhs_1 +-- ... +-- pat_n -> rhs_n +-- @ +-- +-- The following @\\cases@ expression will be created under the hood: +-- +-- @ +-- \\cases +-- pat_1 -> rhs_1 +-- ... +-- pat_n -> rhs_n +-- @ +dLamCaseE :: [DMatch] -> DExp +dLamCaseE = DLamCasesE . map dMatchToDClause + -- | Corresponds to TH's @Pat@ type. data DPat = DLitP Lit | DVarP Name @@ -49,19 +173,7 @@ | DBangP DPat | DSigP DPat DType | DWildP - -- | Note that @th-desugar@ only has partial support for desugaring - -- embedded type patterns. In particular, @th-desugar@ supports - -- desugaring embedded type patterns in function clauses, but not - -- in lambda expressions, @\\case@ expressions, or @\\cases@ - -- expressions. See the \"Known limitations\" section of the - -- @th-desugar@ @README@ for more details. | DTypeP DType - -- | Note that @th-desugar@ only has partial support for desugaring - -- invisible type patterns. In particular, @th-desugar@ supports - -- desugaring invisible type patterns in function clauses, but not - -- in lambda expressions or @\\cases@ expressions. See the \"Known - -- limitations\" section of the @th-desugar@ @README@ for more - -- details. | DInvisP DType deriving (Eq, Show, Data, Generic, Lift) @@ -115,12 +227,37 @@ type DTyVarBndrVis = DTyVarBndr BndrVis -- | Corresponds to TH's @Match@ type. +-- +-- Note that while @Match@ appears in the TH AST, 'DMatch' does not appear +-- directly in the @th-desugar@ AST. This is because TH's 'Match' is used in +-- lambda (@LamE@) and @case@ (@CaseE@) expressions, but @th-desugar@ does not +-- have counterparts to @LamE@ and @CaseE@ in the 'DExp' data type. Instead, +-- 'DExp' only has a @\\cases@ ('DLamCasesE') construct, which uses 'DClause' +-- instead of 'DMatch'. +-- +-- As such, 'DMatch' only plays a \"vestigial\" role in @th-desugar@ for +-- constructing 'DLamCasesE' values that look like lambda or @case@ expressions. +-- For example, 'DMatch' appears in the type signatures for 'dLamE' and +-- 'dCaseE', which convert the supplied 'DMatch'es to 'DClause's under the hood. data DMatch = DMatch DPat DExp deriving (Eq, Show, Data, Generic, Lift) -- | Corresponds to TH's @Clause@ type. data DClause = DClause [DPat] DExp deriving (Eq, Show, Data, Generic, Lift) + +-- | Convert a 'DMatch' to a 'DClause', where the 'DClause' contains a single +-- pattern taken from the 'DMatch'. +dMatchToDClause :: DMatch -> DClause +dMatchToDClause (DMatch pat rhs) = DClause [pat] rhs + +-- | Return @'Just' match@ if the supplied 'DClause' has exactly one 'DPat', +-- where @match@ matches on that 'DPat'. Otherwise, return 'Nothing'. +dMatch_maybe :: DClause -> Maybe DMatch +dMatch_maybe (DClause pats rhs) = + case pats of + [pat] -> Just (DMatch pat rhs) + _ -> Nothing -- | Declarations as used in a @let@ statement. data DLetDec = DFunD Name [DClause] diff --git a/Language/Haskell/TH/Desugar/Core.hs b/Language/Haskell/TH/Desugar/Core.hs --- a/Language/Haskell/TH/Desugar/Core.hs +++ b/Language/Haskell/TH/Desugar/Core.hs @@ -30,7 +30,7 @@ import qualified Data.List as L import qualified Data.Map as M import Data.Map (Map) -import Data.Maybe (isJust, mapMaybe) +import Data.Maybe (catMaybes, isJust, mapMaybe) import Data.Monoid (All(..)) import qualified Data.Set as S import Data.Set (Set) @@ -60,6 +60,8 @@ import Language.Haskell.TH.Desugar.OSet (OSet) import Language.Haskell.TH.Desugar.Util import Language.Haskell.TH.Desugar.Reify +import Language.Haskell.TH.Desugar.Subst (DSubst, IgnoreKinds(..), matchTy) +import qualified Language.Haskell.TH.Desugar.Subst.Capturing as SC -- | Desugar an expression dsExp :: DsMonad q => Exp -> q DExp @@ -73,7 +75,7 @@ lhsName <- newUniqueName "lhs" op' <- dsExp op rhs' <- dsExp rhs - return $ DLamE [lhsName] (foldl DAppE op' [DVarE lhsName, rhs']) + return $ dLamE [DVarP lhsName] (foldl DAppE op' [DVarE lhsName, rhs']) dsExp (InfixE (Just lhs) op (Just rhs)) = DAppE <$> (DAppE <$> dsExp op <*> dsExp lhs) <*> dsExp rhs dsExp (UInfixE _ _ _) = @@ -82,11 +84,10 @@ dsExp (LamE pats exp) = do exp' <- dsExp exp (pats', exp'') <- dsPatsOverExp pats exp' - mkDLamEFromDPats pats' exp'' + return $ dLamE pats' exp'' dsExp (LamCaseE matches) = do - x <- newUniqueName "x" - matches' <- dsMatches x matches - return $ DLamE [x] (DCaseE (DVarE x) matches') + matches' <- dsMatches (LamCaseAlt LamCase) matches + return $ dLamCaseE matches' dsExp (TupE exps) = dsTup tupleDataName exps dsExp (UnboxedTupE exps) = dsTup unboxedTupleDataName exps dsExp (CondE e1 e2 e3) = @@ -106,17 +107,10 @@ (decs', ip_binder) <- dsLetDecs decs exp' <- dsExp exp return $ DLetE decs' $ ip_binder exp' - -- the following special case avoids creating a new "let" when it's not - -- necessary. See #34. -dsExp (CaseE (VarE scrutinee) matches) = do - matches' <- dsMatches scrutinee matches - return $ DCaseE (DVarE scrutinee) matches' dsExp (CaseE exp matches) = do - scrutinee <- newUniqueName "scrutinee" exp' <- dsExp exp - matches' <- dsMatches scrutinee matches - return $ DLetE [DValD (DVarP scrutinee) exp'] $ - DCaseE (DVarE scrutinee) matches' + matches' <- dsMatches CaseAlt matches + return $ dCaseE exp' matches' #if __GLASGOW_HASKELL__ >= 900 dsExp (DoE mb_mod stmts) = dsDoStmts mb_mod stmts #else @@ -182,7 +176,7 @@ let all_matches | length filtered_cons == length cons = matches | otherwise = matches ++ [error_match] - return $ DCaseE exp' all_matches + return $ dCaseE exp' all_matches where extract_first_arg :: DsMonad q => Type -> q Type extract_first_arg (AppT (AppT ArrowT arg) _) = return arg @@ -252,15 +246,7 @@ comp acc f = DVarE '(.) `DAppE` mkGetFieldProj f `DAppE` acc #endif #if __GLASGOW_HASKELL__ >= 903 -dsExp (LamCasesE clauses) = do - clauses' <- dsClauses CaseAlt clauses - numArgs <- - case clauses' of - (DClause pats _:_) -> return $ length pats - [] -> fail "\\cases expression must have at least one alternative" - args <- replicateM numArgs (newUniqueName "x") - return $ DLamE args $ DCaseE (mkUnboxedTupleDExp (map DVarE args)) - (map dClauseToUnboxedTupleMatch clauses') +dsExp (LamCasesE clauses) = DLamCasesE <$> dsClauses (LamCaseAlt LamCases) clauses #endif #if __GLASGOW_HASKELL__ >= 907 dsExp (TypedBracketE exp) = DTypedBracketE <$> dsExp exp @@ -269,24 +255,14 @@ #if __GLASGOW_HASKELL__ >= 909 dsExp (TypeE ty) = DTypeE <$> dsType ty #endif - --- | Convert a 'DClause' to a 'DMatch' by bundling all of the clause's patterns --- into a match on a single unboxed tuple pattern. That is, convert this: --- --- @ --- f x y z = rhs --- @ --- --- To this: --- --- @ --- f (# x, y, z #) = rhs --- @ --- --- This is used to desugar @\\cases@ expressions into lambda expressions. -dClauseToUnboxedTupleMatch :: DClause -> DMatch -dClauseToUnboxedTupleMatch (DClause pats rhs) = - DMatch (mkUnboxedTupleDPat pats) rhs +#if __GLASGOW_HASKELL__ >= 911 +dsExp (ForallE tvbs exp) = + DForallE <$> (DForallInvis <$> mapM dsTvbSpec tvbs) <*> dsExp exp +dsExp (ForallVisE tvbs exp) = + DForallE <$> (DForallVis <$> mapM dsTvbUnit tvbs) <*> dsExp exp +dsExp (ConstrainedE preds exp) = + DConstrainedE <$> mapM dsExp preds <*> dsExp exp +#endif #if __GLASGOW_HASKELL__ >= 809 dsTup :: DsMonad q => (Int -> Name) -> [Maybe Exp] -> q DExp @@ -307,10 +283,10 @@ section_exps <- mapM ds_section_exp mb_exps let section_vars = lefts section_exps tup_body = mk_tup_body section_exps - if null section_vars - then return tup_body -- If this isn't a tuple section, - -- don't create a lambda. - else mkDLamEFromDPats (map DVarP section_vars) tup_body + pure $ + if null section_vars + then tup_body -- If this isn't a tuple section, don't create a lambda. + else dLamE (map DVarP section_vars) tup_body where -- If dealing with an empty field in a tuple section (Nothing), create a -- unique name and return Left. These names will be used to construct the @@ -331,46 +307,53 @@ apply_tup_body f (Left n) = f `DAppE` DVarE n apply_tup_body f (Right e) = f `DAppE` e --- | Convert a list of 'DPat' arguments and a 'DExp' body into a 'DLamE'. This --- is needed since 'DLamE' takes a list of 'Name's for its bound variables --- instead of 'DPat's, so some reorganization is needed. +-- | Construct a 'DExp' value that is equivalent to writing a lambda expression. +-- Under the hood, this uses @\\cases@ ('DLamCasesE'). +-- +-- @'mkDLamEFromDPats' pats exp@ is equivalent to writing +-- @pure ('dLamE' pats exp)@. As such, 'mkDLamEFromDPats' is deprecated in favor +-- of 'dLamE', and 'mkDLamEFromDPats' will be removed in a future @th-desugar@ +-- release. mkDLamEFromDPats :: Quasi q => [DPat] -> DExp -> q DExp -mkDLamEFromDPats pats exp - | Just names <- mapM stripDVarP_maybe pats - = return $ DLamE names exp - | otherwise - = do arg_names <- replicateM (length pats) (newUniqueName "arg") - let scrutinee = mkUnboxedTupleDExp (map DVarE arg_names) - match = DMatch (mkUnboxedTupleDPat pats) exp - return $ DLamE arg_names (DCaseE scrutinee [match]) - where - stripDVarP_maybe :: DPat -> Maybe Name - stripDVarP_maybe (DVarP n) = Just n - stripDVarP_maybe _ = Nothing +mkDLamEFromDPats pats exp = pure $ dLamE pats exp +{-# DEPRECATED mkDLamEFromDPats "Use `dLamE` or `DLamCasesE` instead." #-} #if __GLASGOW_HASKELL__ >= 902 mkGetFieldProj :: String -> DExp mkGetFieldProj field = DVarE 'getField `DAppTypeE` DLitT (StrTyLit field) #endif --- | Desugar a list of matches for a @case@ statement +-- | Desugar a list of matches for a @case@ or @\\case@ expression. dsMatches :: DsMonad q - => Name -- ^ Name of the scrutinee, which must be a bare var - -> [Match] -- ^ Matches of the @case@ statement + => MatchContext -- ^ The context in which the matches arise + -> [Match] -- ^ Matches of the @case@ or @\\case@ expression -> q [DMatch] -dsMatches scr = go +dsMatches _ [] = pure [] +-- Include a special case for guard-less matches to make the desugared output +-- a little nicer. See Note [Desugaring clauses compactly (when possible)]. +dsMatches mc (Match pat (NormalB exp) where_decs : rest) = do + rest' <- dsMatches mc rest + exp' <- dsExp exp + (where_decs', ip_binder) <- dsLetDecs where_decs + let exp_with_wheres = maybeDLetE where_decs' (ip_binder exp') + (pats', exp'') <- dsPatOverExp pat exp_with_wheres + pure $ DMatch pats' exp'' : rest' +dsMatches mc matches@(Match _ _ _ : _) = do + scrutinee_name <- newUniqueName "scrutinee" + let scrutinee = DVarE scrutinee_name + matches' <- foldrM (ds_match scrutinee) [] matches + pure [DMatch (DVarP scrutinee_name) (dCaseE scrutinee matches')] where - go :: DsMonad q => [Match] -> q [DMatch] - go [] = return [] - go (Match pat body where_decs : rest) = do - rest' <- go rest - let failure = maybeDCaseE CaseAlt (DVarE scr) rest' - exp' <- dsBody body where_decs failure - (pat', exp'') <- dsPatOverExp pat exp' + ds_match :: DsMonad q => DExp -> Match -> [DMatch] -> q [DMatch] + ds_match scrutinee (Match pat body where_decs) failure_matches = do + let failure_exp = maybeDCaseE mc scrutinee failure_matches + exp <- dsBody body where_decs failure_exp + (pat', exp') <- dsPatOverExp pat exp uni_pattern <- isUniversalPattern pat' -- incomplete attempt at #6 + let match = DMatch pat' exp' if uni_pattern - then return [DMatch pat' exp''] - else return (DMatch pat' exp'' : rest') + then return [match] + else return (match : failure_matches) -- | Desugar a @Body@ dsBody :: DsMonad q @@ -387,6 +370,39 @@ guarded_exp' <- dsGuards guarded_exps failure return $ maybeDLetE decs' $ ip_binder guarded_exp' +-- | Construct a 'DExp' value that is equivalent to writing a @case@ expression +-- that scrutinizes multiple values at once. Under the hood, this uses +-- @\\cases@ ('DLamCasesE'). For instance, given this code: +-- +-- @ +-- case (scrut_1, ..., scrut_n) of +-- (pat_1_1, ..., pat_1_n) -> rhs_1 +-- ... +-- (pat_m_1, ..., pat_m_n) -> rhs_n +-- @ +-- +-- The following @\\cases@ expression will be created under the hood: +-- +-- @ +-- (\\cases +-- pat_1_1 ... pat_1_n -> rhs_1 +-- ... +-- pat_m_1 ... pat_m_n -> rhs_n) scrut_1 ... scrut_n +-- @ +-- +-- In other words, this creates a 'DLamCasesE' value and then applies it to +-- argument values. +-- +-- Preconditions: +-- +-- * If the list of 'DClause's is non-empty, then the number of patterns in each +-- 'DClause' must be equal to the number of 'DExp' arguments. +-- +-- * If the list of 'DClause's is empty, then there must be exactly one 'DExp' +-- argument. +dCasesE :: [DExp] -> [DClause] -> DExp +dCasesE scruts clauses = applyDExp (DLamCasesE clauses) scruts + -- | If decs is non-empty, delcare them in a let: maybeDLetE :: [DLetDec] -> DExp -> DExp maybeDLetE [] exp = exp @@ -395,8 +411,17 @@ -- | If matches is non-empty, make a case statement; otherwise make an error statement maybeDCaseE :: MatchContext -> DExp -> [DMatch] -> DExp maybeDCaseE mc _ [] = mkErrorMatchExpr mc -maybeDCaseE _ scrut matches = DCaseE scrut matches +maybeDCaseE _ scrut matches = dCaseE scrut matches +-- | If the list of clauses is non-empty, make a @\\cases@ expression and apply +-- it using the expressions as arguments. Otherwise, make an error statement. +-- +-- Precondition: if the list of 'DClause's is non-empty, then the number of +-- patterns in each 'DClause' must be equal to the number of 'DExp' arguments. +maybeDCasesE :: MatchContext -> [DExp] -> [DClause] -> DExp +maybeDCasesE mc _ [] = mkErrorMatchExpr mc +maybeDCasesE _ scruts clauses = dCasesE scruts clauses + -- | Desugar guarded expressions dsGuards :: DsMonad q => [(Guard, Exp)] -- ^ Guarded expressions @@ -421,7 +446,7 @@ success' <- dsGuardStmts rest success failure (pat', success'') <- dsPatOverExp pat success' exp' <- dsExp exp - return $ DCaseE exp' [DMatch pat' success'', DMatch DWildP failure] + return $ dCaseE exp' [DMatch pat' success'', DMatch DWildP failure] dsGuardStmts (LetS decs : rest) success failure = do (decs', ip_binder) <- dsLetDecs decs success' <- dsGuardStmts rest success failure @@ -439,7 +464,7 @@ dsGuardStmts (NoBindS exp : rest) success failure = do exp' <- dsExp exp success' <- dsGuardStmts rest success failure - return $ DCaseE exp' [ DMatch (DConP 'True [] []) success' + return $ dCaseE exp' [ DMatch (DConP 'True [] []) success' , DMatch (DConP 'False [] []) failure ] dsGuardStmts (ParS _ : _) _ _ = impossible "Parallel comprehension in a pattern guard." #if __GLASGOW_HASKELL__ >= 807 @@ -488,7 +513,7 @@ dsComp (ParS stmtss : rest) = do (pat, exp) <- dsParComp stmtss rest' <- dsComp rest - DAppE (DAppE (DVarE '(>>=)) exp) <$> mkDLamEFromDPats [pat] rest' + return $ DAppE (DAppE (DVarE '(>>=)) exp) (dLamE [pat] rest') #if __GLASGOW_HASKELL__ >= 807 dsComp (RecS {} : _) = fail "th-desugar currently does not support RecursiveDo" #endif @@ -505,15 +530,14 @@ dsBindS mb_mod bind_arg_exp success_pat success_exp ctxt = do bind_arg_exp' <- dsExp bind_arg_exp (success_pat', success_exp') <- dsPatOverExp success_pat success_exp - is_univ_pat <- isUniversalPattern success_pat' + is_univ_pat <- isUniversalPattern success_pat' -- incomplete attempt at #6 let bind_into = DAppE (DAppE (DVarE bind_name) bind_arg_exp') if is_univ_pat - then bind_into <$> mkDLamEFromDPats [success_pat'] success_exp' - else do arg_name <- newUniqueName "arg" - fail_name <- mk_fail_name - return $ bind_into $ DLamE [arg_name] $ DCaseE (DVarE arg_name) - [ DMatch success_pat' success_exp' - , DMatch DWildP $ + then return $ bind_into $ dLamE [success_pat'] success_exp' + else do fail_name <- mk_fail_name + return $ bind_into $ DLamCasesE + [ DClause [success_pat'] success_exp' + , DClause [DWildP] $ DVarE fail_name `DAppE` DLitE (StringL $ "Pattern match failure in " ++ ctxt) ] @@ -539,9 +563,21 @@ fail_Prelude_name = mk_qual_do_name mb_mod 'Prelude.fail #endif --- | Desugar the contents of a parallel comprehension. --- Returns a @Pat@ containing a tuple of all bound variables and an expression --- to produce the values for those variables +-- | Desugar the contents of a parallel comprehension (enabled via the +-- @ParallelListComp@ language extension). For example, this expression: +-- +-- @ +-- [ x + y | x <- [1,2,3] | y <- [4,5,6] ] +-- @ +-- +-- Will be desugared to code that looks roughly like: +-- +-- @ +-- 'mzip' [1, 2, 3] [4, 5, 6] '>>=' \\cases (x, y) -> 'return' (x + y) +-- @ +-- +-- This function returns a 'DPat' containing a tuple of all bound variables and +-- a 'DExp' to produce the values for those variables. dsParComp :: DsMonad q => [[Stmt]] -> q (DPat, DExp) dsParComp [] = impossible "Empty list of parallel comprehension statements." dsParComp [r] = do @@ -658,6 +694,10 @@ #endif dsPat (ViewP _ _) = fail "View patterns are not supported in th-desugar. Use pattern guards instead." +#if __GLASGOW_HASKELL__ >= 911 +dsPat (OrP _) = + fail "Or-patterns are not supported in th-desugar." +#endif -- | Convert a 'DPat' to a 'DExp'. Fails on 'DWildP' and 'DInvisP'. dPatToDExp :: DPat -> DExp @@ -799,12 +839,25 @@ -> Maybe Kind -> [Con] -> [DerivingClause] -> q [DDec] dsDataDec nd cxt n tvbs mk cons derivings = do tvbs' <- mapM dsTvbVis tvbs - let h98_tvbs = case mk of - -- If there's an explicit return kind, we're dealing with a - -- GADT, so this argument goes unused in dsCon. - Just {} -> unusedArgument - Nothing -> tvbs' - h98_return_type = nonFamilyDataReturnType n tvbs' + h98_tvbs <- + case mk of + -- If there's an explicit return kind, we're dealing with a + -- GADT, so this argument goes unused in dsCon. + Just {} -> pure unusedArgument + -- If there is no explicit return kind, we're dealing with a + -- Haskell98-style data type, so we must compute the type variable + -- binders to use in the types of the data constructors. + -- + -- Rather than just returning `tvbs'` here, we propagate kind information + -- from the data type's standalone kind signature (if one exists) to make + -- the kinds more precise. + Nothing -> do + mb_sak <- dsReifyType n + let tvbSpecs = changeDTVFlags SpecifiedSpec tvbs' + pure $ maybe tvbSpecs dtvbForAllTyFlagsToSpecs $ do + sak <- mb_sak + dMatchUpSAKWithDecl sak tvbs' + let h98_return_type = nonFamilyDataReturnType n tvbs' (:[]) <$> (DDataD nd <$> dsCxt cxt <*> pure n <*> pure tvbs' <*> mapM dsType mk <*> concatMapM (dsCon h98_tvbs h98_return_type) cons @@ -819,7 +872,7 @@ tys' <- mapM dsTypeArg tys let lhs' = applyDType (DConT n) tys' h98_tvbs = - changeDTVFlags defaultBndrFlag $ + changeDTVFlags SpecifiedSpec $ case (mk, mtvbs') of -- If there's an explicit return kind, we're dealing with a -- GADT, so this argument goes unused in dsCon. @@ -969,10 +1022,10 @@ -- we require passing these as arguments. (If we desugar an actual GADT -- constructor, these arguments are ignored.) dsCon :: DsMonad q - => [DTyVarBndrVis] -- ^ The universally quantified type variables - -- (used if desugaring a non-GADT constructor). - -> DType -- ^ The original data declaration's type - -- (used if desugaring a non-GADT constructor). + => [DTyVarBndrSpec] -- ^ The universally quantified type variables + -- (used if desugaring a non-GADT constructor). + -> DType -- ^ The original data declaration's type + -- (used if desugaring a non-GADT constructor). -> Con -> q [DCon] dsCon univ_dtvbs data_type con = do dcons' <- dsCon' con @@ -980,8 +1033,7 @@ case m_gadt_type of Nothing -> let ex_dtvbs = dtvbs - expl_dtvbs = changeDTVFlags SpecifiedSpec univ_dtvbs ++ - ex_dtvbs + expl_dtvbs = univ_dtvbs ++ ex_dtvbs impl_dtvbs = changeDTVFlags SpecifiedSpec $ toposortKindVarsOfTvbs expl_dtvbs in DCon (impl_dtvbs ++ expl_dtvbs) dcxt n fields data_type @@ -1108,8 +1160,9 @@ -> [Clause] -- ^ Clauses to desugar -> q [DClause] dsClauses _ [] = return [] +-- Include a special case for guard-less clauses to make the desugared output +-- a little nicer. See Note [Desugaring clauses compactly (when possible)]. dsClauses mc (Clause pats (NormalB exp) where_decs : rest) = do - -- this case is necessary to maintain the roundtrip property. rest' <- dsClauses mc rest exp' <- dsExp exp (where_decs', ip_binder) <- dsLetDecs where_decs @@ -1118,21 +1171,21 @@ return $ DClause pats' exp'' : rest' dsClauses mc clauses@(Clause outer_pats _ _ : _) = do arg_names <- replicateM (length outer_pats) (newUniqueName "arg") - let scrutinee = mkUnboxedTupleDExp (map DVarE arg_names) - clause <- DClause (map DVarP arg_names) <$> - (DCaseE scrutinee <$> foldrM (clause_to_dmatch scrutinee) [] clauses) - return [clause] + let scrutinees = map DVarE arg_names + clauses' <- foldrM (ds_clause scrutinees) [] clauses + pure [DClause (map DVarP arg_names) (dCasesE scrutinees clauses')] where - clause_to_dmatch :: DsMonad q => DExp -> Clause -> [DMatch] -> q [DMatch] - clause_to_dmatch scrutinee (Clause pats body where_decs) failure_matches = do - let failure_exp = maybeDCaseE mc scrutinee failure_matches + ds_clause :: DsMonad q => [DExp] -> Clause -> [DClause] -> q [DClause] + ds_clause scrutinees (Clause pats body where_decs) failure_clauses = do + let failure_exp = maybeDCasesE mc scrutinees failure_clauses exp <- dsBody body where_decs failure_exp (pats', exp') <- dsPatsOverExp pats exp + -- incomplete attempt at #6 uni_pats <- fmap getAll $ concatMapM (fmap All . isUniversalPattern) pats' - let match = DMatch (mkUnboxedTupleDPat pats') exp' + let clause = DClause pats' exp' if uni_pats - then return [match] - else return (match : failure_matches) + then return [clause] + else return (clause : failure_clauses) -- | The context of a pattern match. This is used to produce -- @Non-exhaustive patterns in...@ messages that are tailored to specific @@ -1150,7 +1203,17 @@ -- ^ Guards in a multi-way if alternative | CaseAlt -- ^ Patterns and guards in a case alternative + | LamCaseAlt LamCaseVariant + -- ^ Patterns and guards in @\\case@ and @\\cases@ +-- | Which kind of lambda case are we dealing with? Compare this to GHC's +-- @LamCaseVariant@ data type +-- (https://gitlab.haskell.org/ghc/ghc/-/blob/81cf52bb301592ff3d043d03eb9a0d547891a3e1/compiler/Language/Haskell/Syntax/Expr.hs#L686-690) +-- from which we take inspiration. +data LamCaseVariant + = LamCase -- ^ @\\case@ + | LamCases -- ^ @\\cases@ + -- | Construct an expression that throws an error when encountering a pattern -- at runtime that is not covered by pattern matching. mkErrorMatchExpr :: MatchContext -> DExp @@ -1164,7 +1227,99 @@ RecUpd -> "record update" MultiWayIfAlt -> "multi-way if" CaseAlt -> "case" + LamCaseAlt lv -> pp_lam_case_variant lv + pp_lam_case_variant LamCase = "\\case" + pp_lam_case_variant LamCases = "\\cases" + +{- +Note [Desugaring clauses compactly (when possible)] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In the general case, th-desugar's approach to desugaring clauses with guards +requires binding an extra variable. For example, consider this code: + + \case + A x | x == "hello" -> x + B y -> y + _ -> "" + +As part of desugaring, th-desugar will get rid of the guards by rewriting the +code to something that looks closer to this: + + \scrutinee -> + case scrutinee of + A x -> + if x == "hello" + then x + else case scrutinee of + B y -> y + _ -> "" + B y -> y + _ -> "" + +(The fully desugared output would then translate the lambda and `case` +expressions to `\cases` expressions, but let's put that aside for now. We'll +come back to this in a bit.) + +Note the `scrutinee` argument, which is now explicitly named. Binding the +argument to a name is important because we need to further match on it when the +`x == "hello"` guard fails to match. + +This approach gets the job done, but it does add a some amount of extra +clutter. We take steps to avoid this clutter where possible. Consider this +simpler example: + + \case + A x -> x + B y -> y + _ -> "" + +If we were to desugar this example using the same approach as above, we'd end +up with something like this: + + \scrutinee -> + case scrutinee of + A x -> x + B y -> y + _ -> "" + +Recall that th-desugar will desugar lambda and `case` expressions to `\cases` +exprressions. As such, the fully desugared output would be: + + \cases + scrutinee -> + (\cases + A x -> x + B y -> y + _ -> "") scrutinee + +This would technically work, but we would lose something along the way. By +using this approach, we would transform something with a single `\case` +expression to something with multiple `\cases` expressions. Moreover, the +original expression never needed to give a name to the `scrutinee` variable, so +it would be strange for the desugared output to require this extra clutter. + +Luckily, we can avoid the clutter by observing that the `scrutinee` variable +can be eta-contracted away. More generally, if a set of clauses does not use +any guards, then we don't bother explicitly binding a variable like +`scrutinee`, as we never need to use it outside of the initial matching. This +means that we can desugar the simpler example above to: + + \cases + (A x) -> x + (B y) -> y + _ -> "" + +Ahh. Much nicer. + +Of course, the flip side is that we /do/ need the extra `scrutinee` clutter +when desugaring clauses involving guards. Personally, I'm not too bothered by +this, as th-desugar's approach to desugaring guards already has various +limitations (see the "Known limitations" section of the th-desugar README). As +such, I'm not inclined to invest more effort into fixing this unless someone +explicitly asks for it. +-} + -- | Desugar a type dsType :: DsMonad q => Type -> q DType #if __GLASGOW_HASKELL__ >= 900 @@ -1491,41 +1646,26 @@ Nothing -> return $ deflt : rest' reorder (_ : _) [] = error "Internal error in th-desugar." --- mkTupleDExp, mkUnboxedTupleDExp, and friends construct tuples, avoiding the --- use of 1-tuples. These are used to create auxiliary tuple values when --- desugaring pattern-matching constructs to simpler forms. --- See Note [Auxiliary tuples in pattern matching]. +-- mkTupleDExp and friends construct tuples, avoiding the use of 1-tuples. These +-- are used to create auxiliary tuple values when desugaring ParallelListComp +-- expressions (see the Haddocks for dsParComp) and when match-flattening lazy +-- patterns (see the Haddocks for mkSelectorDecs in L.H.TH.Desugar.Match). -- | Make a tuple 'DExp' from a list of 'DExp's. Avoids using a 1-tuple. mkTupleDExp :: [DExp] -> DExp mkTupleDExp [exp] = exp mkTupleDExp exps = foldl DAppE (DConE $ tupleDataName (length exps)) exps --- | Make an unboxed tuple 'DExp' from a list of 'DExp's. Avoids using a 1-tuple. -mkUnboxedTupleDExp :: [DExp] -> DExp -mkUnboxedTupleDExp [exp] = exp -mkUnboxedTupleDExp exps = foldl DAppE (DConE $ unboxedTupleDataName (length exps)) exps - -- | Make a tuple 'Exp' from a list of 'Exp's. Avoids using a 1-tuple. mkTupleExp :: [Exp] -> Exp mkTupleExp [exp] = exp mkTupleExp exps = foldl AppE (ConE $ tupleDataName (length exps)) exps --- | Make an unboxed tuple 'Exp' from a list of 'Exp's. Avoids using a 1-tuple. -mkUnboxedTupleExp :: [Exp] -> Exp -mkUnboxedTupleExp [exp] = exp -mkUnboxedTupleExp exps = foldl AppE (ConE $ unboxedTupleDataName (length exps)) exps - -- | Make a tuple 'DPat' from a list of 'DPat's. Avoids using a 1-tuple. mkTupleDPat :: [DPat] -> DPat mkTupleDPat [pat] = pat mkTupleDPat pats = DConP (tupleDataName (length pats)) [] pats --- | Make an unboxed tuple 'DPat' from a list of 'DPat's. Avoids using a 1-tuple. -mkUnboxedTupleDPat :: [DPat] -> DPat -mkUnboxedTupleDPat [pat] = pat -mkUnboxedTupleDPat pats = DConP (unboxedTupleDataName (length pats)) [] pats - -- | Is this pattern guaranteed to match? isUniversalPattern :: DsMonad q => DPat -> q Bool isUniversalPattern (DLitP {}) = return False @@ -1775,6 +1915,16 @@ dtvbFlag (DPlainTV _ flag) = flag dtvbFlag (DKindedTV _ flag _) = flag +-- | Map over the 'Name' of a 'DTyVarBndr'. +mapDTVName :: (Name -> Name) -> DTyVarBndr flag -> DTyVarBndr flag +mapDTVName f (DPlainTV name flag) = DPlainTV (f name) flag +mapDTVName f (DKindedTV name flag kind) = DKindedTV (f name) flag kind + +-- | Map over the 'DKind' of a 'DTyVarBndr'. +mapDTVKind :: (DKind -> DKind) -> DTyVarBndr flag -> DTyVarBndr flag +mapDTVKind _ tvb@(DPlainTV{}) = tvb +mapDTVKind f (DKindedTV name flag kind) = DKindedTV name flag (f kind) + -- @mk_qual_do_name mb_mod orig_name@ will simply return @orig_name@ if -- @mb_mod@ is Nothing. If @mb_mod@ is @Just mod_@, then a new 'Name' will be -- returned that uses @mod_@ as the new module prefix. This is useful for @@ -1886,6 +2036,349 @@ changeDTVFlags :: newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag] changeDTVFlags new_flag = map (new_flag <$) +-- @'dMatchUpSAKWithDecl' decl_sak decl_bndrs@ produces @'DTyVarBndr' +-- 'ForAllTyFlag'@s for a declaration, using the original declaration's +-- standalone kind signature (@decl_sak@) and its user-written binders +-- (@decl_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 @'DTyVarBndr' 'ForAllTyFlag'@s: +-- +-- @ +-- \@j \@l (a :: l) (b :: j) +-- @ +-- +-- From here, these @'DTyVarBndr' 'ForAllTyFlag'@s can be converted into other +-- forms of 'DTyVarBndr's: +-- +-- * They can be converted to 'DTyVarBndrSpec's using 'dtvbForAllTyFlagsToSpecs'. +-- +-- * They can be converted to 'DTyVarBndrVis'es using 'tvbForAllTyFlagsToVis'. +-- +-- Note that: +-- +-- * This function has a precondition that the length of @decl_bndrs@ must +-- always be equal to the number of visible quantifiers (i.e., the number of +-- function arrows plus the number of visible @forall@–bound variables) in +-- @decl_sak@. +-- +-- * Whenever possible, this function reuses type variable names from the +-- declaration's user-written binders. This is why the @'DTyVarBndr' +-- 'ForAllTyFlag'@ use @\@j \@l@ instead of @\@j \@k@, since the @(a :: l)@ +-- binder uses @l@ instead of @k@. We could have just as well chose the other +-- way around, but we chose to pick variable names from the user-written +-- binders since they scope over other parts of the declaration. (For example, +-- the user-written binders of a @data@ declaration scope over the type +-- variables mentioned in a @deriving@ clause.) As such, keeping these names +-- avoids having to perform some alpha-renaming. +-- +-- This function's implementation was heavily inspired by parts of GHC's +-- kcCheckDeclHeader_sig function: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2524-2643 +dMatchUpSAKWithDecl :: + forall q. + Fail.MonadFail q + => DKind + -- ^ The declaration's standalone kind signature + -> [DTyVarBndrVis] + -- ^ The user-written binders in the declaration + -> q [DTyVarBndr ForAllTyFlag] +dMatchUpSAKWithDecl decl_sak decl_bndrs = do + -- (1) First, explicitly quantify any free kind variables in `decl_sak` using + -- an invisible @forall@. This is done to ensure that precondition (2) in + -- `dMatchUpSigWithDecl` is upheld. (See the Haddocks for that function). + let decl_sak_free_tvbs = + changeDTVFlags SpecifiedSpec $ toposortTyVarsOf [decl_sak] + decl_sak' = DForallT (DForallInvis decl_sak_free_tvbs) decl_sak + + -- (2) Next, compute type variable binders using `dMatchUpSigWithDecl`. Note + -- that these can be biased towards type variable names mention in `decl_sak` + -- over names mentioned in `decl_bndrs`, but we will fix that up in the next + -- step. + let (decl_sak_args, _) = unravelDType decl_sak' + sing_sak_tvbs <- dMatchUpSigWithDecl decl_sak_args decl_bndrs + + -- (3) Finally, swizzle the type variable names so that names in `decl_bndrs` + -- are preferred over names in `decl_sak`. + -- + -- This is heavily inspired by similar code in GHC: + -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616 + let invis_decl_sak_args = filterInvisTvbArgs decl_sak_args + invis_decl_sak_arg_nms = map dtvbName invis_decl_sak_args + + invis_decl_bndrs = toposortKindVarsOfTvbs decl_bndrs + invis_decl_bndr_nms = map dtvbName invis_decl_bndrs + + swizzle_env = + M.fromList $ zip invis_decl_sak_arg_nms invis_decl_bndr_nms + (_, swizzled_sing_sak_tvbs) = + mapAccumL (swizzleTvb swizzle_env) M.empty sing_sak_tvbs + pure swizzled_sing_sak_tvbs + +-- Match the quantifiers in a type-level declaration's standalone kind signature +-- with the user-written binders in the declaration. This function assumes the +-- following preconditions: +-- +-- 1. The number of required binders in the declaration's user-written binders +-- is equal to the number of visible quantifiers (i.e., the number of +-- function arrows plus the number of visible @forall@–bound variables) in +-- the standalone kind signature. +-- +-- 2. The number of invisible \@-binders in the declaration's user-written +-- binders is less than or equal to the number of invisible quantifiers +-- (i.e., the number of invisible @forall@–bound variables) in the +-- standalone kind signature. +-- +-- The implementation of this function is heavily based on a GHC function of +-- the same name: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2645-2715 +dMatchUpSigWithDecl :: + forall q. + Fail.MonadFail q + => DFunArgs + -- ^ The quantifiers in the declaration's standalone kind signature + -> [DTyVarBndrVis] + -- ^ The user-written binders in the declaration + -> q [DTyVarBndr ForAllTyFlag] +dMatchUpSigWithDecl = go_fun_args M.empty + where + go_fun_args :: + DSubst + -- ^ A substitution from the names of @forall@-bound variables in the + -- standalone kind signature to corresponding binder names in the + -- user-written binders. This is because we want to reuse type variable + -- names from the user-written binders whenever possible. For example: + -- + -- @ + -- type T :: forall a. forall b -> Maybe (a, b) -> Type + -- data T @x y z + -- @ + -- + -- After matching up the @a@ in @forall a.@ with @x@ and + -- the @b@ in @forall b ->@ with @y@, this substitution will be + -- extended with @[a :-> x, b :-> y]@. This ensures that we will + -- produce @Maybe (x, y)@ instead of @Maybe (a, b)@ in + -- the kind for @z@. + -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag] + go_fun_args _ DFANil [] = + pure [] + -- This should not happen, per precondition (1). + go_fun_args _ DFANil decl_bndrs = + fail $ "dMatchUpSigWithDecl.go_fun_args: Too many binders: " ++ show decl_bndrs + -- GHC now disallows kind-level constraints, per this GHC proposal: + -- https://github.com/ghc-proposals/ghc-proposals/blob/b0687d96ce8007294173b7f628042ac4260cc738/proposals/0547-no-kind-equalities.rst + -- As such, we reject non-empty kind contexts. Empty contexts (which are + -- benign) can sometimes arise due to @ForallT@, so we add a special case + -- to allow them. + go_fun_args subst (DFACxt [] args) decl_bndrs = + go_fun_args subst args decl_bndrs + go_fun_args _ (DFACxt{}) _ = + fail "dMatchUpSigWithDecl.go_fun_args: Unexpected kind-level constraint" + go_fun_args subst (DFAForalls (DForallInvis tvbs) sig_args) decl_bndrs = + go_invis_tvbs subst tvbs sig_args decl_bndrs + go_fun_args subst (DFAForalls (DForallVis tvbs) sig_args) decl_bndrs = + go_vis_tvbs subst tvbs sig_args decl_bndrs + go_fun_args subst (DFAAnon anon sig_args) (decl_bndr:decl_bndrs) = + case dtvbFlag decl_bndr of + -- If the next decl_bndr is required, then we must match its kind (if + -- one is provided) against the anonymous kind argument. + BndrReq -> do + let decl_bndr_name = dtvbName decl_bndr + mb_decl_bndr_kind = extractTvbKind decl_bndr + anon' = SC.substTy subst anon + + anon'' = + case mb_decl_bndr_kind of + Nothing -> anon' + Just decl_bndr_kind -> + let mb_match_subst = matchTy NoIgnore decl_bndr_kind anon' in + maybe decl_bndr_kind (`SC.substTy` decl_bndr_kind) mb_match_subst + sig_args' <- go_fun_args subst sig_args decl_bndrs + pure $ DKindedTV decl_bndr_name Required anon'' : sig_args' + -- We have a visible, anonymous argument in the kind, but an invisible + -- @-binder as the next decl_bndr. This is ill kinded, so throw an + -- error. + -- + -- This should not happen, per precondition (2). + BndrInvis -> + fail $ "dMatchUpSigWithDecl.go_fun_args: Expected visible binder, encountered invisible binder: " + ++ show decl_bndr + -- This should not happen, per precondition (1). + go_fun_args _ _ [] = + fail "dMatchUpSigWithDecl.go_fun_args: Too few binders" + + go_invis_tvbs :: DSubst -> [DTyVarBndrSpec] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag] + go_invis_tvbs subst [] sig_args decl_bndrs = + go_fun_args subst sig_args decl_bndrs + go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss = + case decl_bndrss of + [] -> skip_invis_bndr + decl_bndr:decl_bndrs -> + case dtvbFlag decl_bndr of + BndrReq -> skip_invis_bndr + -- If the next decl_bndr is an invisible @-binder, then we must match it + -- against the invisible forall–bound variable in the kind. + BndrInvis -> do + let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr + sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs + pure (fmap Invisible sig_tvb : sig_args') + where + -- There is an invisible forall in the kind without a corresponding + -- invisible @-binder, which is allowed. In this case, we simply apply + -- the substitution and recurse. + skip_invis_bndr :: q [DTyVarBndr ForAllTyFlag] + skip_invis_bndr = do + let (subst', invis_tvb') = SC.substTyVarBndr subst invis_tvb + sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrss + pure $ fmap Invisible invis_tvb' : sig_args' + + go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag] + go_vis_tvbs subst [] sig_args decl_bndrs = + go_fun_args subst sig_args decl_bndrs + -- This should not happen, per precondition (1). + go_vis_tvbs _ (_:_) _ [] = + fail "dMatchUpSigWithDecl.go_vis_tvbs: Too few binders" + go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (decl_bndr:decl_bndrs) = do + case dtvbFlag decl_bndr of + -- If the next decl_bndr is required, then we must match it against the + -- visible forall–bound variable in the kind. + BndrReq -> do + let (subst', sig_tvb) = match_tvbs subst vis_tvb decl_bndr + sig_args' <- go_vis_tvbs subst' vis_tvbs sig_args decl_bndrs + pure ((Required <$ sig_tvb) : sig_args') + -- We have a visible forall in the kind, but an invisible @-binder as + -- the next decl_bndr. This is ill kinded, so throw an error. + -- + -- This should not happen, per precondition (2). + BndrInvis -> + fail $ "dMatchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: " + ++ show decl_bndr + + -- @match_tvbs subst sig_tvb decl_bndr@ will match the kind of @decl_bndr@ + -- against the kind of @sig_tvb@ to produce a new kind. This function + -- produces two values as output: + -- + -- 1. A new @subst@ that has been extended such that the name of @sig_tvb@ + -- maps to the name of @decl_bndr@. (See the Haddocks for the 'DSubst' + -- argument to @go_fun_args@ for an explanation of why we do this.) + -- + -- 2. A 'DTyVarBndrSpec' that has the name of @decl_bndr@, but with the new + -- kind resulting from matching. + match_tvbs :: DSubst -> DTyVarBndr flag -> DTyVarBndrVis -> (DSubst, DTyVarBndr flag) + match_tvbs subst sig_tvb decl_bndr = + let decl_bndr_name = dtvbName decl_bndr + mb_decl_bndr_kind = extractTvbKind decl_bndr + + sig_tvb_name = dtvbName sig_tvb + sig_tvb_flag = dtvbFlag sig_tvb + mb_sig_tvb_kind = SC.substTy subst <$> extractTvbKind sig_tvb + + mb_kind :: Maybe DKind + mb_kind = + case (mb_decl_bndr_kind, mb_sig_tvb_kind) of + (Nothing, Nothing) -> Nothing + (Just decl_bndr_kind, Nothing) -> Just decl_bndr_kind + (Nothing, Just sig_tvb_kind) -> Just sig_tvb_kind + (Just decl_bndr_kind, Just sig_tvb_kind) -> do + match_subst <- matchTy NoIgnore decl_bndr_kind sig_tvb_kind + Just $ SC.substTy match_subst decl_bndr_kind + + subst' = M.insert sig_tvb_name (DVarT decl_bndr_name) subst + sig_tvb' = case mb_kind of + Nothing -> DPlainTV decl_bndr_name sig_tvb_flag + Just kind -> DKindedTV decl_bndr_name sig_tvb_flag kind in + + (subst', sig_tvb') + +-- Collect the invisible type variable binders from a sequence of DFunArgs. +filterInvisTvbArgs :: DFunArgs -> [DTyVarBndrSpec] +filterInvisTvbArgs DFANil = [] +filterInvisTvbArgs (DFACxt _ args) = filterInvisTvbArgs args +filterInvisTvbArgs (DFAAnon _ args) = filterInvisTvbArgs args +filterInvisTvbArgs (DFAForalls tele args) = + let res = filterInvisTvbArgs args in + case tele of + DForallVis _ -> res + DForallInvis tvbs' -> tvbs' ++ res + +-- This is heavily inspired by the `swizzleTcb` function in GHC: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2741-2755 +swizzleTvb :: + Map Name Name + -- ^ A \"swizzle environment\" (i.e., a map from binder names in a + -- standalone kind signature to binder names in the corresponding + -- type-level declaration). + -> DSubst + -- ^ Like the swizzle environment, but as a full-blown substitution. + -> DTyVarBndr flag + -> (DSubst, DTyVarBndr flag) +swizzleTvb swizzle_env subst tvb = + (subst', tvb2) + where + subst' = M.insert tvb_name (DVarT (dtvbName tvb2)) subst + tvb_name = dtvbName tvb + tvb1 = mapDTVKind (SC.substTy subst) tvb + tvb2 = + case M.lookup tvb_name swizzle_env of + Just user_name -> mapDTVName (const user_name) tvb1 + Nothing -> tvb1 + +-- | Convert a list of @'DTyVarBndr' 'ForAllTyFlag'@s to a list of +-- 'DTyVarBndrSpec's, which is suitable for use in an invisible @forall@. +-- Specifically: +-- +-- * Variable binders that use @'Invisible' spec@ are converted to @spec@. +-- +-- * Variable binders that are 'Required' are converted to 'SpecifiedSpec', +-- as all of the 'DTyVarBndrSpec's are invisible. As an example of how this +-- is used, consider what would happen when singling this data type: +-- +-- @ +-- type T :: forall k -> k -> Type +-- data T k (a :: k) where ... +-- @ +-- +-- Here, the @k@ binder is 'Required'. When we produce the standalone kind +-- signature for the singled data type, we use 'dtvbForAllTyFlagsToSpecs' to +-- produce the type variable binders in the outermost @forall@: +-- +-- @ +-- type ST :: forall k (a :: k). T k a -> Type +-- data ST z where ... +-- @ +-- +-- Note that the @k@ is bound visibily (i.e., using 'SpecifiedSpec') in the +-- outermost, invisible @forall@. +dtvbForAllTyFlagsToSpecs :: [DTyVarBndr ForAllTyFlag] -> [DTyVarBndrSpec] +dtvbForAllTyFlagsToSpecs = map (fmap to_spec) + where + to_spec :: ForAllTyFlag -> Specificity + to_spec (Invisible spec) = spec + to_spec Required = SpecifiedSpec + +-- | Convert a list of @'DTyVarBndr' 'ForAllTyFlag'@s to a list of +-- 'DTyVarBndrVis'es, which is suitable for use in a type-level declaration +-- (e.g., the @var_1 ... var_n@ in @class C var_1 ... var_n@). Specifically: +-- +-- * Variable binders that use @'Invisible' 'InferredSpec'@ are dropped +-- entirely. Such binders cannot be represented in source Haskell. +-- +-- * Variable binders that use @'Invisible' 'SpecifiedSpec'@ are converted to +-- 'BndrInvis'. +-- +-- * Variable binders that are 'Required' are converted to 'BndrReq'. +dtvbForAllTyFlagsToBndrVis :: [DTyVarBndr ForAllTyFlag] -> [DTyVarBndrVis] +dtvbForAllTyFlagsToBndrVis = catMaybes . map (traverse to_spec_maybe) + where + to_spec_maybe :: ForAllTyFlag -> Maybe BndrVis + to_spec_maybe (Invisible InferredSpec) = Nothing + to_spec_maybe (Invisible SpecifiedSpec) = Just bndrInvis + to_spec_maybe Required = Just BndrReq + -- | Some functions in this module only use certain arguments on particular -- versions of GHC. Other versions of GHC (that don't make use of those -- arguments) might need to conjure up those arguments out of thin air at the @@ -1941,138 +2434,4 @@ * For all other cases, just straightforwardly sweeten `DForallT DForallInvis tvbs ty` to `ForallT tvbs [] ty` and `DConstrainedT ctxt ty` to `ForallT [] ctxt ty`. - -Note [Auxiliary tuples in pattern matching] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -th-desugar simplifies the overall treatment of pattern matching in two -notable ways: - -1. Lambda expressions only bind variables and do not directly perform pattern - matching. For example, this: - - \True False -> () - - Roughly desugars to: - - \x y -> case (x, y) of - (True, False) -> () - _ -> error "Non-exhaustive patterns" -2. th-desugar does not have guards, as guards are desugared into pattern - matches. For example, this: - - f x y | True <- x - , False <- y - = () - - Roughly desugars to: - - f x y = case (x, y) of - (True, False) -> () - _ -> error "Non-exhaustive patterns" - -In both of these examples, there are multiple expressions being matched on -simultaneously. When desugaring these examples to `case` expressions, we need a -construct that allows us to group these patterns together. Auxiliary tuples are -one way to accomplish this. - -While this use of tuples works well when the arguments have lifted types, such -as Bool, it doesn't work when the arguments have unlifted types, such as Int#. -Imagine desugaring this lambda expression, for instance: - - \27# 42# -> () - -The approach above would desugar this to: - - \x y -> case (x, y) of - (27#, 42#) -> () - _ -> error "Non-exhaustive patterns" - -This will not typecheck, however, as we are using _lifted_ tuples, which -require their arguments to have lifted types. If we want to support unlifted -types, we need a different approach. - -One idea that seems tempting at first is to create an auxiliary `let` -expression, e.g., - - \x y -> - let aux 27# 42# = () - in aux x y - -This avoids having to use lifted tuples, but it creates a new problem: type -inference. In the general case, auxiliary `let` expressions aren't enough to -handle GADT pattern matches, such as in this example: - - data T a where - MkT :: Int -> T Int - - g :: T a -> T a -> a - g = \(MkT x1) (MkT x2) -> x1 + x2 - -If you desugar `g` to use an auxiliary `let` expression: - - g :: T a -> T a -> a - g = \t1 t2 -> - let aux (MkT x1) (MkT x2) = x1 + x2 - in aux t1 t2 - -Then it will not typecheck. To make this work, you'd need to give `aux` a type -signature. Doing this in general is tantamount to performing type inference, -however, which is very challenging in a Template Haskell setting. - -Another approach, which is what th-desugar currently uses, is to use auxiliary -_unboxed_ tuples. This is identical to the previous tuple approach, but with -slightly different syntax: - - \x y -> case (# x, y #) of - (# 27#, 42# #) -> () - _ -> error "Non-exhaustive patterns" - -Unboxed tuples can handle lifted and unlifted arguments alike, so it is capable -of handling all the examples above. - -You might worry that this approach would require clients of th-desugar to -enable the UnboxedTuples extension in non-obvious places, but fortunately, this -is not the case. For one thing, all unboxed tuples produced by th-desugar would -be TH-generated, so we would bypass the need to enable UnboxedTuples to lex -unboxed tuple syntax. GHC's typechecker also imposes a requirement that -UnboxedTuples be enabled if a variable has an unboxed tuple type, but this -never happens in th-desugar by construction. It's possible that a future -version of GHC might be stricter about this, but it seems unlikely. - -There are a couple of exceptions to the general rule that auxiliary binders -should be unboxed: - -1. ParallelListComp is desugared using the `mzip` function, which returns a - lifted pair. As a result, the variables bound in a parallel list - comprehension must be lifted. This is a restriction which is inherited from - GHC itself—https://gitlab.haskell.org/ghc/ghc/-/merge_requests/7270. - -2. Match flattening desugars lazy patterns that bind multiple variables to code - that extracts fields from tuples. For instance, this: - - data Pair a b = MkPair a b - - f :: Pair a b -> Pair b a - f ~(MkPair x y) = MkPair y x - - Desugars to this (roughly) when match-flattened: - - f :: Pair a b -> Pair b a - f p = - let tuple = case p of - MkPair x y -> (x, y) - - x = case tuple of - (x, _) -> x - - y = case tuple of - (_, y) -> x - - in MkPair y x - - One could imagine using an unboxed tuple here instead, but since the - intermediate `tuple` value would have an unboxed tuple this, this would - require users of match flattening to enable UnboxedTuples. Fortunately, - using unboxed tuples here isn't necessary, as GHC doesn't support binding - variables with unlifted types in lazy patterns anyway. -} diff --git a/Language/Haskell/TH/Desugar/Match.hs b/Language/Haskell/TH/Desugar/Match.hs --- a/Language/Haskell/TH/Desugar/Match.hs +++ b/Language/Haskell/TH/Desugar/Match.hs @@ -40,23 +40,24 @@ -- a 'DLitPa', or a 'DWildPa'. scExp :: DsMonad q => DExp -> q DExp scExp (DAppE e1 e2) = DAppE <$> scExp e1 <*> scExp e2 -scExp (DLamE names exp) = DLamE names <$> scExp exp -scExp (DCaseE scrut matches) - | DVarE name <- scrut - = simplCaseExp [name] clauses - | otherwise - = do scrut_name <- newUniqueName "scrut" - case_exp <- simplCaseExp [scrut_name] clauses - return $ DLetE [DValD (DVarP scrut_name) scrut] case_exp - where - clauses = map match_to_clause matches - match_to_clause (DMatch pat exp) = DClause [pat] exp - +scExp (DLamCasesE clauses) = do + -- 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 + clause' <- scClauses num_args clauses + pure $ DLamCasesE [clause'] scExp (DLetE decs body) = DLetE <$> mapM scLetDec decs <*> scExp body scExp (DSigE exp ty) = DSigE <$> scExp exp <*> pure ty scExp (DAppTypeE exp ty) = DAppTypeE <$> scExp exp <*> pure ty scExp (DTypedBracketE exp) = DTypedBracketE <$> scExp exp scExp (DTypedSpliceE exp) = DTypedSpliceE <$> scExp exp +scExp (DForallE tele exp) = DForallE tele <$> scExp exp +scExp (DConstrainedE cxt exp) = DConstrainedE <$> mapM scExp cxt <*> scExp exp scExp e@(DVarE {}) = return e scExp e@(DConE {}) = return e scExp e@(DLitE {}) = return e @@ -65,19 +66,36 @@ -- | Like 'scExp', but for a 'DLetDec'. scLetDec :: DsMonad q => DLetDec -> q DLetDec -scLetDec (DFunD name clauses@(DClause pats1 _ : _)) = do - arg_names <- mapM (const (newUniqueName "_arg")) pats1 - clauses' <- mapM sc_clause_rhs clauses - case_exp <- simplCaseExp arg_names clauses' - return $ DFunD name [DClause (map DVarP arg_names) case_exp] - where - sc_clause_rhs (DClause pats exp) = DClause pats <$> scExp exp +scLetDec (DFunD name clauses) = do + -- `DFunD`s are expected to have a non-empty list of clauses where each clause + -- has a number of patterns equal to the number of arguments. + let num_args = + case clauses of + [] -> error $ "The `" ++ nameBase name ++ + "` function has no clauses -- should never happen" + DClause pats _ : _ -> length pats + clause' <- scClauses num_args clauses + pure $ DFunD name [clause'] scLetDec (DValD pat exp) = DValD pat <$> scExp exp scLetDec (DPragmaD prag) = DPragmaD <$> scLetPragma prag scLetDec dec@(DSigD {}) = return dec scLetDec dec@(DInfixD {}) = return dec -scLetDec dec@(DFunD _ []) = return dec +-- | Convert a list of 'DClause's into a single 'DClause', where the right-hand +-- side of the output 'DClause' matches on all of the patterns of the input +-- 'DClause's without using nested pattern matching. +scClauses :: + DsMonad q + => Int -- ^ The number of arguments in each 'DClause'. + -> [DClause] -> q DClause +scClauses num_args clauses = do + arg_names <- replicateM num_args (newUniqueName "_arg") + clauses' <- mapM sc_clause_rhs clauses + case_exp <- simplCaseExp arg_names clauses' + pure $ DClause (map DVarP arg_names) case_exp + where + sc_clause_rhs (DClause pats exp) = DClause pats <$> scExp exp + scLetPragma :: DsMonad q => DPragma -> q DPragma scLetPragma = topEverywhereM scExp -- Only topEverywhereM because scExp already recurses on its own @@ -189,7 +207,34 @@ | new == old = id | otherwise = DLetE [DValD (DVarP new) (DVarE old)] --- like GHC's mkSelectorBinds +-- | Desugar a lazy pattern that bind multiple variables to code that extracts +-- fields from tuples. For instance, this: +-- +-- @ +-- data Pair a b = MkPair a b +-- +-- f :: Pair a b -> Pair b a +-- f ~(MkPair x y) = MkPair y x +-- @ +-- +-- Desugars to this (roughly) when match-flattened: +-- +-- @ +-- f :: Pair a b -> Pair b a +-- f p = +-- let tuple = case p of +-- MkPair x y -> (x, y) +-- +-- x = case tuple of +-- (x, _) -> x +-- +-- y = case tuple of +-- (_, y) -> x +-- +-- in MkPair y x +-- @ +-- +-- This takes heavy inspiration from GHC's own @mkSelectorBinds@ function. mkSelectorDecs :: DsMonad q => DPat -- pattern to deconstruct -> Name -- variable being matched against @@ -227,7 +272,7 @@ -> q DExp mk_projection tup_name i = do var_name <- newUniqueName "proj" - return $ DCaseE (DVarE tup_name) [DMatch (DConP (tupleDataName tuple_size) [] (mk_tuple_pats var_name i)) + return $ dCaseE (DVarE tup_name) [DMatch (DConP (tupleDataName tuple_size) [] (mk_tuple_pats var_name i)) (DVarE var_name)] mk_tuple_pats :: Name -- of the projected element @@ -332,7 +377,7 @@ all_ctors <- get_all_ctors (alt_con $ NE.head case_alts) return $ \fail -> let matches = fmap (mk_alt fail) case_alt_list in - DCaseE (DVarE var) (matches ++ mk_default all_ctors fail) + dCaseE (DVarE var) (matches ++ mk_default all_ctors fail) where case_alt_list = NE.toList case_alts @@ -361,7 +406,7 @@ matchEmpty :: DsMonad q => Name -> q [MatchResult] matchEmpty var = return [mk_seq] where - mk_seq fail = DCaseE (DVarE var) [DMatch DWildP fail] + mk_seq fail = dCaseE (DVarE var) [DMatch DWildP fail] matchLiterals :: DsMonad q => NonEmpty Name -> NonEmpty (NonEmpty EquationInfo) -> q MatchResult matchLiterals (var:|vars) sub_groups @@ -383,7 +428,7 @@ mkCoPrimCaseMatchResult var match_alts = mk_case where mk_case fail = let alts = NE.toList $ fmap (mk_alt fail) match_alts in - DCaseE (DVarE var) (alts ++ [DMatch DWildP fail]) + dCaseE (DVarE var) (alts ++ [DMatch DWildP fail]) mk_alt fail (lit, body_fn) = DMatch (DLitP lit) (body_fn fail) diff --git a/Language/Haskell/TH/Desugar/Reify.hs b/Language/Haskell/TH/Desugar/Reify.hs --- a/Language/Haskell/TH/Desugar/Reify.hs +++ b/Language/Haskell/TH/Desugar/Reify.hs @@ -53,6 +53,7 @@ import Language.Haskell.TH.Datatype.TyVarBndr import Language.Haskell.TH.Instances () import Language.Haskell.TH.Syntax hiding ( lift ) +import qualified Language.Haskell.TH.Syntax.Compat as Compat ( Quote ) import Language.Haskell.TH.Desugar.Util as Util @@ -202,7 +203,8 @@ -- | A convenient implementation of the 'DsMonad' class. Use by calling -- 'withLocalDeclarations'. newtype DsM q a = DsM (ReaderT [Dec] q a) - deriving ( Functor, Applicative, Monad, MonadTrans, Quasi, Fail.MonadFail + deriving ( Functor, Applicative, Monad, MonadTrans, Fail.MonadFail + , Quasi, Compat.Quote #if __GLASGOW_HASKELL__ >= 803 , MonadIO #endif @@ -283,14 +285,25 @@ #endif reifyInDec n decs (DataD _ ty_name tvbs _mk cons _) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) cons + | Just info <- maybeReifyCon n decs ty_name + (matchUpSAKWithTvbsSpec decs ty_name tvbs) + (applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs)) + cons = Just info reifyInDec n decs (NewtypeD _ ty_name tvbs _mk con _) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) [con] + | Just info <- maybeReifyCon n decs ty_name + (matchUpSAKWithTvbsSpec decs ty_name tvbs) + (applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs)) + [con] = Just info -reifyInDec n _decs (ClassD _ ty_name tvbs _ sub_decs) +reifyInDec n decs (ClassD _ cls_name cls_tvbs _ sub_decs) | Just (n', ty) <- findType n sub_decs - = Just (n', ClassOpI n (quantifyClassMethodType ty_name tvbs True ty) ty_name) + = Just (n', ClassOpI n + (quantifyClassMethodType + (matchUpSAKWithTvbsSpec decs cls_name cls_tvbs) + (applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)) + True ty) + cls_name) reifyInDec n decs (ClassD _ _ _ _ sub_decs) | Just info <- firstMatch (reifyInDec n decs) sub_decs -- Important: don't pass (sub_decs ++ decs) to reifyInDec @@ -310,32 +323,66 @@ = Just (n', VarI n full_sel_ty Nothing) #endif #if __GLASGOW_HASKELL__ >= 807 -reifyInDec n decs (DataInstD _ _ lhs _ cons _) +reifyInDec n decs (DataInstD _ mtvbs lhs _ cons _) | (ConT ty_name, tys) <- unfoldType lhs - , Just info <- maybeReifyCon n decs ty_name tys cons + , Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbs mtvbs tys) + -- Why do we reapply `ty_name` to `tys` here instead of just + -- reusing `lhs`? See Note [Apply data family type + -- constructors in prefix form in local reification]. + (applyType (ConT ty_name) tys) + cons = Just info -reifyInDec n decs (NewtypeInstD _ _ lhs _ con _) +reifyInDec n decs (NewtypeInstD _ mtvbs lhs _ con _) | (ConT ty_name, tys) <- unfoldType lhs - , Just info <- maybeReifyCon n decs ty_name tys [con] + , Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbs mtvbs tys) + -- Why do we reapply `ty_name` to `tys` here instead of just + -- reusing `lhs`? See Note [Apply data family type + -- constructors in prefix form in local reification]. + (applyType (ConT ty_name) tys) + [con] = Just info #else reifyInDec n decs (DataInstD _ ty_name tys _ cons _) - | Just info <- maybeReifyCon n decs ty_name (map TANormal tys) cons + | Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbsNoInstTvbs tys) + (applyType (ConT ty_name) (map TANormal tys)) + cons = Just info reifyInDec n decs (NewtypeInstD _ ty_name tys _ con _) - | Just info <- maybeReifyCon n decs ty_name (map TANormal tys) [con] + | Just info <- maybeReifyCon n decs ty_name + (dataFamInstH98ConTvbsNoInstTvbs tys) + (applyType (ConT ty_name) (map TANormal tys)) + [con] = Just info #endif #if __GLASGOW_HASKELL__ >= 906 reifyInDec n decs (TypeDataD ty_name tvbs _mk cons) - | Just info <- maybeReifyCon n decs ty_name (map tyVarBndrVisToTypeArgWithSig tvbs) cons + | Just info <- maybeReifyCon n decs ty_name + (matchUpSAKWithTvbsSpec decs ty_name tvbs) + (applyType (ConT ty_name) (map tyVarBndrVisToTypeArg tvbs)) + cons = Just info #endif reifyInDec _ _ _ = Nothing -maybeReifyCon :: Name -> [Dec] -> Name -> [TypeArg] -> [Con] -> Maybe (Named Info) -maybeReifyCon n _decs ty_name ty_args cons +maybeReifyCon :: + Name + -> [Dec] + -> Name + -> [TyVarBndrSpec] + -- ^ The universally quantified type variables, derived from the parent + -- data declaration. This is only used if reifying a Haskell98-style data + -- constructor. + -> Type + -- ^ The data constructor's return type, derived from the parent data + -- declaration. This is only used if reifying a Haskell98-style data + -- constructor. + -> [Con] + -> Maybe (Named Info) +maybeReifyCon n _decs ty_name h98_tvbs h98_res_ty cons | Just (n', con) <- findCon n cons -- See Note [Use unSigType in maybeReifyCon] , let full_con_ty = unSigType $ con_to_type h98_tvbs h98_res_ty con @@ -355,7 +402,10 @@ extract_rec_sel_info rec_sel_info = case rec_sel_info of RecSelH98 sel_ty -> - ( changeTVFlags SpecifiedSpec h98_tvbs + let -- All of the type variables bound by the data type, with any + -- implicitly quantified kind variables made explicit. + all_h98_tvbs = quantifyAllTvbsSpec h98_tvbs in + ( all_h98_tvbs , sel_ty , h98_res_ty ) @@ -374,11 +424,7 @@ , con_res_ty ) - h98_tvbs = freeVariablesWellScoped $ - map probablyWrongUnTypeArg ty_args - h98_res_ty = applyType (ConT ty_name) ty_args - -maybeReifyCon _ _ _ _ _ = Nothing +maybeReifyCon _ _ _ _ _ _ = Nothing #if __GLASGOW_HASKELL__ >= 801 -- | Attempt to reify the type of a pattern synonym record selector @n@. @@ -537,10 +583,36 @@ This is contrast to GHC's own reification, which will produce `D a` (without the explicit kind signature) as the type of the first argument. + +Note [Apply data family type constructors in prefix form in local reification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we wish to locally reify the type of `MkD` below: + + data family a :&: b + data instance a :&: b = MkD a b + +You might be tempted to think that the return type should be: + + MkD :: a -> b -> a :&: b + +However, keep in mind that local reification tries its best to mimic GHC's +behavior when reifying global declarations using Template Haskell. As it turns +out, if `MkD` were defined globally, then Template Haskell would reify it as: + + MkD :: a -> b -> (:&:) a b + +Note that `(:&:)` is applied prefix, not infix! This is somewhat surprising, +but nevertheless valid code. We mimic this surprising behavior when locally +reifying data family instances such as (:&:). This means that we cannot just +reuse the type `a :&: b` in the return type of `MkD`. Instead, we must +decompose `a :&: b` into its type arguments and apply (:&:) (in prefix form) to +the type arguments. + +The R40 test case checks for this property. -} -- Reverse-engineer the type of a data constructor. -con_to_type :: [TyVarBndrUnit] -- The type variables bound by a data type head. +con_to_type :: [TyVarBndrSpec] -- The type variables bound by a data type head. -- Only used for Haskell98-style constructors. -> Type -- The constructor result type. -- Only used for Haskell98-style constructors. @@ -548,9 +620,7 @@ con_to_type h98_tvbs h98_result_ty con = case go con of (is_gadt, ty) | is_gadt -> ty - | otherwise -> maybeForallT - (changeTVFlags SpecifiedSpec h98_tvbs) - [] ty + | otherwise -> maybeForallT all_h98_tvbs [] ty where -- Note that we deliberately ignore linear types and use (->) everywhere. -- See [Gracefully handling linear types] in L.H.TH.Desugar.Core. @@ -562,6 +632,11 @@ go (GadtC _ stys rty) = (True, mkArrows (map snd stys) rty) go (RecGadtC _ vstys rty) = (True, mkArrows (map thdOf3 vstys) rty) + -- All of the type variables bound by the data type, with any implicitly + -- quantified kind variables made explicit. + all_h98_tvbs :: [TyVarBndrSpec] + all_h98_tvbs = quantifyAllTvbsSpec h98_tvbs + mkVarI :: Name -> [Dec] -> Info mkVarI n decs = mkVarITy n (maybe (no_type n) snd $ findType n decs) @@ -710,7 +785,11 @@ sub_decs' = mapMaybe go sub_decs go (SigD n ty) = Just $ SigD n - $ quantifyClassMethodType cls_name cls_tvbs prepend_cls ty + $ quantifyClassMethodType + (changeTVFlags SpecifiedSpec cls_tvbs) + (applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)) + prepend_cls + ty go d@(TySynInstD {}) = Just d go d@(OpenTypeFamilyD {}) = Just d go d@(DataFamilyD {}) = Just d @@ -731,8 +810,8 @@ -- [d| class C a where -- method :: a -> b -> a |] -- --- If one invokes `quantifyClassMethodType C [a] prepend (a -> b -> a)`, then --- the output will be: +-- If one invokes `quantifyClassMethodType [a] (C a) prepend (a -> b -> a)`, +-- then the output will be: -- -- 1. `forall a. C a => forall b. a -> b -> a` (if `prepend` is True) -- 2. `forall b. a -> b -> a` (if `prepend` is False) @@ -744,22 +823,19 @@ -- a single class method, like `method`, then one needs the class context to -- appear in the reified type, so `True` is appropriate. quantifyClassMethodType - :: Name -- ^ The class name. - -> [TyVarBndrVis] -- ^ The class's type variable binders. - -> Bool -- ^ If 'True', prepend a class predicate. - -> Type -- ^ The method type. + :: [TyVarBndrSpec] -- ^ The class's type variable binders. + -> Pred -- ^ The class context. + -> Bool -- ^ If 'True', prepend a class predicate. + -> Type -- ^ The method type. -> Type -quantifyClassMethodType cls_name cls_tvbs prepend meth_ty = +quantifyClassMethodType cls_tvbs cls_pred prepend meth_ty = add_cls_cxt quantified_meth_ty where add_cls_cxt :: Type -> Type add_cls_cxt - | prepend = ForallT (changeTVFlags SpecifiedSpec all_cls_tvbs) cls_cxt + | prepend = ForallT all_cls_tvbs [cls_pred] | otherwise = id - cls_cxt :: Cxt - cls_cxt = [applyType (ConT cls_name) (map tyVarBndrVisToTypeArg cls_tvbs)] - quantified_meth_ty :: Type quantified_meth_ty | null meth_tvbs @@ -770,13 +846,15 @@ = ForallT meth_tvbs [] meth_ty meth_tvbs :: [TyVarBndrSpec] - meth_tvbs = changeTVFlags SpecifiedSpec $ - List.deleteFirstsBy ((==) `on` tvName) - (freeVariablesWellScoped [meth_ty]) all_cls_tvbs + meth_tvbs = List.deleteFirstsBy ((==) `on` tvName) + (changeTVFlags SpecifiedSpec + (freeVariablesWellScoped [meth_ty])) + all_cls_tvbs - -- Explicitly quantify any kind variables bound by the class, if any. - all_cls_tvbs :: [TyVarBndrUnit] - all_cls_tvbs = freeVariablesWellScoped $ map tvbToTypeWithSig cls_tvbs + -- All of the type variables bound by the class, with any implicitly + -- quantified kind variables made explicit. + all_cls_tvbs :: [TyVarBndrSpec] + all_cls_tvbs = quantifyAllTvbsSpec cls_tvbs stripInstanceDec :: Dec -> Dec stripInstanceDec (InstanceD over cxt ty _) = InstanceD over cxt ty [] @@ -874,6 +952,64 @@ where ret_fvs = Set.fromList $ freeVariables [ret_ty] +-- | Match up the type variable binders from a data type or class declaration +-- with its standalone kind signature (if any) to produce a list of +-- 'TyVarBndrSpec's, which can then be used in the types of data constructors or +-- class methods. This makes the kinds more precise. +matchUpSAKWithTvbsSpec :: + [Dec] + -- ^ The local declarations currently in scope. + -> Name + -- ^ The name of the data type or class declaration. + -> [TyVarBndrVis] + -- ^ The data type or class declaration's type variable binders. + -> [TyVarBndrSpec] +matchUpSAKWithTvbsSpec decs ty_name tvbs = + fromMaybe (changeTVFlags SpecifiedSpec tvbs) $ do + sak <- findKind False ty_name decs + tvbForAllTyFlagsToSpecs <$> matchUpSAKWithDecl sak tvbs + +-- | Compute the type variable binders to use in the type of a Haskell98-style +-- data constructor for a data family instance. If the data family instance +-- comes equipped with explicit type variable binders, this is easy. If not, +-- we must compute the type variable binders from the list of type arguments to +-- the data family instance. +dataFamInstH98ConTvbs :: Maybe [TyVarBndrUnit] -> [TypeArg] -> [TyVarBndrSpec] +dataFamInstH98ConTvbs mtvbs tys = + case mtvbs of + Just tvbs -> + changeTVFlags SpecifiedSpec tvbs + Nothing -> + dataFamInstH98ConTvbsNoInstTvbs $ + map probablyWrongUnTypeArg tys + +-- | Compute the type variable binders to use in the type of a Haskell98-style +-- data constructor for a data family instance where the instance lacks explicit +-- type variable binders. To compute these binders, we must reverse engineer +-- them from the list of type arguments to the data family instance. +dataFamInstH98ConTvbsNoInstTvbs :: [Type] -> [TyVarBndrSpec] +dataFamInstH98ConTvbsNoInstTvbs tys = + changeTVFlags SpecifiedSpec $ + freeVariablesWellScoped tys + +-- | Explicitly quantify all type variable binders in the type of a +-- Haskell98-style data constructor or class method. This is sometimes required +-- in order to ensure that kind variables are all explicitly quantified, e.g., +-- +-- @ +-- -- NB: No standalone kind signature for `T` +-- data T (a :: k) = MkT +-- @ +-- +-- We want the type of @MkT@ to be @forall k (a :: k). T a@, but we are only +-- given @(a :: k)@. We must call 'quantifyAllTvbsSpec' on @(a :: k)@ to obtain +-- @[k, a :: k]@. If we don't, we might accidentally end up with +-- @forall (a :: k). T a@ as the type of @MkT@, which is ill-scoped. +quantifyAllTvbsSpec :: [TyVarBndrSpec] -> [TyVarBndrSpec] +quantifyAllTvbsSpec h98_tvbs = + let h98_kvbs = freeKindVariablesWellScoped h98_tvbs in + changeTVFlags SpecifiedSpec h98_kvbs ++ h98_tvbs + --------------------------------- -- Reifying fixities --------------------------------- @@ -985,7 +1121,7 @@ cls_tvb_kind_map = Map.fromList [ (tvName tvb, tvb_kind) | (tvb, mb_vis_arg_ki) <- zip tvbs mb_vis_arg_kis - , Just tvb_kind <- [mb_vis_arg_ki <|> tvb_kind_maybe tvb] + , Just tvb_kind <- [mb_vis_arg_ki <|> extractTvbKind_maybe tvb] ] = firstMatch (find_assoc_type_kind n cls_tvb_kind_map) sub_decs match_kind_sig n _ dec = find_kind_sig n dec @@ -1027,7 +1163,7 @@ all tvb_is_kinded tvbs , let cls_tvb_kind_map = Map.fromList [ (tvName tvb, tvb_kind) | tvb <- tvbs - , Just tvb_kind <- [tvb_kind_maybe tvb] + , Just tvb_kind <- [extractTvbKind_maybe tvb] ] = firstMatch (find_assoc_type_kind n cls_tvb_kind_map) sub_decs #if __GLASGOW_HASKELL__ >= 906 @@ -1163,13 +1299,10 @@ #endif tvb_is_kinded :: TyVarBndr_ flag -> Bool -tvb_is_kinded = isJust . tvb_kind_maybe - -tvb_kind_maybe :: TyVarBndr_ flag -> Maybe Kind -tvb_kind_maybe = elimTV (\_ -> Nothing) (\_ k -> Just k) +tvb_is_kinded = isJust . extractTvbKind_maybe vis_arg_kind_maybe :: VisFunArg -> Maybe Kind -vis_arg_kind_maybe (VisFADep tvb) = tvb_kind_maybe tvb +vis_arg_kind_maybe (VisFADep tvb) = extractTvbKind_maybe tvb vis_arg_kind_maybe (VisFAAnon k) = Just k default_tvb :: TyVarBndr_ flag -> TyVarBndr_ flag @@ -1181,7 +1314,7 @@ res_sig_to_kind :: FamilyResultSig -> Maybe Kind res_sig_to_kind NoSig = Nothing res_sig_to_kind (KindSig k) = Just k -res_sig_to_kind (TyVarSig tvb) = tvb_kind_maybe tvb +res_sig_to_kind (TyVarSig tvb) = extractTvbKind_maybe tvb whenAlt :: Alternative f => Bool -> f a -> f a whenAlt b fa = if b then fa else empty diff --git a/Language/Haskell/TH/Desugar/Subst.hs b/Language/Haskell/TH/Desugar/Subst.hs --- a/Language/Haskell/TH/Desugar/Subst.hs +++ b/Language/Haskell/TH/Desugar/Subst.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE CPP #-} - ----------------------------------------------------------------------------- -- | -- Module : Language.Haskell.TH.Desugar.Subst @@ -9,7 +7,9 @@ -- Stability : experimental -- Portability : non-portable -- --- Capture-avoiding substitutions on 'DType's +-- Capture-avoiding substitutions on 'DType's. (For non–capture-avoiding +-- substitution functions, use "Language.Haskell.TH.Desugar.Subst.Capturing" +-- instead.) -- ---------------------------------------------------------------------------- @@ -17,7 +17,7 @@ DSubst, -- * Capture-avoiding substitution - substTy, substForallTelescope, substTyVarBndrs, + substTy, substForallTelescope, substTyVarBndrs, substTyVarBndr, unionSubsts, unionMaybeSubsts, -- * Matching a type template against a type @@ -29,13 +29,15 @@ import qualified Data.Set as S import Language.Haskell.TH.Desugar.AST -import Language.Haskell.TH.Syntax import Language.Haskell.TH.Desugar.Util +import Language.Haskell.TH.Syntax --- | A substitution is just a map from names to types +-- | A substitution is just a map from names to types. type DSubst = M.Map Name DType --- | Capture-avoiding substitution on types +-- | Capture-avoiding substitution on 'DType's. This function requires a 'Quasi' +-- constraint because it may need to create fresh names in order to avoid +-- capture when substituting into a @forall@ type (see 'substTyVarBndr'). substTy :: Quasi q => DSubst -> DType -> q DType substTy vars (DForallT tele ty) = do (vars', tele') <- substForallTelescope vars tele @@ -59,6 +61,10 @@ substTy _ ty@(DLitT _) = return ty substTy _ ty@DWildCardT = return ty +-- | Capture-avoiding substitution on 'DForallTelescope's. This returns a pair +-- containing the new 'DSubst' as well as a new 'DForallTelescope' value, where +-- the names have been renamed to avoid capture and the kinds have been +-- substituted. substForallTelescope :: Quasi q => DSubst -> DForallTelescope -> q (DSubst, DForallTelescope) substForallTelescope vars tele = @@ -70,16 +76,25 @@ (vars', tvbs') <- substTyVarBndrs vars tvbs return (vars', DForallInvis tvbs') +-- | Capture-avoiding substitution on a telescope of 'DTyVarBndr's. This returns +-- a pair containing the new 'DSubst' as well as a new telescope of +-- 'DTyVarBndr's, where the names have been renamed to avoid capture and the +-- kinds have been substituted. substTyVarBndrs :: Quasi q => DSubst -> [DTyVarBndr flag] -> q (DSubst, [DTyVarBndr flag]) -substTyVarBndrs = mapAccumLM substTvb +substTyVarBndrs = mapAccumLM substTyVarBndr -substTvb :: Quasi q => DSubst -> DTyVarBndr flag +-- | Capture-avoiding substitution on a 'DTyVarBndr'. This uses the 'Quasi' +-- constraint to create a new, fresh name (based on the name of the supplied +-- 'DTyVarBndr'), update the 'DSubst' to map from the old name to the new name, +-- and this also returns a 'DTyVarBndr' containing the new name and the kind of +-- the supplied 'DTyVarBndr' (with the substitution applied). +substTyVarBndr :: Quasi q => DSubst -> DTyVarBndr flag -> q (DSubst, DTyVarBndr flag) -substTvb vars (DPlainTV n flag) = do +substTyVarBndr vars (DPlainTV n flag) = do new_n <- qNewName (nameBase n) return (M.insert n (DVarT new_n) vars, DPlainTV new_n flag) -substTvb vars (DKindedTV n flag k) = do +substTyVarBndr vars (DKindedTV n flag k) = do new_n <- qNewName (nameBase n) k' <- substTy vars k return (M.insert n (DVarT new_n) vars, DKindedTV new_n flag k') diff --git a/Language/Haskell/TH/Desugar/Subst/Capturing.hs b/Language/Haskell/TH/Desugar/Subst/Capturing.hs new file mode 100644 --- /dev/null +++ b/Language/Haskell/TH/Desugar/Subst/Capturing.hs @@ -0,0 +1,77 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Language.Haskell.TH.Desugar.Subst.Capturing +-- Copyright : (C) 2024 Ryan Scott +-- License : BSD-style (see LICENSE) +-- Maintainer : Ryan Scott +-- Stability : experimental +-- Portability : non-portable +-- +-- Substitutions on 'DType's that do /not/ avoid capture. (For capture-avoiding +-- substitution functions, use "Language.Haskell.TH.Desugar.Subst" instead.) +-- +---------------------------------------------------------------------------- + +module Language.Haskell.TH.Desugar.Subst.Capturing ( + DSubst, + + -- * Non–capture-avoiding substitution + substTy, substForallTelescope, substTyVarBndrs, substTyVarBndr, + unionSubsts, unionMaybeSubsts, + + -- * Matching a type template against a type + IgnoreKinds(..), matchTy + ) where + +import Data.Bifunctor (second) +import qualified Data.List as L +import qualified Data.Map as M + +import Language.Haskell.TH.Desugar.AST +import Language.Haskell.TH.Desugar.Subst + (DSubst, unionSubsts, unionMaybeSubsts, IgnoreKinds(..), matchTy) + +-- | Non–capture-avoiding substitution on 'DType's. Unlike the @substTy@ +-- function in "Language.Haskell.TH.Desugar.Subst", this 'substTy' function is +-- pure, as it never needs to create fresh names. +substTy :: DSubst -> DType -> DType +substTy subst ty | M.null subst = ty +substTy subst (DForallT tele inner_ty) + = DForallT tele' inner_ty' + where + (subst', tele') = substForallTelescope subst tele + inner_ty' = substTy subst' inner_ty +substTy subst (DConstrainedT cxt inner_ty) = + DConstrainedT (map (substTy subst) cxt) (substTy subst inner_ty) +substTy subst (DAppT ty1 ty2) = substTy subst ty1 `DAppT` substTy subst ty2 +substTy subst (DAppKindT ty ki) = substTy subst ty `DAppKindT` substTy subst ki +substTy subst (DSigT ty ki) = substTy subst ty `DSigT` substTy subst ki +substTy subst (DVarT n) = + case M.lookup n subst of + Just ki -> ki + Nothing -> DVarT n +substTy _ ty@(DConT {}) = ty +substTy _ ty@(DArrowT) = ty +substTy _ ty@(DLitT {}) = ty +substTy _ ty@DWildCardT = ty + +-- | Non–capture-avoiding substitution on 'DForallTelescope's. This returns a +-- pair containing the new 'DSubst' as well as a new 'DForallTelescope' value, +-- where the kinds have been substituted. +substForallTelescope :: DSubst -> DForallTelescope -> (DSubst, DForallTelescope) +substForallTelescope s (DForallInvis tvbs) = second DForallInvis $ substTyVarBndrs s tvbs +substForallTelescope s (DForallVis tvbs) = second DForallVis $ substTyVarBndrs s tvbs + +-- | Non–capture-avoiding substitution on a telescope of 'DTyVarBndr's. This +-- returns a pair containing the new 'DSubst' as well as a new telescope of +-- 'DTyVarBndr's, where the kinds have been substituted. +substTyVarBndrs :: DSubst -> [DTyVarBndr flag] -> (DSubst, [DTyVarBndr flag]) +substTyVarBndrs = L.mapAccumL substTyVarBndr + +-- | Non–capture-avoiding substitution on a 'DTyVarBndr'. This updates the +-- 'DSubst' to remove the 'DTyVarBndr' name from the domain (as that name is now +-- bound by the 'DTyVarBndr') and applies the substitution to the kind of the +-- 'DTyVarBndr'. +substTyVarBndr :: DSubst -> DTyVarBndr flag -> (DSubst, DTyVarBndr flag) +substTyVarBndr s tvb@(DPlainTV n _) = (M.delete n s, tvb) +substTyVarBndr s (DKindedTV n f k) = (M.delete n s, DKindedTV n f (substTy s k)) diff --git a/Language/Haskell/TH/Desugar/Sweeten.hs b/Language/Haskell/TH/Desugar/Sweeten.hs --- a/Language/Haskell/TH/Desugar/Sweeten.hs +++ b/Language/Haskell/TH/Desugar/Sweeten.hs @@ -51,8 +51,6 @@ expToTH (DConE n) = ConE n expToTH (DLitE l) = LitE l expToTH (DAppE e1 e2) = AppE (expToTH e1) (expToTH e2) -expToTH (DLamE names exp) = LamE (map VarP names) (expToTH exp) -expToTH (DCaseE exp matches) = CaseE (expToTH exp) (map matchToTH matches) expToTH (DLetE decs exp) = LetE (map letDecToTH decs) (expToTH exp) expToTH (DSigE exp ty) = SigE (expToTH exp) (typeToTH ty) expToTH (DStaticE exp) = StaticE (expToTH exp) @@ -63,6 +61,64 @@ -- type applications, we will simply drop the applied type. expToTH (DAppTypeE exp _) = expToTH exp #endif +expToTH (DLamCasesE clauses) + -- In the source language, `\cases` expressions must have at least one clause. + -- As such, we adopt the convention that a DLamCasesE value with no clauses + -- shall sweeten to a `\case{}` expression. Unlike `\cases`, it is legal for + -- `\case` to have no clauses, and `\case{}` is assumed to have a single + -- argument. + | null clauses + = LamCaseE [] +#if __GLASGOW_HASKELL__ >= 904 + -- If building with GHC 9.4 or later, sweetening a DLamCasesE value is as + -- simple as using LamCasesE... + | otherwise + = LamCasesE (map clauseToTH clauses) +#else + -- ...but if we are building with a pre-9.4 version of GHC, we do not have + -- access to LamCasesE, making our life harder. We want to have at least + -- /some/ support for sweetening DLamCasesE values, since we desugar simpler + -- language constructs like lambda, `case`, and `\case` expressions to + -- DLamCasesE, and we'd like to be able to sweeten them back. + -- + -- Therefore, we add special treatment for DLamCasesE values that look simpler + -- language constructs and sweeten these back to LamE, LamCaseE, etc. If we + -- encounter anything more complicated, we give up and raise an error. + + -- Special case: if a DLamCasesE value has exactly one clause, we can sweeten + -- the DLamCasesE value as though it were a lambda expression (LamE). + | [DClause pats exp] <- clauses + = LamE (map patToTH pats) (expToTH exp) + -- Special case: if a DLamCasesE value's clauses each have exactly one + -- pattern, we can sweeten the DLamCasesE value as though it were a `\case` + -- expression (LamCaseE). + | Just matches <- traverse dMatch_maybe clauses + = LamCaseE (map matchToTH matches) + -- NB: You might wonder why there is not another special case that returns + -- CaseE for things that look like `case` expressions. This is because the + -- special case for LamCaseE above already suffices. Note that we desugar + -- `case` expressions to code that looks like this: + -- + -- (\cases + -- pat_1 -> rhs_1 + -- ... + -- pat_n -> rhs_n) scrut + -- + -- That is, a value that looks like `DAppE (DLamCasesE ...) scrut`. Each + -- clause in the DLamCasesE value has exactly one pattern, however. Therefore, + -- because of the special treatment for LamCaseE above, this code would + -- sweeten to `AppE (LamCaseE ...) scrut`. + + -- If we lack a special case for the DLamCasesE value, then we raise an error. + | otherwise + = error $ unlines + [ "Non-trivial \\cases expressions supported only in GHC 9.4+." + , "Here, \"non-trivial\" means that the \\cases expression cannot easily" + , "be rewritten to a lambda, case, or \\case expression without" + , "significantly rewriting the expression. Either rewrite the expression" + , "yourself or upgrade to a later version of GHC." + ] +#endif #if __GLASGOW_HASKELL__ >= 907 expToTH (DTypedBracketE exp) = TypedBracketE (expToTH exp) expToTH (DTypedSpliceE exp) = TypedSpliceE (expToTH exp) @@ -77,6 +133,20 @@ #else expToTH (DTypeE {}) = error "Embedded type expressions supported only in GHC 9.10+" +#endif +#if __GLASGOW_HASKELL__ >= 911 +expToTH (DForallE tele exp) = + case tele of + DForallInvis tvbs -> ForallE (map tvbToTH tvbs) exp' + DForallVis tvbs -> ForallVisE (map tvbToTH tvbs) exp' + where + exp' = expToTH exp +expToTH (DConstrainedE cxt exp) = ConstrainedE (map expToTH cxt) (expToTH exp) +#else +expToTH (DForallE {}) = + error "Embedded `forall`s supported only in GHC 9.12+" +expToTH (DConstrainedE {}) = + error "Embedded constraints supported only in GHC 9.12+" #endif matchToTH :: DMatch -> Match diff --git a/Language/Haskell/TH/Desugar/Util.hs b/Language/Haskell/TH/Desugar/Util.hs --- a/Language/Haskell/TH/Desugar/Util.hs +++ b/Language/Haskell/TH/Desugar/Util.hs @@ -16,7 +16,7 @@ nameOccursIn, allNamesIn, mkTypeName, mkDataName, mkNameWith, isDataName, stripVarP_maybe, extractBoundNamesStmt, concatMapM, mapAccumLM, mapMaybeM, expectJustM, - stripPlainTV_maybe, + stripPlainTV_maybe, extractTvbKind_maybe, thirdOf3, splitAtList, extractBoundNamesDec, extractBoundNamesPat, tvbToType, tvbToTypeWithSig, @@ -30,27 +30,42 @@ TypeArg(..), applyType, filterTANormals, probablyWrongUnTypeArg, tyVarBndrVisToTypeArg, tyVarBndrVisToTypeArgWithSig, bindIP, - DataFlavor(..) + DataFlavor(..), + freeKindVariablesWellScoped, + ForAllTyFlag(..), tvbForAllTyFlagsToSpecs, tvbForAllTyFlagsToBndrVis, + matchUpSAKWithDecl ) where import Prelude hiding (mapM, foldl, concatMap, any) import Language.Haskell.TH hiding ( cxt ) +import Language.Haskell.TH.Datatype import Language.Haskell.TH.Datatype.TyVarBndr import qualified Language.Haskell.TH.Desugar.OSet as OS import Language.Haskell.TH.Desugar.OSet (OSet) +import Language.Haskell.TH.Instances () import Language.Haskell.TH.Syntax import qualified Control.Monad.Fail as Fail import Data.Foldable -import qualified Data.Kind as Kind +import Data.Function ( on ) import Data.Generics ( Data, Typeable, everything, extM, gmapM, mkQ ) -import Data.Traversable +import qualified Data.Kind as Kind +import qualified Data.List as List +import qualified Data.Map as Map +import Data.Map ( Map ) import Data.Maybe +import qualified Data.Set as Set +import Data.Traversable import GHC.Classes ( IP ) import GHC.Generics ( Generic ) import Unsafe.Coerce ( unsafeCoerce ) +#if __GLASGOW_HASKELL__ >= 900 +import Language.Haskell.TH.Ppr ( PprFlag(..) ) +import qualified Language.Haskell.TH.PprLib as Ppr +#endif + #if __GLASGOW_HASKELL__ >= 906 import GHC.Tuple ( Solo(MkSolo) ) #elif __GLASGOW_HASKELL__ >= 900 @@ -118,6 +133,11 @@ stripPlainTV_maybe :: TyVarBndr_ flag -> Maybe Name stripPlainTV_maybe = elimTV Just (\_ _ -> Nothing) +-- | Extracts the kind from a 'TyVarBndr'. Returns @'Just' k@ if the 'TyVarBndr' +-- is a 'KindedTV' and returns 'Nothing' if it is a 'PlainTV'. +extractTvbKind_maybe :: TyVarBndr_ flag -> Maybe Kind +extractTvbKind_maybe = elimTV (\_ -> Nothing) (\_ k -> Just k) + -- | Report that a certain TH construct is impossible impossible :: Fail.MonadFail q => String -> q a impossible err = Fail.fail (err ++ "\n This should not happen in Haskell.\n Please email rae@cs.brynmawr.edu with your code if you see this.") @@ -542,6 +562,487 @@ probablyWrongUnTypeArg (TANormal t) = t probablyWrongUnTypeArg (TyArg k) = k +------------------------------------------------------------------------------- +-- Matching standalone kind signatures with binders in type-level declarations +------------------------------------------------------------------------------- + +-- @'matchUpSAKWithDecl' decl_sak decl_bndrs@ produces @TyVarBndr' +-- 'ForAllTyFlag'@s for a declaration, using the original declaration's +-- standalone kind signature (@decl_sak@) and its user-written binders +-- (@decl_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 @'TyVarBndr' 'ForAllTyFlag'@s: +-- +-- @ +-- \@j \@l (a :: l) (b :: j) +-- @ +-- +-- From here, these @'TyVarBndr' 'ForAllTyFlag'@s can be converted into other +-- forms of 'TyVarBndr's: +-- +-- * They can be converted to 'TyVarBndrSpec's using 'tvbForAllTyFlagsToSpecs'. +-- +-- * They can be converted to 'TyVarBndrVis'es using 'tvbForAllTyFlagsToVis'. +-- +-- Note that: +-- +-- * This function has a precondition that the length of @decl_bndrs@ must +-- always be equal to the number of visible quantifiers (i.e., the number of +-- function arrows plus the number of visible @forall@–bound variables) in +-- @decl_sak@. +-- +-- * Whenever possible, this function reuses type variable names from the +-- declaration's user-written binders. This is why the @'TyVarBndr' +-- 'ForAllTyFlag'@ use @\@j \@l@ instead of @\@j \@k@, since the @(a :: l)@ +-- binder uses @l@ instead of @k@. We could have just as well chose the other +-- way around, but we chose to pick variable names from the user-written +-- binders since they scope over other parts of the declaration. (For example, +-- the user-written binders of a @data@ declaration scope over the type +-- variables mentioned in a @deriving@ clause.) As such, keeping these names +-- avoids having to perform some alpha-renaming. +-- +-- This function's implementation was heavily inspired by parts of GHC's +-- kcCheckDeclHeader_sig function: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2524-2643 +matchUpSAKWithDecl :: + forall q. + Fail.MonadFail q + => Kind + -- ^ The declaration's standalone kind signature + -> [TyVarBndrVis] + -- ^ The user-written binders in the declaration + -> q [TyVarBndr_ ForAllTyFlag] +matchUpSAKWithDecl decl_sak decl_bndrs = do + -- (1) First, explicitly quantify any free kind variables in `decl_sak` using + -- an invisible @forall@. This is done to ensure that precondition (2) in + -- `matchUpSigWithDecl` is upheld. (See the Haddocks for that function). + let decl_sak_free_tvbs = + changeTVFlags SpecifiedSpec $ freeVariablesWellScoped [decl_sak] + decl_sak' = ForallT decl_sak_free_tvbs [] decl_sak + + -- (2) Next, compute type variable binders using `matchUpSigWithDecl`. Note + -- that these can be biased towards type variable names mention in `decl_sak` + -- over names mentioned in `decl_bndrs`, but we will fix that up in the next + -- step. + let (decl_sak_args, _) = unravelType decl_sak' + sing_sak_tvbs <- matchUpSigWithDecl decl_sak_args decl_bndrs + + -- (3) Finally, swizzle the type variable names so that names in `decl_bndrs` + -- are preferred over names in `decl_sak`. + -- + -- This is heavily inspired by similar code in GHC: + -- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2607-2616 + let invis_decl_sak_args = filterInvisTvbArgs decl_sak_args + invis_decl_sak_arg_nms = map tvName invis_decl_sak_args + + invis_decl_bndrs = freeKindVariablesWellScoped decl_bndrs + invis_decl_bndr_nms = map tvName invis_decl_bndrs + + swizzle_env = + Map.fromList $ zip invis_decl_sak_arg_nms invis_decl_bndr_nms + (_, swizzled_sing_sak_tvbs) = + List.mapAccumL (swizzleTvb swizzle_env) Map.empty sing_sak_tvbs + pure swizzled_sing_sak_tvbs + +-- Match the quantifiers in a type-level declaration's standalone kind signature +-- with the user-written binders in the declaration. This function assumes the +-- following preconditions: +-- +-- 1. The number of required binders in the declaration's user-written binders +-- is equal to the number of visible quantifiers (i.e., the number of +-- function arrows plus the number of visible @forall@–bound variables) in +-- the standalone kind signature. +-- +-- 2. The number of invisible \@-binders in the declaration's user-written +-- binders is less than or equal to the number of invisible quantifiers +-- (i.e., the number of invisible @forall@–bound variables) in the +-- standalone kind signature. +-- +-- The implementation of this function is heavily based on a GHC function of +-- the same name: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/1464a2a8de082f66ae250d63ab9d94dbe2ef8620/compiler/GHC/Tc/Gen/HsType.hs#L2645-2715 +matchUpSigWithDecl :: + forall q. + Fail.MonadFail q + => FunArgs + -- ^ The quantifiers in the declaration's standalone kind signature + -> [TyVarBndrVis] + -- ^ The user-written binders in the declaration + -> q [TyVarBndr_ ForAllTyFlag] +matchUpSigWithDecl = go_fun_args Map.empty + where + go_fun_args :: + Map Name Type + -- ^ A substitution from the names of @forall@-bound variables in the + -- standalone kind signature to corresponding binder names in the + -- user-written binders. This is because we want to reuse type variable + -- names from the user-written binders whenever possible. For example: + -- + -- @ + -- type T :: forall a. forall b -> Maybe (a, b) -> Type + -- data T @x y z + -- @ + -- + -- After matching up the @a@ in @forall a.@ with @x@ and + -- the @b@ in @forall b ->@ with @y@, this substitution will be + -- extended with @[a :-> x, b :-> y]@. This ensures that we will + -- produce @Maybe (x, y)@ instead of @Maybe (a, b)@ in + -- the kind for @z@. + -> FunArgs -> [TyVarBndrVis] -> q [TyVarBndr_ ForAllTyFlag] + go_fun_args _ FANil [] = + pure [] + -- This should not happen, per precondition (1). + go_fun_args _ FANil decl_bndrs = + fail $ "matchUpSigWithDecl.go_fun_args: Too many binders: " ++ show decl_bndrs + -- GHC now disallows kind-level constraints, per this GHC proposal: + -- https://github.com/ghc-proposals/ghc-proposals/blob/b0687d96ce8007294173b7f628042ac4260cc738/proposals/0547-no-kind-equalities.rst + -- As such, we reject non-empty kind contexts. Empty contexts (which are + -- benign) can sometimes arise due to @ForallT@, so we add a special case + -- to allow them. + go_fun_args subst (FACxt [] args) decl_bndrs = + go_fun_args subst args decl_bndrs + go_fun_args _ (FACxt (_:_) _) _ = + fail "matchUpSigWithDecl.go_fun_args: Unexpected kind-level constraint" + go_fun_args subst (FAForalls (ForallInvis tvbs) sig_args) decl_bndrs = + go_invis_tvbs subst tvbs sig_args decl_bndrs + go_fun_args subst (FAForalls (ForallVis tvbs) sig_args) decl_bndrs = + go_vis_tvbs subst tvbs sig_args decl_bndrs + go_fun_args subst (FAAnon anon sig_args) (decl_bndr:decl_bndrs) = + case tvFlag decl_bndr of + -- If the next decl_bndr is required, then we must match its kind (if + -- one is provided) against the anonymous kind argument. + BndrReq -> do + let decl_bndr_name = tvName decl_bndr + mb_decl_bndr_kind = extractTvbKind_maybe decl_bndr + anon' = applySubstitution subst anon + + anon'' = + case mb_decl_bndr_kind of + Nothing -> anon' + Just decl_bndr_kind -> do + let mb_match_subst = matchTy decl_bndr_kind anon' + maybe decl_bndr_kind (`applySubstitution` decl_bndr_kind) mb_match_subst + sig_args' <- go_fun_args subst sig_args decl_bndrs + pure $ kindedTVFlag decl_bndr_name Required anon'' : sig_args' + -- We have a visible, anonymous argument in the kind, but an invisible + -- @-binder as the next decl_bndr. This is ill kinded, so throw an + -- error. + -- + -- This should not happen, per precondition (2). + BndrInvis -> + fail $ "dMatchUpSigWithDecl.go_fun_args: Expected visible binder, encountered invisible binder: " + ++ show decl_bndr + -- This should not happen, per precondition (1). + go_fun_args _ _ [] = + fail "matchUpSigWithDecl.go_fun_args: Too few binders" + + go_invis_tvbs :: + Map Name Type + -> [TyVarBndrSpec] + -> FunArgs + -> [TyVarBndrVis] + -> q [TyVarBndr_ ForAllTyFlag] + go_invis_tvbs subst [] sig_args decl_bndrs = + go_fun_args subst sig_args decl_bndrs + go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss = + case decl_bndrss of + [] -> skip_invis_bndr + decl_bndr:decl_bndrs -> + case tvFlag decl_bndr of + BndrReq -> skip_invis_bndr + -- If the next decl_bndr is an invisible @-binder, then we must match it + -- against the invisible forall–bound variable in the kind. + BndrInvis -> do + let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr + sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs + pure (mapTVFlag Invisible sig_tvb : sig_args') + where + -- There is an invisible forall in the kind without a corresponding + -- invisible @-binder, which is allowed. In this case, we simply apply + -- the substitution and recurse. + skip_invis_bndr :: q [TyVarBndr_ ForAllTyFlag] + skip_invis_bndr = do + let (subst', invis_tvb') = substTvb subst invis_tvb + sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrss + pure $ mapTVFlag Invisible invis_tvb' : sig_args' + + go_vis_tvbs :: + Map Name Type + -> [TyVarBndrUnit] + -> FunArgs + -> [TyVarBndrVis] + -> q [TyVarBndr_ ForAllTyFlag] + go_vis_tvbs subst [] sig_args decl_bndrs = + go_fun_args subst sig_args decl_bndrs + -- This should not happen, per precondition (1). + go_vis_tvbs _ (_:_) _ [] = + fail "matchUpSigWithDecl.go_vis_tvbs: Too few binders" + go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (decl_bndr:decl_bndrs) = do + case tvFlag decl_bndr of + -- If the next decl_bndr is required, then we must match it against the + -- visible forall–bound variable in the kind. + BndrReq -> do + let (subst', sig_tvb) = match_tvbs subst vis_tvb decl_bndr + sig_args' <- go_vis_tvbs subst' vis_tvbs sig_args decl_bndrs + pure (mapTVFlag (const Required) sig_tvb : sig_args') + -- We have a visible forall in the kind, but an invisible @-binder as + -- the next decl_bndr. This is ill kinded, so throw an error. + -- + -- This should not happen, per precondition (2). + BndrInvis -> + fail $ "matchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: " + ++ show decl_bndr + + -- @match_tvbs subst sig_tvb decl_bndr@ will match the kind of @decl_bndr@ + -- against the kind of @sig_tvb@ to produce a new kind. This function + -- produces two values as output: + -- + -- 1. A new @subst@ that has been extended such that the name of @sig_tvb@ + -- maps to the name of @decl_bndr@. (See the Haddocks for the @Map Name + -- Type@ argument to @go_fun_args@ for an explanation of why we do this.) + -- + -- 2. A 'TyVarBndrSpec' that has the name of @decl_bndr@, but with the new + -- kind resulting from matching. + match_tvbs :: + Map Name Type + -> TyVarBndr_ flag + -> TyVarBndrVis + -> (Map Name Type, TyVarBndr_ flag) + match_tvbs subst sig_tvb decl_bndr = + let decl_bndr_name = tvName decl_bndr + mb_decl_bndr_kind = extractTvbKind_maybe decl_bndr + + sig_tvb_name = tvName sig_tvb + sig_tvb_flag = tvFlag sig_tvb + mb_sig_tvb_kind = applySubstitution subst <$> extractTvbKind_maybe sig_tvb + + mb_kind :: Maybe Kind + mb_kind = + case (mb_decl_bndr_kind, mb_sig_tvb_kind) of + (Nothing, Nothing) -> Nothing + (Just decl_bndr_kind, Nothing) -> Just decl_bndr_kind + (Nothing, Just sig_tvb_kind) -> Just sig_tvb_kind + (Just decl_bndr_kind, Just sig_tvb_kind) -> do + match_subst <- matchTy decl_bndr_kind sig_tvb_kind + Just $ applySubstitution match_subst decl_bndr_kind + + subst' = Map.insert sig_tvb_name (VarT decl_bndr_name) subst + sig_tvb' = case mb_kind of + Nothing -> plainTVFlag decl_bndr_name sig_tvb_flag + Just kind -> kindedTVFlag decl_bndr_name sig_tvb_flag kind in + + (subst', sig_tvb') + +-- Collect the invisible type variable binders from a sequence of FunArgs. +filterInvisTvbArgs :: FunArgs -> [TyVarBndrSpec] +filterInvisTvbArgs FANil = [] +filterInvisTvbArgs (FACxt _ args) = filterInvisTvbArgs args +filterInvisTvbArgs (FAAnon _ args) = filterInvisTvbArgs args +filterInvisTvbArgs (FAForalls tele args) = + let res = filterInvisTvbArgs args in + case tele of + ForallVis _ -> res + ForallInvis tvbs' -> tvbs' ++ res + +-- | Take a telescope of 'TyVarBndr's, find the free variables in their kinds, +-- and sort them in reverse topological order to ensure that they are well +-- scoped. Because the argument list is assumed to be telescoping, kind +-- variables that are bound earlier in the list are not returned. For example, +-- this: +-- +-- @ +-- 'freeKindVariablesWellScoped' [a :: k, b :: Proxy a] +-- @ +-- +-- Will return @[k]@, not @[k, a]@, since @a@ is bound earlier by @a :: k@. +freeKindVariablesWellScoped :: [TyVarBndr_ flag] -> [TyVarBndrUnit] +freeKindVariablesWellScoped tvbs = + foldr (\tvb kvs -> + foldMap (\t -> freeVariablesWellScoped [t]) (extractTvbKind_maybe tvb) `List.union` + List.deleteBy ((==) `on` tvName) tvb kvs) + [] + (changeTVFlags () tvbs) + +-- | @'matchTy' tmpl targ@ matches a type template @tmpl@ against a type target +-- @targ@. This returns a Map from names of type variables in the type template +-- to types if the types indeed match up, or @Nothing@ otherwise. In the @Just@ +-- case, it is guaranteed that every type variable mentioned in the template is +-- mapped by the returned substitution. +-- +-- Note that this function will always return @Nothing@ if the template contains +-- an explicit kind signature or visible kind application. +-- +-- This is heavily inspired by the function of the same name in +-- "Language.Haskell.TH.Desugar.Subst", which works over 'DType's instead of +-- 'Type's. +matchTy :: Type -> Type -> Maybe (Map Name Type) +matchTy (VarT var_name) arg = Just $ Map.singleton var_name arg +matchTy (SigT {}) _ = Nothing +matchTy pat (SigT ty _ki) = matchTy pat ty +#if __GLASGOW_HASKELL__ >= 807 +matchTy (AppKindT {}) _ = Nothing +matchTy pat (AppKindT ty _ki) = matchTy pat ty +#endif +matchTy (ForallT {}) _ = + error "Cannot match a forall in a pattern" +matchTy _ (ForallT {}) = + error "Cannot match a forall in a target" +matchTy (AppT pat1 pat2) (AppT arg1 arg2) = + unionMaybeSubsts [matchTy pat1 arg1, matchTy pat2 arg2] +matchTy (ConT pat_con) (ConT arg_con) + | pat_con == arg_con + = Just Map.empty + | otherwise + = Nothing +matchTy ArrowT ArrowT = Just Map.empty +matchTy (LitT pat_lit) (LitT arg_lit) + | pat_lit == arg_lit + = Just Map.empty + | otherwise + = Nothing +matchTy _ _ = Nothing + +-- | This is inspired by the function of the same name in +-- "Language.Haskell.TH.Desugar.Subst". +unionMaybeSubsts :: [Maybe (Map Name Type)] -> Maybe (Map Name Type) +unionMaybeSubsts = List.foldl' union_subst1 (Just Map.empty) + where + union_subst1 :: + Maybe (Map Name Type) -> Maybe (Map Name Type) -> Maybe (Map Name Type) + union_subst1 ma mb = do + a <- ma + b <- mb + unionSubsts a b + +-- | Computes the union of two substitutions. Fails if both subsitutions map +-- the same variable to different types. +-- +-- This is inspired by the function of the same name in +-- "Language.Haskell.TH.Desugar.Subst". +unionSubsts :: Map Name Type -> Map Name Type -> Maybe (Map Name Type) +unionSubsts a b = + let shared_key_set = Map.keysSet a `Set.intersection` Map.keysSet b + matches_up = Set.foldr (\name -> ((a Map.! name) == (b Map.! name) &&)) + True shared_key_set + in + if matches_up then return (a `Map.union` b) else Nothing + +-- | This is inspired by the function of the same name in +-- "Language.Haskell.TH.Desugar.Subst.Capturing". +substTvb :: Map Name Kind -> TyVarBndr_ flag -> (Map Name Kind, TyVarBndr_ flag) +substTvb s tvb = (Map.delete (tvName tvb) s, mapTVKind (applySubstitution s) tvb) + +-- This is heavily inspired by the `swizzleTcb` function in GHC: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/cec903899234bf9e25ea404477ba846ac1e963bb/compiler/GHC/Tc/Gen/HsType.hs#L2741-2755 +swizzleTvb :: + Map Name Name + -- ^ A \"swizzle environment\" (i.e., a map from binder names in a + -- standalone kind signature to binder names in the corresponding + -- type-level declaration). + -> Map Name Type + -- ^ Like the swizzle environment, but as a full-blown substitution. + -> TyVarBndr_ flag + -> (Map Name Type, TyVarBndr_ flag) +swizzleTvb swizzle_env subst tvb = + (subst', tvb2) + where + subst' = Map.insert tvb_name (VarT (tvName tvb2)) subst + tvb_name = tvName tvb + tvb1 = mapTVKind (applySubstitution subst) tvb + tvb2 = + case Map.lookup tvb_name swizzle_env of + Just user_name -> mapTVName (const user_name) tvb1 + Nothing -> tvb1 + +-- The visibility of a binder in a type-level declaration. This generalizes +-- 'Specificity' (which lacks an equivalent to 'Required') and 'BndrVis' (which +-- lacks an equivalent to @'Invisible' 'Inferred'@). +-- +-- This is heavily inspired by a data type of the same name in GHC: +-- https://gitlab.haskell.org/ghc/ghc/-/blob/98597ad5fca81544d74f721fb508295fd2650232/compiler/GHC/Types/Var.hs#L458-465 +data ForAllTyFlag + = Invisible !Specificity + -- ^ If the 'Specificity' value is 'SpecifiedSpec', then the binder is + -- permitted by request (e.g., @\@a@). If the 'Specificity' value is + -- 'InferredSpec', then the binder is prohibited from appearing in source + -- Haskell (e.g., @\@{a}@). + | Required + -- ^ The binder is required to appear in source Haskell (e.g., @a@). + deriving (Show, Eq, Ord, Data, Generic, Lift) + +instance DefaultBndrFlag ForAllTyFlag where + defaultBndrFlag = Required + +#if __GLASGOW_HASKELL__ >= 900 +instance PprFlag ForAllTyFlag where + pprTyVarBndr (PlainTV nm vis) = + pprForAllTyFlag vis (ppr nm) + pprTyVarBndr (KindedTV nm vis k) = + pprForAllTyFlag vis (Ppr.parens (ppr nm Ppr.<+> Ppr.dcolon Ppr.<+> ppr k)) + +pprForAllTyFlag :: ForAllTyFlag -> Ppr.Doc -> Ppr.Doc +pprForAllTyFlag (Invisible SpecifiedSpec) d = Ppr.char '@' Ppr.<> d +pprForAllTyFlag (Invisible InferredSpec) d = Ppr.braces d +pprForAllTyFlag Required d = d +#endif + +-- | Convert a list of @'TyVarBndr' 'ForAllTyFlag'@s to a list of +-- 'TyVarBndrSpec's, which is suitable for use in an invisible @forall@. +-- Specifically: +-- +-- * Variable binders that use @'Invisible' spec@ are converted to @spec@. +-- +-- * Variable binders that are 'Required' are converted to 'SpecifiedSpec', +-- as all of the 'TyVarBndrSpec's are invisible. As an example of how this +-- is used, consider what would happen when singling this data type: +-- +-- @ +-- type T :: forall k -> k -> Type +-- data T k (a :: k) where ... +-- @ +-- +-- Here, the @k@ binder is 'Required'. When we produce the standalone kind +-- signature for the singled data type, we use 'tvbForAllTyFlagsToSpecs' to +-- produce the type variable binders in the outermost @forall@: +-- +-- @ +-- type ST :: forall k (a :: k). T k a -> Type +-- data ST z where ... +-- @ +-- +-- Note that the @k@ is bound visibily (i.e., using 'SpecifiedSpec') in the +-- outermost, invisible @forall@. +tvbForAllTyFlagsToSpecs :: [TyVarBndr_ ForAllTyFlag] -> [TyVarBndrSpec] +tvbForAllTyFlagsToSpecs = map (mapTVFlag to_spec) + where + to_spec :: ForAllTyFlag -> Specificity + to_spec (Invisible spec) = spec + to_spec Required = SpecifiedSpec + +-- | Convert a list of @'TyVarBndr' 'ForAllTyFlag'@s to a list of +-- 'TyVarBndrVis'es, which is suitable for use in a type-level declaration +-- (e.g., the @var_1 ... var_n@ in @class C var_1 ... var_n@). Specifically: +-- +-- * Variable binders that use @'Invisible' 'InferredSpec'@ are dropped +-- entirely. Such binders cannot be represented in source Haskell. +-- +-- * Variable binders that use @'Invisible' 'SpecifiedSpec'@ are converted to +-- 'BndrInvis'. +-- +-- * Variable binders that are 'Required' are converted to 'BndrReq'. +tvbForAllTyFlagsToBndrVis :: [TyVarBndr_ ForAllTyFlag] -> [TyVarBndrVis] +tvbForAllTyFlagsToBndrVis = catMaybes . map (traverseTVFlag to_spec_maybe) + where + to_spec_maybe :: ForAllTyFlag -> Maybe BndrVis + to_spec_maybe (Invisible InferredSpec) = Nothing + to_spec_maybe (Invisible SpecifiedSpec) = Just bndrInvis + to_spec_maybe Required = Just BndrReq + ---------------------------------------- -- Free names, etc. ---------------------------------------- @@ -611,6 +1112,9 @@ #if __GLASGOW_HASKELL__ >= 909 extractBoundNamesPat (TypeP _) = OS.empty extractBoundNamesPat (InvisP _) = OS.empty +#endif +#if __GLASGOW_HASKELL__ >= 911 +extractBoundNamesPat (OrP pats) = foldMap extractBoundNamesPat pats #endif ---------------------------------------- diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -145,92 +145,267 @@ impossible to tell whether a reified function type is linear or not. See, for instance, [GHC#18378](https://gitlab.haskell.org/ghc/ghc/-/issues/18378). -## Limited support for embedded types in patterns +## Limitations of support for desugaring guards -In GHC 9.10 or later, the `RequiredTypeArguments` language extension allows one -to write definitions with embedded types in patterns, e.g., +`th-desugar` supports guards in the sense that it will desugar guards to +equivalent code that instead uses `case` expressions. For example, this code: ```hs -idv :: forall a -> a -> a -idv (type a) = id @a +f (x, y) + | x == "hello" = x + | otherwise = y ``` -`th-desugar` supports writing patterns like `(type a)` via the `DTypeP` data -constructor of `DPat`. Be warned, however, that `th-desugar` only supports -desugaring `DTypeP` in the clauses of function declarations, such as the -declaration of `idv` above. As a result, `th-desugar` does not support -desugaring `DTypeP` in any other position, including: +Will be desugared to this code: -* Lambda expressions. For example, the following is not supported: +```hs +f arg = + case arg of + (x, y) -> + case x2 == "hello" of + True -> x + False -> y +``` - ```hs - idv2 :: forall a -> a -> a - idv2 = \(type a) -> id @a - ``` -* `\case` expressions. For example, the following is not supported: +This has the advantage that it saves users from needing to care about the +complexities of guards. It does have some drawbacks, however, which we describe +below. - ```hs - idv3 :: forall a -> a -> a - idv3 = \case - (type a) -> id @a - ``` -* `\cases` expressions. For example, the following is not supported: +### Desugaring guards can result in quadratic code size - ```hs - idv4 :: forall a -> a -> a - idv4 = \cases - (type a) x -> x :: a - ``` +If you desugar this program involving guards: -Note that all of the example above use an explicit `type` keyword, but the same -considerations apply for embedded type patterns that do not use the `type` -keyword. That is, `th-desugar` supports desugaring the following: +```hs +data T = A Int | B Int | C Int +f :: T -> T -> Maybe Int +f (A x1) (A x2) + | x1 == x2 + = Just x1 +f (B x1) (B x2) + | x1 == x2 + = Just x1 +f (C x1) (C x2) + | x1 == x2 + = Just x1 +f _ _ = Nothing +``` + +You will end up with: + ```hs -idv' :: forall a -> a -> a -idv' a = id @a +f :: T -> T -> Maybe Int +f arg1 arg2 = + case (# arg1, arg2 #) of + (# A x1, A x2 #) -> + case x1 == x2 of + True -> + Just x1 + False -> + case (# arg1, arg2 #) of + (# B y1, B y2 #) -> + case y1 == y2 of + True -> + Just y1 + False -> + case (# arg1, arg2 #) of + (# C z1, C z2 #) -> + case z1 == z2 of + True -> + Just z1 + False -> + case (# arg1, arg2 #) of + (# _, _ #) -> + Nothing + (# _, _ #) -> + Nothing + (# C y1, C y2 #) -> + case y1 == y2 of + True -> + Just y1 + False -> + case (# arg1, arg2 #) of + (# _, _ #) -> + Nothing + (# _, _ #) -> + Nothing + (# B x1, B x2 #) -> + case x1 == x2 of + True -> + Just x1 + False -> + case (# arg1, arg2 #) of + (# C y1, C y2 #) -> + case y1 == y2 of + True -> + Just y1 + False -> + case (# arg1, arg2 #) of + (# _, _ #) -> + Nothing + (# _, _ #) -> + Nothing + (# C x1, C x2 #) -> + case x1 == x2 of + True -> + Just x1 + False -> + case (# arg1, arg2 #) of + (# _, _ #) -> + Nothing + (# _, _ #) -> + Nothing ``` -But `th-desugar` does not support desugaring any of the following: +That is signficantly more code. In the worst case, the algorithm that +`th-desugar` uses for desugaring guards can lead to a quadratic increase in +code size. One way to avoid this is avoid having incomplete guards that fall +through to later clauses. That is, if you rewrite the original code to this: ```hs -idv2' :: forall a -> a -> a -idv2' = \a -> id @a +f :: T -> T -> Maybe Int +f (A x1) (A x2) + | x1 == x2 + = Just x1 + | otherwise + = Nothing +f (B x1) (B x2) + | x1 == x2 + = Just x1 + | otherwise + = Nothing +f (C x1) (C x2) + | x1 == x2 + = Just x1 + | otherwise + = Nothing +``` -idv3' :: forall a -> a -> a -idv3' = \case - a -> id @a +Then `th-desugar` will desugar it to: -idv4' :: forall a -> a -> a -idv4' = \cases - a x -> x :: a +```hs +f :: T -> T -> Maybe Int +f arg1 arg2 = + case (# arg1, arg2 #) of + (# A x1, A x2 #) -> + case x1 == x2 of + True -> + Just x1 + False -> + Nothing + (# B x1, B x2 #) -> + case x1 == x2 of + True -> + Just x1 + False -> + Nothing + (# C x1, C x2 #) -> + case x1 == x2 of + True -> + Just x1 + False -> + Nothing ``` -As a workaround, one can convert uses of lambdas and `LambdaCase` to function -declarations, which are fully supported. See also [this `th-desugar` -issue](https://github.com/goldfirere/th-desugar/issues/210), which proposes a -different approach to desugaring that would allow all of the examples above to -be accepted. +This code, while still more verbose than the original, uses a constant amount +of extra code per clause. -## Limited support for invisible type patterns +### Desugaring guards can produce more warnings than the original code -In GHC 9.10 or later, the `TypeAbstractions` language extension allows one to -write definitions with invisible type patterns, e.g., +The approach that `th-desugar` uses to desugar guards can result in code that +produces GHC compiler warnings (if `-fenable-th-splice-warnings` is enabled) +where the original code does not. For example, consider the example from above: ```hs -f :: a -> a -f @a = id @a +data T = A Int | B Int | C Int + +f :: T -> T -> Maybe Int +f (A x1) (A x2) + | x1 == x2 + = Just x1 +f (B x1) (B x2) + | x1 == x2 + = Just x1 +f (C x1) (C x2) + | x1 == x2 + = Just x1 +f _ _ = Nothing ``` -`th-desugar` supports writing patterns like `@a` via the `DInvisP` data -constructor of `DPat`. Be warned, however, that `th-desugar` only supports -desugaring `DInvisP` in the clauses of function declarations, such as the -declaration of `f` above. As a result, `th-desugar` does not support desugaring -`DInvisP` in any other position, such as lambda expressions or `\cases` -expressions. +This code compiles without any GHC warnings. If you desugar this code using +`th-desugar`, however, it will produce these warnings: -Ultimately, this limitation has the same underlying cause as `th-desugar`'s -limitations surrounding embedded types in patterns (see the "Limited support -for embedded types in patterns" section above). As a result, the same -workaround applies: convert uses of lambdas and `LambdaCase` to function -declarations, which are fully supported. +``` +warning: [-Woverlapping-patterns] + Pattern match is redundant + In a case alternative: (# B y1, B y2 #) -> ... + | + | (# B y1, B y2 #) -> + | ^^^^^^^^^^^^^^^^^^^... + +warning: [-Woverlapping-patterns] + Pattern match is redundant + In a case alternative: (# C y1, C y2 #) -> ... + | + | (# C y1, C y2 #) -> + | ^^^^^^^^^^^^^^^^^^^... + +warning: [-Woverlapping-patterns] + Pattern match is redundant + In a case alternative: (# C y1, C y2 #) -> ... + | + | (# C y1, C y2 #) -> + | ^^^^^^^^^^^^^^^^^^^... +``` + +GHC is correct here: these matches are wholly redundant. `th-desugar` could +potentially recognize this and perform a more sophisticated analysis to detect +and remove such matches when desugaring guards, but it currently doesn't do +such an analysis. + +## No support for view patterns + +`th-desugar` does not support desugaring view patterns. An alternative to using +view patterns in the patterns of a function is to use pattern guards. +Currently, there is not a viable workaround for using view patterns in pattern +synonym definitions—see [this `th-desugar` +issue](https://github.com/goldfirere/th-desugar/issues/174). + +## No support for or-patterns + +`th-desugar` does not support desugaring +[or-patterns](https://github.com/ghc-proposals/ghc-proposals/blob/c9401f037cb22d1661931b2ec621925101052997/proposals/0522-or-patterns.rst). +See [this `th-desugar` +issue](https://github.com/goldfirere/th-desugar/issues/232). + +## No support for `ApplicativeDo` + +`th-desugar` does not take the `ApplicativeDo` extension into account when +desugaring `do` notation. For example, if you desugar this: + +```hs +{-# LANGUAGE ApplicativeDo #-} + +f x y = do + x' <- x + y' <- y + return (x' ++ y') +``` + +Then `th-desugar` will translate the uses of `<-` in the `do` block to uses of +`Monad` operations (e.g., `(>>=)`) rather than `Applicative` operations (e.g., +`(<*>)`). See [this `th-desugar` +issue](https://github.com/goldfirere/th-desugar/issues/138). + +## No support for `RecursiveDo` + +`th-desugar` does not support the `RecursiveDo` extension at all, so it cannot +desugar any uses of `mdo` expressions or `rec` statements. + +## No support for unresolved infix operators + +`th-desugar` does not support desugaring unresolved infix operators, such as +`UInfixE`. You are unlikely to encounter this limitation when dealing with +Template Haskell quotes, since quoted infix operators will translate to uses of +`InfixE` rather than `UInfixE`. Rather, this limitation would only be +encountered if you manually construct a Template Haskell `Exp` using `UInfixE`. diff --git a/Test/Run.hs b/Test/Run.hs --- a/Test/Run.hs +++ b/Test/Run.hs @@ -42,6 +42,10 @@ {-# LANGUAGE RequiredTypeArguments #-} #endif +#if __GLASGOW_HASKELL__ >= 911 +{-# LANGUAGE ImpredicativeTypes #-} +#endif + module Main where import Prelude hiding ( exp ) @@ -72,6 +76,7 @@ import Data.Proxy #if __GLASGOW_HASKELL__ >= 900 +import Data.Kind (Constraint) import Prelude as P #endif @@ -193,7 +198,20 @@ , "embedded_types_keyword" ~: $test59_embedded_types_keyword @=? $(dsSplice test59_embedded_types_keyword) , "embedded_types_no_keyword" ~: $test60_embedded_types_no_keyword @=? $(dsSplice test60_embedded_types_no_keyword) , "invis_type_pat" ~: $test61_invis_type_pat @=? $(dsSplice test61_invis_type_pat) + , "embedded_types_lambda_keyword" ~: $test62_embedded_types_lambda_keyword @=? $(dsSplice test62_embedded_types_lambda_keyword) + , "embedded_types_case_keyword" ~: $test63_embedded_types_case_keyword @=? $(dsSplice test63_embedded_types_case_keyword) + , "embedded_types_cases_keyword" ~: $test64_embedded_types_cases_keyword @=? $(dsSplice test64_embedded_types_cases_keyword) + , "embedded_types_lambda_no_keyword" ~: $test65_embedded_types_lambda_no_keyword @=? $(dsSplice test65_embedded_types_lambda_no_keyword) + , "embedded_types_case_no_keyword" ~: $test66_embedded_types_case_no_keyword @=? $(dsSplice test66_embedded_types_case_no_keyword) + , "embedded_types_cases_no_keyword" ~: $test67_embedded_types_cases_no_keyword @=? $(dsSplice test67_embedded_types_cases_no_keyword) + , "invis_type_pat_lambda" ~: $test68_invis_type_pat_lambda @=? $(dsSplice test68_invis_type_pat_lambda) + , "invis_type_pat_cases" ~: $test69_invis_type_pat_cases @=? $(dsSplice test69_invis_type_pat_cases) #endif +#if __GLASGOW_HASKELL__ >= 911 + , "embedded_forall_invis" ~: $(test70_embedded_forall_invis) @=? $(dsSplice test70_embedded_forall_invis) + , "embedded_forall_vis" ~: $(test71_embedded_forall_vis) @=? $(dsSplice test71_embedded_forall_vis) + , "embedded_constraint" ~: $(test72_embedded_constraint) @=? $(dsSplice test72_embedded_constraint) +#endif ] test35a = $test35_expand @@ -688,6 +706,46 @@ toposortKindVarsOfTvbs [DKindedTV a1 () (DVarT a2), DKindedTV a2 () (DVarT a1)] == [DPlainTV a2 ()] +#if __GLASGOW_HASKELL__ >= 900 +-- A regression test for #199, which ensures that a locally reified data +-- constructor is given a type signature that takes into account the fact that +-- its parent data type's standalone kind signature marks `k` as inferred. +test_t199 :: [Bool] +test_t199 = + $(do decs <- [d| type P :: forall {k}. k -> Type + data P (a :: k) = MkP |] + + withLocalDeclarations decs $ do + let k = mkName "k" + a = mkName "a" + kTvb = DPlainTV k InferredSpec + aTvb = DKindedTV a SpecifiedSpec (DVarT k) + p = mkName "P" + mkP = mkName "MkP" + pTy = DConT p `DAppT` DVarT a + mbPInfo <- dsReify p + let b1 = + case mbPInfo of + Just (DTyConI (DDataD _ _ _ _ _ [conActual] _) _) -> + let conExpected = + DCon [kTvb, aTvb] [] mkP (DNormalC False []) pTy in + conExpected `eqTH` conActual + _ -> + False + + mbMkPInfo <- dsReify mkP + let b2 = + case mbMkPInfo of + Just (DVarI _ conTyActual _) -> + let conTyExpected = + DForallT (DForallInvis [kTvb, aTvb]) pTy in + conTyExpected `eqTH` conTyActual + _ -> + False + + [| [b1, b2] |]) +#endif + -- Unit tests for unboxedTupleNameDegree_maybe and unboxedSumNameDegree_maybe. -- These also act as a regression test for #213. test_t213 :: [Bool] @@ -732,6 +790,51 @@ ] #endif +#if __GLASGOW_HASKELL__ >= 900 +-- A regression test for #220, which ensures that a locally reified class method +-- is given a type signature that takes into account the fact that its parent +-- class's standalone kind signature marks `k` as inferred. +test_t220 :: Bool +test_t220 = + $(do decs <- [d| type C :: forall {k}. k -> Constraint + class C (a :: k) where + m :: Proxy a |] + + withLocalDeclarations decs $ do + let k = mkName "k" + a = mkName "a" + kTvb = DPlainTV k InferredSpec + aTvb = DKindedTV a SpecifiedSpec (DVarT k) + c = mkName "C" + m = mkName "m" + cTy = DConT c `DAppT` DVarT a + mbMInfo <- dsReify m + case mbMInfo of + Just (DVarI _ mTyActual _) -> + let mTyExpected = + DForallT (DForallInvis [kTvb, aTvb]) $ + DConstrainedT [cTy] $ + DConT ''Proxy `DAppT` DVarT a in + mTyExpected `eqTHSplice` mTyActual + _ -> + [| False |]) +#endif + +-- A regression test for #228, which ensures that dMatchUpSAKWithDecl behaves +-- as expected on code that looks like this: +-- +-- @ +-- type D :: forall (a :: Type). Type +-- data D +-- @ +test_t228 :: Bool +test_t228 = + let sak = DForallT (DForallInvis [DKindedTV (mkName "a") SpecifiedSpec (DConT ''Type)]) (DConT ''Type) + expected_bndrs = [DKindedTV (mkName "a") (Invisible SpecifiedSpec) (DConT ''Type)] in + case dMatchUpSAKWithDecl sak [] of + Nothing -> False + Just actual_bndrs -> expected_bndrs `eqTH` actual_bndrs + -- Unit tests for functions that compute free variables (e.g., fvDType) test_fvs :: [Bool] test_fvs = @@ -971,8 +1074,19 @@ it "computes free kind variables correctly in a telescope that uses shadowing" $ test_t188 +#if __GLASGOW_HASKELL__ >= 900 + zipWithM (\b n -> it ("correctly reifies the type of a data constructor with an inferred type variable binder " ++ show n) b) + test_t199 [1..] +#endif + zipWithM (\b n -> it ("recognizes unboxed {tuple,sum} names with unboxed{Tuple,Sum}Degree_maybe correctly " ++ show n) b) test_t213 [1..] + +#if __GLASGOW_HASKELL__ >= 900 + it "correctly reifies the type of a class method with an inferred type variable binder" $ test_t220 +#endif + + it "correctly matches up an invisible forall without a corresponding @-binder" $ test_t228 -- Remove map pprints here after switch to th-orphans zipWithM (\t t' -> it ("can do Type->DType->Type of " ++ t) $ t == t') diff --git a/Test/Splices.hs b/Test/Splices.hs --- a/Test/Splices.hs +++ b/Test/Splices.hs @@ -413,8 +413,74 @@ f @a = id @a in f @Bool True |] + +test62_embedded_types_lambda_keyword = + [| let idv :: forall a -> a -> a + idv = \(type a) (x :: a) -> x :: a + + in idv (type Bool) True |] + +test63_embedded_types_case_keyword = + [| let idv :: forall a -> a -> a + idv = \case + (type a) -> id @a + + in idv (type Bool) True |] + +test64_embedded_types_cases_keyword = + [| let idv :: forall a -> a -> a + idv = \cases + (type a) (x :: a) -> x :: a + + in idv (type Bool) True |] + +test65_embedded_types_lambda_no_keyword = + [| let idv :: forall a -> a -> a + idv = \a (x :: a) -> x :: a + + in idv Bool True |] + +test66_embedded_types_case_no_keyword = + [| let idv :: forall a -> a -> a + idv = \case + a -> id @a + + in idv Bool True |] + +test67_embedded_types_cases_no_keyword = + [| let idv :: forall a -> a -> a + idv = \cases + a (x :: a) -> x :: a + + in idv Bool True |] + +aux :: (forall a. a -> a) -> (forall a. a -> a) +aux f x = f x + +test68_invis_type_pat_lambda = + [| aux (\ @a (x :: a) -> x :: a) @Bool True |] + +test69_invis_type_pat_cases = + [| aux (\cases @a (x :: a) -> x :: a) @Bool True |] #endif +#if __GLASGOW_HASKELL__ >= 911 +test70_embedded_forall_invis = + [| let idv :: forall a -> a -> a + idv _ x = x + in idv (forall a. a -> a) id True |] + +test71_embedded_forall_vis = + [| let idv :: forall a -> a -> a + idv _ x = x + in idv (forall a -> a -> a) idv Bool True |] + +test72_embedded_constraint = + [| let idv :: forall a -> a -> a + idv _ x = x + in idv (forall a. (a ~ Bool) => a -> a) (\x -> not x) False |] +#endif + type family TFExpand x type instance TFExpand Int = Bool type instance TFExpand (Maybe a) = [a] @@ -884,5 +950,18 @@ , test59_embedded_types_keyword , test60_embedded_types_no_keyword , test61_invis_type_pat + , test62_embedded_types_lambda_keyword + , test63_embedded_types_case_keyword + , test64_embedded_types_cases_keyword + , test65_embedded_types_lambda_no_keyword + , test66_embedded_types_case_no_keyword + , test67_embedded_types_cases_no_keyword + , test68_invis_type_pat_lambda + , test69_invis_type_pat_cases +#endif +#if __GLASGOW_HASKELL__ >= 911 + , test70_embedded_forall_invis + , test71_embedded_forall_vis + , test72_embedded_constraint #endif ] diff --git a/th-desugar.cabal b/th-desugar.cabal --- a/th-desugar.cabal +++ b/th-desugar.cabal @@ -1,5 +1,5 @@ name: th-desugar -version: 1.17 +version: 1.18 cabal-version: >= 1.10 synopsis: Functions to desugar Template Haskell homepage: https://github.com/goldfirere/th-desugar @@ -21,9 +21,10 @@ , GHC == 9.0.2 , GHC == 9.2.8 , GHC == 9.4.8 - , GHC == 9.6.4 - , GHC == 9.8.2 + , GHC == 9.6.6 + , GHC == 9.8.4 , GHC == 9.10.1 + , GHC == 9.12.1 description: This package provides the Language.Haskell.TH.Desugar module, which desugars Template Haskell's rich encoding of Haskell syntax into a simpler encoding. @@ -49,13 +50,14 @@ build-depends: base >= 4.9 && < 5, ghc-prim, - template-haskell >= 2.11 && < 2.23, + template-haskell >= 2.11 && < 2.24, containers >= 0.5, mtl >= 2.1 && < 2.4, ordered-containers >= 0.2.2, syb >= 0.4, th-abstraction >= 0.6 && < 0.8, - th-orphans >= 0.13.7, + th-compat >= 0.1 && < 0.2, + th-orphans >= 0.13.11, transformers-compat >= 0.6.3 default-extensions: TemplateHaskell exposed-modules: Language.Haskell.TH.Desugar @@ -65,6 +67,7 @@ Language.Haskell.TH.Desugar.OMap.Strict Language.Haskell.TH.Desugar.OSet Language.Haskell.TH.Desugar.Subst + Language.Haskell.TH.Desugar.Subst.Capturing Language.Haskell.TH.Desugar.Sweeten other-modules: Language.Haskell.TH.Desugar.AST Language.Haskell.TH.Desugar.Core @@ -105,4 +108,4 @@ hspec >= 1.3, th-abstraction, th-desugar, - th-orphans >= 0.13.9 + th-orphans