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
114
115
116
117
118
119
120
121
122
123
124
|
-- (c) The University of Glasgow 2006-2012
{-# LANGUAGE CPP #-}
module Kind (
-- * Main data type
Kind, typeKind,
-- ** Predicates on Kinds
isLiftedTypeKind, isUnliftedTypeKind,
isConstraintKind,
returnsConstraintKind,
okArrowArgKind, okArrowResultKind,
classifiesTypeWithValues,
isKindLevPoly
) where
#include "HsVersions.h"
import {-# SOURCE #-} Type ( typeKind, coreView )
import TyCoRep
import TyCon
import PrelNames
import Outputable
import Util
{-
************************************************************************
* *
Functions over Kinds
* *
************************************************************************
-}
-- | Does the given type "end" in the given tycon? For example @k -> [a] -> *@
-- ends in @*@ and @Maybe a -> [a]@ ends in @[]@.
returnsConstraintKind :: Type -> Bool
returnsConstraintKind = go
where
go (ForAllTy _ ty) = go ty
go (FunTy _ ty) = go ty
go other = isConstraintKind other
-- | Tests whether the given kind (which should look like @TYPE v x@)
-- is something other than a constructor tree (that is, constructors at every node).
isKindLevPoly :: Kind -> Bool
isKindLevPoly k = ASSERT2( _is_type k, ppr k )
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 ty
| Just ty' <- coreView ty
= _is_type ty'
| TyConApp typ [_, _] <- ty
= typ `hasKey` tYPETyConKey
| otherwise
= False
--------------------------------------------
-- Kinding for arrow (->)
-- Says when a kind is acceptable on lhs or rhs of an arrow
-- arg -> res
--
-- See Note [Levity polymorphism]
okArrowArgKind, okArrowResultKind :: Kind -> Bool
okArrowArgKind = classifiesTypeWithValues
okArrowResultKind = classifiesTypeWithValues
-----------------------------------------
-- 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 *, #, TYPEvis Lifted, TYPE v r, Constraint.
classifiesTypeWithValues :: Kind -> Bool
classifiesTypeWithValues t | Just t' <- coreView t = classifiesTypeWithValues t'
classifiesTypeWithValues (TyConApp tc [_,_]) = tc `hasKey` tYPETyConKey
classifiesTypeWithValues _ = False
{- Note [Levity polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is this type legal?
(a :: TYPEvis rep) -> Int
where 'rep :: RuntimeRep'
You might think not, because no lambda can have a
runtime-rep-polymorphic binder. So no lambda has the
above type. BUT here's a way it can be useful (taken from
Trac #12708):
data T rep (a :: TYPEvis rep)
= MkT (a -> Int)
x1 :: T LiftedRep Int
x1 = MkT LiftedRep Int (\x::Int -> 3)
x2 :: T IntRep Int#
x2 = MkT IntRep Int# (\x:Int# -> 3)
Note that the lambdas are just fine!
Hence, okArrowArgKind and okArrowResultKind both just
check that the type is of the form (TYPEvis r) for some
representation type r.
-}
|
