TypeRep.lhs 18.3 KB
Newer Older
1
2
3
4
5
6
7
%
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%
\section[TypeRep]{Type - friends' interface}

\begin{code}
module TypeRep (
8
	TyThing(..), 
9
	Type(..), TyNote(..), 		-- Representation visible 
10
	PredType(..),	 		-- to friends
11
	
12
 	Kind, ThetaType,		-- Synonyms
13

14
15
	funTyCon,

16
	-- Pretty-printing
17
	pprType, pprParendType, pprTyThingCategory,
18
19
	pprPred, pprTheta, pprThetaArrow, pprClassPred,

20
	-- Kinds
21
	liftedTypeKind, unliftedTypeKind, openTypeKind,
22
23
        argTypeKind, ubxTupleKind,
	isLiftedTypeKindCon, isLiftedTypeKind,
24
	mkArrowKind, mkArrowKinds,
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

        -- Kind constructors...
        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
        argTypeKindTyCon, ubxTupleKindTyCon,

        -- And their names
        unliftedTypeKindTyConName, openTypeKindTyConName,
        ubxTupleKindTyConName, argTypeKindTyConName,
        liftedTypeKindTyConName,

        -- Super Kinds
	tySuperKind, coSuperKind,
        isTySuperKind, isCoSuperKind,
	tySuperKindTyCon, coSuperKindTyCon,
        
        isCoercionKindTyCon,

42
	pprKind, pprParendKind
43
44
45
46
    ) where

#include "HsVersions.h"

47
import {-# SOURCE #-} DataCon( DataCon, dataConName )
48
import Monad 	  ( guard )
49
-- friends:
50

51
import Var	  ( Var, Id, TyVar, tyVarKind )
52
import VarSet     ( TyVarSet )
53
import Name	  ( Name, NamedThing(..), BuiltInSyntax(..), mkWiredInName )
54
import OccName	  ( mkOccNameFS, tcName, parenSymOcc )
55
import BasicTypes ( IPName, tupleParens )
56
import TyCon	  ( TyCon, mkFunTyCon, tyConArity, tupleTyConBoxity, isTupleTyCon, isRecursiveTyCon, isNewTyCon, mkVoidPrimTyCon, mkSuperKindTyCon, isSuperKindTyCon, mkCoercionTyCon )
57
import Class	  ( Class )
58
59

-- others
60
61
62
63
64
import PrelNames  ( gHC_PRIM, funTyConKey, tySuperKindTyConKey, 
                    coSuperKindTyConKey, liftedTypeKindTyConKey,
                    openTypeKindTyConKey, unliftedTypeKindTyConKey,
                    ubxTupleKindTyConKey, argTypeKindTyConKey, listTyConKey, 
                    parrTyConKey, hasKey, eqCoercionKindTyConKey )
65
import Outputable
66
67
68
69
70
71
72
73
74
75
76
\end{code}

%************************************************************************
%*									*
\subsection{Type Classifications}
%*									*
%************************************************************************

A type is

	*unboxed*	iff its representation is other than a pointer
77
			Unboxed types are also unlifted.
78
79
80
81
82
83

	*lifted*	A type is lifted iff it has bottom as an element.
			Closures always have lifted types:  i.e. any
			let-bound identifier in Core must have a lifted
			type.  Operationally, a lifted object is one that
			can be entered.
84
85

			Only lifted types may be unified with a type variable.
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

	*algebraic*	A type with one or more constructors, whether declared
			with "data" or "newtype".   
			An algebraic type is one that can be deconstructed
			with a case expression.  
			*NOT* the same as lifted types,  because we also 
			include unboxed tuples in this classification.

	*data*		A type declared with "data".  Also boxed tuples.

	*primitive*	iff it is a built-in type that can't be expressed
			in Haskell.

Currently, all primitive types are unlifted, but that's not necessarily
the case.  (E.g. Int could be primitive.)

Some primitive types are unboxed, such as Int#, whereas some are boxed
but unlifted (such as ByteArray#).  The only primitive types that we
classify as algebraic are the unboxed tuples.

examples of type classifications:

Type		primitive	boxed		lifted		algebraic    
-----------------------------------------------------------------------------
Int#,		Yes		No		No		No
ByteArray#	Yes		Yes		No		No
(# a, b #)	Yes		No		No		Yes
(  a, b  )	No		Yes		Yes		Yes
[a]		No		Yes		Yes		Yes

116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136


	----------------------
	A note about newtypes
	----------------------

Consider
	newtype N = MkN Int

Then we want N to be represented as an Int, and that's what we arrange.
The front end of the compiler [TcType.lhs] treats N as opaque, 
the back end treats it as transparent [Type.lhs].

There's a bit of a problem with recursive newtypes
	newtype P = MkP P
	newtype Q = MkQ (Q->Q)

Here the 'implicit expansion' we get from treating P and Q as transparent
would give rise to infinite types, which in turn makes eqType diverge.
Similarly splitForAllTys and splitFunTys can get into a loop.  

137
138
Solution: 

139
* Newtypes are always represented using TyConApp.
140

141
142
143
144
145
* For non-recursive newtypes, P, treat P just like a type synonym after 
  type-checking is done; i.e. it's opaque during type checking (functions
  from TcType) but transparent afterwards (functions from Type).  
  "Treat P as a type synonym" means "all functions expand NewTcApps 
  on the fly".
146

147
148
149
  Applications of the data constructor P simply vanish:
	P x = x
  
150

151
152
153
154
155
* For recursive newtypes Q, treat the Q and its representation as 
  distinct right through the compiler.  Applications of the data consructor
  use a coerce:
	Q = \(x::Q->Q). coerce Q x
  They are rare, so who cares if they are a tiny bit less efficient.
156

157
158
The typechecker (TcTyDecls) identifies enough type construtors as 'recursive'
to cut all loops.  The other members of the loop may be marked 'non-recursive'.
159
160


161
162
163
164
165
166
167
168
169
%************************************************************************
%*									*
\subsection{The data type}
%*									*
%************************************************************************


\begin{code}
data Type
170
  = TyVarTy TyVar	
171
172

  | AppTy
173
	Type		-- Function is *not* a TyConApp
174
175
	Type		-- It must be another AppTy, or TyVarTy
			-- (or NoteTy of these)
176

177
  | TyConApp		-- Application of a TyCon, including newtypes *and* synonyms
178
	TyCon		--  *Invariant* saturated appliations of FunTyCon and
179
			-- 	synonyms have their own constructors, below.
180
181
			-- However, *unsaturated* FunTyCons do appear as TyConApps.  
			-- 
182
	[Type]		-- Might not be saturated.
183
184
185
			-- Even type synonyms are not necessarily saturated;
			-- for example unsaturated type synonyms can appear as the 
			-- RHS of a type synonym.
186

187
  | FunTy		-- Special case of TyConApp: TyConApp FunTyCon [t1,t2]
188
189
190
	Type
	Type

191
192
193
194
  | ForAllTy		-- A polymorphic type
	TyVar
	Type	

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
195
  | PredTy		-- The type of evidence for a type predictate
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
196
	PredType	-- See Note [PredTy], and Note [Equality predicates]
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
197
198
199
	-- NB: A PredTy (EqPred _ _) can appear only as the kind
	--     of a coercion variable; never as the argument or result
	--     of a FunTy (unlike ClassP, IParam)
200
201

  | NoteTy 		-- A type with a note attached
202
203
204
	TyNote
	Type		-- The expanded version

205
206
207
208
209
210
211
212
213
214
215
216
217
type Kind = Type 	-- Invariant: a kind is always
			--	FunTy k1 k2
			-- or	TyConApp PrimTyCon [...]
			-- or	TyVar kv (during inference only)
			-- or   ForAll ... (for top-level coercions)

type SuperKind = Type   -- Invariant: a super kind is always 
                        --   TyConApp SuperKindTyCon ...

type Coercion = Type

type CoercionKind = Kind

218
data TyNote = FTVNote TyVarSet	-- The free type variables of the noted expression
219
220
221
\end{code}

-------------------------------------
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
222
 		Note [PredTy]
223
224

A type of the form
225
226
227
	PredTy p
represents a value whose type is the Haskell predicate p, 
where a predicate is what occurs before the '=>' in a Haskell type.
228
229
230
231
232
It can be expanded into its representation, but: 

	* The type checker must treat it as opaque
	* The rest of the compiler treats it as transparent

233
234
235
236
237
238
239
240
241
Consider these examples:
	f :: (Eq a) => a -> Int
	g :: (?x :: Int -> Int) => a -> Int
	h :: (r\l) => {r} => {l::Int | r}

Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates*
Predicates are represented inside GHC by PredType:

\begin{code}
242
data PredType 
243
244
  = ClassP Class [Type]		-- Class predicate
  | IParam (IPName Name) Type	-- Implicit parameter
245
  | EqPred Type Type		-- Equality predicate (ty1 :=: ty2)
246

247
type ThetaType = [PredType]
248
249
\end{code}

250
251
252
253
254
255
256
257
258
259
260
261
(We don't support TREX records yet, but the setup is designed
to expand to allow them.)

A Haskell qualified type, such as that for f,g,h above, is
represented using 
	* a FunTy for the double arrow
	* with a PredTy as the function argument

The predicate really does turn into a real extra argument to the
function.  If the argument has type (PredTy p) then the predicate p is
represented by evidence (a dictionary, for example, of type (predRepTy p).

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
Note [Equality predicates]
~~~~~~~~~~~~~~~~~~~~~~~~~~
	forall a b. (a :=: S b) => a -> b
could be represented by
	ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
OR
	ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))

The latter is what we do.  (Unlike for class and implicit parameter
constraints, which do use FunTy.)

Reason:
	* FunTy is always a *value* function
	* ForAllTy is discarded at runtime

We often need to make a "wildcard" (c::PredTy..).  We always use the same
name (wildCoVarName), since it's not mentioned.

280

281
282
283
284
285
286
287
288
289
%************************************************************************
%*									*
			TyThing
%*									*
%************************************************************************

Despite the fact that DataCon has to be imported via a hi-boot route, 
this module seems the right place for TyThing, because it's needed for
funTyCon and all the types in TysPrim.
290
291

\begin{code}
292
293
294
295
data TyThing = AnId     Id
	     | ADataCon DataCon
	     | ATyCon   TyCon
	     | AClass   Class
296
297

instance Outputable TyThing where
298
299
300
301
302
303
304
  ppr thing = pprTyThingCategory thing <+> quotes (ppr (getName thing))

pprTyThingCategory :: TyThing -> SDoc
pprTyThingCategory (ATyCon _) 	= ptext SLIT("Type constructor")
pprTyThingCategory (AClass _)   = ptext SLIT("Class")
pprTyThingCategory (AnId   _)   = ptext SLIT("Identifier")
pprTyThingCategory (ADataCon _) = ptext SLIT("Data constructor")
305
306
307
308
309
310

instance NamedThing TyThing where	-- Can't put this with the type
  getName (AnId id)     = getName id	-- decl, because the DataCon instance
  getName (ATyCon tc)   = getName tc	-- isn't visible there
  getName (AClass cl)   = getName cl
  getName (ADataCon dc) = dataConName dc
311
\end{code}
312

313

314
315
%************************************************************************
%*									*
316
		Wired-in type constructors
317
318
319
320
321
322
%*									*
%************************************************************************

We define a few wired-in type constructors here to avoid module knots

\begin{code}
323
324
325
--------------------------
-- First the TyCons...

326
327
funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
	-- You might think that (->) should have type (?? -> ? -> *), and you'd be right
328
329
330
331
332
333
	-- But if we do that we get kind errors when saying
	--	instance Control.Arrow (->)
	-- becuase the expected kind is (*->*->*).  The trouble is that the
	-- expected/actual stuff in the unifier does not go contra-variant, whereas
	-- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
	-- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
334

335
336

tySuperKindTyCon     = mkSuperKindTyCon tySuperKindTyConName
337
coSuperKindTyCon     = mkSuperKindTyCon coSuperKindTyConName
338
339
340
341
342
343
344
345
346
347

liftedTypeKindTyCon   = mkKindTyCon liftedTypeKindTyConName
openTypeKindTyCon     = mkKindTyCon openTypeKindTyConName
unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName
ubxTupleKindTyCon     = mkKindTyCon ubxTupleKindTyConName
argTypeKindTyCon      = mkKindTyCon argTypeKindTyConName
eqCoercionKindTyCon = 
  mkCoercionTyCon eqCoercionKindTyConName 2 (\ _ -> coSuperKind)

mkKindTyCon :: Name -> TyCon
348
mkKindTyCon name = mkVoidPrimTyCon name tySuperKind 0
349
350
351
352

--------------------------
-- ... and now their names

353
354
tySuperKindTyConName      = mkPrimTyConName FSLIT("BOX") tySuperKindTyConKey tySuperKindTyCon
coSuperKindTyConName      = mkPrimTyConName FSLIT("COERCION") coSuperKindTyConKey coSuperKindTyCon
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
liftedTypeKindTyConName   = mkPrimTyConName FSLIT("*") liftedTypeKindTyConKey liftedTypeKindTyCon
openTypeKindTyConName     = mkPrimTyConName FSLIT("?") openTypeKindTyConKey openTypeKindTyCon
unliftedTypeKindTyConName = mkPrimTyConName FSLIT("#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
ubxTupleKindTyConName     = mkPrimTyConName FSLIT("(##)") ubxTupleKindTyConKey ubxTupleKindTyCon
argTypeKindTyConName      = mkPrimTyConName FSLIT("??") argTypeKindTyConKey argTypeKindTyCon
funTyConName              = mkPrimTyConName FSLIT("(->)") funTyConKey funTyCon

eqCoercionKindTyConName   = mkWiredInName gHC_PRIM (mkOccNameFS tcName (FSLIT(":=:"))) 
					eqCoercionKindTyConKey Nothing (ATyCon eqCoercionKindTyCon) 
					BuiltInSyntax
 
mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkOccNameFS tcName occ) 
					      key 
					      Nothing 		-- No parent object
					      (ATyCon tycon)
					      BuiltInSyntax
	-- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
	-- because they are never in scope in the source

------------------
-- We also need Kinds and SuperKinds, locally and in TyCon

kindTyConType :: TyCon -> Type
kindTyConType kind = TyConApp kind []

liftedTypeKind   = kindTyConType liftedTypeKindTyCon
unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
openTypeKind     = kindTyConType openTypeKindTyCon
argTypeKind      = kindTyConType argTypeKindTyCon
ubxTupleKind	 = kindTyConType ubxTupleKindTyCon

mkArrowKind :: Kind -> Kind -> Kind
mkArrowKind k1 k2 = FunTy k1 k2

mkArrowKinds :: [Kind] -> Kind -> Kind
mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds

tySuperKind, coSuperKind :: SuperKind
tySuperKind = kindTyConType tySuperKindTyCon 
coSuperKind = kindTyConType coSuperKindTyCon 

396
isTySuperKind (NoteTy _ ty)    = isTySuperKind ty
397
398
399
isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
isTySuperKind other            = False

400
isCoSuperKind :: SuperKind -> Bool
401
isCoSuperKind (NoteTy _ ty)    = isCoSuperKind ty
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
isCoSuperKind other            = False

isCoercionKindTyCon kc = kc `hasKey` eqCoercionKindTyConKey


-------------------
-- lastly we need a few functions on Kinds

isLiftedTypeKindCon tc    = tc `hasKey` liftedTypeKindTyConKey

isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
isLiftedTypeKind other            = False


417
418
419
\end{code}


420

421
422
%************************************************************************
%*									*
423
\subsection{The external interface}
424
425
426
%*									*
%************************************************************************

427
428
429
430
431
@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
defined to use this.  @pprParendType@ is the same, except it puts
parens around the type, except for the atomic cases.  @pprParendType@
works just by setting the initial context precedence very high.

432
\begin{code}
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
data Prec = TopPrec 	-- No parens
	  | FunPrec 	-- Function args; no parens for tycon apps
	  | TyConPrec 	-- Tycon args; no parens for atomic
	  deriving( Eq, Ord )

maybeParen :: Prec -> Prec -> SDoc -> SDoc
maybeParen ctxt_prec inner_prec pretty
  | ctxt_prec < inner_prec = pretty
  | otherwise		   = parens pretty

------------------
pprType, pprParendType :: Type -> SDoc
pprType       ty = ppr_type TopPrec   ty
pprParendType ty = ppr_type TyConPrec ty

------------------
pprPred :: PredType -> SDoc
pprPred (ClassP cls tys) = pprClassPred cls tys
pprPred (IParam ip ty)   = ppr ip <> dcolon <> pprType ty
452
pprPred (EqPred ty1 ty2) = sep [ppr ty1, nest 2 (ptext SLIT(":=:")), ppr ty2]
453
454

pprClassPred :: Class -> [Type] -> SDoc
455
456
pprClassPred clas tys = parenSymOcc (getOccName clas) (ppr clas) 
			<+> sep (map pprParendType tys)
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478

pprTheta :: ThetaType -> SDoc
pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))

pprThetaArrow :: ThetaType -> SDoc
pprThetaArrow theta 
  | null theta = empty
  | otherwise  = parens (sep (punctuate comma (map pprPred theta))) <+> ptext SLIT("=>")

------------------
instance Outputable Type where
    ppr ty = pprType ty

instance Outputable PredType where
    ppr = pprPred

instance Outputable name => OutputableBndr (IPName name) where
    pprBndr _ n = ppr n	-- Simple for now

------------------
	-- OK, here's the main printer

479
480
481
pprKind = pprType
pprParendKind = pprParendType

482
ppr_type :: Prec -> Type -> SDoc
483
484
485
486
ppr_type p (TyVarTy tv)       = ppr tv
ppr_type p (PredTy pred)      = braces (ppr pred)
ppr_type p (NoteTy other ty2) = ppr_type p ty2
ppr_type p (TyConApp tc tys)  = ppr_tc_app p tc tys
487
488
489
490

ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
			   pprType t1 <+> ppr_type TyConPrec t2

491
492
493
ppr_type p ty@(ForAllTy _ _)       = ppr_forall_type p ty
ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty

494
495
496
497
498
499
500
501
ppr_type p (FunTy ty1 ty2)
  = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
    maybeParen p FunPrec $
    sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
  where
    ppr_fun_tail (FunTy ty1 ty2) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
    ppr_fun_tail other_ty        = [arrow <+> pprType other_ty]

502
503
ppr_forall_type :: Prec -> Type -> SDoc
ppr_forall_type p ty
504
505
506
507
508
509
  = maybeParen p FunPrec $
    sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
  where
    (tvs,  rho) = split1 [] ty
    (ctxt, tau) = split2 [] rho

510
511
512
    split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
    split1 tvs (NoteTy _ ty)    = split1 tvs ty
    split1 tvs ty		= (reverse tvs, ty)
513
 
514
    split2 ps (NoteTy _ arg 	-- Rather a disgusting case
515
	       `FunTy` res) 	      = split2 ps (arg `FunTy` res)
516
    split2 ps (PredTy p `FunTy` ty)   = split2 (p:ps) ty
517
    split2 ps (NoteTy _ ty) 	      = split2 ps ty
518
    split2 ps ty		      = (reverse ps, ty)
519
520

ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
521
ppr_tc_app p tc [] 
522
  = ppr_tc tc
523
524
525
ppr_tc_app p tc [ty] 
  | tc `hasKey` listTyConKey = brackets (pprType ty)
  | tc `hasKey` parrTyConKey = ptext SLIT("[:") <> pprType ty <> ptext SLIT(":]")
526
527
528
529
530
531
  | tc `hasKey` liftedTypeKindTyConKey   = ptext SLIT("*")
  | tc `hasKey` unliftedTypeKindTyConKey = ptext SLIT("#")
  | tc `hasKey` openTypeKindTyConKey     = ptext SLIT("(?)")
  | tc `hasKey` ubxTupleKindTyConKey     = ptext SLIT("(#)")
  | tc `hasKey` argTypeKindTyConKey      = ptext SLIT("??")

532
533
534
535
536
ppr_tc_app p tc tys
  | isTupleTyCon tc && tyConArity tc == length tys
  = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
  | otherwise
  = maybeParen p TyConPrec $
537
538
539
    ppr_tc tc <+> sep (map (ppr_type TyConPrec) tys)

ppr_tc :: TyCon -> SDoc
540
541
542
543
544
545
546
ppr_tc tc = parenSymOcc (getOccName tc) (pp_nt_debug <> ppr tc)
  where
   pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc 
				             then ptext SLIT("<recnt>")
					     else ptext SLIT("<nt>"))
	       | otherwise     = empty

547
-------------------
548
pprForAll []  = empty
549
550
551
552
553
554
555
556
pprForAll tvs = ptext SLIT("forall") <+> sep (map pprTvBndr tvs) <> dot

pprTvBndr tv | isLiftedTypeKind kind = ppr tv
	     | otherwise	     = parens (ppr tv <+> dcolon <+> pprKind kind)
	     where
	       kind = tyVarKind tv
\end{code}