diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2011-12-13 12:30:40 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2011-12-13 12:30:40 +0000 |
commit | 0f34f30839c9f382bdeab0335675ce8491361d67 (patch) | |
tree | 30ee044a06c78e035df2bfc76c4e9a3e4547ff9e /compiler | |
parent | 83030e70225fcf5bbeb6683194fd7b66c47fe3dc (diff) | |
download | haskell-0f34f30839c9f382bdeab0335675ce8491361d67.tar.gz |
Document the "kind invariant", and check it
See Note [The kind invariant] in TypeRep
Checked in CoreLint
All this arises from Trac #5426
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/coreSyn/CoreLint.lhs | 43 | ||||
-rw-r--r-- | compiler/typecheck/TcMType.lhs | 4 | ||||
-rw-r--r-- | compiler/types/Type.lhs | 14 | ||||
-rw-r--r-- | compiler/types/TypeRep.lhs | 67 |
4 files changed, 39 insertions, 89 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index f6627f3aa7..fa22e7efea 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/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)) diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 409dd722e7..2bbb2e11eb 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/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 diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index ebf542ab5a..a344fd151b 100644 --- a/compiler/types/Type.lhs +++ b/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 diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs index 0b8a1bf2cc..6d1050fde2 100644 --- a/compiler/types/TypeRep.lhs +++ b/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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |