Kind.lhs 12.6 KB
Newer Older
1 2 3 4 5
%
% (c) The University of Glasgow 2006
%

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
6 7 8 9 10 11 12
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

13 14 15 16 17
module Kind (
        -- * Main data type
        Kind, typeKind,

	-- Kinds
dreixel's avatar
dreixel committed
18
	anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind,
batterseapower's avatar
batterseapower committed
19
        argTypeKind, ubxTupleKind, constraintKind,
20 21 22
        mkArrowKind, mkArrowKinds,

        -- Kind constructors...
dreixel's avatar
dreixel committed
23 24 25
        anyKindTyCon, liftedTypeKindTyCon, openTypeKindTyCon,
        unliftedTypeKindTyCon, argTypeKindTyCon, ubxTupleKindTyCon,
        constraintKindTyCon,
26 27 28 29 30 31 32 33 34 35 36 37

        -- Super Kinds
	tySuperKind, tySuperKindTyCon, 
        
	pprKind, pprParendKind,

        -- ** Deconstructing Kinds
        kindFunResult, kindAppResult, synTyConResKind,
        splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,

        -- ** Predicates on Kinds
        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
dreixel's avatar
dreixel committed
38 39
        isUbxTupleKind, isArgTypeKind, isConstraintKind,
        isConstraintOrLiftedKind, isKind,
dreixel's avatar
dreixel committed
40
        isSuperKind, noHashInKind,
batterseapower's avatar
batterseapower committed
41
        isLiftedTypeKindCon, isConstraintKindCon,
dreixel's avatar
dreixel committed
42
        isAnyKind, isAnyKindCon,
43

dreixel's avatar
dreixel committed
44 45
        isSubArgTypeKind, tcIsSubArgTypeKind, 
        isSubOpenTypeKind, tcIsSubOpenTypeKind,
46
        isSubKind, tcIsSubKind, defaultKind,
dreixel's avatar
dreixel committed
47 48 49 50 51 52 53 54
        isSubKindCon, tcIsSubKindCon, isSubOpenTypeKindCon,

        -- ** Functions on variables
        isKiVar, splitKiTyVars, partitionKiTyVars,
        kiVarsOfKind, kiVarsOfKinds,

        -- ** Promotion related functions
        promoteType, isPromotableType, isPromotableKind,
55 56 57 58 59

       ) where

#include "HsVersions.h"

dreixel's avatar
dreixel committed
60
import {-# SOURCE #-} Type      ( typeKind, substKiWith, eqKind )
batterseapower's avatar
batterseapower committed
61

62 63 64
import TypeRep
import TysPrim
import TyCon
dreixel's avatar
dreixel committed
65 66
import Var
import VarSet
67 68
import PrelNames
import Outputable
dreixel's avatar
dreixel committed
69 70

import Data.List ( partition )
71 72 73 74 75 76 77 78 79 80 81 82 83 84
\end{code}

%************************************************************************
%*									*
        Predicates over Kinds
%*									*
%************************************************************************

\begin{code}
-------------------
-- Lastly we need a few functions on Kinds

isLiftedTypeKindCon :: TyCon -> Bool
isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
dreixel's avatar
dreixel committed
85 86 87 88 89 90 91 92 93 94 95 96

-- This checks that its argument does not contain # or (#).
-- It is used in tcTyVarBndrs.
noHashInKind :: Kind -> Bool
noHashInKind (TyVarTy {}) = True
noHashInKind (FunTy k1 k2) = noHashInKind k1 && noHashInKind k2
noHashInKind (ForAllTy _ ki) = noHashInKind ki
noHashInKind (TyConApp kc kis)
  =  not (kc `hasKey` unliftedTypeKindTyConKey)
  && not (kc `hasKey` ubxTupleKindTyConKey)
  && all noHashInKind kis
noHashInKind _ = panic "noHashInKind"
97 98 99 100 101 102 103 104 105
\end{code}

%************************************************************************
%*									*
	Functions over Kinds		
%*									*
%************************************************************************

\begin{code}
dreixel's avatar
dreixel committed
106 107 108 109 110
-- | Essentially 'funResultTy' on kinds handling pi-types too
kindFunResult :: Kind -> KindOrType -> Kind
kindFunResult (FunTy _ res) _ = res
kindFunResult (ForAllTy kv res) arg = substKiWith [kv] [arg] res
kindFunResult k _ = pprPanic "kindFunResult" (ppr k)
111

dreixel's avatar
dreixel committed
112
kindAppResult :: Kind -> [Type] -> Kind
113
kindAppResult k []     = k
dreixel's avatar
dreixel committed
114
kindAppResult k (a:as) = kindAppResult (kindFunResult k a) as
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137

-- | 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
dreixel's avatar
dreixel committed
138
synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyVars tycon))
139 140

-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
dreixel's avatar
dreixel committed
141
isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind,
dreixel's avatar
dreixel committed
142
  isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
dreixel's avatar
dreixel committed
143

144
isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
dreixel's avatar
dreixel committed
145 146 147 148 149 150 151 152
  isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon,
  isSubOpenTypeKindCon, tcIsSubOpenTypeKindCon, isConstraintKindCon,
  isAnyKindCon :: TyCon -> Bool

isAnyKindCon tc     = tyConUnique tc == anyKindTyConKey

isAnyKind (TyConApp tc _) = isAnyKindCon tc
isAnyKind _               = False
153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173

isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey

isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
isOpenTypeKind _               = False

isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey

isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
isUbxTupleKind _               = False

isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey

isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
isArgTypeKind _               = False

isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey

isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
isUnliftedTypeKind _               = False

batterseapower's avatar
batterseapower committed
174 175 176 177 178
isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey

isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
isConstraintKind _               = False

dreixel's avatar
dreixel committed
179 180 181
isConstraintOrLiftedKind (TyConApp tc _)
  = isConstraintKindCon tc || isLiftedTypeKindCon tc
isConstraintOrLiftedKind _ = False
dreixel's avatar
dreixel committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206

-- 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 argTypeKind
isSubOpenTypeKind, tcIsSubOpenTypeKind :: Kind -> Bool
-- ^ True of any sub-kind of OpenTypeKind
isSubOpenTypeKind (TyConApp kc []) = isSubOpenTypeKindCon kc
isSubOpenTypeKind _                = False

-- ^ True of any sub-kind of OpenTypeKind
tcIsSubOpenTypeKind (TyConApp kc []) = tcIsSubOpenTypeKindCon kc
tcIsSubOpenTypeKind _                = False

isSubOpenTypeKindCon kc
  | isSubArgTypeKindCon kc   = True
  | isUbxTupleKindCon kc     = True
  | isOpenTypeKindCon kc     = True
  | otherwise                = False

tcIsSubOpenTypeKindCon kc
  | tcIsSubArgTypeKindCon kc = True
  | isUbxTupleKindCon kc     = True
  | isOpenTypeKindCon kc     = True
  | otherwise                = False
207 208 209 210 211

isSubArgTypeKindCon kc
  | isUnliftedTypeKindCon kc = True
  | isLiftedTypeKindCon kc   = True
  | isArgTypeKindCon kc      = True
batterseapower's avatar
batterseapower committed
212
  | isConstraintKindCon kc   = True
213 214
  | otherwise                = False

dreixel's avatar
dreixel committed
215 216 217 218 219
tcIsSubArgTypeKindCon kc
  | isConstraintKindCon kc   = False
  | otherwise                = isSubArgTypeKindCon kc

isSubArgTypeKind, tcIsSubArgTypeKind :: Kind -> Bool
220 221 222 223
-- ^ True of any sub-kind of ArgTypeKind 
isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
isSubArgTypeKind _                = False

dreixel's avatar
dreixel committed
224 225 226
tcIsSubArgTypeKind (TyConApp kc []) = tcIsSubArgTypeKindCon kc
tcIsSubArgTypeKind _                = False

227 228 229 230 231 232 233 234 235
-- | Is this a super-kind (i.e. a type-of-kinds)?
isSuperKind :: Type -> Bool
isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
isSuperKind _                   = False

-- | Is this a kind (i.e. a type-of-types)?
isKind :: Kind -> Bool
isKind k = isSuperKind (typeKind k)

236 237 238 239 240 241
isSubKind, tcIsSubKind :: Kind -> Kind -> Bool
isSubKind   = isSubKind' False
tcIsSubKind = isSubKind' True

-- The first argument denotes whether we are in the type-checking phase or not
isSubKind' :: Bool -> Kind -> Kind -> Bool
242
-- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
dreixel's avatar
dreixel committed
243

244 245
isSubKind' duringTc (FunTy a1 r1) (FunTy a2 r2)
  = (isSubKind' duringTc a2 a1) && (isSubKind' duringTc r1 r2)
dreixel's avatar
dreixel committed
246

247
isSubKind' duringTc k1@(TyConApp kc1 k1s) k2@(TyConApp kc2 k2s)
dreixel's avatar
dreixel committed
248 249 250 251 252 253 254 255 256 257 258
  | isPromotedTypeTyCon kc1 || isPromotedTypeTyCon kc2
    -- handles promoted kinds (List *, Nat, etc.)
    = eqKind k1 k2

  | isSuperKindTyCon kc1 || isSuperKindTyCon kc2
    -- handles BOX
    = ASSERT2( isSuperKindTyCon kc2 && null k1s && null k2s, ppr kc1 <+> ppr kc2 )
      True

  | otherwise = -- handles usual kinds (*, #, (#), etc.)
                ASSERT2( null k1s && null k2s, ppr k1 <+> ppr k2 )
259 260
                if duringTc then kc1 `tcIsSubKindCon` kc2
                else kc1 `isSubKindCon` kc2
dreixel's avatar
dreixel committed
261

262
isSubKind' _duringTc k1 k2 = eqKind k1 k2
263 264 265 266

isSubKindCon :: TyCon -> TyCon -> Bool
-- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
isSubKindCon kc1 kc2
dreixel's avatar
dreixel committed
267 268 269
  | kc1 == kc2                                             = True
  | isSubArgTypeKindCon  kc1  && isArgTypeKindCon  kc2     = True
  | isSubOpenTypeKindCon kc1  && isOpenTypeKindCon kc2     = True
270 271
  | otherwise                                              = False

dreixel's avatar
dreixel committed
272 273 274 275 276 277
tcIsSubKindCon :: TyCon -> TyCon -> Bool
tcIsSubKindCon kc1 kc2
  | kc1 == kc2                                         = True
  | isConstraintKindCon kc1 || isConstraintKindCon kc2 = False
  | otherwise                                          = isSubKindCon kc1 kc2

278
defaultKind :: Kind -> Kind
279
-- ^ Used when generalising: default OpenKind and ArgKind to *.
dreixel's avatar
dreixel committed
280
-- See "Type#kind_subtyping" for more information on what that means
281 282 283 284 285 286 287 288 289

-- 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 
290
--	f :: forall (a::ArgKind). a -> Bool
291
-- because that would allow a call like (f 3#) as well as (f True),
dreixel's avatar
dreixel committed
292 293 294
-- and the calling conventions differ.
-- This defaulting is done in TcMType.zonkTcTyVarBndr.
defaultKind k
dreixel's avatar
dreixel committed
295 296
  | tcIsSubOpenTypeKind k = liftedTypeKind
  | otherwise             = k
dreixel's avatar
dreixel committed
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366

splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
-- Precondition: kind variables should precede type variables
-- Postcondition: appending the two result lists gives the input!
splitKiTyVars = span (isSuperKind . tyVarKind)

partitionKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
partitionKiTyVars = partition (isSuperKind . tyVarKind)

-- Checks if this "type or kind" variable is a kind variable
isKiVar :: TyVar -> Bool
isKiVar v = isSuperKind (varType v)

-- Returns the free kind variables in a kind
kiVarsOfKind :: Kind -> VarSet
kiVarsOfKind = tyVarsOfType

kiVarsOfKinds :: [Kind] -> VarSet
kiVarsOfKinds = tyVarsOfTypes

-- Datatype promotion
isPromotableType :: Type -> Bool
isPromotableType = go emptyVarSet
  where
    go vars (TyConApp tc tys) = ASSERT( not (isPromotedDataTyCon tc) ) all (go vars) tys
    go vars (FunTy arg res) = all (go vars) [arg,res]
    go vars (TyVarTy tvar) = tvar `elemVarSet` vars
    go vars (ForAllTy tvar ty) = isPromotableTyVar tvar && go (vars `extendVarSet` tvar) ty
    go _ _ = panic "isPromotableType"  -- argument was not kind-shaped

isPromotableTyVar :: TyVar -> Bool
isPromotableTyVar = isLiftedTypeKind . varType

-- | Promotes a type to a kind. Assumes the argument is promotable.
promoteType :: Type -> Kind
promoteType (TyConApp tc tys) = mkTyConApp (mkPromotedTypeTyCon tc) 
                                           (map promoteType tys)
  -- T t1 .. tn  ~~>  'T k1 .. kn  where  ti ~~> ki
promoteType (FunTy arg res) = mkArrowKind (promoteType arg) (promoteType res)
  -- t1 -> t2  ~~>  k1 -> k2  where  ti ~~> ki
promoteType (TyVarTy tvar) = mkTyVarTy (promoteTyVar tvar)
  -- a :: *  ~~>  a :: BOX
promoteType (ForAllTy tvar ty) = ForAllTy (promoteTyVar tvar) (promoteType ty)
  -- forall (a :: *). t  ~~> forall (a :: BOX). k  where  t ~~> k
promoteType _ = panic "promoteType"  -- argument was not kind-shaped

promoteTyVar :: TyVar -> KindVar
promoteTyVar tvar = mkKindVar (tyVarName tvar) tySuperKind

-- If kind is [ *^n -> * ] returns [ Just n ], else returns [ Nothing ]
isPromotableKind :: Kind -> Maybe Int
isPromotableKind kind =
  let (args, res) = splitKindFunTys kind in
  if all isLiftedTypeKind (res:args)
  then Just $ length args
  else Nothing

{- Note [Promoting a Type to a Kind]
   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only promote the followings.
- Type variables: a
- Fully applied arrow types: tau -> sigma
- Fully applied type constructors of kind:
     n >= 0
  /-----------\
  * -> ... -> * -> *
- Polymorphic types over type variables of kind star:
  forall (a::*). tau
-}
\end{code}