0594f7f53af2a254e1e8c9e137552ca849d574ae
[ghc.git] / compiler / types / Kind.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module Kind (
7         -- * Main data type
8         Kind, typeKind,
9
10         -- Kinds
11         liftedTypeKind, unliftedTypeKind, openTypeKind,
12         argTypeKind, ubxTupleKind,
13         mkArrowKind, mkArrowKinds,
14
15         -- Kind constructors...
16         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
17         argTypeKindTyCon, ubxTupleKindTyCon,
18
19         -- Super Kinds
20         tySuperKind, tySuperKindTyCon, 
21         
22         pprKind, pprParendKind,
23
24         -- ** Deconstructing Kinds
25         kindFunResult, kindAppResult, synTyConResKind,
26         splitKindFunTys, splitKindFunTysN, splitKindFunTy_maybe,
27
28         -- ** Predicates on Kinds
29         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
30         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
31         isSuperKind, isCoercionKind, 
32         isLiftedTypeKindCon,
33
34         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind,
35         isSubKindCon,
36
37        ) where
38
39 #include "HsVersions.h"
40
41 import TypeRep
42 import TysPrim
43 import TyCon
44 import Var
45 import PrelNames
46 import Outputable
47 \end{code}
48
49 %************************************************************************
50 %*                                                                      *
51         Predicates over Kinds
52 %*                                                                      *
53 %************************************************************************
54
55 \begin{code}
56 isTySuperKind :: SuperKind -> Bool
57 isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
58 isTySuperKind _                = False
59
60 -------------------
61 -- Lastly we need a few functions on Kinds
62
63 isLiftedTypeKindCon :: TyCon -> Bool
64 isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey
65 \end{code}
66
67 %************************************************************************
68 %*                                                                      *
69         The kind of a type
70 %*                                                                      *
71 %************************************************************************
72
73 \begin{code}
74 typeKind :: Type -> Kind
75 typeKind _ty@(TyConApp tc tys) 
76   = ASSERT2( not (tc `hasKey` eqPredPrimTyConKey) || length tys == 2, ppr _ty )
77              -- Assertion checks for unsaturated application of (~)
78              -- See Note [The (~) TyCon] in TysPrim
79     kindAppResult (tyConKind tc) tys
80
81 typeKind (PredTy pred)        = predKind pred
82 typeKind (AppTy fun _)        = kindFunResult (typeKind fun)
83 typeKind (ForAllTy _ ty)      = typeKind ty
84 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
85 typeKind (FunTy _arg res)
86     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
87     --              not unliftedTypKind (#)
88     -- The only things that can be after a function arrow are
89     --   (a) types (of kind openTypeKind or its sub-kinds)
90     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
91     | isTySuperKind k         = k
92     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
93     where
94       k = typeKind res
95
96 ------------------
97 predKind :: PredType -> Kind
98 predKind (EqPred {}) = unliftedTypeKind -- Coercions are unlifted
99 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
100 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
101 \end{code}
102
103 %************************************************************************
104 %*                                                                      *
105         Functions over Kinds            
106 %*                                                                      *
107 %************************************************************************
108
109 \begin{code}
110 -- | Essentially 'funResultTy' on kinds
111 kindFunResult :: Kind -> Kind
112 kindFunResult (FunTy _ res) = res
113 kindFunResult k = pprPanic "kindFunResult" (ppr k)
114
115 kindAppResult :: Kind -> [arg] -> Kind
116 kindAppResult k []     = k
117 kindAppResult k (_:as) = kindAppResult (kindFunResult k) as
118
119 -- | Essentially 'splitFunTys' on kinds
120 splitKindFunTys :: Kind -> ([Kind],Kind)
121 splitKindFunTys (FunTy a r) = case splitKindFunTys r of
122                               (as, k) -> (a:as, k)
123 splitKindFunTys k = ([], k)
124
125 splitKindFunTy_maybe :: Kind -> Maybe (Kind,Kind)
126 splitKindFunTy_maybe (FunTy a r) = Just (a,r)
127 splitKindFunTy_maybe _           = Nothing
128
129 -- | Essentially 'splitFunTysN' on kinds
130 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
131 splitKindFunTysN 0 k           = ([], k)
132 splitKindFunTysN n (FunTy a r) = case splitKindFunTysN (n-1) r of
133                                    (as, k) -> (a:as, k)
134 splitKindFunTysN n k = pprPanic "splitKindFunTysN" (ppr n <+> ppr k)
135
136 -- | Find the result 'Kind' of a type synonym, 
137 -- after applying it to its 'arity' number of type variables
138 -- Actually this function works fine on data types too, 
139 -- but they'd always return '*', so we never need to ask
140 synTyConResKind :: TyCon -> Kind
141 synTyConResKind tycon = kindAppResult (tyConKind tycon) (tyConTyVars tycon)
142
143 -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
144 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
145 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
146         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
147
148 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
149
150 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
151 isOpenTypeKind _               = False
152
153 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
154
155 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
156 isUbxTupleKind _               = False
157
158 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
159
160 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
161 isArgTypeKind _               = False
162
163 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
164
165 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
166 isUnliftedTypeKind _               = False
167
168 isSubOpenTypeKind :: Kind -> Bool
169 -- ^ True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
170 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
171                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
172                                      False
173 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
174 isSubOpenTypeKind other            = ASSERT( isKind other ) False
175          -- This is a conservative answer
176          -- It matters in the call to isSubKind in
177          -- checkExpectedKind.
178
179 isSubArgTypeKindCon kc
180   | isUnliftedTypeKindCon kc = True
181   | isLiftedTypeKindCon kc   = True
182   | isArgTypeKindCon kc      = True
183   | otherwise                = False
184
185 isSubArgTypeKind :: Kind -> Bool
186 -- ^ True of any sub-kind of ArgTypeKind 
187 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
188 isSubArgTypeKind _                = False
189
190 -- | Is this a super-kind (i.e. a type-of-kinds)?
191 isSuperKind :: Type -> Bool
192 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
193 isSuperKind _                   = False
194
195 -- | Is this a kind (i.e. a type-of-types)?
196 isKind :: Kind -> Bool
197 isKind k = isSuperKind (typeKind k)
198
199 isSubKind :: Kind -> Kind -> Bool
200 -- ^ @k1 \`isSubKind\` k2@ checks that @k1@ <: @k2@
201 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
202 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
203 isSubKind _             _                     = False
204
205 isSubKindCon :: TyCon -> TyCon -> Bool
206 -- ^ @kc1 \`isSubKindCon\` kc2@ checks that @kc1@ <: @kc2@
207 isSubKindCon kc1 kc2
208   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
209   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
210   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
211   | isOpenTypeKindCon kc2                                  = True 
212                            -- we already know kc1 is not a fun, its a TyCon
213   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
214   | otherwise                                              = False
215
216 defaultKind :: Kind -> Kind
217 -- ^ Used when generalising: default kind ? and ?? to *. See "Type#kind_subtyping" for more
218 -- information on what that means
219
220 -- When we generalise, we make generic type variables whose kind is
221 -- simple (* or *->* etc).  So generic type variables (other than
222 -- built-in constants like 'error') always have simple kinds.  This is important;
223 -- consider
224 --      f x = True
225 -- We want f to get type
226 --      f :: forall (a::*). a -> Bool
227 -- Not 
228 --      f :: forall (a::??). a -> Bool
229 -- because that would allow a call like (f 3#) as well as (f True),
230 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
231 defaultKind k 
232   | isSubOpenTypeKind k = liftedTypeKind
233   | isSubArgTypeKind k  = liftedTypeKind
234   | otherwise        = k
235 \end{code}