[Git][ghc/ghc][master] Clearer error msg for newtype GADTs with defaulted kind
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu Oct 13 10:00:41 UTC 2022
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
eda6c05e by Finley McIlwaine at 2022-10-13T06:00:17-04:00
Clearer error msg for newtype GADTs with defaulted kind
When a newtype introduces GADT eq_specs due to a defaulted
RuntimeRep, we detect this and print the error message with
explicit kinds.
This also refactors newtype type checking to use the new
diagnostic infra.
Fixes #21447
- - - - -
18 changed files:
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Types/Error/Codes.hs
- testsuite/tests/gadt/T14719.stderr
- testsuite/tests/indexed-types/should_fail/T14033.stderr
- testsuite/tests/indexed-types/should_fail/T2334A.stderr
- testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr
- testsuite/tests/parser/should_fail/readFail008.stderr
- testsuite/tests/polykinds/T11459.stderr
- testsuite/tests/typecheck/should_fail/T15523.stderr
- testsuite/tests/typecheck/should_fail/T15796.stderr
- testsuite/tests/typecheck/should_fail/T17955.stderr
- testsuite/tests/typecheck/should_fail/T18891a.stderr
- + testsuite/tests/typecheck/should_fail/T21447.hs
- + testsuite/tests/typecheck/should_fail/T21447.stderr
- testsuite/tests/typecheck/should_fail/all.T
- testsuite/tests/typecheck/should_fail/tcfail156.stderr
Changes:
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1000,6 +1000,40 @@ instance Diagnostic TcRnMessage where
TcRnTypeDataForbids feature
-> mkSimpleDecorated $
ppr feature <+> text "are not allowed in type data declarations."
+ TcRnIllegalNewtype con show_linear_types reason
+ -> mkSimpleDecorated $
+ vcat [msg, additional]
+ where
+ (msg,additional) =
+ case reason of
+ DoesNotHaveSingleField n_flds ->
+ (sep [
+ text "A newtype constructor must have exactly one field",
+ nest 2 $
+ text "but" <+> quotes (ppr con) <+> text "has" <+> speakN n_flds
+ ],
+ ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con))
+ IsNonLinear ->
+ (text "A newtype constructor must be linear",
+ ppr con <+> dcolon <+> ppr (dataConDisplayType True con))
+ IsGADT ->
+ (text "A newtype must not be a GADT",
+ ppr con <+> dcolon <+> pprWithExplicitKindsWhen sneaky_eq_spec (ppr $ dataConDisplayType show_linear_types con))
+ HasConstructorContext ->
+ (text "A newtype constructor must not have a context in its type",
+ ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con))
+ HasExistentialTyVar ->
+ (text "A newtype constructor must not have existential type variables",
+ ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con))
+ HasStrictnessAnnotation ->
+ (text "A newtype constructor must not have a strictness annotation", empty)
+
+ -- Is there an EqSpec involving an invisible binder? If so, print the
+ -- error message with explicit kinds.
+ invisible_binders = filter isInvisibleTyConBinder (tyConBinders $ dataConTyCon con)
+ sneaky_eq_spec
+ = any (\eq -> any (( == eqSpecTyVar eq) . binderVar) invisible_binders)
+ $ dataConEqSpec con
diagnosticReason = \case
TcRnUnknownMessage m
@@ -1334,6 +1368,8 @@ instance Diagnostic TcRnMessage where
-> ErrorWithoutFlag
TcRnTypeDataForbids{}
-> ErrorWithoutFlag
+ TcRnIllegalNewtype{}
+ -> ErrorWithoutFlag
diagnosticHints = \case
TcRnUnknownMessage m
@@ -1670,10 +1706,11 @@ instance Diagnostic TcRnMessage where
-> [suggestExtension LangExt.TypeData]
TcRnTypeDataForbids{}
-> noHints
+ TcRnIllegalNewtype{}
+ -> noHints
diagnosticCode = constructorCode
-
-- | Change [x] to "x", [x, y] to "x and y", [x, y, z] to "x, y, and z",
-- and so on. The `and` stands for any `conjunction`, which is passed in.
commafyWith :: SDoc -> [SDoc] -> [SDoc]
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -13,6 +13,7 @@ module GHC.Tc.Errors.Types (
, pprFixedRuntimeRepProvenance
, ShadowedNameProvenance(..)
, RecordFieldPart(..)
+ , IllegalNewtypeReason(..)
, InjectivityErrReason(..)
, HasKinds(..)
, hasKinds
@@ -2288,6 +2289,34 @@ data TcRnMessage where
TcRnNoExplicitAssocTypeOrDefaultDeclaration
:: Name
-> TcRnMessage
+ {-| TcRnIllegalNewtype is an error that occurs when a newtype:
+
+ * Does not have exactly one field, or
+ * is non-linear, or
+ * is a GADT, or
+ * has a context in its constructor's type, or
+ * has existential type variables in its constructor's type, or
+ * has strictness annotations.
+
+ Test cases:
+ testsuite/tests/gadt/T14719
+ testsuite/tests/indexed-types/should_fail/T14033
+ testsuite/tests/indexed-types/should_fail/T2334A
+ testsuite/tests/linear/should_fail/LinearGADTNewtype
+ testsuite/tests/parser/should_fail/readFail008
+ testsuite/tests/polykinds/T11459
+ testsuite/tests/typecheck/should_fail/T15523
+ testsuite/tests/typecheck/should_fail/T15796
+ testsuite/tests/typecheck/should_fail/T17955
+ testsuite/tests/typecheck/should_fail/T18891a
+ testsuite/tests/typecheck/should_fail/T21447
+ testsuite/tests/typecheck/should_fail/tcfail156
+ -}
+ TcRnIllegalNewtype
+ :: DataCon
+ -> Bool -- ^ True if linear types enabled
+ -> IllegalNewtypeReason
+ -> TcRnMessage
{-| TcRnIllegalTypeData is an error that occurs when a @type data@
declaration occurs without the TypeOperators extension.
@@ -2333,6 +2362,7 @@ instance Outputable TypeDataForbids where
-- | Specifies which back ends can handle a requested foreign import or export
type ExpectedBackends = [Backend]
+
-- | Specifies which calling convention is unsupported on the current platform
data UnsupportedCallConvention
= StdCallConvUnsupported
@@ -2384,6 +2414,17 @@ pprFixedRuntimeRepProvenance FixedRuntimeRepDataConField = text "data constructo
pprFixedRuntimeRepProvenance FixedRuntimeRepPatSynSigArg = text "pattern synonym argument"
pprFixedRuntimeRepProvenance FixedRuntimeRepPatSynSigRes = text "pattern synonym scrutinee"
+-- | Why the particular illegal newtype error arose together with more
+-- information, if any.
+data IllegalNewtypeReason
+ = DoesNotHaveSingleField !Int
+ | IsNonLinear
+ | IsGADT
+ | HasConstructorContext
+ | HasExistentialTyVar
+ | HasStrictnessAnnotation
+ deriving Generic
+
-- | Why the particular injectivity error arose together with more information,
-- if any.
data InjectivityErrReason
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -35,7 +35,7 @@ import GHC.Driver.Config.HsToCore
import GHC.Hs
import GHC.Tc.Errors.Types ( TcRnMessage(..), FixedRuntimeRepProvenance(..)
- , mkTcRnUnknownMessage )
+ , mkTcRnUnknownMessage, IllegalNewtypeReason (..) )
import GHC.Tc.TyCl.Build
import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX
, reportUnsolvedEqualities )
@@ -4530,40 +4530,30 @@ checkValidDataCon dflags existential_ok tc con
-------------------------------
checkNewDataCon :: DataCon -> TcM ()
-- Further checks for the data constructor of a newtype
+-- You might wonder if we need to check for an unlifted newtype
+-- without -XUnliftedNewTypes, such as
+-- newtype C = MkC Int#
+-- But they are caught earlier, by GHC.Tc.Gen.HsType.checkDataKindSig
checkNewDataCon con
- = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
- -- One argument
-
- ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
- ; let allowedArgType =
- unlifted_newtypes || typeLevity_maybe (scaledThing arg_ty1) == Just Lifted
- ; checkTc allowedArgType $ mkTcRnUnknownMessage $ mkPlainError noHints $ vcat
- [ text "A newtype cannot have an unlifted argument type"
- , text "Perhaps you intended to use UnliftedNewtypes"
- ]
- ; show_linear_types <- xopt LangExt.LinearTypes <$> getDynFlags
-
- ; let check_con what msg =
- checkTc what $ mkTcRnUnknownMessage $ mkPlainError noHints $
- (msg $$ ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con))
+ = do { show_linear_types <- xopt LangExt.LinearTypes <$> getDynFlags
+
+ ; checkTc (isSingleton arg_tys) $
+ TcRnIllegalNewtype con show_linear_types (DoesNotHaveSingleField $ length arg_tys)
; checkTc (ok_mult (scaledMult arg_ty1)) $
- mkTcRnUnknownMessage $ mkPlainError noHints $ text "A newtype constructor must be linear"
+ TcRnIllegalNewtype con show_linear_types IsNonLinear
- ; check_con (null eq_spec) $
- text "A newtype constructor must have a return type of form T a1 ... an"
- -- Return type is (T a b c)
+ ; checkTc (null eq_spec) $
+ TcRnIllegalNewtype con show_linear_types IsGADT
- ; check_con (null theta) $
- text "A newtype constructor cannot have a context in its type"
+ ; checkTc (null theta) $
+ TcRnIllegalNewtype con show_linear_types HasConstructorContext
- ; check_con (null ex_tvs) $
- text "A newtype constructor cannot have existential type variables"
- -- No existentials
+ ; checkTc (null ex_tvs) $
+ TcRnIllegalNewtype con show_linear_types HasExistentialTyVar
- ; checkTc (all ok_bang (dataConSrcBangs con))
- (newtypeStrictError con)
- -- No strictness annotations
+ ; checkTc (all ok_bang (dataConSrcBangs con)) $
+ TcRnIllegalNewtype con show_linear_types HasStrictnessAnnotation
}
where
(_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
@@ -5334,18 +5324,6 @@ newtypeConError tycon n
sep [text "A newtype must have exactly one constructor,",
nest 2 $ text "but" <+> quotes (ppr tycon) <+> text "has" <+> speakN n ]
-newtypeStrictError :: DataCon -> TcRnMessage
-newtypeStrictError con
- = mkTcRnUnknownMessage $ mkPlainError noHints $
- sep [text "A newtype constructor cannot have a strictness annotation,",
- nest 2 $ text "but" <+> quotes (ppr con) <+> text "does"]
-
-newtypeFieldErr :: DataCon -> Int -> TcRnMessage
-newtypeFieldErr con_name n_flds
- = mkTcRnUnknownMessage $ mkPlainError noHints $
- sep [text "The constructor of a newtype must have exactly one field",
- nest 2 $ text "but" <+> quotes (ppr con_name) <+> text "has" <+> speakN n_flds]
-
badSigTyDecl :: Name -> TcRnMessage
badSigTyDecl tc_name
= mkTcRnUnknownMessage $ mkPlainError noHints $
=====================================
compiler/GHC/Types/Error/Codes.hs
=====================================
@@ -468,6 +468,12 @@ type family GhcDiagnosticCode c = n | n -> c where
GhcDiagnosticCode "TcRnNoExplicitAssocTypeOrDefaultDeclaration" = 08585
GhcDiagnosticCode "TcRnIllegalTypeData" = 15013
GhcDiagnosticCode "TcRnTypeDataForbids" = 67297
+ GhcDiagnosticCode "DoesNotHaveSingleField" = 23517
+ GhcDiagnosticCode "IsNonLinear" = 38291
+ GhcDiagnosticCode "IsGADT" = 89498
+ GhcDiagnosticCode "HasConstructorContext" = 17440
+ GhcDiagnosticCode "HasExistentialTyVar" = 07525
+ GhcDiagnosticCode "HasStrictnessAnnotation" = 04049
-- TcRnPragmaWarning
GhcDiagnosticCode "WarningTxt" = 63394
@@ -587,6 +593,7 @@ type family ConRecursInto con where
ConRecursInto "TcRnCannotDeriveInstance" = 'Just DeriveInstanceErrReason
ConRecursInto "TcRnPragmaWarning" = 'Just (WarningTxt GhcRn)
ConRecursInto "TcRnNotInScope" = 'Just NotInScopeError
+ ConRecursInto "TcRnIllegalNewtype" = 'Just IllegalNewtypeReason
------------------
-- FFI errors
=====================================
testsuite/tests/gadt/T14719.stderr
=====================================
@@ -8,9 +8,10 @@ T14719.hs:5:3: error:
5 | MkFoo1 :: Bool
| ^^^^^^^^^^^^^^
-T14719.hs:8:3: error:
- • The constructor of a newtype must have exactly one field
+T14719.hs:8:3: error: [GHC-23517]
+ • A newtype constructor must have exactly one field
but ‘MkFoo2’ has none
+ MkFoo2 :: Foo2
• In the definition of data constructor ‘MkFoo2’
In the newtype declaration for ‘Foo2’
|
=====================================
testsuite/tests/indexed-types/should_fail/T14033.stderr
=====================================
@@ -1,6 +1,7 @@
-T14033.hs:5:16: error:
- • The constructor of a newtype must have exactly one field
+T14033.hs:5:16: error: [GHC-23517]
+ • A newtype constructor must have exactly one field
but ‘Zero’ has none
+ Zero :: Zero
• In the definition of data constructor ‘Zero’
In the newtype declaration for ‘Zero’
=====================================
testsuite/tests/indexed-types/should_fail/T2334A.stderr
=====================================
@@ -1,13 +1,14 @@
-T2334A.hs:9:26: error:
- • The constructor of a newtype must have exactly one field
- but ‘F’ has two
+T2334A.hs:9:26: error: [GHC-23517]
+ • A newtype constructor must have exactly one field but ‘F’ has two
+ F :: () -> () -> F ()
• In the definition of data constructor ‘F’
In the newtype instance declaration for ‘F’
-T2334A.hs:10:27: error:
- • The constructor of a newtype must have exactly one field
+T2334A.hs:10:27: error: [GHC-23517]
+ • A newtype constructor must have exactly one field
but ‘H’ has none
+ H :: F Int
• In the definition of data constructor ‘H’
In the newtype instance declaration for ‘F’
=====================================
testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr
=====================================
@@ -1,5 +1,6 @@
-LinearGADTNewtype.hs:3:4: error:
+LinearGADTNewtype.hs:3:4: error: [GHC-38291]
• A newtype constructor must be linear
+ A :: Int -> A
• In the definition of data constructor ‘A’
In the newtype declaration for ‘A’
=====================================
testsuite/tests/parser/should_fail/readFail008.stderr
=====================================
@@ -1,6 +1,5 @@
-readFail008.hs:5:15:
- A newtype constructor cannot have a strictness annotation,
- but ‘T’ does
- In the definition of data constructor ‘T’
- In the newtype declaration for ‘N’
+readFail008.hs:5:15: error: [GHC-04049]
+ • A newtype constructor must not have a strictness annotation
+ • In the definition of data constructor ‘T’
+ In the newtype declaration for ‘N’
=====================================
testsuite/tests/polykinds/T11459.stderr
=====================================
@@ -1,6 +1,6 @@
-T11459.hs:9:20: error:
- • A newtype constructor cannot have existential type variables
+T11459.hs:9:20: error: [GHC-07525]
+ • A newtype constructor must not have existential type variables
Parser :: forall a {k}.
(forall (f :: k -> *) (r :: k).
Failure f r -> Success a f r -> f r)
=====================================
testsuite/tests/typecheck/should_fail/T15523.stderr
=====================================
@@ -1,6 +1,7 @@
-T15523.hs:5:20: error:
- • The constructor of a newtype must have exactly one field
+T15523.hs:5:20: error: [GHC-23517]
+ • A newtype constructor must have exactly one field
but ‘Foo’ has none
+ Foo :: Duration
• In the definition of data constructor ‘Foo’
In the newtype declaration for ‘Duration’
=====================================
testsuite/tests/typecheck/should_fail/T15796.stderr
=====================================
@@ -1,6 +1,6 @@
-T15796.hs:6:3: error:
- • A newtype constructor cannot have a context in its type
+T15796.hs:6:3: error: [GHC-17440]
+ • A newtype constructor must not have a context in its type
MkN :: forall a. Show a => a -> N a
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
=====================================
testsuite/tests/typecheck/should_fail/T17955.stderr
=====================================
@@ -1,6 +1,6 @@
-T17955.hs:6:13: error:
- • A newtype constructor cannot have a context in its type
+T17955.hs:6:13: error: [GHC-17440]
+ • A newtype constructor must not have a context in its type
T :: Coercible () T => () -> T
• In the definition of data constructor ‘T’
In the newtype declaration for ‘T’
=====================================
testsuite/tests/typecheck/should_fail/T18891a.stderr
=====================================
@@ -1,12 +1,12 @@
-T18891a.hs:8:4: error:
- • A newtype constructor must have a return type of form T a1 ... an
- MkN1 :: N1 -> N1
+T18891a.hs:8:4: error: [GHC-89498]
+ • A newtype must not be a GADT
+ MkN1 :: N1 @GHC.Types.LiftedRep -> N1 @GHC.Types.LiftedRep
• In the definition of data constructor ‘MkN1’
In the newtype declaration for ‘N1’
-T18891a.hs:12:3: error:
- • A newtype constructor must have a return type of form T a1 ... an
- MkN2 :: N2 -> N2
+T18891a.hs:12:3: error: [GHC-89498]
+ • A newtype must not be a GADT
+ MkN2 :: N2 @GHC.Types.LiftedRep -> N2 @GHC.Types.LiftedRep
• In the definition of data constructor ‘MkN2’
In the newtype declaration for ‘N2’
=====================================
testsuite/tests/typecheck/should_fail/T21447.hs
=====================================
@@ -0,0 +1,8 @@
+module T21447 where
+
+import Data.Kind (Type)
+import GHC.Exts (TYPE)
+
+type H :: TYPE r -> Type
+newtype H a where
+ H :: a -> H a
=====================================
testsuite/tests/typecheck/should_fail/T21447.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T21447.hs:8:3: error: [GHC-89498]
+ • A newtype must not be a GADT
+ H :: forall a. a -> H @GHC.Types.LiftedRep a
+ • In the definition of data constructor ‘H’
+ In the newtype declaration for ‘H’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -659,3 +659,4 @@ test('T21338', normal, compile_fail, [''])
test('T21158', normal, compile_fail, [''])
test('T21583', normal, compile_fail, [''])
test('MissingDefaultMethodBinding', normal, compile_fail, [''])
+test('T21447', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_fail/tcfail156.stderr
=====================================
@@ -1,6 +1,6 @@
-tcfail156.hs:7:15:
- A newtype constructor cannot have existential type variables
- Foo :: forall a. a -> Foo
- In the definition of data constructor ‘Foo’
- In the newtype declaration for ‘Foo’
+tcfail156.hs:7:15: error: [GHC-07525]
+ • A newtype constructor must not have existential type variables
+ Foo :: forall a. a -> Foo
+ • In the definition of data constructor ‘Foo’
+ In the newtype declaration for ‘Foo’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/eda6c05e65144b35de62c33d0fd5d35a417233ac
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/eda6c05e65144b35de62c33d0fd5d35a417233ac
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/20221013/30aa57d8/attachment-0001.html>
More information about the ghc-commits
mailing list