5fd17f9ee2478d5236cc76653b8111069c8bddb6
[ghc.git] / compiler / types / Kind.hs
1 -- (c) The University of Glasgow 2006-2012
2
3 {-# LANGUAGE CPP #-}
4 module Kind (
5 -- * Main data type
6 Kind, typeKind,
7
8 -- ** Predicates on Kinds
9 isLiftedTypeKind, isUnliftedTypeKind,
10 isConstraintKind,
11 isTYPEApp,
12 returnsTyCon, returnsConstraintKind,
13 isConstraintKindCon,
14 okArrowArgKind, okArrowResultKind,
15
16 classifiesTypeWithValues,
17 isStarKind, isStarKindSynonymTyCon,
18 isKindLevPoly
19 ) where
20
21 #include "HsVersions.h"
22
23 import {-# SOURCE #-} Type ( typeKind, coreViewOneStarKind
24 , splitTyConApp_maybe )
25 import {-# SOURCE #-} DataCon ( DataCon )
26
27 import TyCoRep
28 import TyCon
29 import PrelNames
30
31 import Outputable
32 import Util
33
34 {-
35 ************************************************************************
36 * *
37 Functions over Kinds
38 * *
39 ************************************************************************
40
41 Note [Kind Constraint and kind *]
42 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
43 The kind Constraint is the kind of classes and other type constraints.
44 The special thing about types of kind Constraint is that
45 * They are displayed with double arrow:
46 f :: Ord a => a -> a
47 * They are implicitly instantiated at call sites; so the type inference
48 engine inserts an extra argument of type (Ord a) at every call site
49 to f.
50
51 However, once type inference is over, there is *no* distinction between
52 Constraint and *. Indeed we can have coercions between the two. Consider
53 class C a where
54 op :: a -> a
55 For this single-method class we may generate a newtype, which in turn
56 generates an axiom witnessing
57 C a ~ (a -> a)
58 so on the left we have Constraint, and on the right we have *.
59 See Trac #7451.
60
61 Bottom line: although '*' and 'Constraint' are distinct TyCons, with
62 distinct uniques, they are treated as equal at all times except
63 during type inference.
64 -}
65
66 isConstraintKind :: Kind -> Bool
67 isConstraintKindCon :: TyCon -> Bool
68
69 isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
70
71 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
72 isConstraintKind _ = False
73
74 isTYPEApp :: Kind -> Maybe DataCon
75 isTYPEApp (TyConApp tc args)
76 | tc `hasKey` tYPETyConKey
77 , [arg] <- args
78 , Just (tc, []) <- splitTyConApp_maybe arg
79 , Just dc <- isPromotedDataCon_maybe tc
80 = Just dc
81 isTYPEApp _ = Nothing
82
83 -- | Does the given type "end" in the given tycon? For example @k -> [a] -> *@
84 -- ends in @*@ and @Maybe a -> [a]@ ends in @[]@.
85 returnsTyCon :: Unique -> Type -> Bool
86 returnsTyCon tc_u (ForAllTy _ ty) = returnsTyCon tc_u ty
87 returnsTyCon tc_u (FunTy _ ty) = returnsTyCon tc_u ty
88 returnsTyCon tc_u (TyConApp tc' _) = tc' `hasKey` tc_u
89 returnsTyCon _ _ = False
90
91 returnsConstraintKind :: Kind -> Bool
92 returnsConstraintKind = returnsTyCon constraintKindTyConKey
93
94 -- | Tests whether the given kind (which should look like @TYPE x@)
95 -- is something other than a constructor tree (that is, constructors at every node).
96 isKindLevPoly :: Kind -> Bool
97 isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
98 -- the isStarKind check is necessary b/c of Constraint
99 go k
100 where
101 go ty | Just ty' <- coreViewOneStarKind ty = go ty'
102 go TyVarTy{} = True
103 go AppTy{} = True -- it can't be a TyConApp
104 go (TyConApp tc tys) = isFamilyTyCon tc || any go tys
105 go ForAllTy{} = True
106 go (FunTy t1 t2) = go t1 || go t2
107 go LitTy{} = False
108 go CastTy{} = True
109 go CoercionTy{} = True
110
111 _is_type
112 | TyConApp typ [_] <- k
113 = typ `hasKey` tYPETyConKey
114 | otherwise
115 = False
116
117
118 --------------------------------------------
119 -- Kinding for arrow (->)
120 -- Says when a kind is acceptable on lhs or rhs of an arrow
121 -- arg -> res
122 --
123 -- See Note [Levity polymorphism]
124
125 okArrowArgKind, okArrowResultKind :: Kind -> Bool
126 okArrowArgKind = classifiesTypeWithValues
127 okArrowResultKind = classifiesTypeWithValues
128
129 -----------------------------------------
130 -- Subkinding
131 -- The tc variants are used during type-checking, where ConstraintKind
132 -- is distinct from all other kinds
133 -- After type-checking (in core), Constraint and liftedTypeKind are
134 -- indistinguishable
135
136 -- | Does this classify a type allowed to have values? Responds True to things
137 -- like *, #, TYPE Lifted, TYPE v, Constraint.
138 classifiesTypeWithValues :: Kind -> Bool
139 -- ^ True of any sub-kind of OpenTypeKind
140 classifiesTypeWithValues t | Just t' <- coreViewOneStarKind t = classifiesTypeWithValues t'
141 classifiesTypeWithValues (TyConApp tc [_]) = tc `hasKey` tYPETyConKey
142 classifiesTypeWithValues _ = False
143
144 -- | Is this kind equivalent to *?
145 isStarKind :: Kind -> Bool
146 isStarKind k | Just k' <- coreViewOneStarKind k = isStarKind k'
147 isStarKind (TyConApp tc [TyConApp ptr_rep []])
148 = tc `hasKey` tYPETyConKey
149 && ptr_rep `hasKey` liftedRepDataConKey
150 isStarKind _ = False
151 -- See Note [Kind Constraint and kind *]
152
153 -- | Is the tycon @Constraint@?
154 isStarKindSynonymTyCon :: TyCon -> Bool
155 isStarKindSynonymTyCon tc = tc `hasKey` constraintKindTyConKey
156
157
158 {- Note [Levity polymorphism]
159 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
160 Is this type legal?
161 (a :: TYPE rep) -> Int
162 where 'rep :: RuntimeRep'
163
164 You might think not, because no lambda can have a
165 runtime-rep-polymorphic binder. So no lambda has the
166 above type. BUT here's a way it can be useful (taken from
167 Trac #12708):
168
169 data T rep (a :: TYPE rep)
170 = MkT (a -> Int)
171
172 x1 :: T LiftedRep Int
173 x1 = MkT LiftedRep Int (\x::Int -> 3)
174
175 x2 :: T IntRep Int#
176 x2 = MkT IntRep Int# (\x:Int# -> 3)
177
178 Note that the lambdas are just fine!
179
180 Hence, okArrowArgKind and okArrowResultKind both just
181 check that the type is of the form (TYPE r) for some
182 representation type r.
183 -}