diff options
author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-03-02 11:26:17 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2023-03-03 11:41:23 -0500 |
commit | bd0536afee5d5f91d99af2ab193b6eee5b1da07a (patch) | |
tree | f0db4e794192865368cf8529477a111897e7ad73 /compiler/GHC | |
parent | 0c6948957f62d96a8234683fdf67b34369aad240 (diff) | |
download | haskell-bd0536afee5d5f91d99af2ab193b6eee5b1da07a.tar.gz |
More fixes for `type data` declarations
This MR fixes #23022 and #23023. Specifically
* Beef up Note [Type data declarations] in GHC.Rename.Module,
to make invariant (I1) explicit, and to name the several
wrinkles.
And add references to these specific wrinkles.
* Add a Lint check for invariant (I1) above.
See GHC.Core.Lint.checkTypeDataConOcc
* Disable the `caseRules` for dataToTag# for `type data` values.
See Wrinkle (W2c) in the Note above. Fixes #23023.
* Refine the assertion in dataConRepArgTys, so that it does not
complain about the absence of a wrapper for a `type data` constructor
Fixes #23022.
Acked-by: Simon Peyton Jones <simon.peytonjones@gmail.com>
Diffstat (limited to 'compiler/GHC')
-rw-r--r-- | compiler/GHC/Core/DataCon.hs | 20 | ||||
-rw-r--r-- | compiler/GHC/Core/Lint.hs | 19 | ||||
-rw-r--r-- | compiler/GHC/Core/Opt/ConstantFold.hs | 4 | ||||
-rw-r--r-- | compiler/GHC/Core/Utils.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/HsToCore/Pmc/Solver.hs | 4 | ||||
-rw-r--r-- | compiler/GHC/Rename/Module.hs | 120 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 3 |
7 files changed, 111 insertions, 62 deletions
diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs index a9e540769e..f54f42d99d 100644 --- a/compiler/GHC/Core/DataCon.hs +++ b/compiler/GHC/Core/DataCon.hs @@ -1669,13 +1669,25 @@ dataConOtherTheta dc = dcOtherTheta dc -- evidence, after any flattening has been done and without substituting for -- any type variables dataConRepArgTys :: DataCon -> [Scaled Type] -dataConRepArgTys (MkData { dcRep = rep - , dcEqSpec = eq_spec +dataConRepArgTys (MkData { dcRep = rep + , dcEqSpec = eq_spec , dcOtherTheta = theta - , dcOrigArgTys = orig_arg_tys }) + , dcOrigArgTys = orig_arg_tys + , dcRepTyCon = tc }) = case rep of - NoDataConRep -> assert (null eq_spec) $ map unrestricted theta ++ orig_arg_tys DCR { dcr_arg_tys = arg_tys } -> arg_tys + NoDataConRep + | isTypeDataTyCon tc -> assert (null theta) $ + orig_arg_tys + -- `type data` declarations can be GADTs (and hence have an eq_spec) + -- but no wrapper. They cannot have a theta. + -- See Note [Type data declarations] in GHC.Rename.Module + -- You might wonder why we ever call dataConRepArgTys for `type data`; + -- I think it's because of the call in mkDataCon, which in turn feeds + -- into dcRepArity, which in turn is used in mkDataConWorkId. + -- c.f. #23022 + | otherwise -> assert (null eq_spec) $ + map unrestricted theta ++ orig_arg_tys -- | The string @package:module.name@ identifying a constructor, which is attached -- to its info table and used by the GHCi debugger and the heap profiler diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index 2f7ab56b5b..2465a2ffdf 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -1021,6 +1021,9 @@ lintIdOcc var nargs ; checkDeadIdOcc var ; checkJoinOcc var nargs + ; case isDataConId_maybe var of + Nothing -> return () + Just dc -> checkTypeDataConOcc "expression" dc ; usage <- varCallSiteUsage var @@ -1107,6 +1110,13 @@ checkJoinOcc var n_args | otherwise = return () +checkTypeDataConOcc :: String -> DataCon -> LintM () +-- Check that the Id is not a data constructor of a `type data` declaration +-- Invariant (I1) of Note [Type data declarations] in GHC.Rename.Module +checkTypeDataConOcc what dc + = checkL (not (isTypeDataTyCon (dataConTyCon dc))) $ + (text "type data constructor found in a" <+> text what <> colon <+> ppr dc) + -- | This function checks that we are able to perform eta expansion for -- functions with no binding, in order to satisfy invariant I3 -- from Note [Representation polymorphism invariants] in GHC.Core. @@ -1561,10 +1571,11 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh = zeroUE <$ addErrL (mkNewTyDataConAltMsg scrut_ty alt) | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty = addLoc (CaseAlt alt) $ do - { -- First instantiate the universally quantified - -- type variables of the data constructor - -- We've already check - lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con) + { checkTypeDataConOcc "pattern" con + ; lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con) + + -- Instantiate the universally quantified + -- type variables of the data constructor ; let { con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys ; binderMult (Named _) = ManyTy ; binderMult (Anon st _) = scaledMult st diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs index 2e5c6aabf6..86fdc5cdb5 100644 --- a/compiler/GHC/Core/Opt/ConstantFold.hs +++ b/compiler/GHC/Core/Opt/ConstantFold.hs @@ -55,7 +55,7 @@ import GHC.Core.TyCo.Compare( eqType ) import GHC.Core.TyCon ( tyConDataCons_maybe, isAlgTyCon, isEnumerationTyCon , isNewTyCon, tyConDataCons - , tyConFamilySize ) + , tyConFamilySize, isTypeDataTyCon ) import GHC.Core.Map.Expr ( eqCoreExpr ) import GHC.Builtin.PrimOps ( PrimOp(..), tagToEnumKey ) @@ -3184,6 +3184,8 @@ caseRules _ (App (App (Var f) (Type ty)) v) -- dataToTag x | Just DataToTagOp <- isPrimOpId_maybe f , Just (tc, _) <- tcSplitTyConApp_maybe ty , isAlgTyCon tc + , not (isTypeDataTyCon tc) -- See wrinkle (W2c) in GHC.Rename.Module + -- Note [Type data declarations] = Just (v, tx_con_dtt ty , \v -> App (App (Var f) (Type ty)) (Var v)) diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs index 89824889ef..21ceb2a7bb 100644 --- a/compiler/GHC/Core/Utils.hs +++ b/compiler/GHC/Core/Utils.hs @@ -845,7 +845,8 @@ There are two exceptions where we avoid refining a DEFAULT case: __DEFAULT -> () Namely, we do _not_ want to match on `A`, as it doesn't exist at the value - level! + level! See wrinkle (W2b) in Note [Type data declarations] in GHC.Rename.Module + Note [Combine identical alternatives] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs index 18b5b5c2d6..b493d41889 100644 --- a/compiler/GHC/HsToCore/Pmc/Solver.hs +++ b/compiler/GHC/HsToCore/Pmc/Solver.hs @@ -152,8 +152,8 @@ vanillaCompleteMatchTC tc = tc == tYPETyCon = Just [] | -- Similarly, treat `type data` declarations as empty data types on -- the term level, as `type data` data constructors only exist at - -- the type level (#22964). - -- See Note [Type data declarations] in GHC.Rename.Module. + -- the type level (#22964). See wrinkle (W2a) in + -- Note [Type data declarations] in GHC.Rename.Module. isTypeDataTyCon tc = Just [] | otherwise = tyConDataCons_maybe tc in vanillaCompleteMatch . mkUniqDSet . map RealDataCon <$> mb_dcs diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs index 29a12299c4..5441d0419a 100644 --- a/compiler/GHC/Rename/Module.hs +++ b/compiler/GHC/Rename/Module.hs @@ -2073,9 +2073,79 @@ preceded by `type`, with the following restrictions: (R5) There are no deriving clauses. +The data constructors of a `type data` declaration obey the following +Core invariant: + +(I1) The data constructors of a `type data` declaration may be mentioned in + /types/, but never in /terms/ or the /pattern of a case alternative/. + +Wrinkles: + +(W0) Wrappers. The data constructor of a `type data` declaration has a worker + (like every data constructor) but does /not/ have a wrapper. Wrappers + only make sense for value-level data constructors. Indeed, the worker Id + is never used (invariant (I1)), so it barely makes sense to talk about + the worker. A `type data` constructor only shows up in types, where it + appears as a TyCon, specifically a PromotedDataCon -- no Id in sight. + + See `wrapped_reqd` in GHC.Types.Id.Make.mkDataConRep` for the place where + this check is implemented. + + This specifically includes `type data` declarations implemented as GADTs, + such as this example from #22948: + + type data T a where + A :: T Int + B :: T a + + If `T` were an ordinary `data` declaration, then `A` would have a wrapper + to account for the GADT-like equality in its return type. Because `T` is + declared as a `type data` declaration, however, the wrapper is omitted. + +(W1) To prevent users from conjuring up `type data` values at the term level, + we disallow using the tagToEnum# function on a type headed by a `type + data` type. For instance, GHC will reject this code: + + type data Letter = A | B | C + + f :: Letter + f = tagToEnum# 0# + + See `GHC.Tc.Gen.App.checkTagToEnum`, specifically `check_enumeration`. + +(W2) Although `type data` data constructors do not exist at the value level, + it is still possible to match on a value whose type is headed by a `type data` + type constructor, such as this example from #22964: + + type data T a where + A :: T Int + B :: T a + + f :: T a -> () + f x = case x of {} + + And yet we must guarantee invariant (I1). This has three consequences: + + (W2a) During checking the coverage of `f`'s pattern matches, we treat `T` + as if it were an empty data type so that GHC does not warn the user + to match against `A` or `B`. (Otherwise, you end up with the bug + reported in #22964.) See GHC.HsToCore.Pmc.Solver.vanillaCompleteMatchTC. + + (W2b) In `GHC.Core.Utils.refineDataAlt`, do /not/ fill in the DEFAULT case + with the data constructor, else (I1) is violated. See GHC.Core.Utils + Note [Refine DEFAULT case alternatives] Exception 2 + + (W2c) In `GHC.Core.Opt.ConstantFold.caseRules`, disable the rule for + `dataToTag#` in the case of `type data`. We do not want to transform + case dataToTag# x of t -> blah + into + case x of { A -> ...; B -> .. } + because again that conjures up the type-level-only data contructors + `A` and `B` in a pattern, violating (I1) (#23023). + The main parts of the implementation are: -* (R0): The parser recognizes `type data` (but not `type newtype`). +* The parser recognizes `type data` (but not `type newtype`); this ensures (R0). * During the initial construction of the AST, GHC.Parser.PostProcess.checkNewOrData sets the `Bool` argument of the @@ -2134,54 +2204,6 @@ The main parts of the implementation are: `type data` declarations. When these are converted back to Hs types in a splice, the constructors are placed in the TcCls namespace. -* A `type data` declaration _never_ generates wrappers for its data - constructors, as they only make sense for value-level data constructors. - See `wrapped_reqd` in GHC.Types.Id.Make.mkDataConRep` for the place where - this check is implemented. - - This includes `type data` declarations implemented as GADTs, such as - this example from #22948: - - type data T a where - A :: T Int - B :: T a - - If `T` were an ordinary `data` declaration, then `A` would have a wrapper - to account for the GADT-like equality in its return type. Because `T` is - declared as a `type data` declaration, however, the wrapper is omitted. - -* Although `type data` data constructors do not exist at the value level, - it is still possible to match on a value whose type is headed by a `type data` - type constructor, such as this example from #22964: - - type data T a where - A :: T Int - B :: T a - - f :: T a -> () - f x = case x of {} - - This has two consequences: - - * During checking the coverage of `f`'s pattern matches, we treat `T` as if it - were an empty data type so that GHC does not warn the user to match against - `A` or `B`. (Otherwise, you end up with the bug reported in #22964.) - See GHC.HsToCore.Pmc.Solver.vanillaCompleteMatchTC. - - * In `GHC.Core.Utils.refineDataAlt`, do /not/ fill in the DEFAULT case with - the data constructor. See - Note [Refine DEFAULT case alternatives] Exception 2, in GHC.Core.Utils. - -* To prevent users from conjuring up `type data` values at the term level, we - disallow using the tagToEnum# function on a type headed by a `type data` - type. For instance, GHC will reject this code: - - type data Letter = A | B | C - - f :: Letter - f = tagToEnum# 0# - - See `GHC.Tc.Gen.App.checkTagToEnum`, specifically `check_enumeration`. -} warnNoDerivStrat :: Maybe (LDerivStrategy GhcRn) diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 44a35028cd..818ec4e991 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -1222,7 +1222,8 @@ tcTagToEnum tc_fun fun_ctxt tc_args res_ty vanilla_result = rebuildHsApps tc_fun fun_ctxt tc_args res_ty check_enumeration ty' tc - | -- isTypeDataTyCon: see Note [Type data declarations] in GHC.Rename.Module + | -- isTypeDataTyCon: see wrinkle (W1) in + -- Note [Type data declarations] in GHC.Rename.Module isTypeDataTyCon tc = addErrTc (TcRnTagToEnumResTyTypeData ty') | isEnumerationTyCon tc = return () | otherwise = addErrTc (TcRnTagToEnumResTyNotAnEnum ty') |