0ce6bfe7e09fd9e75a6c6a99da13dad95f7c4e27
[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 tcIsLiftedTypeKind,
17 isKindLevPoly
18 ) where
19
20 #include "HsVersions.h"
21
22 import GhcPrelude
23
24 import {-# SOURCE #-} Type ( coreView
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 Type]
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 Type. 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 Type.
60 See Trac #7451.
61
62 Bottom line: although 'Type' 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 -- E.g. True of TYPE k, TYPE (F Int)
98 -- False of TYPE 'LiftedRep
99 isKindLevPoly :: Kind -> Bool
100 isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
101 -- the isLiftedTypeKind check is necessary b/c of Constraint
102 go k
103 where
104 go ty | Just ty' <- coreView ty = go ty'
105 go TyVarTy{} = True
106 go AppTy{} = True -- it can't be a TyConApp
107 go (TyConApp tc tys) = isFamilyTyCon tc || any go tys
108 go ForAllTy{} = True
109 go (FunTy t1 t2) = go t1 || go t2
110 go LitTy{} = False
111 go CastTy{} = True
112 go CoercionTy{} = True
113
114 _is_type
115 | TyConApp typ [_] <- k
116 = typ `hasKey` tYPETyConKey
117 | otherwise
118 = False
119
120
121 -----------------------------------------
122 -- Subkinding
123 -- The tc variants are used during type-checking, where ConstraintKind
124 -- is distinct from all other kinds
125 -- After type-checking (in core), Constraint and liftedTypeKind are
126 -- indistinguishable
127
128 -- | Does this classify a type allowed to have values? Responds True to things
129 -- like *, #, TYPE Lifted, TYPE v, Constraint.
130 classifiesTypeWithValues :: Kind -> Bool
131 -- ^ True of any sub-kind of OpenTypeKind
132 classifiesTypeWithValues = isTYPE (const True)
133
134 -- | Is this kind equivalent to @*@?
135 --
136 -- This considers 'Constraint' to be distinct from @*@. For a version that
137 -- treats them as the same type, see 'isLiftedTypeKind'.
138 tcIsLiftedTypeKind :: Kind -> Bool
139 tcIsLiftedTypeKind = tcIsTYPE is_lifted
140 where
141 is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey
142 is_lifted _ = False