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

3 files changed, 17 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"
 
 {-