Refactor the escaping kind check for data constructorswip/T20929

As #20929 pointed out, we were in-elegantly checking for escaping
kinds in `checkValidType`, even though that check was guaranteed
to succeed for type signatures -- it's part of kind-checking a type.

But for /data constructors/ we kind-check the pieces separately,
so we still need the check.

This MR is a pure refactor, moving the test from `checkValidType` to
`checkValidDataCon`.

No new tests; external behaviour doesn't change.

2 files changed, 64 insertions, 58 deletions

diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 3ada6b6dc3..e184bd178f 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4350,7 +4350,9 @@ checkValidDataCon dflags existential_ok tc con
     addErrCtxt (dataConCtxt [L (noAnnSrcSpan con_loc) con_name]) $
     do  { let tc_tvs      = tyConTyVars tc
               res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
-              orig_res_ty = dataConOrigResTy con
+              arg_tys     = dataConOrigArgTys con
+              orig_res_ty = dataConOrigResTy  con
+
         ; traceTc "checkValidDataCon" (vcat
               [ ppr con, ppr tc, ppr tc_tvs
               , ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl)
@@ -4387,15 +4389,20 @@ checkValidDataCon dflags existential_ok tc con
           -- Reason: it's really the argument of an equality constraint
         ; checkValidMonoType orig_res_ty
 
-          -- If we are dealing with a newtype, we allow representation
-          -- polymorphism regardless of whether or not UnliftedNewtypes
-          -- is enabled. A later check in checkNewDataCon handles this,
-          -- producing a better error message than checkTypeHasFixedRuntimeRep would.
+        -- Check for an escaping result kind
+        -- See Note [Check for escaping result kind]
+        ; checkEscapingKind con
+
+        -- For /data/ types check that each argument has a fixed runtime rep
+        -- If we are dealing with a /newtype/, we allow representation
+        -- polymorphism regardless of whether or not UnliftedNewtypes
+        -- is enabled. A later check in checkNewDataCon handles this,
+        -- producing a better error message than checkTypeHasFixedRuntimeRep would.
+        ; let check_rr = checkTypeHasFixedRuntimeRep FixedRuntimeRepDataConField
         ; unless (isNewTyCon tc) $
-            checkNoErrs $
-              mapM_ (checkTypeHasFixedRuntimeRep FixedRuntimeRepDataConField)
-                (map scaledThing $ dataConOrigArgTys con)
-            -- the checkNoErrs is to prevent a panic in isVanillaDataCon
+          checkNoErrs            $
+          mapM_ (check_rr . scaledThing) arg_tys
+            -- The checkNoErrs is to prevent a panic in isVanillaDataCon
             -- (called a a few lines down), which can fall over if there is a
             -- bang on a representation-polymorphic argument. This is #18534,
             -- typecheck/should_fail/T18534
@@ -4489,9 +4496,9 @@ checkValidDataCon dflags existential_ok tc con
     }
   where
     bang_opts = initBangOpts dflags
-    con_name = dataConName con
-    con_loc  = nameSrcSpan con_name
-    ctxt = ConArgCtxt con_name
+    con_name  = dataConName con
+    con_loc   = nameSrcSpan con_name
+    ctxt      = ConArgCtxt con_name
     is_strict = \case
       NoSrcStrict -> bang_opt_strict_data bang_opts
       bang        -> isSrcStrict bang
@@ -4554,6 +4561,47 @@ checkNewDataCon con
     ok_mult One = True
     ok_mult _   = False
 
+
+-- | Reject nullary data constructors where a type variables
+-- would escape through the result kind
+-- See Note [Check for escaping result kind]
+checkEscapingKind :: DataCon -> TcM ()
+checkEscapingKind data_con
+  | null eq_spec, null theta, null arg_tys
+  , let tau_kind = tcTypeKind res_ty
+  , Nothing <- occCheckExpand (univ_tvs ++ ex_tvs) tau_kind
+    -- Ensure that none of the tvs occur in the kind of the forall
+    -- /after/ expanding type synonyms.
+    -- See Note [Phantom type variables in kinds] in GHC.Core.Type
+  = failWithTc $ TcRnForAllEscapeError (dataConWrapperType data_con) tau_kind
+  | otherwise
+  = return ()
+  where
+    (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty)
+      = dataConFullSig data_con
+
+{- Note [Check for escaping result kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:
+  type T :: TYPE (BoxedRep l)
+  data T = MkT
+This is not OK: we get
+  MkT :: forall l. T @l :: TYPE (BoxedRep l)
+which is ill-kinded.
+
+For ordinary type signatures f :: blah, we make this check as part of kind-checking
+the type signature; see Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType.
+But for data constructors we check the type piecemeal, and there is no very
+convenient place to do it.  For example, note that it only applies for /nullary/
+constructors.  If we had
+  data T = MkT Int
+then the type of MkT would be MkT :: forall l. Int -> T @l, which is fine.
+
+So we make the check in checkValidDataCon.
+
+Historical note: we used to do the check in checkValidType (#20929 discusses).
+-}
+
 -------------------------------
 checkValidClass :: Class -> TcM ()
 checkValidClass cls
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 898a716980..9d6a05c7aa 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -345,6 +345,8 @@ This might not necessarily show up in kind checking.
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that a user-written type is valid for the given context
 -- Assumes argument is fully zonked
+-- Assumes arugment is well-kinded;
+--    that is, checkValidType doesn't need to do kind checking
 -- Not used for instance decls; checkValidInstance instead
 checkValidType ctxt ty
   = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
@@ -738,11 +740,11 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
         ; check_type (ve{ve_tidy_env = env'}) tau
                 -- Allow foralls to right of arrow
 
-        ; checkEscapingKind env' tvbs' theta tau }
+        }
   where
     (tvbs, phi)   = tcSplitForAllTyVarBinders ty
     (theta, tau)  = tcSplitPhiTy phi
-    (env', tvbs') = tidyTyCoVarBinders env tvbs
+    (env', _)     = tidyTyCoVarBinders env tvbs
 
 check_type (ve@ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
                           , ve_rank = rank })
@@ -908,50 +910,6 @@ check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
         ; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
 
 ----------------------------------------
-
--- | Reject type variables that would escape their escape through a kind.
--- See @Note [Type variables escaping through kinds]@.
-checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
-checkEscapingKind env tvbs theta tau =
-  case occCheckExpand (binderVars tvbs) phi_kind of
-    -- Ensure that none of the tvs occur in the kind of the forall
-    -- /after/ expanding type synonyms.
-    -- See Note [Phantom type variables in kinds] in GHC.Core.Type
-    Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind
-    Just _  -> pure ()
-  where
-    tau_kind              = tcTypeKind tau
-    phi_kind | null theta = tau_kind
-             | otherwise  = liftedTypeKind
-        -- If there are any constraints, the kind is *. (#11405)
-
-forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
-                -> (TidyEnv, TcRnMessage)
-forAllEscapeErr env tvbs theta tau tau_kind
-  -- NB: Don't tidy the sigma type since the tvbs were already tidied
-  -- previously, and re-tidying them will make the names of type
-  -- variables different from tau_kind.
-  = (env, TcRnForAllEscapeError (mkSigmaTy tvbs theta tau) (tidyType env tau_kind))
-
-{-
-Note [Type variables escaping through kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:
-
-  type family T (r :: RuntimeRep) :: TYPE r
-  foo :: forall r. T r
-
-Something smells funny about the type of `foo`. If you spell out the kind
-explicitly, it becomes clearer from where the smell originates:
-
-  foo :: ((forall r. T r) :: TYPE r)
-
-The type variable `r` appears in the result kind, which escapes the scope of
-its binding site! This is not desirable, so we establish a validity check
-(`checkEscapingKind`) to catch any type variables that might escape through
-kinds in this way.
--}
-
 checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
 checkConstraintsOK ve theta ty
   | null theta                         = return ()