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