Clarify comments on kinds (Trac #12536)

- Remove misleading comments from TyCoRep.
- Remove 'check_lifted' calls (which were no-ops) from TcValidity.

compiler/typecheck/TcValidity.hs

@@ -452,24 +452,6 @@ representationPolymorphismForbidden = go
     go _              = False    -- Other cases are caught by zonker
 
 ----------------------------------------
--- | Fail with error message if the type is unlifted
-check_lifted :: Type -> TcM ()
-check_lifted _ = return ()
-
-{- ------ Legacy comment ---------
-The check_unlifted function seems entirely redundant.  The
-kind system should check for uses of unlifted types.  So I've
-removed the check.  See Trac #11120 comment:19.
-
-check_lifted ty
-  = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty)
-       ; checkTcM (not (isUnliftedType ty)) (unliftedArgErr env ty) }
-
-unliftedArgErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
-unliftedArgErr env ty = (env, sep [text "Illegal unlifted type:", ppr_tidy env ty])
------- End of legacy comment --------- -}
-
-
 check_type :: TidyEnv -> UserTypeCtxt -> Rank -> Type -> TcM ()
 -- The args say what the *type context* requires, independent
 -- of *flag* settings.  You test the flag settings at usage sites.
@@ -610,12 +592,7 @@ check_arg_type env ctxt rank ty
                         --    (Ord (forall a.a)) => a -> a
                         -- and so that if it Must be a monotype, we check that it is!
 
-        ; check_type env ctxt rank' ty
-        ; check_lifted ty }
-             -- NB the isUnliftedType test also checks for
-             --    T State#
-             -- where there is an illegal partial application of State# (which has
-             -- kind * -> #); see Note [The kind invariant] in TyCoRep
+        ; check_type env ctxt rank' ty }
 
 ----------------------------------------
 forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
@@ -1628,7 +1605,6 @@ checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
          --             type instance F Int              = Int#
          -- See Trac #9357
        ; checkValidMonoType rhs
-       ; check_lifted rhs
 
          -- We have a decidable instance unless otherwise permitted
        ; undecidable_ok <- xoptM LangExt.UndecidableInstances
@@ -1701,9 +1677,7 @@ checkValidTypePat pat_ty
 
           -- Ensure that no type family instances occur a type pattern
        ; checkTc (isTyFamFree pat_ty) $
-         tyFamInstIllegalErr pat_ty
-
-      ; check_lifted pat_ty }
+         tyFamInstIllegalErr pat_ty }
 
 isTyFamFree :: Type -> Bool
 -- ^ Check that a type does not contain any type family applications.

compiler/types/TyCoRep.hs

@@ -247,7 +247,7 @@ data Type
   -- See Note [Non-trivial definitional equality]
   = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
 
-  | AppTy         -- See Note [AppTy rep]
+  | AppTy
         Type
         Type            -- ^ Type application to something other than a 'TyCon'. Parameters:
                         --
@@ -256,7 +256,7 @@ data Type
                         --
                         --  2) Argument type
 
-  | TyConApp      -- See Note [AppTy rep]
+  | TyConApp
         TyCon
         [KindOrType]    -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
                         -- Invariant: saturated applications of 'FunTyCon' must
@@ -304,34 +304,7 @@ data TyLit
   | StrTyLit FastString
   deriving (Eq, Ord, Data.Data)
 
-{- Note [The kind invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The kinds
-   #          UnliftedTypeKind
-   OpenKind   super-kind of *, #
-
-can never appear under an arrow or type constructor in a kind; they
-can only be at the top level of a kind.  It follows that primitive TyCons,
-which have a naughty pseudo-kind
-   State# :: * -> #
-must always be saturated, so that we can never get a type whose kind
-has a UnliftedTypeKind or ArgTypeKind underneath an arrow.
-
-Nor can we abstract over a type variable with any of these kinds.
-
-    k :: = kk | # | ArgKind | (#) | OpenKind
-    kk :: = * | kk -> kk | T kk1 ... kkn
-
-So a type variable can only be abstracted kk.
-
-Note [AppTy rep]
-~~~~~~~~~~~~~~~~
-Types of the form 'f a' must be of kind *, not #, so we are guaranteed
-that they are represented by pointers.  The reason is that f must have
-kind (kk -> kk) and kk cannot be unlifted; see Note [The kind invariant]
-in TyCoRep.
-
-Note [Arguments to type constructors]
+{- Note [Arguments to type constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Because of kind polymorphism, in addition to type application we now
 have kind instantiation. We reuse the same notations to do so.