-- (c) The University of Glasgow 2006-2012 {-# LANGUAGE CPP #-} module Kind ( -- * Main data type SuperKind, Kind, typeKind, -- Kinds anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind, mkArrowKind, mkArrowKinds, -- Kind constructors... anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon, constraintKindTyCon, -- Super Kinds superKind, superKindTyCon, pprKind, pprParendKind, -- ** Deconstructing Kinds kindAppResult, synTyConResKind, splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe, -- ** Predicates on Kinds isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind, isKind, isKindVar, isSuperKind, isSuperKindTyCon, isLiftedTypeKindCon, isConstraintKindCon, isAnyKind, isAnyKindCon, okArrowArgKind, okArrowResultKind, isSubOpenTypeKind, isSubOpenTypeKindKey, isSubKind, isSubKindCon, tcIsSubKind, tcIsSubKindCon, defaultKind, defaultKind_maybe, -- ** Functions on variables kiVarsOfKind, kiVarsOfKinds ) where #include "HsVersions.h" import {-# SOURCE #-} Type ( typeKind, substKiWith, eqKind ) import TypeRep import TysPrim import TyCon import VarSet import PrelNames import Outputable import Maybes( orElse ) import Util import FastString {- ************************************************************************ * * Functions over Kinds * * ************************************************************************ Note [Kind Constraint and kind *] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The kind Constraint is the kind of classes and other type constraints. The special thing about types of kind Constraint is that * They are displayed with double arrow: f :: Ord a => a -> a * They are implicitly instantiated at call sites; so the type inference engine inserts an extra argument of type (Ord a) at every call site to f. However, once type inference is over, there is *no* distinction between Constraint and *. Indeed we can have coercions between the two. Consider class C a where op :: a -> a For this single-method class we may generate a newtype, which in turn generates an axiom witnessing Ord a ~ (a -> a) so on the left we have Constraint, and on the right we have *. See Trac #7451. Bottom line: although '*' and 'Constraint' are distinct TyCons, with distinct uniques, they are treated as equal at all times except during type inference. Hence cmpTc treats them as equal. -} -- | Essentially 'funResultTy' on kinds handling pi-types too kindFunResult :: SDoc -> Kind -> KindOrType -> Kind kindFunResult _ (FunTy _ res) _ = res kindFunResult _ (ForAllTy kv res) arg = substKiWith [kv] [arg] res #ifdef DEBUG kindFunResult doc k _ = pprPanic "kindFunResult" (ppr k $$ doc) #else -- Without DEBUG, doc becomes an unsed arg, and will be optimised away kindFunResult _ _ _ = panic "kindFunResult" #endif kindAppResult :: SDoc -> Kind -> [Type] -> Kind kindAppResult _ k [] = k kindAppResult doc k (a:as) = kindAppResult doc (kindFunResult doc k a) as -- | Essentially 'splitFunTys' on kinds splitKindFunTys :: Kind -> ([Kind],Kind) splitKindFunTys (FunTy a r) = case splitKindFunTys r of (as, k) -> (a:as, k) splitKindFunTys k = ([], k) splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind) splitKindFunTy_maybe (FunTy a r) = Just (a,r) splitKindFunTy_maybe _ = Nothing -- | Essentially 'splitFunTysN' on kinds splitKindFunTysN :: Int -> Kind -> ([Kind],Kind) splitKindFunTysN 0 k = ([], k) splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of (as, k) -> (a:as, k) splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k) -- | Find the result 'Kind' of a type synonym, -- after applying it to its 'arity' number of type variables -- Actually this function works fine on data types too, -- but they'd always return '*', so we never need to ask synTyConResKind :: TyCon -> Kind synTyConResKind tycon = kindAppResult (ptext (sLit "synTyConResKind") <+> ppr tycon) (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon)) -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's isOpenTypeKind, isUnliftedTypeKind, isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool isOpenTypeKindCon, isUnliftedTypeKindCon, isSubOpenTypeKindCon, isConstraintKindCon, isLiftedTypeKindCon, isAnyKindCon, isSuperKindTyCon :: TyCon -> Bool isLiftedTypeKindCon tc = tyConUnique tc == liftedTypeKindTyConKey isAnyKindCon tc = tyConUnique tc == anyKindTyConKey isOpenTypeKindCon tc = tyConUnique tc == openTypeKindTyConKey isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey isSuperKindTyCon tc = tyConUnique tc == superKindTyConKey isAnyKind (TyConApp tc _) = isAnyKindCon tc isAnyKind _ = False isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc isOpenTypeKind _ = False isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc isUnliftedTypeKind _ = False isConstraintKind (TyConApp tc _) = isConstraintKindCon tc isConstraintKind _ = False isConstraintOrLiftedKind (TyConApp tc _) = isConstraintKindCon tc || isLiftedTypeKindCon tc isConstraintOrLiftedKind _ = False returnsConstraintKind :: Kind -> Bool returnsConstraintKind (ForAllTy _ k) = returnsConstraintKind k returnsConstraintKind (FunTy _ k) = returnsConstraintKind k returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc returnsConstraintKind _ = False -------------------------------------------- -- Kinding for arrow (->) -- Says when a kind is acceptable on lhs or rhs of an arrow -- arg -> res okArrowArgKindCon, okArrowResultKindCon :: TyCon -> Bool okArrowArgKindCon = isSubOpenTypeKindCon okArrowResultKindCon = isSubOpenTypeKindCon okArrowArgKind, okArrowResultKind :: Kind -> Bool okArrowArgKind (TyConApp kc []) = okArrowArgKindCon kc okArrowArgKind _ = False okArrowResultKind (TyConApp kc []) = okArrowResultKindCon kc okArrowResultKind _ = False ----------------------------------------- -- Subkinding -- The tc variants are used during type-checking, where we don't want the -- Constraint kind to be a subkind of anything -- After type-checking (in core), Constraint is a subkind of openTypeKind isSubOpenTypeKind :: Kind -> Bool -- ^ True of any sub-kind of OpenTypeKind isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc isSubOpenTypeKind _ = False isSubOpenTypeKindCon kc = isSubOpenTypeKindKey (tyConUnique kc) isSubOpenTypeKindKey :: Unique -> Bool isSubOpenTypeKindKey uniq = uniq == openTypeKindTyConKey || uniq == unliftedTypeKindTyConKey || uniq == liftedTypeKindTyConKey || uniq == constraintKindTyConKey -- Needed for error (Num a) "blah" -- and so that (Ord a -> Eq a) is well-kinded -- and so that (# Eq a, Ord b #) is well-kinded -- See Note [Kind Constraint and kind *] -- | Is this a kind (i.e. a type-of-types)? isKind :: Kind -> Bool isKind k = isSuperKind (typeKind k) isSubKind :: Kind -> Kind -> Bool -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@ -- Sub-kinding is extremely simple and does not look -- under arrrows or type constructors -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs isSubKind k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s) | isPromotedTyCon kc1 || isPromotedTyCon kc2 -- handles promoted kinds (List *, Nat, etc.) = eqKind k1 k2 | otherwise -- handles usual kinds (*, #, (#), etc.) = ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 ) kc1 `isSubKindCon` kc2 isSubKind k1 k2 = eqKind k1 k2 isSubKindCon :: TyCon -> TyCon -> Bool -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@ -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs isSubKindCon kc1 kc2 | kc1 == kc2 = True | isOpenTypeKindCon kc2 = isSubOpenTypeKindCon kc1 | isConstraintKindCon kc1 = isLiftedTypeKindCon kc2 | isLiftedTypeKindCon kc1 = isConstraintKindCon kc2 -- See Note [Kind Constraint and kind *] | otherwise = False ------------------------- -- Hack alert: we need a tiny variant for the typechecker -- Reason: f :: Int -> (a~b) -- g :: forall (c::Constraint). Int -> c -- h :: Int => Int -- We want to reject these, even though Constraint is -- a sub-kind of OpenTypeKind. It must be a sub-kind of OpenTypeKind -- *after* the typechecker -- a) So that (Ord a -> Eq a) is a legal type -- b) So that the simplifer can generate (error (Eq a) "urk") -- Moreover, after the type checker, Constraint and * -- are identical; see Note [Kind Constraint and kind *] -- -- Easiest way to reject is simply to make Constraint a compliete -- below OpenTypeKind when type checking tcIsSubKind :: Kind -> Kind -> Bool tcIsSubKind k1 k2 | isConstraintKind k1 = isConstraintKind k2 | isConstraintKind k2 = isConstraintKind k1 | otherwise = isSubKind k1 k2 tcIsSubKindCon :: TyCon -> TyCon -> Bool tcIsSubKindCon kc1 kc2 | isConstraintKindCon kc1 = isConstraintKindCon kc2 | isConstraintKindCon kc2 = isConstraintKindCon kc1 | otherwise = isSubKindCon kc1 kc2 ------------------------- defaultKind :: Kind -> Kind defaultKind_maybe :: Kind -> Maybe Kind -- ^ Used when generalising: default OpenKind and ArgKind to *. -- See "Type#kind_subtyping" for more information on what that means -- When we generalise, we make generic type variables whose kind is -- simple (* or *->* etc). So generic type variables (other than -- built-in constants like 'error') always have simple kinds. This is important; -- consider -- f x = True -- We want f to get type -- f :: forall (a::*). a -> Bool -- Not -- f :: forall (a::ArgKind). a -> Bool -- because that would allow a call like (f 3#) as well as (f True), -- and the calling conventions differ. -- This defaulting is done in TcMType.zonkTcTyVarBndr. -- -- The test is really whether the kind is strictly above '*' defaultKind_maybe (TyConApp kc _args) | isOpenTypeKindCon kc = ASSERT( null _args ) Just liftedTypeKind defaultKind_maybe _ = Nothing defaultKind k = defaultKind_maybe k `orElse` k -- Returns the free kind variables in a kind kiVarsOfKind :: Kind -> VarSet kiVarsOfKind = tyVarsOfType kiVarsOfKinds :: [Kind] -> VarSet kiVarsOfKinds = tyVarsOfTypes