58e38f267e0279149b5551913c8650a720838689
[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,
7
8 -- ** Predicates on Kinds
9 isLiftedTypeKind, isUnliftedTypeKind,
10 isConstraintKind,
11 isTYPEApp,
12 returnsTyCon, returnsConstraintKind,
13 isConstraintKindCon,
14
15 classifiesTypeWithValues,
16 isStarKind, isStarKindSynonymTyCon,
17 tcIsStarKind,
18 isKindLevPoly
19 ) where
20
21 #include "HsVersions.h"
22
23 import GhcPrelude
24
25 import {-# SOURCE #-} Type ( coreView
26 , splitTyConApp_maybe )
27 import {-# SOURCE #-} DataCon ( DataCon )
28
29 import TyCoRep
30 import TyCon
31 import PrelNames
32
33 import Outputable
34 import Util
35
36 {-
37 ************************************************************************
38 * *
39 Functions over Kinds
40 * *
41 ************************************************************************
42
43 Note [Kind Constraint and kind *]
44 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
45 The kind Constraint is the kind of classes and other type constraints.
46 The special thing about types of kind Constraint is that
47 * They are displayed with double arrow:
48 f :: Ord a => a -> a
49 * They are implicitly instantiated at call sites; so the type inference
50 engine inserts an extra argument of type (Ord a) at every call site
51 to f.
52
53 However, once type inference is over, there is *no* distinction between
54 Constraint and *. Indeed we can have coercions between the two. Consider
55 class C a where
56 op :: a -> a
57 For this single-method class we may generate a newtype, which in turn
58 generates an axiom witnessing
59 C a ~ (a -> a)
60 so on the left we have Constraint, and on the right we have *.
61 See Trac #7451.
62
63 Bottom line: although '*' and 'Constraint' are distinct TyCons, with
64 distinct uniques, they are treated as equal at all times except
65 during type inference.
66 -}
67
68 isConstraintKind :: Kind -> Bool
69 isConstraintKindCon :: TyCon -> Bool
70
71 isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
72
73 isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
74 isConstraintKind _ = False
75
76 isTYPEApp :: Kind -> Maybe DataCon
77 isTYPEApp (TyConApp tc args)
78 | tc `hasKey` tYPETyConKey
79 , [arg] <- args
80 , Just (tc, []) <- splitTyConApp_maybe arg
81 , Just dc <- isPromotedDataCon_maybe tc
82 = Just dc
83 isTYPEApp _ = Nothing
84
85 -- | Does the given type "end" in the given tycon? For example @k -> [a] -> *@
86 -- ends in @*@ and @Maybe a -> [a]@ ends in @[]@.
87 returnsTyCon :: Unique -> Type -> Bool
88 returnsTyCon tc_u (ForAllTy _ ty) = returnsTyCon tc_u ty
89 returnsTyCon tc_u (FunTy _ ty) = returnsTyCon tc_u ty
90 returnsTyCon tc_u (TyConApp tc' _) = tc' `hasKey` tc_u
91 returnsTyCon _ _ = False
92
93 returnsConstraintKind :: Kind -> Bool
94 returnsConstraintKind = returnsTyCon constraintKindTyConKey
95
96 -- | Tests whether the given kind (which should look like @TYPE x@)
97 -- is something other than a constructor tree (that is, constructors at every node).
98 -- E.g. True of TYPE k, TYPE (F Int)
99 -- False of TYPE 'LiftedRep
100 isKindLevPoly :: Kind -> Bool
101 isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
102 -- the isStarKind check is necessary b/c of Constraint
103 go k
104 where
105 go ty | Just ty' <- coreView ty = go ty'
106 go TyVarTy{} = True
107 go AppTy{} = True -- it can't be a TyConApp
108 go (TyConApp tc tys) = isFamilyTyCon tc || any go tys
109 go ForAllTy{} = True
110 go (FunTy t1 t2) = go t1 || go t2
111 go LitTy{} = False
112 go CastTy{} = True
113 go CoercionTy{} = True
114
115 _is_type
116 | TyConApp typ [_] <- k
117 = typ `hasKey` tYPETyConKey
118 | otherwise
119 = False
120
121
122 -----------------------------------------
123 -- Subkinding
124 -- The tc variants are used during type-checking, where ConstraintKind
125 -- is distinct from all other kinds
126 -- After type-checking (in core), Constraint and liftedTypeKind are
127 -- indistinguishable
128
129 -- | Does this classify a type allowed to have values? Responds True to things
130 -- like *, #, TYPE Lifted, TYPE v, Constraint.
131 classifiesTypeWithValues :: Kind -> Bool
132 -- ^ True of any sub-kind of OpenTypeKind
133 classifiesTypeWithValues = isTYPE (const True)
134
135 -- | Is this kind equivalent to @*@?
136 --
137 -- This considers 'Constraint' to be distinct from @*@. For a version that
138 -- treats them as the same type, see 'isStarKind'.
139 tcIsStarKind :: Kind -> Bool
140 tcIsStarKind = tcIsTYPE is_lifted
141 where
142 is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey
143 is_lifted _ = False
144
145 -- | Is this kind equivalent to @*@?
146 --
147 -- This considers 'Constraint' to be the same as @*@. For a version that
148 -- treats them as different types, see 'tcIsStarKind'.
149 isStarKind :: Kind -> Bool
150 isStarKind = isLiftedTypeKind
151 -- See Note [Kind Constraint and kind *]
152
153 -- | Is the tycon @Constraint@?
154 isStarKindSynonymTyCon :: TyCon -> Bool
155 isStarKindSynonymTyCon tc = tc `hasKey` constraintKindTyConKey