Kind TyCons: require KindSignatures, not DataKinds

  Uses of a TyCon in a kind signature required users to enable
  DataKinds, which didn't make much sense, e.g. in

    type U = Type
    type MyMaybe (a :: U) = MyNothing | MyJust a

  Now the DataKinds error is restricted to data constructors;
  the use of kind-level type constructors is instead gated behind
  -XKindSignatures.

  This patch also adds a convenience pattern synonym for patching
  on both a TyCon or a TcTyCon stored in a TcTyThing, used in
  tcTyVar and tc_infer_id.

  fixes #20873

10 files changed, 78 insertions, 26 deletions

diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 216b7c057e..b878a5b45b 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
+{-# LANGUAGE ViewPatterns        #-}
 {-# LANGUAGE DisambiguateRecordFields #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
@@ -752,8 +753,7 @@ tc_infer_id id_name
 
              AGlobal (AConLike (RealDataCon con)) -> tcInferDataCon con
              AGlobal (AConLike (PatSynCon ps)) -> tcInferPatSyn id_name ps
-             AGlobal (ATyCon tc) -> fail_tycon tc
-             ATcTyCon tc -> fail_tycon tc
+             (tcTyThingTyCon_maybe -> Just tc) -> fail_tycon tc -- TyCon or TcTyCon
              ATyVar name _ -> fail_tyvar name
 
              _ -> failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 6fd2be5b05..b5386aa6a7 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1536,8 +1536,8 @@ tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
 -- application. In particular, for a HsTyVar (which includes type
 -- constructors, it does not zoom off into tcInferTyApps and family
 -- saturation
-tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
-  = tcTyVar mode tv
+tcInferTyAppHead _ (L _ (HsTyVar _ _ (L _ tv)))
+  = tcTyVar tv
 tcInferTyAppHead mode ty
   = tc_infer_lhs_type mode ty
 
@@ -1558,7 +1558,7 @@ tcInferTyApps, tcInferTyApps_nosat
     -> LHsType GhcRn        -- ^ Function (for printing only)
     -> TcType               -- ^ Function
     -> [LHsTypeArg GhcRn]   -- ^ Args
-    -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
+    -> TcM (TcType, TcKind) -- ^ (f args, result kind)
 tcInferTyApps mode hs_ty fun hs_args
   = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args
        ; saturateFamApp f_args res_k }
@@ -1967,24 +1967,19 @@ tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
 tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
 
 ---------------------------
-tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
+tcTyVar :: Name -> TcM (TcType, TcKind)
 -- See Note [Type checking recursive type and class declarations]
 -- in GHC.Tc.TyCl
 -- This does not instantiate. See Note [Do not always instantiate eagerly in types]
-tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
+tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
   = do { traceTc "lk1" (ppr name)
        ; thing <- tcLookup name
        ; case thing of
            ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
 
            -- See Note [Recursion through the kinds]
-           ATcTyCon tc_tc
-             -> do { check_tc tc_tc
-                   ; return (mkTyConTy tc_tc, tyConKind tc_tc) }
-
-           AGlobal (ATyCon tc)
-             -> do { check_tc tc
-                   ; return (mkTyConTy tc, tyConKind tc) }
+           (tcTyThingTyCon_maybe -> Just tc) -- TyCon or TcTyCon
+             -> return (mkTyConTy tc, tyConKind tc)
 
            AGlobal (AConLike (RealDataCon dc))
              -> do { data_kinds <- xoptM LangExt.DataKinds
@@ -2006,13 +2001,6 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
 
            _  -> wrongThingErr "type" thing name }
   where
-    check_tc :: TyCon -> TcM ()
-    check_tc tc = do { data_kinds   <- xoptM LangExt.DataKinds
-                     ; unless (isTypeLevel (mode_tyki mode) ||
-                               data_kinds ||
-                               isKindTyCon tc) $
-                       promotionErr name NoDataKindsTC }
-
     -- We cannot promote a data constructor with a context that contains
     -- constraints other than equalities, so error if we find one.
     -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
@@ -4279,7 +4267,6 @@ promotionErr name err
                               -> text "it has an unpromotable context"
                                  <+> quotes (ppr pred)
                FamDataConPE   -> text "it comes from a data family instance"
-               NoDataKindsTC  -> text "perhaps you intended to use DataKinds"
                NoDataKindsDC  -> text "perhaps you intended to use DataKinds"
                PatSynPE       -> text "pattern synonyms cannot be promoted"
                RecDataConPE   -> same_rec_group_msg
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index df9384fea2..2de119b416 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -46,7 +46,8 @@ module GHC.Tc.Types(
 
         -- Typechecker types
         TcTypeEnv, TcBinderStack, TcBinder(..),
-        TcTyThing(..), PromotionErr(..),
+        TcTyThing(..), tcTyThingTyCon_maybe,
+        PromotionErr(..),
         IdBindingInfo(..), ClosedTypeId, RhsNames,
         IsGroupClosed(..),
         SelfBootInfo(..),
@@ -1125,6 +1126,12 @@ data TcTyThing
 
   | APromotionErr PromotionErr
 
+-- | Matches on either a global 'TyCon' or a 'TcTyCon'.
+tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon
+tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc
+tcTyThingTyCon_maybe (ATcTyCon tc_tc)      = Just tc_tc
+tcTyThingTyCon_maybe _                     = Nothing
+
 data PromotionErr
   = TyConPE          -- TyCon used in a kind before we are ready
                      --     data T :: T -> * where ...
@@ -1142,7 +1149,6 @@ data PromotionErr
 
   | RecDataConPE     -- Data constructor in a recursive loop
                      -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
-  | NoDataKindsTC    -- -XDataKinds not enabled (for a tycon)
   | NoDataKindsDC    -- -XDataKinds not enabled (for a datacon)
 
 instance Outputable TcTyThing where     -- Debugging only
@@ -1337,7 +1343,6 @@ instance Outputable PromotionErr where
   ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
                                       <+> parens (ppr pred)
   ppr RecDataConPE                = text "RecDataConPE"
-  ppr NoDataKindsTC               = text "NoDataKindsTC"
   ppr NoDataKindsDC               = text "NoDataKindsDC"
 
 --------------
@@ -1362,7 +1367,6 @@ peCategory PatSynPE               = "pattern synonym"
 peCategory FamDataConPE           = "data constructor"
 peCategory ConstrainedDataConPE{} = "data constructor"
 peCategory RecDataConPE           = "data constructor"
-peCategory NoDataKindsTC          = "type constructor"
 peCategory NoDataKindsDC          = "data constructor"
 
 {-
diff --git a/testsuite/tests/typecheck/should_compile/T20873.hs b/testsuite/tests/typecheck/should_compile/T20873.hs
new file mode 100644
index 0000000000..825b12aece
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20873.hs
@@ -0,0 +1,23 @@
+
+{-# LANGUAGE GADTSyntax, StandaloneKindSignatures, NoDataKinds #-}
+
+module T20873 where
+
+import Data.Kind ( Type )
+
+type U a = Type
+type V a = a
+
+type MyMaybe1 :: U Type -> U Type
+data MyMaybe1 a = MyJust1 a | MyNothing1
+
+type MyMaybe2 :: V Type -> V Type
+data MyMaybe2 a = MyJust2 a | MyNothing2
+
+data MyMaybe3 (a :: U Type) :: U Type where
+  MyJust3    :: a -> MyMaybe3 a
+  MyNothing3 ::      MyMaybe3 a
+
+data MyMaybe4 (a :: V Type) :: V Type where
+  MyJust4    :: a -> MyMaybe4 a
+  MyNothing4 ::      MyMaybe4 a
diff --git a/testsuite/tests/typecheck/should_compile/T20873b.hs b/testsuite/tests/typecheck/should_compile/T20873b.hs
new file mode 100644
index 0000000000..5abe5942a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20873b.hs
@@ -0,0 +1,11 @@
+
+{-# LANGUAGE NoDataKinds #-}
+
+module T20873b where
+
+import T20873b_aux (P)
+
+type Q = P
+  -- P = 'MkA is a promoted data constructor,
+  -- but we should still allow users to use P with -XNoDataKinds,
+  -- to avoid implementation details of M1 leaking.
diff --git a/testsuite/tests/typecheck/should_compile/T20873b_aux.hs b/testsuite/tests/typecheck/should_compile/T20873b_aux.hs
new file mode 100644
index 0000000000..efd498471a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20873b_aux.hs
@@ -0,0 +1,7 @@
+
+{-# LANGUAGE DataKinds #-}
+
+module T20873b_aux where
+
+data A = MkA
+type P = 'MkA
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a3c89c0ab0..8b31c8b3cc 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -804,3 +804,6 @@ test('T20584b', normal, compile, [''])
 test('T20588b', [extra_files(['T20588b.hs', 'T20588b.hs-boot', 'T20588b_aux.hs'])], multimod_compile, ['T20588b_aux.hs', '-v0'])
 test('T20588d', [extra_files(['T20588d.hs', 'T20588d.hs-boot', 'T20588d_aux.hs'])], multimod_compile, ['T20588d_aux.hs', '-v0'])
 test('T20661', [extra_files(['T20661.hs', 'T20661.hs-boot', 'T20661_aux.hs'])], multimod_compile, ['T20661_aux.hs', '-v0'])
+
+test('T20873', normal, compile, [''])
+test('T20873b', [extra_files(['T20873b_aux.hs'])], multimod_compile, ['T20873b', '-v0'])
diff --git a/testsuite/tests/typecheck/should_fail/T20873c.hs b/testsuite/tests/typecheck/should_fail/T20873c.hs
new file mode 100644
index 0000000000..776c061f13
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20873c.hs
@@ -0,0 +1,11 @@
+
+{-# LANGUAGE GADTSyntax, NoKindSignatures, NoDataKinds #-}
+
+module T20873c where
+
+import Data.Kind ( Type )
+
+type U a = Type
+
+data Foo :: U Int where
+  MkFoo :: Foo
diff --git a/testsuite/tests/typecheck/should_fail/T20873c.stderr b/testsuite/tests/typecheck/should_fail/T20873c.stderr
new file mode 100644
index 0000000000..972d01c583
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20873c.stderr
@@ -0,0 +1,5 @@
+
+T20873c.hs:10:1: error:
+    • Illegal kind signature ‘Foo’
+        (Use KindSignatures to allow kind signatures)
+    • In the data declaration for ‘Foo’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 908edcfe27..ff092df478 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -628,3 +628,4 @@ test('T20542', normal, compile_fail, [''])
 test('T20588', [extra_files(['T20588.hs', 'T20588.hs-boot', 'T20588_aux.hs'])], multimod_compile_fail, ['T20588_aux.hs', '-v0'])
 test('T20588c', [extra_files(['T20588c.hs', 'T20588c.hs-boot', 'T20588c_aux.hs'])], multimod_compile_fail, ['T20588c_aux.hs', '-v0'])
 test('T20189', normal, compile_fail, [''])
+test('T20873c', normal, compile_fail, [''])