2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
7 Kind(..), KindVar(..), SimpleKind,
8 openTypeKind, liftedTypeKind, unliftedTypeKind,
9 argTypeKind, ubxTupleKind,
11 isLiftedTypeKind, isUnliftedTypeKind,
12 isArgTypeKind, isOpenTypeKind,
13 mkArrowKind, mkArrowKinds,
15 isSubKind, defaultKind,
16 kindFunResult, splitKindFunTys, mkKindVar,
18 pprKind, pprParendKind
21 #include "HsVersions.h"
23 import Unique ( Unique )
30 There's a little subtyping at the kind level:
39 where * [LiftedTypeKind] means boxed type
40 # [UnliftedTypeKind] means unboxed type
41 (#) [UbxTupleKind] means unboxed tuple
42 ?? [ArgTypeKind] is the lub of *,#
43 ? [OpenTypeKind] means any type at all
47 error :: forall a:<any>. String -> a
49 (\(x::t) -> ...) Here t::<any> (i.e. not unboxed tuple)
55 | UnliftedTypeKind -- #
56 | UbxTupleKind -- (##)
58 | FunKind Kind Kind -- k1 -> k2
62 data KindVar = KVar Unique (IORef (Maybe SimpleKind))
63 -- INVARIANT: a KindVar can only be instantaited by a SimpleKind
65 type SimpleKind = Kind
66 -- A SimpleKind has no ? or # kinds in it:
67 -- sk ::= * | sk1 -> sk2 | kvar
69 instance Eq KindVar where
70 (KVar u1 _) == (KVar u2 _) = u1 == u2
72 mkKindVar :: Unique -> IORef (Maybe Kind) -> KindVar
78 During kind inference, a kind variable unifies only with
82 data T a = MkT a (T Int#)
83 fails. We give T the kind (k -> *), and the kind variable k won't unify
84 with # (the kind of Int#).
88 When creating a fresh internal type variable, we give it a kind to express
89 constraints on it. E.g. in (\x->e) we make up a fresh type variable for x,
92 During unification we only bind an internal type variable to a type
93 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
95 When unifying two internal type variables, we collect their kind constraints by
96 finding the GLB of the two. Since the partial order is a tree, they only
97 have a glb if one is a sub-kind of the other. In that case, we bind the
98 less-informative one to the more informative one. Neat, eh?
100 In the olden days, when we generalise, we make generic type variables
101 whose kind is simple. So generic type variables (other than built-in
102 constants like 'error') always have simple kinds. But I don't see any
103 reason to do that any more (TcMType.zapTcTyVarToTyVar).
107 liftedTypeKind = LiftedTypeKind
108 unliftedTypeKind = UnliftedTypeKind
109 openTypeKind = OpenTypeKind
110 argTypeKind = ArgTypeKind
111 ubxTupleKind = UbxTupleKind
113 mkArrowKind :: Kind -> Kind -> Kind
114 mkArrowKind k1 k2 = k1 `FunKind` k2
116 mkArrowKinds :: [Kind] -> Kind -> Kind
117 mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
120 %************************************************************************
124 %************************************************************************
127 kindFunResult :: Kind -> Kind
128 kindFunResult (FunKind _ k) = k
129 kindFunResult k = pprPanic "kindFunResult" (ppr k)
131 splitKindFunTys :: Kind -> ([Kind],Kind)
132 splitKindFunTys (FunKind k1 k2) = case splitKindFunTys k2 of
133 (as, r) -> (k1:as, r)
134 splitKindFunTys k = ([], k)
136 isLiftedTypeKind, isUnliftedTypeKind :: Kind -> Bool
137 isLiftedTypeKind LiftedTypeKind = True
138 isLiftedTypeKind other = False
140 isUnliftedTypeKind UnliftedTypeKind = True
141 isUnliftedTypeKind other = False
143 isArgTypeKind :: Kind -> Bool
144 -- True of any sub-kind of ArgTypeKind
145 isArgTypeKind LiftedTypeKind = True
146 isArgTypeKind UnliftedTypeKind = True
147 isArgTypeKind ArgTypeKind = True
148 isArgTypeKind other = False
150 isOpenTypeKind :: Kind -> Bool
151 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
152 isOpenTypeKind (FunKind _ _) = False
153 isOpenTypeKind other = True
155 isSubKind :: Kind -> Kind -> Bool
156 -- (k1 `isSubKind` k2) checks that k1 <: k2
157 isSubKind LiftedTypeKind LiftedTypeKind = True
158 isSubKind UnliftedTypeKind UnliftedTypeKind = True
159 isSubKind UbxTupleKind UbxTupleKind = True
160 isSubKind k1 OpenTypeKind = isOpenTypeKind k1
161 isSubKind k1 ArgTypeKind = isArgTypeKind k1
162 isSubKind (FunKind a1 r1) (FunKind a2 r2)
163 = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
164 isSubKind k1 k2 = False
166 defaultKind :: Kind -> Kind
167 -- Used when generalising: default kind '?' and '??' to '*'
168 defaultKind OpenTypeKind = LiftedTypeKind
169 defaultKind ArgTypeKind = LiftedTypeKind
170 defaultKind kind = kind
174 %************************************************************************
178 %************************************************************************
181 instance Outputable KindVar where
182 ppr (KVar uniq _) = text "k_" <> ppr uniq
184 instance Outputable Kind where
187 pprParendKind :: Kind -> SDoc
188 pprParendKind k@(FunKind _ _) = parens (pprKind k)
189 pprParendKind k = pprKind k
191 pprKind (KindVar v) = ppr v
192 pprKind LiftedTypeKind = ptext SLIT("*")
193 pprKind UnliftedTypeKind = ptext SLIT("#")
194 pprKind OpenTypeKind = ptext SLIT("?")
195 pprKind ArgTypeKind = ptext SLIT("??")
196 pprKind UbxTupleKind = ptext SLIT("(#)")
197 pprKind (FunKind k1 k2) = sep [ pprKind k1, arrow <+> pprParendKind k2]