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