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

3 files changed, 97 insertions, 41 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 $