Note [The equality types story] in TysPrim
[ghc.git] / compiler / prelude / TysPrim.hs
1 {-
2 (c) The AQUA Project, Glasgow University, 1994-1998
3
4
5 \section[TysPrim]{Wired-in knowledge about primitive types}
6 -}
7
8 {-# LANGUAGE CPP #-}
9
10 -- | This module defines TyCons that can't be expressed in Haskell.
11 -- They are all, therefore, wired-in TyCons. C.f module TysWiredIn
12 module TysPrim(
13 mkPrimTyConName, -- For implicit parameters in TysWiredIn only
14
15 mkTemplateTyVars,
16 alphaTyVars, alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar,
17 alphaTys, alphaTy, betaTy, gammaTy, deltaTy,
18 levity1TyVar, levity2TyVar, levity1Ty, levity2Ty,
19 openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar,
20 kKiVar,
21
22 -- Kind constructors...
23 tYPETyCon, unliftedTypeKindTyCon, unliftedTypeKind,
24
25 tYPETyConName, unliftedTypeKindTyConName,
26
27 -- Kinds
28 tYPE,
29
30 funTyCon, funTyConName,
31 primTyCons,
32
33 charPrimTyCon, charPrimTy,
34 intPrimTyCon, intPrimTy,
35 wordPrimTyCon, wordPrimTy,
36 addrPrimTyCon, addrPrimTy,
37 floatPrimTyCon, floatPrimTy,
38 doublePrimTyCon, doublePrimTy,
39
40 voidPrimTyCon, voidPrimTy,
41 statePrimTyCon, mkStatePrimTy,
42 realWorldTyCon, realWorldTy, realWorldStatePrimTy,
43
44 proxyPrimTyCon, mkProxyPrimTy,
45
46 arrayPrimTyCon, mkArrayPrimTy,
47 byteArrayPrimTyCon, byteArrayPrimTy,
48 arrayArrayPrimTyCon, mkArrayArrayPrimTy,
49 smallArrayPrimTyCon, mkSmallArrayPrimTy,
50 mutableArrayPrimTyCon, mkMutableArrayPrimTy,
51 mutableByteArrayPrimTyCon, mkMutableByteArrayPrimTy,
52 mutableArrayArrayPrimTyCon, mkMutableArrayArrayPrimTy,
53 smallMutableArrayPrimTyCon, mkSmallMutableArrayPrimTy,
54 mutVarPrimTyCon, mkMutVarPrimTy,
55
56 mVarPrimTyCon, mkMVarPrimTy,
57 tVarPrimTyCon, mkTVarPrimTy,
58 stablePtrPrimTyCon, mkStablePtrPrimTy,
59 stableNamePrimTyCon, mkStableNamePrimTy,
60 bcoPrimTyCon, bcoPrimTy,
61 weakPrimTyCon, mkWeakPrimTy,
62 threadIdPrimTyCon, threadIdPrimTy,
63
64 int32PrimTyCon, int32PrimTy,
65 word32PrimTyCon, word32PrimTy,
66
67 int64PrimTyCon, int64PrimTy,
68 word64PrimTyCon, word64PrimTy,
69
70 eqPrimTyCon, -- ty1 ~# ty2
71 eqReprPrimTyCon, -- ty1 ~R# ty2 (at role Representational)
72 eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom)
73
74 -- * Any
75 anyTy, anyTyCon, anyTypeOfKind,
76
77 -- * SIMD
78 #include "primop-vector-tys-exports.hs-incl"
79 ) where
80
81 #include "HsVersions.h"
82
83 import {-# SOURCE #-} TysWiredIn ( levityTy, unliftedDataConTy, liftedTypeKind )
84
85 import Var ( TyVar, KindVar, mkTyVar )
86 import Name
87 import TyCon
88 import SrcLoc
89 import Unique
90 import PrelNames
91 import FastString
92 import TyCoRep -- doesn't need special access, but this is easier to avoid
93 -- import loops
94
95 import Data.Char
96
97 {-
98 ************************************************************************
99 * *
100 \subsection{Primitive type constructors}
101 * *
102 ************************************************************************
103 -}
104
105 primTyCons :: [TyCon]
106 primTyCons
107 = [ addrPrimTyCon
108 , arrayPrimTyCon
109 , byteArrayPrimTyCon
110 , arrayArrayPrimTyCon
111 , smallArrayPrimTyCon
112 , charPrimTyCon
113 , doublePrimTyCon
114 , floatPrimTyCon
115 , intPrimTyCon
116 , int32PrimTyCon
117 , int64PrimTyCon
118 , bcoPrimTyCon
119 , weakPrimTyCon
120 , mutableArrayPrimTyCon
121 , mutableByteArrayPrimTyCon
122 , mutableArrayArrayPrimTyCon
123 , smallMutableArrayPrimTyCon
124 , mVarPrimTyCon
125 , tVarPrimTyCon
126 , mutVarPrimTyCon
127 , realWorldTyCon
128 , stablePtrPrimTyCon
129 , stableNamePrimTyCon
130 , statePrimTyCon
131 , voidPrimTyCon
132 , proxyPrimTyCon
133 , threadIdPrimTyCon
134 , wordPrimTyCon
135 , word32PrimTyCon
136 , word64PrimTyCon
137 , anyTyCon
138 , eqPrimTyCon
139 , eqReprPrimTyCon
140 , eqPhantPrimTyCon
141
142 , unliftedTypeKindTyCon
143 , tYPETyCon
144
145 #include "primop-vector-tycons.hs-incl"
146 ]
147
148 mkPrimTc :: FastString -> Unique -> TyCon -> Name
149 mkPrimTc fs unique tycon
150 = mkWiredInName gHC_PRIM (mkTcOccFS fs)
151 unique
152 (ATyCon tycon) -- Relevant TyCon
153 UserSyntax
154
155 mkBuiltInPrimTc :: FastString -> Unique -> TyCon -> Name
156 mkBuiltInPrimTc fs unique tycon
157 = mkWiredInName gHC_PRIM (mkTcOccFS fs)
158 unique
159 (ATyCon tycon) -- Relevant TyCon
160 BuiltInSyntax
161
162
163 charPrimTyConName, intPrimTyConName, int32PrimTyConName, int64PrimTyConName, wordPrimTyConName, word32PrimTyConName, word64PrimTyConName, addrPrimTyConName, floatPrimTyConName, doublePrimTyConName, statePrimTyConName, proxyPrimTyConName, realWorldTyConName, arrayPrimTyConName, arrayArrayPrimTyConName, smallArrayPrimTyConName, byteArrayPrimTyConName, mutableArrayPrimTyConName, mutableByteArrayPrimTyConName, mutableArrayArrayPrimTyConName, smallMutableArrayPrimTyConName, mutVarPrimTyConName, mVarPrimTyConName, tVarPrimTyConName, stablePtrPrimTyConName, stableNamePrimTyConName, bcoPrimTyConName, weakPrimTyConName, threadIdPrimTyConName, eqPrimTyConName, eqReprPrimTyConName, eqPhantPrimTyConName, voidPrimTyConName :: Name
164 charPrimTyConName = mkPrimTc (fsLit "Char#") charPrimTyConKey charPrimTyCon
165 intPrimTyConName = mkPrimTc (fsLit "Int#") intPrimTyConKey intPrimTyCon
166 int32PrimTyConName = mkPrimTc (fsLit "Int32#") int32PrimTyConKey int32PrimTyCon
167 int64PrimTyConName = mkPrimTc (fsLit "Int64#") int64PrimTyConKey int64PrimTyCon
168 wordPrimTyConName = mkPrimTc (fsLit "Word#") wordPrimTyConKey wordPrimTyCon
169 word32PrimTyConName = mkPrimTc (fsLit "Word32#") word32PrimTyConKey word32PrimTyCon
170 word64PrimTyConName = mkPrimTc (fsLit "Word64#") word64PrimTyConKey word64PrimTyCon
171 addrPrimTyConName = mkPrimTc (fsLit "Addr#") addrPrimTyConKey addrPrimTyCon
172 floatPrimTyConName = mkPrimTc (fsLit "Float#") floatPrimTyConKey floatPrimTyCon
173 doublePrimTyConName = mkPrimTc (fsLit "Double#") doublePrimTyConKey doublePrimTyCon
174 statePrimTyConName = mkPrimTc (fsLit "State#") statePrimTyConKey statePrimTyCon
175 voidPrimTyConName = mkPrimTc (fsLit "Void#") voidPrimTyConKey voidPrimTyCon
176 proxyPrimTyConName = mkPrimTc (fsLit "Proxy#") proxyPrimTyConKey proxyPrimTyCon
177 eqPrimTyConName = mkPrimTc (fsLit "~#") eqPrimTyConKey eqPrimTyCon
178 eqReprPrimTyConName = mkBuiltInPrimTc (fsLit "~R#") eqReprPrimTyConKey eqReprPrimTyCon
179 eqPhantPrimTyConName = mkBuiltInPrimTc (fsLit "~P#") eqPhantPrimTyConKey eqPhantPrimTyCon
180 realWorldTyConName = mkPrimTc (fsLit "RealWorld") realWorldTyConKey realWorldTyCon
181 arrayPrimTyConName = mkPrimTc (fsLit "Array#") arrayPrimTyConKey arrayPrimTyCon
182 byteArrayPrimTyConName = mkPrimTc (fsLit "ByteArray#") byteArrayPrimTyConKey byteArrayPrimTyCon
183 arrayArrayPrimTyConName = mkPrimTc (fsLit "ArrayArray#") arrayArrayPrimTyConKey arrayArrayPrimTyCon
184 smallArrayPrimTyConName = mkPrimTc (fsLit "SmallArray#") smallArrayPrimTyConKey smallArrayPrimTyCon
185 mutableArrayPrimTyConName = mkPrimTc (fsLit "MutableArray#") mutableArrayPrimTyConKey mutableArrayPrimTyCon
186 mutableByteArrayPrimTyConName = mkPrimTc (fsLit "MutableByteArray#") mutableByteArrayPrimTyConKey mutableByteArrayPrimTyCon
187 mutableArrayArrayPrimTyConName= mkPrimTc (fsLit "MutableArrayArray#") mutableArrayArrayPrimTyConKey mutableArrayArrayPrimTyCon
188 smallMutableArrayPrimTyConName= mkPrimTc (fsLit "SmallMutableArray#") smallMutableArrayPrimTyConKey smallMutableArrayPrimTyCon
189 mutVarPrimTyConName = mkPrimTc (fsLit "MutVar#") mutVarPrimTyConKey mutVarPrimTyCon
190 mVarPrimTyConName = mkPrimTc (fsLit "MVar#") mVarPrimTyConKey mVarPrimTyCon
191 tVarPrimTyConName = mkPrimTc (fsLit "TVar#") tVarPrimTyConKey tVarPrimTyCon
192 stablePtrPrimTyConName = mkPrimTc (fsLit "StablePtr#") stablePtrPrimTyConKey stablePtrPrimTyCon
193 stableNamePrimTyConName = mkPrimTc (fsLit "StableName#") stableNamePrimTyConKey stableNamePrimTyCon
194 bcoPrimTyConName = mkPrimTc (fsLit "BCO#") bcoPrimTyConKey bcoPrimTyCon
195 weakPrimTyConName = mkPrimTc (fsLit "Weak#") weakPrimTyConKey weakPrimTyCon
196 threadIdPrimTyConName = mkPrimTc (fsLit "ThreadId#") threadIdPrimTyConKey threadIdPrimTyCon
197
198 {-
199 ************************************************************************
200 * *
201 \subsection{Support code}
202 * *
203 ************************************************************************
204
205 alphaTyVars is a list of type variables for use in templates:
206 ["a", "b", ..., "z", "t1", "t2", ... ]
207 -}
208
209 mkTemplateTyVars :: [Kind] -> [TyVar]
210 mkTemplateTyVars kinds =
211 [ mkTyVar (mkInternalName (mkAlphaTyVarUnique u)
212 (mkTyVarOccFS (mkFastString name))
213 noSrcSpan) k
214 | (k,u) <- zip kinds [2..],
215 let name | c <= 'z' = [c]
216 | otherwise = 't':show u
217 where c = chr (u-2 + ord 'a')
218 ]
219
220 alphaTyVars :: [TyVar]
221 alphaTyVars = mkTemplateTyVars $ repeat liftedTypeKind
222
223 alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar :: TyVar
224 (alphaTyVar:betaTyVar:gammaTyVar:deltaTyVar:_) = alphaTyVars
225
226 alphaTys :: [Type]
227 alphaTys = mkTyVarTys alphaTyVars
228 alphaTy, betaTy, gammaTy, deltaTy :: Type
229 (alphaTy:betaTy:gammaTy:deltaTy:_) = alphaTys
230
231 levity1TyVar, levity2TyVar :: TyVar
232 (levity1TyVar : levity2TyVar : _)
233 = drop 21 (mkTemplateTyVars (repeat levityTy)) -- selects 'v','w'
234
235 levity1Ty, levity2Ty :: Type
236 levity1Ty = mkTyVarTy levity1TyVar
237 levity2Ty = mkTyVarTy levity2TyVar
238
239 openAlphaTyVar, openBetaTyVar :: TyVar
240 [openAlphaTyVar,openBetaTyVar]
241 = mkTemplateTyVars [tYPE levity1Ty, tYPE levity2Ty]
242
243 openAlphaTy, openBetaTy :: Type
244 openAlphaTy = mkTyVarTy openAlphaTyVar
245 openBetaTy = mkTyVarTy openBetaTyVar
246
247 kKiVar :: KindVar
248 kKiVar = (mkTemplateTyVars $ repeat liftedTypeKind) !! 10
249 -- the 10 selects the 11th letter in the alphabet: 'k'
250
251 {-
252 ************************************************************************
253 * *
254 FunTyCon
255 * *
256 ************************************************************************
257 -}
258
259 funTyConName :: Name
260 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
261
262 funTyCon :: TyCon
263 funTyCon = mkFunTyCon funTyConName kind tc_rep_nm
264 where
265 kind = mkFunTys [liftedTypeKind, liftedTypeKind] liftedTypeKind
266 -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
267 -- But if we do that we get kind errors when saying
268 -- instance Control.Arrow (->)
269 -- because the expected kind is (*->*->*). The trouble is that the
270 -- expected/actual stuff in the unifier does not go contra-variant, whereas
271 -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
272 -- a prefix way, thus: (->) Int# Int#. And this is unusual.
273 -- because they are never in scope in the source
274
275 tc_rep_nm = mkSpecialTyConRepName (fsLit "tcFun") funTyConName
276
277 -- One step to remove subkinding.
278 -- (->) :: * -> * -> *
279 -- but we should have (and want) the following typing rule for fully applied arrows
280 -- Gamma |- tau :: k1 k1 in {*, #}
281 -- Gamma |- sigma :: k2 k2 in {*, #, (#)}
282 -- -----------------------------------------
283 -- Gamma |- tau -> sigma :: *
284 -- Currently we have the following rule which achieves more or less the same effect
285 -- Gamma |- tau :: ??
286 -- Gamma |- sigma :: ?
287 -- --------------------------
288 -- Gamma |- tau -> sigma :: *
289 -- In the end we don't want subkinding at all.
290
291 {-
292 ************************************************************************
293 * *
294 Kinds
295 * *
296 ************************************************************************
297
298 Note [TYPE]
299 ~~~~~~~~~~~
300 There are a few places where we wish to be able to deal interchangeably
301 with kind * and kind #. unsafeCoerce#, error, and (->) are some of these
302 places. The way we do this is to use levity polymorphism.
303
304 We have (levityTyCon, liftedDataCon, unliftedDataCon)
305
306 data Levity = Lifted | Unlifted
307
308 and a magical constant (tYPETyCon)
309
310 TYPE :: Levity -> TYPE Lifted
311
312 We then have synonyms (liftedTypeKindTyCon, unliftedTypeKindTyCon)
313
314 type Type = TYPE Lifted
315 type # = TYPE Unlifted
316
317 So, for example, we get
318
319 unsafeCoerce# :: forall (v1 :: Levity) (v2 :: Levity)
320 (a :: TYPE v1) (b :: TYPE v2). a -> b
321
322 This replaces the old sub-kinding machinery. We call variables `a` and `b`
323 above "levity polymorphic".
324 -}
325
326 tYPETyCon, unliftedTypeKindTyCon :: TyCon
327 tYPETyConName, unliftedTypeKindTyConName :: Name
328
329 tYPETyCon = mkKindTyCon tYPETyConName
330 (ForAllTy (Anon levityTy) liftedTypeKind)
331 [Nominal]
332 (mkSpecialTyConRepName (fsLit "tcTYPE") tYPETyConName)
333
334 -- See Note [TYPE]
335 -- NB: unlifted is wired in because there is no way to parse it in
336 -- Haskell. That's the only reason for wiring it in.
337 unliftedTypeKindTyCon = mkSynonymTyCon unliftedTypeKindTyConName
338 liftedTypeKind
339 [] []
340 (tYPE unliftedDataConTy)
341
342 --------------------------
343 -- ... and now their names
344
345 -- If you edit these, you may need to update the GHC formalism
346 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
347 tYPETyConName = mkPrimTyConName (fsLit "TYPE") tYPETyConKey tYPETyCon
348 unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
349
350 unliftedTypeKind :: Kind
351 unliftedTypeKind = tYPE unliftedDataConTy
352
353 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
354 mkPrimTyConName = mkPrimTcName BuiltInSyntax
355 -- All of the super kinds and kinds are defined in Prim,
356 -- and use BuiltInSyntax, because they are never in scope in the source
357
358 mkPrimTcName :: BuiltInSyntax -> FastString -> Unique -> TyCon -> Name
359 mkPrimTcName built_in_syntax occ key tycon
360 = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (ATyCon tycon) built_in_syntax
361
362 -----------------------------
363 -- | Given a Levity, applies TYPE to it. See Note [TYPE].
364 tYPE :: Type -> Type
365 tYPE lev = TyConApp tYPETyCon [lev]
366
367 {-
368 ************************************************************************
369 * *
370 \subsection[TysPrim-basic]{Basic primitive types (@Char#@, @Int#@, etc.)}
371 * *
372 ************************************************************************
373 -}
374
375 -- only used herein
376 pcPrimTyCon :: Name -> [Role] -> PrimRep -> TyCon
377 pcPrimTyCon name roles rep
378 = mkPrimTyCon name kind roles rep
379 where
380 kind = mkFunTys (map (const liftedTypeKind) roles) result_kind
381 result_kind = unliftedTypeKind
382
383 pcPrimTyCon0 :: Name -> PrimRep -> TyCon
384 pcPrimTyCon0 name rep
385 = mkPrimTyCon name result_kind [] rep
386 where
387 result_kind = unliftedTypeKind
388
389 charPrimTy :: Type
390 charPrimTy = mkTyConTy charPrimTyCon
391 charPrimTyCon :: TyCon
392 charPrimTyCon = pcPrimTyCon0 charPrimTyConName WordRep
393
394 intPrimTy :: Type
395 intPrimTy = mkTyConTy intPrimTyCon
396 intPrimTyCon :: TyCon
397 intPrimTyCon = pcPrimTyCon0 intPrimTyConName IntRep
398
399 int32PrimTy :: Type
400 int32PrimTy = mkTyConTy int32PrimTyCon
401 int32PrimTyCon :: TyCon
402 int32PrimTyCon = pcPrimTyCon0 int32PrimTyConName IntRep
403
404 int64PrimTy :: Type
405 int64PrimTy = mkTyConTy int64PrimTyCon
406 int64PrimTyCon :: TyCon
407 int64PrimTyCon = pcPrimTyCon0 int64PrimTyConName Int64Rep
408
409 wordPrimTy :: Type
410 wordPrimTy = mkTyConTy wordPrimTyCon
411 wordPrimTyCon :: TyCon
412 wordPrimTyCon = pcPrimTyCon0 wordPrimTyConName WordRep
413
414 word32PrimTy :: Type
415 word32PrimTy = mkTyConTy word32PrimTyCon
416 word32PrimTyCon :: TyCon
417 word32PrimTyCon = pcPrimTyCon0 word32PrimTyConName WordRep
418
419 word64PrimTy :: Type
420 word64PrimTy = mkTyConTy word64PrimTyCon
421 word64PrimTyCon :: TyCon
422 word64PrimTyCon = pcPrimTyCon0 word64PrimTyConName Word64Rep
423
424 addrPrimTy :: Type
425 addrPrimTy = mkTyConTy addrPrimTyCon
426 addrPrimTyCon :: TyCon
427 addrPrimTyCon = pcPrimTyCon0 addrPrimTyConName AddrRep
428
429 floatPrimTy :: Type
430 floatPrimTy = mkTyConTy floatPrimTyCon
431 floatPrimTyCon :: TyCon
432 floatPrimTyCon = pcPrimTyCon0 floatPrimTyConName FloatRep
433
434 doublePrimTy :: Type
435 doublePrimTy = mkTyConTy doublePrimTyCon
436 doublePrimTyCon :: TyCon
437 doublePrimTyCon = pcPrimTyCon0 doublePrimTyConName DoubleRep
438
439 {-
440 ************************************************************************
441 * *
442 \subsection[TysPrim-state]{The @State#@ type (and @_RealWorld@ types)}
443 * *
444 ************************************************************************
445
446 Note [The equality types story]
447 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
448 GHC sports a veritable menagerie of equality types:
449
450 Hetero? Levity Result Role Defining module
451 ------------------------------------------------------------
452 ~# hetero unlifted # nominal GHC.Prim
453 ~~ hetero lifted Constraint nominal GHC.Types
454 ~ homo lifted Constraint nominal Data.Type.Equality
455 :~: homo lifted * nominal Data.Type.Equality
456
457 ~R# hetero unlifted # repr. GHC.Prim
458 Coercible homo lifted Constraint repr. GHC.Types
459 Coercion homo lifted * repr. Data.Type.Coercion
460
461 ~P# hetero unlifted phantom GHC.Prim
462
463 Recall that "hetero" means the equality can related types of different
464 kinds. Knowing that (t1 ~# t2) or (t1 ~R# t2) or even that (t1 ~P# t2)
465 also means that (k1 ~# k2), where (t1 :: k1) and (t2 :: k2).
466
467 To produce less confusion for end users, when not dumping and without
468 -fprint-equality-relations, each of these groups is printed as the bottommost
469 listed equality. That is, (~#) and (~~) are both rendered as (~) in
470 error messages, and (~R#) is rendered as Coercible.
471
472 Let's take these one at a time:
473
474 (~#) :: forall k1 k2. k1 -> k2 -> #
475 This is The Type Of Equality in GHC. It classifies nominal coercions.
476 This type is used in the solver for recording equality constraints.
477 It responds "yes" to Type.isEqPred and classifies as an EqPred in
478 Type.classifyPredType.
479
480 All wanted constraints of this type are built with coercion holes.
481 (See Note [Coercion holes] in TyCoRep.) But see also
482 Note [Deferred errors for coercion holes] in TcErrors to see how
483 equality constraints are deferred.
484
485 Within GHC, ~# is called eqPrimTyCon, and it is defined in TysPrim.
486
487
488 (~~) :: forall k1 k2. k1 -> k2 -> Constraint
489 This is (almost) an ordinary class, defined as if by
490 class a ~# b => a ~~ b
491 instance a ~# b => a ~~ b
492 Here's what's unusual about it:
493 * We can't actually declare it that way because we don't have syntax for ~#.
494 And ~# isn't a constraint, so even if we could write it, it wouldn't kind
495 check.
496
497 * Users cannot write instances of it.
498
499 * It is "naturally coherent". This means that the solver won't hesitate to
500 solve a goal of type (a ~~ b) even if there is, say (Int ~~ c) in the
501 context. (Normally, it waits to learn more, just in case the given
502 influences what happens next.) This is quite like having
503 IncoherentInstances enabled.
504
505 * It always terminates. That is, in the UndecidableInstances checks, we
506 don't worry if a (~~) constraint is too big, as we know that solving
507 equality terminates.
508
509 On the other hand, this behaves just like any class w.r.t. eager superclass
510 unpacking in the solver. So a lifted equality given quickly becomes an unlifted
511 equality given. This is good, because the solver knows all about unlifted
512 equalities. There is some special-casing in TcInteract.matchClassInst to
513 pretend that there is an instance of this class, as we can't write the instance
514 in Haskell.
515
516 Within GHC, ~~ is called heqTyCon, and it is defined in TysWiredIn.
517
518
519 (~) :: forall k. k -> k -> Constraint
520 This is defined in Data.Type.Equality:
521 class a ~~ b => (a :: k) ~ (b :: k)
522 instance a ~~ b => a ~ b
523 This is even more so an ordinary class than (~~), with the following exceptions:
524 * Users cannot write instances of it.
525
526 * It is "naturally coherent". (See (~~).)
527
528 * (~) is magical syntax, as ~ is a reserved symbol. It cannot be exported
529 or imported.
530
531 * It always terminates.
532
533 Within GHC, ~ is called eqTyCon, and it is defined in PrelNames. Note that
534 it is *not* wired in.
535
536
537 (:~:) :: forall k. k -> k -> *
538 This is a perfectly ordinary GADT, wrapping (~). It is not defined within
539 GHC at all.
540
541
542 (~R#) :: forall k1 k2. k1 -> k2 -> #
543 The is the representational analogue of ~#. This is the type of representational
544 equalities that the solver works on. All wanted constraints of this type are
545 built with coercion holes.
546
547 Within GHC, ~R# is called eqReprPrimTyCon, and it is defined in TysPrim.
548
549
550 Coercible :: forall k. k -> k -> Constraint
551 This is quite like (~~) in the way it's defined and treated within GHC, but
552 it's homogeneous. Homogeneity helps with type inference (as GHC can solve one
553 kind from the other) and, in my (Richard's) estimation, will be more intuitive
554 for users.
555
556 An alternative design included HCoercible (like (~~)) and Coercible (like (~)).
557 One annoyance was that we want `coerce :: Coercible a b => a -> b`, and
558 we need the type of coerce to be fully wired-in. So the HCoercible/Coercible
559 split required that both types be fully wired-in. Instead of doing this,
560 I just got rid of HCoercible, as I'm not sure who would use it, anyway.
561
562 Within GHC, Coercible is called coercibleTyCon, and it is defined in
563 TysWiredIn.
564
565
566 Coercion :: forall k. k -> k -> *
567 This is a perfectly ordinary GADT, wrapping Coercible. It is not defined
568 within GHC at all.
569
570
571 (~P#) :: forall k1 k2. k1 -> k2 -> #
572 This is the phantom analogue of ~# and it is barely used at all.
573 (The solver has no idea about this one.) Here is the motivation:
574
575 data Phant a = MkPhant
576 type role Phant phantom
577
578 Phant <Int, Bool>_P :: Phant Int ~P# Phant Bool
579
580 We just need to have something to put on that last line. You probably
581 don't need to worry about it.
582
583
584
585 Note [The State# TyCon]
586 ~~~~~~~~~~~~~~~~~~~~~~~
587 State# is the primitive, unlifted type of states. It has one type parameter,
588 thus
589 State# RealWorld
590 or
591 State# s
592
593 where s is a type variable. The only purpose of the type parameter is to
594 keep different state threads separate. It is represented by nothing at all.
595
596 The type parameter to State# is intended to keep separate threads separate.
597 Even though this parameter is not used in the definition of State#, it is
598 given role Nominal to enforce its intended use.
599 -}
600
601 mkStatePrimTy :: Type -> Type
602 mkStatePrimTy ty = TyConApp statePrimTyCon [ty]
603
604 statePrimTyCon :: TyCon -- See Note [The State# TyCon]
605 statePrimTyCon = pcPrimTyCon statePrimTyConName [Nominal] VoidRep
606
607 {-
608 RealWorld is deeply magical. It is *primitive*, but it is not
609 *unlifted* (hence ptrArg). We never manipulate values of type
610 RealWorld; it's only used in the type system, to parameterise State#.
611 -}
612
613 realWorldTyCon :: TyCon
614 realWorldTyCon = mkLiftedPrimTyCon realWorldTyConName liftedTypeKind [] PtrRep
615 realWorldTy :: Type
616 realWorldTy = mkTyConTy realWorldTyCon
617 realWorldStatePrimTy :: Type
618 realWorldStatePrimTy = mkStatePrimTy realWorldTy -- State# RealWorld
619
620 -- Note: the ``state-pairing'' types are not truly primitive,
621 -- so they are defined in \tr{TysWiredIn.hs}, not here.
622
623
624 voidPrimTy :: Type
625 voidPrimTy = TyConApp voidPrimTyCon []
626
627 voidPrimTyCon :: TyCon
628 voidPrimTyCon = pcPrimTyCon voidPrimTyConName [] VoidRep
629
630 mkProxyPrimTy :: Type -> Type -> Type
631 mkProxyPrimTy k ty = TyConApp proxyPrimTyCon [k, ty]
632
633 proxyPrimTyCon :: TyCon
634 proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
635 where kind = ForAllTy (Named kv Invisible) $
636 mkFunTy k unliftedTypeKind
637 kv = kKiVar
638 k = mkTyVarTy kv
639
640
641 {- *********************************************************************
642 * *
643 Primitive equality constraints
644 See Note [The equality types story]
645 * *
646 ********************************************************************* -}
647
648 eqPrimTyCon :: TyCon -- The representation type for equality predicates
649 -- See Note [The equality types story]
650 eqPrimTyCon = mkPrimTyCon eqPrimTyConName kind roles VoidRep
651 where kind = ForAllTy (Named kv1 Invisible) $
652 ForAllTy (Named kv2 Invisible) $
653 mkFunTys [k1, k2] unliftedTypeKind
654 [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
655 k1 = mkTyVarTy kv1
656 k2 = mkTyVarTy kv2
657 roles = [Nominal, Nominal, Nominal, Nominal]
658
659 -- like eqPrimTyCon, but the type for *Representational* coercions
660 -- this should only ever appear as the type of a covar. Its role is
661 -- interpreted in coercionRole
662 eqReprPrimTyCon :: TyCon -- See Note [The equality types story]
663 eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName kind
664 roles VoidRep
665 where kind = ForAllTy (Named kv1 Invisible) $
666 ForAllTy (Named kv2 Invisible) $
667 mkFunTys [k1, k2] unliftedTypeKind
668 [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
669 k1 = mkTyVarTy kv1
670 k2 = mkTyVarTy kv2
671 roles = [Nominal, Nominal, Representational, Representational]
672
673 -- like eqPrimTyCon, but the type for *Phantom* coercions.
674 -- This is only used to make higher-order equalities. Nothing
675 -- should ever actually have this type!
676 eqPhantPrimTyCon :: TyCon
677 eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName kind
678 [Nominal, Nominal, Phantom, Phantom]
679 VoidRep
680 where kind = ForAllTy (Named kv1 Invisible) $
681 ForAllTy (Named kv2 Invisible) $
682 mkFunTys [k1, k2] unliftedTypeKind
683 [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
684 k1 = mkTyVarTy kv1
685 k2 = mkTyVarTy kv2
686
687
688 {- *********************************************************************
689 * *
690 The primitive array types
691 * *
692 ********************************************************************* -}
693
694 arrayPrimTyCon, mutableArrayPrimTyCon, mutableByteArrayPrimTyCon,
695 byteArrayPrimTyCon, arrayArrayPrimTyCon, mutableArrayArrayPrimTyCon,
696 smallArrayPrimTyCon, smallMutableArrayPrimTyCon :: TyCon
697 arrayPrimTyCon = pcPrimTyCon arrayPrimTyConName [Representational] PtrRep
698 mutableArrayPrimTyCon = pcPrimTyCon mutableArrayPrimTyConName [Nominal, Representational] PtrRep
699 mutableByteArrayPrimTyCon = pcPrimTyCon mutableByteArrayPrimTyConName [Nominal] PtrRep
700 byteArrayPrimTyCon = pcPrimTyCon0 byteArrayPrimTyConName PtrRep
701 arrayArrayPrimTyCon = pcPrimTyCon0 arrayArrayPrimTyConName PtrRep
702 mutableArrayArrayPrimTyCon = pcPrimTyCon mutableArrayArrayPrimTyConName [Nominal] PtrRep
703 smallArrayPrimTyCon = pcPrimTyCon smallArrayPrimTyConName [Representational] PtrRep
704 smallMutableArrayPrimTyCon = pcPrimTyCon smallMutableArrayPrimTyConName [Nominal, Representational] PtrRep
705
706 mkArrayPrimTy :: Type -> Type
707 mkArrayPrimTy elt = TyConApp arrayPrimTyCon [elt]
708 byteArrayPrimTy :: Type
709 byteArrayPrimTy = mkTyConTy byteArrayPrimTyCon
710 mkArrayArrayPrimTy :: Type
711 mkArrayArrayPrimTy = mkTyConTy arrayArrayPrimTyCon
712 mkSmallArrayPrimTy :: Type -> Type
713 mkSmallArrayPrimTy elt = TyConApp smallArrayPrimTyCon [elt]
714 mkMutableArrayPrimTy :: Type -> Type -> Type
715 mkMutableArrayPrimTy s elt = TyConApp mutableArrayPrimTyCon [s, elt]
716 mkMutableByteArrayPrimTy :: Type -> Type
717 mkMutableByteArrayPrimTy s = TyConApp mutableByteArrayPrimTyCon [s]
718 mkMutableArrayArrayPrimTy :: Type -> Type
719 mkMutableArrayArrayPrimTy s = TyConApp mutableArrayArrayPrimTyCon [s]
720 mkSmallMutableArrayPrimTy :: Type -> Type -> Type
721 mkSmallMutableArrayPrimTy s elt = TyConApp smallMutableArrayPrimTyCon [s, elt]
722
723
724 {- *********************************************************************
725 * *
726 The mutable variable type
727 * *
728 ********************************************************************* -}
729
730 mutVarPrimTyCon :: TyCon
731 mutVarPrimTyCon = pcPrimTyCon mutVarPrimTyConName [Nominal, Representational] PtrRep
732
733 mkMutVarPrimTy :: Type -> Type -> Type
734 mkMutVarPrimTy s elt = TyConApp mutVarPrimTyCon [s, elt]
735
736 {-
737 ************************************************************************
738 * *
739 \subsection[TysPrim-synch-var]{The synchronizing variable type}
740 * *
741 ************************************************************************
742 -}
743
744 mVarPrimTyCon :: TyCon
745 mVarPrimTyCon = pcPrimTyCon mVarPrimTyConName [Nominal, Representational] PtrRep
746
747 mkMVarPrimTy :: Type -> Type -> Type
748 mkMVarPrimTy s elt = TyConApp mVarPrimTyCon [s, elt]
749
750 {-
751 ************************************************************************
752 * *
753 \subsection[TysPrim-stm-var]{The transactional variable type}
754 * *
755 ************************************************************************
756 -}
757
758 tVarPrimTyCon :: TyCon
759 tVarPrimTyCon = pcPrimTyCon tVarPrimTyConName [Nominal, Representational] PtrRep
760
761 mkTVarPrimTy :: Type -> Type -> Type
762 mkTVarPrimTy s elt = TyConApp tVarPrimTyCon [s, elt]
763
764 {-
765 ************************************************************************
766 * *
767 \subsection[TysPrim-stable-ptrs]{The stable-pointer type}
768 * *
769 ************************************************************************
770 -}
771
772 stablePtrPrimTyCon :: TyCon
773 stablePtrPrimTyCon = pcPrimTyCon stablePtrPrimTyConName [Representational] AddrRep
774
775 mkStablePtrPrimTy :: Type -> Type
776 mkStablePtrPrimTy ty = TyConApp stablePtrPrimTyCon [ty]
777
778 {-
779 ************************************************************************
780 * *
781 \subsection[TysPrim-stable-names]{The stable-name type}
782 * *
783 ************************************************************************
784 -}
785
786 stableNamePrimTyCon :: TyCon
787 stableNamePrimTyCon = pcPrimTyCon stableNamePrimTyConName [Representational] PtrRep
788
789 mkStableNamePrimTy :: Type -> Type
790 mkStableNamePrimTy ty = TyConApp stableNamePrimTyCon [ty]
791
792 {-
793 ************************************************************************
794 * *
795 \subsection[TysPrim-BCOs]{The ``bytecode object'' type}
796 * *
797 ************************************************************************
798 -}
799
800 bcoPrimTy :: Type
801 bcoPrimTy = mkTyConTy bcoPrimTyCon
802 bcoPrimTyCon :: TyCon
803 bcoPrimTyCon = pcPrimTyCon0 bcoPrimTyConName PtrRep
804
805 {-
806 ************************************************************************
807 * *
808 \subsection[TysPrim-Weak]{The ``weak pointer'' type}
809 * *
810 ************************************************************************
811 -}
812
813 weakPrimTyCon :: TyCon
814 weakPrimTyCon = pcPrimTyCon weakPrimTyConName [Representational] PtrRep
815
816 mkWeakPrimTy :: Type -> Type
817 mkWeakPrimTy v = TyConApp weakPrimTyCon [v]
818
819 {-
820 ************************************************************************
821 * *
822 \subsection[TysPrim-thread-ids]{The ``thread id'' type}
823 * *
824 ************************************************************************
825
826 A thread id is represented by a pointer to the TSO itself, to ensure
827 that they are always unique and we can always find the TSO for a given
828 thread id. However, this has the unfortunate consequence that a
829 ThreadId# for a given thread is treated as a root by the garbage
830 collector and can keep TSOs around for too long.
831
832 Hence the programmer API for thread manipulation uses a weak pointer
833 to the thread id internally.
834 -}
835
836 threadIdPrimTy :: Type
837 threadIdPrimTy = mkTyConTy threadIdPrimTyCon
838 threadIdPrimTyCon :: TyCon
839 threadIdPrimTyCon = pcPrimTyCon0 threadIdPrimTyConName PtrRep
840
841 {-
842 ************************************************************************
843 * *
844 Any
845 * *
846 ************************************************************************
847
848 Note [Any types]
849 ~~~~~~~~~~~~~~~~
850 The type constructor Any of kind forall k. k has these properties:
851
852 * It is defined in module GHC.Prim, and exported so that it is
853 available to users. For this reason it's treated like any other
854 primitive type:
855 - has a fixed unique, anyTyConKey,
856 - lives in the global name cache
857
858 * It is a *closed* type family, with no instances. This means that
859 if ty :: '(k1, k2) we add a given coercion
860 g :: ty ~ (Fst ty, Snd ty)
861 If Any was a *data* type, then we'd get inconsistency because 'ty'
862 could be (Any '(k1,k2)) and then we'd have an equality with Any on
863 one side and '(,) on the other. See also #9097.
864
865 * It is lifted, and hence represented by a pointer
866
867 * It is inhabited by at least one value, namely bottom
868
869 * You can unsafely coerce any lifted type to Any, and back.
870
871 * It does not claim to be a *data* type, and that's important for
872 the code generator, because the code gen may *enter* a data value
873 but never enters a function value.
874
875 * It is used to instantiate otherwise un-constrained type variables
876 For example length Any []
877 See Note [Strangely-kinded void TyCons]
878
879 Note [Strangely-kinded void TyCons]
880 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
881 See Trac #959 for more examples
882
883 When the type checker finds a type variable with no binding, which
884 means it can be instantiated with an arbitrary type, it usually
885 instantiates it to Void. Eg.
886
887 length []
888 ===>
889 length Any (Nil Any)
890
891 But in really obscure programs, the type variable might have a kind
892 other than *, so we need to invent a suitably-kinded type.
893
894 This commit uses
895 Any for kind *
896 Any(*->*) for kind *->*
897 etc
898 -}
899
900 anyTyConName :: Name
901 anyTyConName = mkPrimTc (fsLit "Any") anyTyConKey anyTyCon
902
903 anyTy :: Type
904 anyTy = mkTyConTy anyTyCon
905
906 anyTyCon :: TyCon
907 anyTyCon = mkFamilyTyCon anyTyConName kind [kKiVar] Nothing
908 (ClosedSynFamilyTyCon Nothing)
909 Nothing
910 NotInjective
911 where
912 kind = ForAllTy (Named kKiVar Invisible) (mkTyVarTy kKiVar)
913
914 anyTypeOfKind :: Kind -> Type
915 anyTypeOfKind kind = TyConApp anyTyCon [kind]
916
917 {-
918 ************************************************************************
919 * *
920 \subsection{SIMD vector types}
921 * *
922 ************************************************************************
923 -}
924
925 #include "primop-vector-tys.hs-incl"