Type.lhs 51.2 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
4
5
% (c) The GRASP/AQUA Project, Glasgow University, 1998
%

6
Type - public interface
7

8
9
\begin{code}
module Type (
10
        -- re-exports from TypeRep
11
	TyThing(..), Type, PredType(..), ThetaType, 
12
	funTyCon,
13

14
15
	-- Kinds
        Kind, SimpleKind, KindVar,
16
        kindFunResult, splitKindFunTys, splitKindFunTysN,
17
18
19
20
21
22
23
24
25
26
27

        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
        argTypeKindTyCon, ubxTupleKindTyCon,

        liftedTypeKind, unliftedTypeKind, openTypeKind,
        argTypeKind, ubxTupleKind,

        tySuperKind, coSuperKind, 

        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
        isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
28
        isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
29
30
31
32
	mkArrowKind, mkArrowKinds,

        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
        isSubKindCon,
33

34
35
	-- Re-exports from TyCon
	PrimRep(..),
36

37
38
	mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,

39
40
	mkAppTy, mkAppTys, splitAppTy, splitAppTys, 
	splitAppTy_maybe, repSplitAppTy_maybe,
41

42
43
	mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
	splitFunTys, splitFunTysN,
44
	funResultTy, funArgTy, zipFunTys, isFunTy,
45

46
	mkTyConApp, mkTyConTy, 
47
	tyConAppTyCon, tyConAppArgs, 
48
49
	splitTyConApp_maybe, splitTyConApp, 
        splitNewTyConApp_maybe, splitNewTyConApp,
50

mnislaih's avatar
mnislaih committed
51
	repType, repType', typePrimRep, coreView, tcView, kindView,
52

53
	mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
54
	applyTy, applyTys, isForAllTy, dropForAlls,
55

56
	-- Source types
57
	predTypeRep, mkPredTy, mkPredTys,
58

59
	-- Newtypes
60
	splitRecNewType_maybe, newTyConInstRhs,
61

62
	-- Lifting and boxity
63
64
	isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
	isStrictType, isStrictPred, 
65

66
	-- Free variables
67
	tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
68
	typeKind, addFreeTyVars,
69

70
	-- Tidying up for printing
71
72
73
74
75
	tidyType,      tidyTypes,
	tidyOpenType,  tidyOpenTypes,
	tidyTyVarBndr, tidyFreeTyVars,
	tidyOpenTyVar, tidyOpenTyVars,
	tidyTopType,   tidyPred,
76
	tidyKind,
77

78
	-- Comparison
79
80
	coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
	tcEqPred, tcCmpPred, tcEqTypeX, 
81

82
	-- Seq
83
	seqType, seqTypes,
84

85
	-- Type substitutions
86
87
	TvSubstEnv, emptyTvSubstEnv,	-- Representation widely visible
	TvSubst(..), emptyTvSubst,	-- Representation visible to a few friends
88
	mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
89
	getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
90
 	extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
91
92

	-- Performing substitution on types
93
	substTy, substTys, substTyWith, substTheta, 
94
	substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
95

96
	-- Pretty-printing
97
	pprType, pprParendType, pprTyThingCategory, pprForAll,
98
	pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
99
    ) where
100

101
102
#include "HsVersions.h"

103
104
105
106
107
-- We import the representation and primitive functions from TypeRep.
-- Many things are reexported, but not the representation!

import TypeRep

108
-- friends:
109
import Var
110
111
112
import VarEnv
import VarSet

113
114
115
116
import Name
import Class
import PrelNames
import TyCon
117

118
-- others
119
120
import StaticFlags
import Util
121
import Outputable
122
import UniqSet
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
123

124
import Data.Maybe	( isJust )
125
126
\end{code}

127

128
129
130
131
132
133
134
135
136
137
138
%************************************************************************
%*									*
		Type representation
%*									*
%************************************************************************

In Core, we "look through" non-recursive newtypes and PredTypes.

\begin{code}
{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
139
-- Strips off the *top layer only* of a type to give 
140
141
142
-- its underlying representation type. 
-- Returns Nothing if there is nothing to look through.
--
143
-- In the case of newtypes, it returns
144
145
146
147
148
149
150
151
152
153
154
155
--	*either* a vanilla TyConApp (recursive newtype, or non-saturated)
--	*or*     the newtype representation (otherwise), meaning the
--			type written in the RHS of the newtype decl,
--			which may itself be a newtype
--
-- Example: newtype R = MkR S
--	    newtype S = MkS T
--	    newtype T = MkT (T -> T)
--   expandNewTcApp on R gives Just S
--	            on S gives Just T
--		    on T gives Nothing	 (no expansion)

156
157
158
-- By being non-recursive and inlined, this case analysis gets efficiently
-- joined onto the case analysis that the caller is already doing
coreView (NoteTy _ ty) 	   = Just ty
159
160
161
coreView (PredTy p)
  | isEqPred p             = Nothing
  | otherwise    	   = Just (predTypeRep p)
162
163
164
165
166
167
168
coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
			   = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
				-- Its important to use mkAppTys, rather than (foldl AppTy),
				-- because the function part might well return a 
				-- partially-applied type constructor; indeed, usually will!
coreView ty		   = Nothing

169
170


171
172
173
174
175
176
177
178
-----------------------------------------------
{-# INLINE tcView #-}
tcView :: Type -> Maybe Type
-- Same, but for the type checker, which just looks through synonyms
tcView (NoteTy _ ty) 	 = Just ty
tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
			 = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
tcView ty		 = Nothing
179
180
181
182
183
184
185
186

-----------------------------------------------
{-# INLINE kindView #-}
kindView :: Kind -> Maybe Kind
-- C.f. coreView, tcView
-- For the moment, we don't even handle synonyms in kinds
kindView (NoteTy _ k) = Just k
kindView other	      = Nothing
187
188
189
\end{code}


190
191
192
193
194
%************************************************************************
%*									*
\subsection{Constructor-specific functions}
%*									*
%************************************************************************
sof's avatar
sof committed
195
196


197
198
199
---------------------------------------------------------------------
				TyVarTy
				~~~~~~~
200
\begin{code}
201
mkTyVarTy  :: TyVar   -> Type
202
mkTyVarTy  = TyVarTy
203

204
mkTyVarTys :: [TyVar] -> [Type]
205
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
206

207
getTyVar :: String -> Type -> TyVar
208
209
210
getTyVar msg ty = case getTyVar_maybe ty of
		    Just tv -> tv
		    Nothing -> panic ("getTyVar: " ++ msg)
211

212
isTyVarTy :: Type -> Bool
213
214
215
isTyVarTy ty = isJust (getTyVar_maybe ty)

getTyVar_maybe :: Type -> Maybe TyVar
216
217
218
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) 	 	    = Just tv  
getTyVar_maybe other	         	    = Nothing
219

220
221
222
\end{code}


223
224
225
226
227
228
---------------------------------------------------------------------
				AppTy
				~~~~~
We need to be pretty careful with AppTy to make sure we obey the 
invariant that a TyConApp is always visibly so.  mkAppTy maintains the
invariant: use it.
229

230
\begin{code}
231
mkAppTy orig_ty1 orig_ty2
232
  = mk_app orig_ty1
233
  where
234
    mk_app (NoteTy _ ty1)    = mk_app ty1
235
    mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
236
    mk_app ty1		     = AppTy orig_ty1 orig_ty2
237
	-- Note that the TyConApp could be an 
238
239
240
241
242
243
244
	-- under-saturated type synonym.  GHC allows that; e.g.
	--	type Foo k = k a -> k a
	--	type Id x = x
	--	foo :: Foo Id -> Foo Id
	--
	-- Here Id is partially applied in the type sig for Foo,
	-- but once the type synonyms are expanded all is well
245

246
mkAppTys :: Type -> [Type] -> Type
247
248
mkAppTys orig_ty1 []	    = orig_ty1
	-- This check for an empty list of type arguments
249
	-- avoids the needless loss of a type synonym constructor.
250
251
252
	-- For example: mkAppTys Rational []
	--   returns to (Ratio Integer), which has needlessly lost
	--   the Rational part.
253
mkAppTys orig_ty1 orig_tys2
254
  = mk_app orig_ty1
255
  where
256
    mk_app (NoteTy _ ty1)    = mk_app ty1
257
258
    mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
				-- mkTyConApp: see notes with mkAppTy
259
    mk_app ty1		     = foldl AppTy orig_ty1 orig_tys2
260

261
-------------
262
splitAppTy_maybe :: Type -> Maybe (Type, Type)
263
264
265
splitAppTy_maybe ty | Just ty' <- coreView ty
		    = splitAppTy_maybe ty'
splitAppTy_maybe ty = repSplitAppTy_maybe ty
266

267
268
269
270
271
272
273
274
275
276
-------------
repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
-- Does the AppTy split, but assumes that any view stuff is already done
repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
						Just (tys', ty') -> Just (TyConApp tc tys', ty')
						Nothing		 -> Nothing
repSplitAppTy_maybe other = Nothing
-------------
277
splitAppTy :: Type -> (Type, Type)
278
279
280
splitAppTy ty = case splitAppTy_maybe ty of
			Just pr -> pr
			Nothing -> panic "splitAppTy"
281

282
-------------
283
splitAppTys :: Type -> (Type, [Type])
284
splitAppTys ty = split ty ty []
285
  where
286
    split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
287
    split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
288
    split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
289
    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
290
					       (TyConApp funTyCon [], [ty1,ty2])
291
    split orig_ty ty		        args = (orig_ty, args)
292

293
294
\end{code}

295
296
297
298
299

---------------------------------------------------------------------
				FunTy
				~~~~~

300
\begin{code}
301
mkFunTy :: Type -> Type -> Type
302
mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
303
mkFunTy arg res = FunTy arg res
304

305
mkFunTys :: [Type] -> Type -> Type
306
mkFunTys tys ty = foldr mkFunTy ty tys
307

308
309
310
isFunTy :: Type -> Bool 
isFunTy ty = isJust (splitFunTy_maybe ty)

311
splitFunTy :: Type -> (Type, Type)
312
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
313
splitFunTy (FunTy arg res)   = (arg, res)
314
splitFunTy other	     = pprPanic "splitFunTy" (ppr other)
315

316
splitFunTy_maybe :: Type -> Maybe (Type, Type)
317
splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
318
319
splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
splitFunTy_maybe other	           = Nothing
320

321
splitFunTys :: Type -> ([Type], Type)
322
splitFunTys ty = split [] ty ty
323
  where
324
    split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
325
326
    split args orig_ty (FunTy arg res) 	 = split (arg:args) res res
    split args orig_ty ty                = (reverse args, orig_ty)
327

328
329
330
331
332
333
334
splitFunTysN :: Int -> Type -> ([Type], Type)
-- Split off exactly n arg tys
splitFunTysN 0 ty = ([], ty)
splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
		    case splitFunTysN (n-1) res of { (args, res) ->
		    (arg:args, res) }}

335
336
337
zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
  where
338
    split acc []     nty ty  	           = (reverse acc, nty)
339
340
    split acc xs     nty ty 
	  | Just ty' <- coreView ty 	   = split acc xs nty ty'
341
    split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
342
    split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
343
344
    
funResultTy :: Type -> Type
345
funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
346
funResultTy (FunTy arg res)   = res
347
funResultTy ty		      = pprPanic "funResultTy" (ppr ty)
348
349

funArgTy :: Type -> Type
350
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
351
funArgTy (FunTy arg res)   = arg
352
funArgTy ty		   = pprPanic "funArgTy" (ppr ty)
353
354
355
\end{code}


356
357
358
---------------------------------------------------------------------
				TyConApp
				~~~~~~~~
359
@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
360
as apppropriate.
361

362
\begin{code}
363
mkTyConApp :: TyCon -> [Type] -> Type
364
mkTyConApp tycon tys
365
  | isFunTyCon tycon, [ty1,ty2] <- tys
366
  = FunTy ty1 ty2
367

368
  | otherwise
369
  = TyConApp tycon tys
370

371
mkTyConTy :: TyCon -> Type
372
mkTyConTy tycon = mkTyConApp tycon []
373
374
375
376
377

-- splitTyConApp "looks through" synonyms, because they don't
-- mean a distinct type, but all other type-constructor applications
-- including functions are returned as Just ..

378
tyConAppTyCon :: Type -> TyCon
379
tyConAppTyCon ty = fst (splitTyConApp ty)
380
381

tyConAppArgs :: Type -> [Type]
382
tyConAppArgs ty = snd (splitTyConApp ty)
383
384
385
386

splitTyConApp :: Type -> (TyCon, [Type])
splitTyConApp ty = case splitTyConApp_maybe ty of
			Just stuff -> stuff
387
			Nothing	   -> pprPanic "splitTyConApp" (ppr ty)
388

389
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
390
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
391
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
392
splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
393
splitTyConApp_maybe other	      = Nothing
394
395
396
397
398
399
400
401
402
403
404
405
406
407

-- Sometimes we do NOT want to look throught a newtype.  When case matching
-- on a newtype we want a convenient way to access the arguments of a newty
-- constructor so as to properly form a coercion.
splitNewTyConApp :: Type -> (TyCon, [Type])
splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
			Just stuff -> stuff
			Nothing	   -> pprPanic "splitNewTyConApp" (ppr ty)
splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
splitNewTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
splitNewTyConApp_maybe other	      = Nothing

408
409
410
411
412
413
-- get instantiated newtype rhs, the arguments had better saturate 
-- the constructor
newTyConInstRhs :: TyCon -> [Type] -> Type
newTyConInstRhs tycon tys =
    let (tvs, ty) = newTyConRhs tycon in substTyWith tvs tys ty

sof's avatar
sof committed
414
\end{code}
415

416

417
418
419
420
421
422
423
424
---------------------------------------------------------------------
				SynTy
				~~~~~

Notes on type synonyms
~~~~~~~~~~~~~~~~~~~~~~
The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
to return type synonyms whereever possible. Thus
425

426
427
428
429
430
431
432
433
	type Foo a = a -> a

we want 
	splitFunTys (a -> Foo a) = ([a], Foo a)
not			           ([a], a -> a)

The reason is that we then get better (shorter) type signatures in 
interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
434
435


436
437
		Representation types
		~~~~~~~~~~~~~~~~~~~~
438
439
repType looks through 
	(a) for-alls, and
440
441
442
	(b) synonyms
	(c) predicates
	(d) usage annotations
443
	(e) all newtypes, including recursive ones, but not newtype families
444
It's useful in the back end.
445
446
447

\begin{code}
repType :: Type -> Type
448
-- Only applied to types of kind *; hence tycons are saturated
449
repType ty | Just ty' <- coreView ty = repType ty'
450
451
repType (ForAllTy _ ty)  = repType ty
repType (TyConApp tc tys)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
452
  | isClosedNewTyCon tc  = -- Recursive newtypes are opaque to coreView
453
454
455
			   -- but we must expand them here.  Sure to
			   -- be saturated because repType is only applied
			   -- to types of kind *
456
			   ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
457
458
459
			   repType (new_type_rep tc tys)
repType ty = ty

mnislaih's avatar
mnislaih committed
460
461
462
463
464
465
466
467
468
469
-- repType' aims to be a more thorough version of repType
-- For now it simply looks through the TyConApp args too
repType' ty -- | pprTrace "repType'" (ppr ty $$ ppr (go1 ty)) False = undefined
            | otherwise = go1 ty 
 where 
        go1 = go . repType
        go (TyConApp tc tys) = mkTyConApp tc (map repType' tys)
        go ty = ty


470
471
472
473
474
-- new_type_rep doesn't ask any questions: 
-- it just expands newtype, whether recursive or not
new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
			     case newTyConRep new_tycon of
				 (tvs, rep_ty) -> substTyWith tvs tys rep_ty
475

476
477
-- ToDo: this could be moved to the code generator, using splitTyConApp instead
-- of inspecting the type directly.
478
479
480
481
typePrimRep :: Type -> PrimRep
typePrimRep ty = case repType ty of
		   TyConApp tc _ -> tyConPrimRep tc
		   FunTy _ _	 -> PtrRep
482
		   AppTy _ _	 -> PtrRep	-- See note below
483
		   TyVarTy _	 -> PtrRep
484
		   other	 -> pprPanic "typePrimRep" (ppr ty)
485
486
487
488
489
	-- Types of the form 'f a' must be of kind *, not *#, so
	-- we are guaranteed that they are represented by pointers.
	-- The reason is that f must have kind *->*, not *->*#, because
	-- (we claim) there is no way to constrain f's kind any other
	-- way.
490

491
492
493
\end{code}


494
495
496
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
497
498

\begin{code}
499
mkForAllTy :: TyVar -> Type -> Type
500
501
mkForAllTy tyvar ty
  = mkForAllTys [tyvar] ty
502

503
mkForAllTys :: [TyVar] -> Type -> Type
504
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
505
506
507
508
509

isForAllTy :: Type -> Bool
isForAllTy (NoteTy _ ty)  = isForAllTy ty
isForAllTy (ForAllTy _ _) = True
isForAllTy other_ty	  = False
510

511
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
512
splitForAllTy_maybe ty = splitFAT_m ty
513
  where
514
515
516
    splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
    splitFAT_m (ForAllTy tyvar ty)	    = Just(tyvar, ty)
    splitFAT_m _			    = Nothing
sof's avatar
sof committed
517

518
splitForAllTys :: Type -> ([TyVar], Type)
519
splitForAllTys ty = split ty ty []
520
   where
521
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
522
523
     split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
     split orig_ty t		     tvs = (reverse tvs, orig_ty)
524
525
526

dropForAlls :: Type -> Type
dropForAlls ty = snd (splitForAllTys ty)
527
528
\end{code}

529
-- (mkPiType now in CoreUtils)
530

531
532
533
534
535
536
537
applyTy, applyTys
~~~~~~~~~~~~~~~~~
Instantiate a for-all type with one or more type arguments.
Used when we have a polymorphic function applied to type args:
	f t1 t2
Then we use (applyTys type-of-f [t1,t2]) to compute the type of
the expression. 
538

539
\begin{code}
540
applyTy :: Type -> Type -> Type
541
542
543
applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
applyTy other		 arg = panic "applyTy"
544

545
applyTys :: Type -> [Type] -> Type
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
-- This function is interesting because 
--	a) the function may have more for-alls than there are args
--	b) less obviously, it may have fewer for-alls
-- For case (b) think of 
--	applyTys (forall a.a) [forall b.b, Int]
-- This really can happen, via dressing up polymorphic types with newtype
-- clothing.  Here's an example:
--	newtype R = R (forall a. a->a)
--	foo = case undefined :: R of
--		R f -> f ()

applyTys orig_fun_ty []      = orig_fun_ty
applyTys orig_fun_ty arg_tys 
  | n_tvs == n_args 	-- The vastly common case
  = substTyWith tvs arg_tys rho_ty
  | n_tvs > n_args 	-- Too many for-alls
  = substTyWith (take n_args tvs) arg_tys 
		(mkForAllTys (drop n_args tvs) rho_ty)
  | otherwise		-- Too many type args
565
  = ASSERT2( n_tvs > 0, ppr orig_fun_ty )	-- Zero case gives infnite loop!
566
567
568
569
570
571
    applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
	     (drop n_tvs arg_tys)
  where
    (tvs, rho_ty) = splitForAllTys orig_fun_ty 
    n_tvs = length tvs
    n_args = length arg_tys     
572
\end{code}
573

574

575
576
%************************************************************************
%*									*
577
\subsection{Source types}
578
579
%*									*
%************************************************************************
580

581
582
A "source type" is a type that is a separate type as far as the type checker is
concerned, but which has low-level representation as far as the back end is concerned.
583

584
Source types are always lifted.
585

586
The key function is predTypeRep which gives the representation of a source type:
587
588

\begin{code}
589
mkPredTy :: PredType -> Type
590
mkPredTy pred = PredTy pred
591
592

mkPredTys :: ThetaType -> [Type]
593
594
595
596
597
mkPredTys preds = map PredTy preds

predTypeRep :: PredType -> Type
-- Convert a PredType to its "representation type";
-- the post-type-checking type used by all the Core passes of GHC.
598
-- Unwraps only the outermost level; for example, the result might
599
-- be a newtype application
600
601
predTypeRep (IParam _ ty)     = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
602
	-- Result might be a newtype application, but the consumer will
603
	-- look through that too if necessary
604
predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
605
\end{code}
606
607


608
609
610
611
612
%************************************************************************
%*									*
		NewTypes
%*									*
%************************************************************************
613

614
615
616
\begin{code}
splitRecNewType_maybe :: Type -> Maybe Type
-- Sometimes we want to look through a recursive newtype, and that's what happens here
617
-- It only strips *one layer* off, so the caller will usually call itself recursively
618
-- Only applied to types of kind *, hence the newtype is always saturated
619
620
splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
splitRecNewType_maybe (TyConApp tc tys)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
621
  | isClosedNewTyCon tc
622
623
624
625
  = ASSERT( tys `lengthIs` tyConArity tc )	-- splitRecNewType_maybe only be applied 
						-- 	to *types* (of kind *)
    ASSERT( isRecursiveTyCon tc ) 		-- Guaranteed by coreView
    case newTyConRhs tc of
626
627
628
	(tvs, rep_ty) -> ASSERT( length tvs == length tys )
			 Just (substTyWith tvs tys rep_ty)
	
629
splitRecNewType_maybe other = Nothing
630
631
632



633
634
\end{code}

635

636
637
638
639
640
641
642
643
644
%************************************************************************
%*									*
\subsection{Kinds and free variables}
%*									*
%************************************************************************

---------------------------------------------------------------------
		Finding the kind of a type
		~~~~~~~~~~~~~~~~~~~~~~~~~~
645
\begin{code}
646
typeKind :: Type -> Kind
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
				   -- We should be looking for the coercion kind,
				   -- not the type kind
				foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
typeKind (NoteTy _ ty)	      = typeKind ty
typeKind (PredTy pred)	      = predKind pred
typeKind (AppTy fun arg)      = kindFunResult (typeKind fun)
typeKind (ForAllTy tv ty)     = typeKind ty
typeKind (TyVarTy tyvar)      = tyVarKind tyvar
typeKind (FunTy arg res)
    -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
    --              not unliftedTypKind (#)
    -- The only things that can be after a function arrow are
    --   (a) types (of kind openTypeKind or its sub-kinds)
    --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
    | isTySuperKind k         = k
    | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
    where
      k = typeKind res

predKind :: PredType -> Kind
predKind (EqPred {}) = coSuperKind	-- A coercion kind!
predKind (ClassP {}) = liftedTypeKind	-- Class and implicitPredicates are
predKind (IParam {}) = liftedTypeKind 	-- always represented by lifted types
671
672
673
\end{code}


674
675
676
---------------------------------------------------------------------
		Free variables of a type
		~~~~~~~~~~~~~~~~~~~~~~~~
677
\begin{code}
678
tyVarsOfType :: Type -> TyVarSet
679
-- NB: for type synonyms tyVarsOfType does *not* expand the synonym
680
tyVarsOfType (TyVarTy tv)		= unitVarSet tv
681
tyVarsOfType (TyConApp tycon tys)	= tyVarsOfTypes tys
682
tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
683
tyVarsOfType (PredTy sty)		= tyVarsOfPred sty
684
685
tyVarsOfType (FunTy arg res)		= tyVarsOfType arg `unionVarSet` tyVarsOfType res
tyVarsOfType (AppTy fun arg)		= tyVarsOfType fun `unionVarSet` tyVarsOfType arg
686
tyVarsOfType (ForAllTy tyvar ty)	= delVarSet (tyVarsOfType ty) tyvar
687

688
tyVarsOfTypes :: [Type] -> TyVarSet
689
690
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys

691
tyVarsOfPred :: PredType -> TyVarSet
692
693
694
tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
695
696

tyVarsOfTheta :: ThetaType -> TyVarSet
697
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
698

699
-- Add a Note with the free tyvars to the top of the type
700
addFreeTyVars :: Type -> Type
701
702
addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
addFreeTyVars ty			     = NoteTy (FTVNote (tyVarsOfType ty)) ty
703
\end{code}
704

705

706
707
708
709
710
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
711

712
713
tidyTy tidies up a type for printing in an error message, or in
an interface file.
714

715
It doesn't change the uniques at all, just the print names.
716
717

\begin{code}
718
719
720
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidyTyVarBndr (tidy_env, subst) tyvar
  = case tidyOccName tidy_env (getOccName name) of
721
      (tidy', occ') -> 	((tidy', subst'), tyvar')
722
723
724
		    where
			subst' = extendVarEnv subst tyvar tyvar'
			tyvar' = setTyVarName tyvar name'
725
			name'  = tidyNameOcc name occ'
726
727
  where
    name = tyVarName tyvar
728

729
730
731
tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
-- Add the free tyvars to the env in tidy form,
-- so that we can tidy the type they are free in
732
733
734
735
736
737
738
739
740
741
742
tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))

tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars

tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
-- Treat a new tyvar as a binder, and give it a fresh tidy name
tidyOpenTyVar env@(tidy_env, subst) tyvar
  = case lookupVarEnv subst tyvar of
	Just tyvar' -> (env, tyvar')		-- Already substituted
	Nothing	    -> tidyTyVarBndr env tyvar	-- Treat it as a binder
743

744
745
746
tidyType :: TidyEnv -> Type -> Type
tidyType env@(tidy_env, subst) ty
  = go ty
747
  where
748
749
750
    go (TyVarTy tv)	    = case lookupVarEnv subst tv of
				Nothing  -> TyVarTy tv
				Just tv' -> TyVarTy tv'
751
752
    go (TyConApp tycon tys) = let args = map go tys
			      in args `seqList` TyConApp tycon args
sof's avatar
sof committed
753
    go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
754
    go (PredTy sty)	    = PredTy (tidyPred env sty)
sof's avatar
sof committed
755
756
757
    go (AppTy fun arg)	    = (AppTy $! (go fun)) $! (go arg)
    go (FunTy fun arg)	    = (FunTy $! (go fun)) $! (go arg)
    go (ForAllTy tv ty)	    = ForAllTy tvp $! (tidyType envp ty)
758
			      where
759
			        (envp, tvp) = tidyTyVarBndr env tv
760
761
762

    go_note note@(FTVNote ftvs) = note	-- No need to tidy the free tyvars

763
tidyTypes env tys = map (tidyType env) tys
764

765
766
767
tidyPred :: TidyEnv -> PredType -> PredType
tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
768
tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
769
770
771
\end{code}


772
@tidyOpenType@ grabs the free type variables, tidies them
773
774
775
776
777
778
779
and then uses @tidyType@ to work over the type itself

\begin{code}
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType env ty
  = (env', tidyType env' ty)
  where
780
    env' = tidyFreeTyVars env (tyVarsOfType ty)
781
782
783
784
785
786

tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes env tys = mapAccumL tidyOpenType env tys

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
787
788
\end{code}

789
\begin{code}
790

791
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
792
tidyKind env k = tidyOpenType env k
793
794
795

\end{code}

796

797
798
%************************************************************************
%*									*
799
\subsection{Liftedness}
800
801
802
%*									*
%************************************************************************

803
\begin{code}
804
isUnLiftedType :: Type -> Bool
805
806
807
808
809
810
	-- isUnLiftedType returns True for forall'd unlifted types:
	--	x :: forall a. Int#
	-- I found bindings like these were getting floated to the top level.
	-- They are pretty bogus types, mind you.  It would be better never to
	-- construct them

811
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
812
813
814
isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
isUnLiftedType other		 = False	
815

816
isUnboxedTupleType :: Type -> Bool
817
818
819
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
			   Just (tc, ty_args) -> isUnboxedTupleTyCon tc
			   other	      -> False
820

821
-- Should only be applied to *types*; hence the assert
822
isAlgType :: Type -> Bool
823
isAlgType ty = case splitTyConApp_maybe ty of
sof's avatar
sof committed
824
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
825
826
					      isAlgTyCon tc
			other		   -> False
827
828
\end{code}

829
830
831
832
833
834
835
836
@isStrictType@ computes whether an argument (or let RHS) should
be computed strictly or lazily, based only on its type.
Works just like isUnLiftedType, except that it has a special case 
for dictionaries.  Since it takes account of ClassP, you might think
this function should be in TcType, but isStrictType is used by DataCon,
which is below TcType in the hierarchy, so it's convenient to put it here.

\begin{code}
837
838
isStrictType (PredTy pred)     = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
839
840
841
842
843
844
isStrictType (ForAllTy tv ty)  = isStrictType ty
isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
isStrictType other	       = False	

isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
isStrictPred other	     = False
845
846
847
848
849
850
851
852
853
854
855
856
	-- We may be strict in dictionary types, but only if it 
	-- has more than one component.
	-- [Being strict in a single-component dictionary risks
	--  poking the dictionary component, which is wrong.]
\end{code}

\begin{code}
isPrimitiveType :: Type -> Bool
-- Returns types that are opaque to Haskell.
-- Most of these are unlifted, but now that we interact with .NET, we
-- may have primtive (foreign-imported) types that are lifted
isPrimitiveType ty = case splitTyConApp_maybe ty of
sof's avatar
sof committed
857
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
858
859
860
861
					      isPrimTyCon tc
			other		   -> False
\end{code}

862

863
864
865
866
867
868
869
870
871
872
873
874
%************************************************************************
%*									*
\subsection{Sequencing on types
%*									*
%************************************************************************

\begin{code}
seqType :: Type -> ()
seqType (TyVarTy tv) 	  = tv `seq` ()
seqType (AppTy t1 t2) 	  = seqType t1 `seq` seqType t2
seqType (FunTy t1 t2) 	  = seqType t1 `seq` seqType t2
seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
875
seqType (PredTy p) 	  = seqPred p
876
877
878
879
880
881
882
883
884
seqType (TyConApp tc tys) = tc `seq` seqTypes tys
seqType (ForAllTy tv ty)  = tv `seq` seqType ty

seqTypes :: [Type] -> ()
seqTypes []       = ()
seqTypes (ty:tys) = seqType ty `seq` seqTypes tys

seqNote :: TyNote -> ()
seqNote (FTVNote set) = sizeUniqSet set `seq` ()
885

886
seqPred :: PredType -> ()
887
888
889
seqPred (ClassP c tys)   = c `seq` seqTypes tys
seqPred (IParam n ty)    = n `seq` seqType ty
seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
890
891
892
893
894
\end{code}


%************************************************************************
%*									*
895
		Equality for Core types 
896
	(We don't use instances so that we know where it happens)
897
898
899
%*									*
%************************************************************************

900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
Note that eqType works right even for partial applications of newtypes.
See Note [Newtype eta] in TyCon.lhs

\begin{code}
coreEqType :: Type -> Type -> Bool
coreEqType t1 t2
  = eq rn_env t1 t2
  where
    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))

    eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
    eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
    eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
    eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
    eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
	| tc1 == tc2, all2 (eq env) tys1 tys2 = True
			-- The lengths should be equal because
			-- the two types have the same kind
	-- NB: if the type constructors differ that does not 
	--     necessarily mean that the types aren't equal
	--     (synonyms, newtypes)
	-- Even if the type constructors are the same, but the arguments
	-- differ, the two types could be the same (e.g. if the arg is just
	-- ignored in the RHS).  In both these cases we fall through to an 
	-- attempt to expand one side or the other.

	-- Now deal with newtypes, synonyms, pred-tys
927
928
    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
		 | Just t2' <- coreView t2 = eq env t1 t2' 
929
930
931
932

	-- Fall through case; not equal!
    eq env t1 t2 = False
\end{code}
933

934

935
936
937
938
939
940
%************************************************************************
%*									*
		Comparision for source types 
	(We don't use instances so that we know where it happens)
%*									*
%************************************************************************
941

942
943
944
Note that 
	tcEqType, tcCmpType 
do *not* look through newtypes, PredTypes
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970

\begin{code}
tcEqType :: Type -> Type -> Bool
tcEqType t1 t2 = isEqual $ cmpType t1 t2

tcEqTypes :: [Type] -> [Type] -> Bool
tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2

tcCmpType :: Type -> Type -> Ordering
tcCmpType t1 t2 = cmpType t1 t2

tcCmpTypes :: [Type] -> [Type] -> Ordering
tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2

tcEqPred :: PredType -> PredType -> Bool
tcEqPred p1 p2 = isEqual $ cmpPred p1 p2

tcCmpPred :: PredType -> PredType -> Ordering
tcCmpPred p1 p2 = cmpPred p1 p2

tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
\end{code}

Now here comes the real worker

971
\begin{code}
972
973
974
975
976
977
978
979
980
981
982
983
984
985
cmpType :: Type -> Type -> Ordering
cmpType t1 t2 = cmpTypeX rn_env t1 t2
  where
    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))

cmpTypes :: [Type] -> [Type] -> Ordering
cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
  where
    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))

cmpPred :: PredType -> PredType -> Ordering
cmpPred p1 p2 = cmpPredX rn_env p1 p2
  where
    rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
986

987
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
988
989
cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
		   | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
990

991
992
993
994
995
996
997
998
999
1000
cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
cmpTypeX env t1			(NoteTy _ t2)	     = cmpTypeX env t1 t2

    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
cmpTypeX env (AppTy _ _) (TyVarTy _) = GT