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