Document the "kind invariant", and check it

See Note [The kind invariant] in TypeRep
Checked in CoreLint
All this arises from Trac #5426

compiler/coreSyn/CoreLint.lhs

@@ -700,29 +700,6 @@ lintTyBndrKind tv =
   else lintKind ki  -- type forall
 
 -------------------
-{-
-lint_prim_eq_co :: TyCon -> OutCoercion -> [OutCoercion] -> LintM (OutType,OutType)
-lint_prim_eq_co tc co arg_cos = case arg_cos of 
-  [co1,co2] -> do { (t1,s1) <- lintCoercion co1
-                  ; (t2,s2) <- lintCoercion co2
-                  ; checkL (typeKind t1 `eqKind` typeKind t2) $ 
-                    ptext (sLit "Mismatched arg kinds in coercion application:") <+> ppr co
-                  ; return (mkTyConApp tc [t1,t2], mkTyConApp tc [s1,s2]) }
-  _ -> failWithL (ptext (sLit "Unsaturated or oversaturated ~# coercion") <+> ppr co)
-
-lint_eq_co :: TyCon -> OutCoercion -> [OutCoercion] -> LintM (OutType,OutType) 
-lint_eq_co tc co arg_cos = case arg_cos of 
-  [co1,co2] -> do { (t1,s1) <- lintCoercion co1
-                  ; (t2,s2) <- lintCoercion co2
-                  ; checkL (typeKind t1 `eqKind` typeKind t2) $
-                    ptext (sLit "Mismatched arg kinds in coercion application:") <+> ppr co
-                  ; return (mkTyConApp tc [t1,t2], mkTyConApp tc [s1,s2]) }
-  [co1] -> do { (t1,s1) <- lintCoercion co1
-              ; return (mkTyConApp tc [t1], mkTyConApp tc [s1]) }
-  [] -> return (mkTyConApp tc [], mkTyConApp tc [])
-  _ -> failWithL (ptext (sLit "Oversaturated ~ coercion") <+> ppr co) 
--}
-
 lintKindCoercion :: OutCoercion -> LintM OutKind
 -- Kind coercions are only reflexivity because they mean kind
 -- instantiation.  See Note [Kind coercions] in Coercion
@@ -742,21 +719,6 @@ lintCoercion (Refl ty)
        ; return (ty, ty) }
 
 lintCoercion co@(TyConAppCo tc cos)
-{- DV: This grievous hack (from ghc-constraint-solver) should not be needed any more:
-  | tc `hasKey` eqPrimTyConKey      -- Just as in lintType, treat applications of (~) and (~#)
-  = lint_prim_eq_co tc co cos       -- specially to allow for polymorphism. This hack will 
-                                    -- hopefully go away when we merge in kind polymorphism.
-  | tc `hasKey` eqTyConKey
-  = lint_eq_co tc co cos
-
-  | otherwise
-  = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
-       ; let kind_to_check = if (tc `hasKey` funTyConKey) && (length cos == 2)
-                             then mkArrowKinds [argTypeKind,openTypeKind] liftedTypeKind
-                             else tyConKind tc -- TODO: Fix this when kind polymorphism is in! 
-       ; check_co_app co kind_to_check ss
-       ; return (mkTyConApp tc ss, mkTyConApp tc ts) }
--}
   = do   -- We use the kind of the type constructor to know how many
          -- kind coercions we have (one kind coercion for one kind
          -- instantiation).
@@ -876,7 +838,10 @@ lintType ty@(FunTy t1 t2)
   = lint_ty_app ty (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind) [t1,t2]
 
 lintType ty@(TyConApp tc tys)
-  | tyConHasKind tc
+  | tyConHasKind tc   -- Guards for SuperKindOon
+  , not (isUnLiftedTyCon tc) || tys `lengthIs` tyConArity tc
+       -- Check that primitive types are saturated
+       -- See Note [The kind invariant] in TypeRep
   = lint_ty_app ty (tyConKind tc) tys
   | otherwise
   = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))

compiler/typecheck/TcMType.lhs

@@ -1116,6 +1116,10 @@ check_arg_type rank ty
 
 	; check_type rank' UT_NotOk ty
 	; checkTc (not (isUnLiftedType ty)) (unliftedArgErr 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 TypeRep
 
 ----------------------------------------
 forAllTyErr :: Rank -> Type -> SDoc

compiler/types/Type.lhs

@@ -654,20 +654,22 @@ carefullySplitNewType_maybe rec_nts tc tys
 -- of inspecting the type directly.
 
 -- | Discovers the primitive representation of a more abstract 'Type'
+-- Only applied to types of values
 typePrimRep :: Type -> PrimRep
 typePrimRep ty = case repType ty of
 		   TyConApp tc _ -> tyConPrimRep tc
 		   FunTy _ _	 -> PtrRep
-		   AppTy _ _	 -> PtrRep	-- See note below
+		   AppTy _ _	 -> PtrRep	-- See Note [AppTy rep] 
 		   TyVarTy _	 -> PtrRep
 		   _             -> pprPanic "typePrimRep" (ppr ty)
-	-- 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 *->*, not *->*#, because
-	-- (we claim) there is no way to constrain f's kind any other
-	-- way.
 \end{code}
 
+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 TypeRep.
 
 ---------------------------------------------------------------------
 				ForAllTy

compiler/types/TypeRep.lhs

@@ -64,48 +64,6 @@ import Pair
 import qualified Data.Data        as Data hiding ( TyCon )
 \end{code}
 
-	----------------------
-	A note about newtypes
-	----------------------
-
-Consider
-	newtype N = MkN Int
-
-Then we want N to be represented as an Int, and that's what we arrange.
-The front end of the compiler [TcType.lhs] treats N as opaque, 
-the back end treats it as transparent [Type.lhs].
-
-There's a bit of a problem with recursive newtypes
-	newtype P = MkP P
-	newtype Q = MkQ (Q->Q)
-
-Here the 'implicit expansion' we get from treating P and Q as transparent
-would give rise to infinite types, which in turn makes eqType diverge.
-Similarly splitForAllTys and splitFunTys can get into a loop.  
-
-Solution: 
-
-* Newtypes are always represented using TyConApp.
-
-* For non-recursive newtypes, P, treat P just like a type synonym after 
-  type-checking is done; i.e. it's opaque during type checking (functions
-  from TcType) but transparent afterwards (functions from Type).  
-  "Treat P as a type synonym" means "all functions expand NewTcApps 
-  on the fly".
-
-  Applications of the data constructor P simply vanish:
-	P x = x
-  
-
-* For recursive newtypes Q, treat the Q and its representation as 
-  distinct right through the compiler.  Applications of the data consructor
-  use a coerce:
-	Q = \(x::Q->Q). coerce Q x
-  They are rare, so who cares if they are a tiny bit less efficient.
-
-The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
-to cut all loops.  The other members of the loop may be marked 'non-recursive'.
-
 
 %************************************************************************
 %*									*
@@ -119,7 +77,7 @@ to cut all loops.  The other members of the loop may be marked 'non-recursive'.
 data Type
   = TyVarTy Var	-- ^ Vanilla type or kind variable (*never* a coercion variable)
 
-  | AppTy
+  | AppTy         -- See Note [AppTy invariant]
 	Type
 	Type		-- ^ Type application to something other than a 'TyCon'. Parameters:
 	                --
@@ -128,7 +86,7 @@ data Type
 	                --
 	                --  2) Argument type
 
-  | TyConApp
+  | TyConApp      -- See Note [AppTy invariant]
 	TyCon
 	[KindOrType]	-- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
 	                -- Invariant: saturated appliations of 'FunTyCon' must
@@ -174,6 +132,27 @@ type Kind = Type
 type SuperKind = Type
 \end{code}
 
+Note [The kind invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+The kinds
+   #          UnliftedTypeKind
+   ArgKind    super-kind of *, #
+   (#)        UbxTupleKind
+   OpenKind   super-kind of ArgKind, ubxTupleKind
+
+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 [Arguments to type constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~