[Git][ghc/ghc][wip/T22948] 3 commits: Don't generate datacon wrappers for `type data` declarations
Ryan Scott (@RyanGlScott)
gitlab at gitlab.haskell.org
Tue Feb 21 01:44:47 UTC 2023
Ryan Scott pushed to branch wip/T22948 at Glasgow Haskell Compiler / GHC
Commits:
4327d635 by Ryan Scott at 2023-02-20T20:44:34-05:00
Don't generate datacon wrappers for `type data` declarations
Data constructor wrappers only make sense for _value_-level data constructors,
but data constructors for `type data` declarations only exist at the _type_
level. This patch does the following:
* The criteria in `GHC.Types.Id.Make.mkDataConRep` for whether a data
constructor receives a wrapper now consider whether or not its parent data
type was declared with `type data`, omitting a wrapper if this is the case.
* Now that `type data` data constructors no longer receive wrappers, there is a
spot of code in `refineDefaultAlt` that panics when it encounters a value
headed by a `type data` type constructor. I've fixed this with a special case
in `refineDefaultAlt` and expanded `Note [Refine DEFAULT case alternatives]`
to explain why we do this.
Fixes #22948.
- - - - -
96dc58b9 by Ryan Scott at 2023-02-20T20:44:35-05:00
Treat type data declarations as empty when checking pattern-matching coverage
The data constructors for a `type data` declaration don't exist at the value
level, so we don't want GHC to warn users to match on them.
Fixes #22964.
- - - - -
ff8e99f6 by Ryan Scott at 2023-02-20T20:44:35-05:00
Disallow `tagToEnum#` on `type data` types
We don't want to allow users to conjure up values of a `type data` type using
`tagToEnum#`, as these simply don't exist at the value level.
- - - - -
18 changed files:
- compiler/GHC/Core/Utils.hs
- compiler/GHC/HsToCore/Pmc/Solver.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Types/Error/Codes.hs
- compiler/GHC/Types/Id/Make.hs
- + testsuite/tests/pmcheck/should_compile/T22964.hs
- testsuite/tests/pmcheck/should_compile/all.T
- + testsuite/tests/type-data/should_compile/T22948b.hs
- + testsuite/tests/type-data/should_compile/T22948b.stderr
- testsuite/tests/type-data/should_compile/all.T
- + testsuite/tests/type-data/should_fail/TDTagToEnum.hs
- + testsuite/tests/type-data/should_fail/TDTagToEnum.stderr
- testsuite/tests/type-data/should_fail/all.T
- + testsuite/tests/type-data/should_run/T22948a.hs
- testsuite/tests/type-data/should_run/all.T
Changes:
=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -728,9 +728,8 @@ refineDefaultAlt :: [Unique] -- ^ Uniques for constructing new binders
refineDefaultAlt us mult tycon tys imposs_deflt_cons all_alts
| Alt DEFAULT _ rhs : rest_alts <- all_alts
, isAlgTyCon tycon -- It's a data type, tuple, or unboxed tuples.
- , not (isNewTyCon tycon) -- We can have a newtype, if we are just doing an eval:
- -- case x of { DEFAULT -> e }
- -- and we don't want to fill in a default for them!
+ , not (isNewTyCon tycon) -- Exception 1 in Note [Refine DEFAULT case alternatives]
+ , not (isTypeDataTyCon tycon) -- Exception 2 in Note [Refine DEFAULT case alternatives]
, Just all_cons <- tyConDataCons_maybe tycon
, let imposs_data_cons = mkUniqSet [con | DataAlt con <- imposs_deflt_cons]
-- We now know it's a data type, so we can use
@@ -815,6 +814,39 @@ with a specific constructor is desirable.
`imposs_deflt_cons` argument is populated with constructors which
are matched elsewhere.
+There are two exceptions where we avoid refining a DEFAULT case:
+
+* Exception 1: Newtypes
+
+ We can have a newtype, if we are just doing an eval:
+
+ case x of { DEFAULT -> e }
+
+ And we don't want to fill in a default for them!
+
+* Exception 2: `type data` declarations
+
+ The data constructors for a `type data` declaration (see
+ Note [Type data declarations] in GHC.Rename.Module) do not exist at the
+ value level. Nevertheless, it is possible to strictly evaluate a value
+ whose type is a `type data` declaration. Test case
+ type-data/should_compile/T2294b.hs contains an example:
+
+ type data T a where
+ A :: T Int
+
+ f :: T a -> ()
+ f !x = ()
+
+ We want to generate the following Core for f:
+
+ f = \(@a) (x :: T a) ->
+ case x of
+ __DEFAULT -> ()
+
+ Namely, we do _not_ want to match on `A`, as it doesn't exist at the value
+ level!
+
Note [Combine identical alternatives]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If several alternatives are identical, merge them into a single
=====================================
compiler/GHC/HsToCore/Pmc/Solver.hs
=====================================
@@ -146,11 +146,16 @@ updRcm f (RCM vanilla pragmas)
-- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
vanillaCompleteMatchTC tc =
- let -- TYPE acts like an empty data type on the term-level (#14086), but
- -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
- -- special case.
- mb_dcs | tc == tYPETyCon = Just []
- | otherwise = tyConDataCons_maybe tc
+ let mb_dcs | -- TYPE acts like an empty data type on the term level (#14086),
+ -- but it is a PrimTyCon, so tyConDataCons_maybe returns Nothing.
+ -- Hence a special case.
+ 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.
+ isTypeDataTyCon tc = Just []
+ | otherwise = tyConDataCons_maybe tc
in vanillaCompleteMatch . mkUniqDSet . map RealDataCon <$> mb_dcs
-- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas)
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -2132,6 +2132,54 @@ 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)
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -277,6 +277,10 @@ instance Diagnostic TcRnMessage where
-> mkSimpleDecorated $
hang (text "Bad call to tagToEnum# at type" <+> ppr ty)
2 (text "Result type must be an enumeration type")
+ TcRnTagToEnumResTyTypeData ty
+ -> mkSimpleDecorated $
+ hang (text "Bad call to tagToEnum# at type" <+> ppr ty)
+ 2 (text "Result type cannot be headed by a `type data` type")
TcRnArrowIfThenElsePredDependsOnResultTy
-> mkSimpleDecorated $
text "Predicate type of `ifThenElse' depends on result type"
@@ -1391,6 +1395,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnTagToEnumResTyNotAnEnum{}
-> ErrorWithoutFlag
+ TcRnTagToEnumResTyTypeData{}
+ -> ErrorWithoutFlag
TcRnArrowIfThenElsePredDependsOnResultTy
-> ErrorWithoutFlag
TcRnIllegalHsBootFileDecl
@@ -1821,6 +1827,8 @@ instance Diagnostic TcRnMessage where
-> noHints
TcRnTagToEnumResTyNotAnEnum{}
-> noHints
+ TcRnTagToEnumResTyTypeData{}
+ -> noHints
TcRnArrowIfThenElsePredDependsOnResultTy
-> noHints
TcRnIllegalHsBootFileDecl
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -665,6 +665,20 @@ data TcRnMessage where
-}
TcRnTagToEnumResTyNotAnEnum :: Type -> TcRnMessage
+ {-| TcRnTagToEnumResTyTypeData is an error that occurs when the 'tagToEnum#'
+ function is given a result type that is headed by a @type data@ type, as
+ the data constructors of a @type data@ do not exist at the term level.
+
+ Example(s):
+ type data Letter = A | B | C
+
+ foo :: Letter
+ foo = tagToEnum# 0#
+
+ Test cases: type-data/should_fail/TDTagToEnum.hs
+ -}
+ TcRnTagToEnumResTyTypeData :: Type -> TcRnMessage
+
{-| TcRnArrowIfThenElsePredDependsOnResultTy is an error that occurs when the
predicate type of an ifThenElse expression in arrow notation depends on
the type of the result.
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -1222,6 +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 tc = addErrTc (TcRnTagToEnumResTyTypeData ty')
| isEnumerationTyCon tc = return ()
| otherwise = addErrTc (TcRnTagToEnumResTyNotAnEnum ty')
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -354,6 +354,7 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnTagToEnumMissingValArg" = 36495
GhcDiagnosticCode "TcRnTagToEnumUnspecifiedResTy" = 08522
GhcDiagnosticCode "TcRnTagToEnumResTyNotAnEnum" = 49356
+ GhcDiagnosticCode "TcRnTagToEnumResTyTypeData" = 96189
GhcDiagnosticCode "TcRnArrowIfThenElsePredDependsOnResultTy" = 55868
GhcDiagnosticCode "TcRnIllegalHsBootFileDecl" = 58195
GhcDiagnosticCode "TcRnRecursivePatternSynonym" = 72489
=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -789,20 +789,40 @@ mkDataConRep dc_bang_opts fam_envs wrap_name data_con
(unboxers, boxers) = unzip wrappers
(rep_tys, rep_strs) = unzip (concat rep_tys_w_strs)
+ -- This is True if the data constructor or class dictionary constructor
+ -- needs a wrapper. This wrapper is injected into the program later in the
+ -- CoreTidy pass. See Note [Injecting implicit bindings] in GHC.Iface.Tidy,
+ -- along with the accompanying implementation in getTyConImplicitBinds.
wrapper_reqd =
(not new_tycon
-- (Most) newtypes have only a worker, with the exception
- -- of some newtypes written with GADT syntax. See below.
+ -- of some newtypes written with GADT syntax.
+ -- See dataConUserTyVarsNeedWrapper below.
&& (any isBanged (ev_ibangs ++ arg_ibangs)))
-- Some forcing/unboxing (includes eq_spec)
|| isFamInstTyCon tycon -- Cast result
- || dataConUserTyVarsNeedWrapper data_con
+ || (dataConUserTyVarsNeedWrapper data_con
-- If the data type was written with GADT syntax and
-- orders the type variables differently from what the
-- worker expects, it needs a data con wrapper to reorder
-- the type variables.
-- See Note [Data con wrappers and GADT syntax].
- -- NB: All GADTs return true from this function
+ --
+ -- NB: All GADTs return true from this function, but there
+ -- is one exception that we must check below.
+ && not (isTypeDataTyCon tycon))
+ -- An exception to this rule is `type data` declarations.
+ -- Their data constructors only live at the type level and
+ -- therefore do not need wrappers.
+ -- See Note [Type data declarations] in GHC.Rename.Module.
+ --
+ -- Note that the other checks in this definition will
+ -- return False for `type data` declarations, as:
+ --
+ -- - They cannot be newtypes
+ -- - They cannot have strict fields
+ -- - They cannot be data family instances
+ -- - They cannot have datatype contexts
|| not (null stupid_theta)
-- If the data constructor has a datatype context,
-- we need a wrapper in order to drop the stupid arguments.
=====================================
testsuite/tests/pmcheck/should_compile/T22964.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeData #-}
+module X where
+
+type data T1 a where
+ A1 :: T1 Int
+ B1 :: T1 a
+
+f1 :: T1 a -> ()
+f1 x = case x of {}
+
+type data T2 a where
+ A2 :: T2 Int
+
+f2 :: T2 a -> ()
+f2 x = case x of {}
=====================================
testsuite/tests/pmcheck/should_compile/all.T
=====================================
@@ -158,3 +158,4 @@ test('EmptyCase009', [], compile, [overlapping_incomplete])
test('EmptyCase010', [], compile, [overlapping_incomplete])
test('T19271', [], compile, [overlapping_incomplete])
test('T21761', [], compile, [overlapping_incomplete])
+test('T22964', [], compile, [overlapping_incomplete])
=====================================
testsuite/tests/type-data/should_compile/T22948b.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeData #-}
+module T22948b where
+
+type data T a where
+ A :: T Int
+
+f :: T a -> ()
+f !x = ()
=====================================
testsuite/tests/type-data/should_compile/T22948b.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T22948b.hs:8:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
+ Pattern match has inaccessible right hand side
+ In an equation for ‘f’: f !x = ...
=====================================
testsuite/tests/type-data/should_compile/all.T
=====================================
@@ -5,3 +5,4 @@ test('TDGoodConsConstraints', normal, compile, [''])
test('TDVector', normal, compile, [''])
test('TD_TH_splice', js_broken(22576), compile, [''])
test('T22315a', [extra_files(['T22315a/'])], multimod_compile, ['T22315a.Lib T22315a.Main', '-v0'])
+test('T22948b', normal, compile, [''])
=====================================
testsuite/tests/type-data/should_fail/TDTagToEnum.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeData #-}
+module TDTagToEnum where
+
+import GHC.Exts (tagToEnum#)
+
+type data Letter = A | B | C
+
+f :: Letter
+f = tagToEnum# 0#
=====================================
testsuite/tests/type-data/should_fail/TDTagToEnum.stderr
=====================================
@@ -0,0 +1,6 @@
+
+TDTagToEnum.hs:10:5: error: [GHC-96189]
+ • Bad call to tagToEnum# at type Letter
+ Result type cannot be headed by a `type data` type
+ • In the expression: tagToEnum# 0#
+ In an equation for ‘f’: f = tagToEnum# 0#
=====================================
testsuite/tests/type-data/should_fail/all.T
=====================================
@@ -11,4 +11,5 @@ test('TDRecordsH98', normal, compile_fail, [''])
test('TDRecursive', normal, compile_fail, [''])
test('TDStrictnessGADT', normal, compile_fail, [''])
test('TDStrictnessH98', normal, compile_fail, [''])
+test('TDTagToEnum', normal, compile_fail, [''])
test('T22332b', normal, compile_fail, [''])
=====================================
testsuite/tests/type-data/should_run/T22948a.hs
=====================================
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeData #-}
+module Main where
+
+type data T a where
+ A :: T Int
+ B :: T a
+
+main = return ()
=====================================
testsuite/tests/type-data/should_run/all.T
=====================================
@@ -1,3 +1,4 @@
test('T22332a', exit_code(1), compile_and_run, [''])
test('T22315b', extra_files(['T22315b.hs']), ghci_script, ['T22315b.script'])
test('T22500', normal, compile_and_run, [''])
+test('T22948a', normal, compile_and_run, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/974a9fa85f53ad583c459712749fc8eea2e1f496...ff8e99f69b203559b784014ab26c59b5553d128a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/974a9fa85f53ad583c459712749fc8eea2e1f496...ff8e99f69b203559b784014ab26c59b5553d128a
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230220/0ff2a552/attachment-0001.html>
More information about the ghc-commits
mailing list