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 files changed, 157 insertions, 75 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 3f6989e9f9..8dae970dee 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/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]
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index a2daa7d900..854ebd3bf6 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/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
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 3539b6e0e5..31da54dca7 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/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 $
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 58353483dc..00346aa722 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/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
diff --git a/testsuite/tests/gadt/T14719.stderr b/testsuite/tests/gadt/T14719.stderr
index cfac00c0c0..e71f0e78e5 100644
--- a/testsuite/tests/gadt/T14719.stderr
+++ b/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’
   |
diff --git a/testsuite/tests/indexed-types/should_fail/T14033.stderr b/testsuite/tests/indexed-types/should_fail/T14033.stderr
index fbc6b54486..d302c6dfdc 100644
--- a/testsuite/tests/indexed-types/should_fail/T14033.stderr
+++ b/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’
diff --git a/testsuite/tests/indexed-types/should_fail/T2334A.stderr b/testsuite/tests/indexed-types/should_fail/T2334A.stderr
index d4cd3285c2..75d33cd3eb 100644
--- a/testsuite/tests/indexed-types/should_fail/T2334A.stderr
+++ b/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’
 
diff --git a/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr b/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr
index 42207d4f72..465476d603 100644
--- a/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr
+++ b/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’
diff --git a/testsuite/tests/parser/should_fail/readFail008.stderr b/testsuite/tests/parser/should_fail/readFail008.stderr
index 8fd289a301..e79a4ef8f2 100644
--- a/testsuite/tests/parser/should_fail/readFail008.stderr
+++ b/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’
diff --git a/testsuite/tests/polykinds/T11459.stderr b/testsuite/tests/polykinds/T11459.stderr
index 724395ecd7..ae65ea5613 100644
--- a/testsuite/tests/polykinds/T11459.stderr
+++ b/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)
diff --git a/testsuite/tests/typecheck/should_fail/T15523.stderr b/testsuite/tests/typecheck/should_fail/T15523.stderr
index 83b7cdbc60..07133257c5 100644
--- a/testsuite/tests/typecheck/should_fail/T15523.stderr
+++ b/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’
diff --git a/testsuite/tests/typecheck/should_fail/T15796.stderr b/testsuite/tests/typecheck/should_fail/T15796.stderr
index 3aa7ae8d65..81cbc85b63 100644
--- a/testsuite/tests/typecheck/should_fail/T15796.stderr
+++ b/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’
diff --git a/testsuite/tests/typecheck/should_fail/T17955.stderr b/testsuite/tests/typecheck/should_fail/T17955.stderr
index 0762facf45..3b5a5b2676 100644
--- a/testsuite/tests/typecheck/should_fail/T17955.stderr
+++ b/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’
diff --git a/testsuite/tests/typecheck/should_fail/T18891a.stderr b/testsuite/tests/typecheck/should_fail/T18891a.stderr
index 881924c8a1..a1ef9607bf 100644
--- a/testsuite/tests/typecheck/should_fail/T18891a.stderr
+++ b/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’
diff --git a/testsuite/tests/typecheck/should_fail/T21447.hs b/testsuite/tests/typecheck/should_fail/T21447.hs
new file mode 100644
index 0000000000..7a6938d5ad
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/typecheck/should_fail/T21447.stderr b/testsuite/tests/typecheck/should_fail/T21447.stderr
new file mode 100644
index 0000000000..aeba975cba
--- /dev/null
+++ b/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’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 51d73be7ed..efad13aacd 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail156.stderr b/testsuite/tests/typecheck/should_fail/tcfail156.stderr
index 280f118f90..e50ebcbde4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail156.stderr
+++ b/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’