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

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

12
13
14
	-- Re-exports from Kind
	module Kind,

15
16
	-- Re-exports from TyCon
	PrimRep(..),
17

18
19
	mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,

20
	mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
21

22
23
	mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
	splitFunTys, splitFunTysN,
24
	funResultTy, funArgTy, zipFunTys, isFunTy,
25

26
	mkTyConApp, mkTyConTy, 
27
28
	tyConAppTyCon, tyConAppArgs, 
	splitTyConApp_maybe, splitTyConApp,
29

30
	repType, typePrimRep, coreView, tcView,
31

32
	mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
33
	applyTy, applyTys, isForAllTy, dropForAlls,
34

35
	-- Source types
36
	predTypeRep, mkPredTy, mkPredTys,
37

38
	-- Newtypes
39
	splitRecNewType_maybe,
40

41
	-- Lifting and boxity
42
43
	isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
	isStrictType, isStrictPred, 
44

45
	-- Free variables
46
	tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
47
	typeKind, addFreeTyVars,
48

49
	-- Tidying up for printing
50
51
52
53
54
	tidyType,      tidyTypes,
	tidyOpenType,  tidyOpenTypes,
	tidyTyVarBndr, tidyFreeTyVars,
	tidyOpenTyVar, tidyOpenTyVars,
	tidyTopType,   tidyPred,
55
	tidyKind,
56

57
	-- Comparison
58
59
	coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
	tcEqPred, tcCmpPred, tcEqTypeX, 
60

61
	-- Seq
62
	seqType, seqTypes,
63

64
	-- Type substitutions
65
66
	TvSubstEnv, emptyTvSubstEnv,	-- Representation widely visible
	TvSubst(..), emptyTvSubst,	-- Representation visible to a few friends
67
	mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
68
	getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
69
 	extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
70
71

	-- Performing substitution on types
72
	substTy, substTys, substTyWith, substTheta, 
73
	substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
74

75
	-- Pretty-printing
76
	pprType, pprParendType, pprTyThingCategory,
77
	pprPred, pprTheta, pprThetaArrow, pprClassPred
78
    ) where
79

80
81
#include "HsVersions.h"

82
83
84
85
86
-- We import the representation and primitive functions from TypeRep.
-- Many things are reexported, but not the representation!

import TypeRep

87
-- friends:
88
import Kind
89
import Var	( Var, TyVar, tyVarKind, tyVarName, setTyVarName, mkTyVar )
90
91
92
import VarEnv
import VarSet

93
94
import OccName	( tidyOccName )
import Name	( NamedThing(..), mkInternalName, tidyNameOcc )
95
import Class	( Class, classTyCon )
96
import TyCon	( TyCon, isRecursiveTyCon, isPrimTyCon,
97
		  isUnboxedTupleTyCon, isUnLiftedTyCon,
98
		  isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
99
100
101
		  isAlgTyCon, tyConArity, 
		  tcExpandTyCon_maybe, coreExpandTyCon_maybe,
	          tyConKind, PrimRep(..), tyConPrimRep,
102
103
		)

104
-- others
105
import StaticFlags	( opt_DictsStrict )
106
import SrcLoc		( noSrcLoc )
107
import Util		( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
108
import Outputable
109
import UniqSet		( sizeUniqSet )		-- Should come via VarSet
110
import Maybe		( isJust )
111
112
\end{code}

113

114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
%************************************************************************
%*									*
		Type representation
%*									*
%************************************************************************

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

\begin{code}
{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
-- Srips off the *top layer only* of a type to give 
-- its underlying representation type. 
-- Returns Nothing if there is nothing to look through.
--
129
-- In the case of newtypes, it returns
130
131
132
133
134
135
136
137
138
139
140
141
--	*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)

142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
-- 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
coreView (PredTy p)    	   = Just (predTypeRep p)
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

-----------------------------------------------
{-# 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
161
162
163
\end{code}


164
165
166
167
168
%************************************************************************
%*									*
\subsection{Constructor-specific functions}
%*									*
%************************************************************************
sof's avatar
sof committed
169
170


171
172
173
---------------------------------------------------------------------
				TyVarTy
				~~~~~~~
174
\begin{code}
175
mkTyVarTy  :: TyVar   -> Type
176
mkTyVarTy  = TyVarTy
177

178
mkTyVarTys :: [TyVar] -> [Type]
179
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
180

181
getTyVar :: String -> Type -> TyVar
182
183
184
getTyVar msg ty = case getTyVar_maybe ty of
		    Just tv -> tv
		    Nothing -> panic ("getTyVar: " ++ msg)
185

186
isTyVarTy :: Type -> Bool
187
188
189
isTyVarTy ty = isJust (getTyVar_maybe ty)

getTyVar_maybe :: Type -> Maybe TyVar
190
191
192
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) 	 	    = Just tv  
getTyVar_maybe other	         	    = Nothing
193
194
195
\end{code}


196
197
198
199
200
201
---------------------------------------------------------------------
				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.
202

203
\begin{code}
204
mkAppTy orig_ty1 orig_ty2
205
  = mk_app orig_ty1
206
  where
207
    mk_app (NoteTy _ ty1)    = mk_app ty1
208
    mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
209
    mk_app ty1		     = AppTy orig_ty1 orig_ty2
210
	-- Note that the TyConApp could be an 
211
212
213
214
215
216
217
	-- 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
218

219
mkAppTys :: Type -> [Type] -> Type
220
221
mkAppTys orig_ty1 []	    = orig_ty1
	-- This check for an empty list of type arguments
222
	-- avoids the needless loss of a type synonym constructor.
223
224
225
	-- For example: mkAppTys Rational []
	--   returns to (Ratio Integer), which has needlessly lost
	--   the Rational part.
226
mkAppTys orig_ty1 orig_tys2
227
  = mk_app orig_ty1
228
  where
229
    mk_app (NoteTy _ ty1)    = mk_app ty1
230
231
    mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
				-- mkTyConApp: see notes with mkAppTy
232
    mk_app ty1		     = foldl AppTy orig_ty1 orig_tys2
233

234
splitAppTy_maybe :: Type -> Maybe (Type, Type)
235
splitAppTy_maybe ty | Just ty' <- coreView ty = splitAppTy_maybe ty'
236
splitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
237
splitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
238
splitAppTy_maybe (TyConApp tc tys) = case snocView tys of
239
240
					Nothing         -> Nothing
					Just (tys',ty') -> Just (TyConApp tc tys', ty')
241
splitAppTy_maybe other	     	   = Nothing
242

243
splitAppTy :: Type -> (Type, Type)
244
245
246
splitAppTy ty = case splitAppTy_maybe ty of
			Just pr -> pr
			Nothing -> panic "splitAppTy"
247

248
splitAppTys :: Type -> (Type, [Type])
249
splitAppTys ty = split ty ty []
250
  where
251
    split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
252
    split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
253
    split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
254
    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
255
					       (TyConApp funTyCon [], [ty1,ty2])
256
    split orig_ty ty		        args = (orig_ty, args)
257
258
\end{code}

259
260
261
262
263

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

264
\begin{code}
265
mkFunTy :: Type -> Type -> Type
266
mkFunTy arg res = FunTy arg res
267

268
mkFunTys :: [Type] -> Type -> Type
269
mkFunTys tys ty = foldr FunTy ty tys
270

271
272
273
isFunTy :: Type -> Bool 
isFunTy ty = isJust (splitFunTy_maybe ty)

274
splitFunTy :: Type -> (Type, Type)
275
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
276
splitFunTy (FunTy arg res)   = (arg, res)
277
splitFunTy other	     = pprPanic "splitFunTy" (ppr other)
278

279
splitFunTy_maybe :: Type -> Maybe (Type, Type)
280
splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
281
282
splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
splitFunTy_maybe other	           = Nothing
283

284
splitFunTys :: Type -> ([Type], Type)
285
splitFunTys ty = split [] ty ty
286
  where
287
    split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
288
289
    split args orig_ty (FunTy arg res) 	 = split (arg:args) res res
    split args orig_ty ty                = (reverse args, orig_ty)
290

291
292
293
294
295
296
297
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) }}

298
299
300
zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
  where
301
    split acc []     nty ty  	           = (reverse acc, nty)
302
303
    split acc xs     nty ty 
	  | Just ty' <- coreView ty 	   = split acc xs nty ty'
304
    split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
305
    split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
306
307
    
funResultTy :: Type -> Type
308
funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
309
funResultTy (FunTy arg res)   = res
310
funResultTy ty		      = pprPanic "funResultTy" (ppr ty)
311
312

funArgTy :: Type -> Type
313
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
314
funArgTy (FunTy arg res)   = arg
315
funArgTy ty		   = pprPanic "funArgTy" (ppr ty)
316
317
318
\end{code}


319
320
321
---------------------------------------------------------------------
				TyConApp
				~~~~~~~~
322
@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
323
as apppropriate.
324

325
\begin{code}
326
mkTyConApp :: TyCon -> [Type] -> Type
327
mkTyConApp tycon tys
328
  | isFunTyCon tycon, [ty1,ty2] <- tys
329
  = FunTy ty1 ty2
330

331
  | otherwise
332
  = TyConApp tycon tys
333

334
mkTyConTy :: TyCon -> Type
335
mkTyConTy tycon = mkTyConApp tycon []
336
337
338
339
340

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

341
tyConAppTyCon :: Type -> TyCon
342
tyConAppTyCon ty = fst (splitTyConApp ty)
343
344

tyConAppArgs :: Type -> [Type]
345
tyConAppArgs ty = snd (splitTyConApp ty)
346
347
348
349

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

352
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
353
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
354
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
355
splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
356
splitTyConApp_maybe other	      = Nothing
sof's avatar
sof committed
357
\end{code}
358

359

360
361
362
363
364
365
366
367
---------------------------------------------------------------------
				SynTy
				~~~~~

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

369
370
371
372
373
374
375
376
	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.
377
378


379
380
		Representation types
		~~~~~~~~~~~~~~~~~~~~
381
382
repType looks through 
	(a) for-alls, and
383
384
385
	(b) synonyms
	(c) predicates
	(d) usage annotations
386
	(e) all newtypes, including recursive ones
387
It's useful in the back end.
388
389
390

\begin{code}
repType :: Type -> Type
391
-- Only applied to types of kind *; hence tycons are saturated
392
repType ty | Just ty' <- coreView ty = repType ty'
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
repType (ForAllTy _ ty)  = repType ty
repType (TyConApp tc tys)
  | isNewTyCon tc 	 = -- Recursive newtypes are opaque to coreView
			   -- but we must expand them here.  Sure to
			   -- be saturated because repType is only applied
			   -- to types of kind *
			   ASSERT( isRecursiveTyCon tc && 
				   tys `lengthIs` tyConArity tc )
			   repType (new_type_rep tc tys)
repType ty = ty

-- 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
409

410
411
-- ToDo: this could be moved to the code generator, using splitTyConApp instead
-- of inspecting the type directly.
412
413
414
415
typePrimRep :: Type -> PrimRep
typePrimRep ty = case repType ty of
		   TyConApp tc _ -> tyConPrimRep tc
		   FunTy _ _	 -> PtrRep
416
		   AppTy _ _	 -> PtrRep	-- See note below
417
		   TyVarTy _	 -> PtrRep
418
		   other	 -> pprPanic "typePrimRep" (ppr ty)
419
420
421
422
423
	-- 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.
424

425
426
427
\end{code}


428
429
430
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
431
432

\begin{code}
433
mkForAllTy :: TyVar -> Type -> Type
434
435
mkForAllTy tyvar ty
  = mkForAllTys [tyvar] ty
436

437
mkForAllTys :: [TyVar] -> Type -> Type
438
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
439
440
441
442
443

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

445
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
446
splitForAllTy_maybe ty = splitFAT_m ty
447
  where
448
449
450
    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
451

452
splitForAllTys :: Type -> ([TyVar], Type)
453
splitForAllTys ty = split ty ty []
454
   where
455
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
456
457
     split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
     split orig_ty t		     tvs = (reverse tvs, orig_ty)
458
459
460

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

463
-- (mkPiType now in CoreUtils)
464

465
466
467
468
469
470
471
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. 
472

473
\begin{code}
474
applyTy :: Type -> Type -> Type
475
476
477
applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
applyTy other		 arg = panic "applyTy"
478

479
applyTys :: Type -> [Type] -> Type
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
-- 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
499
  = ASSERT2( n_tvs > 0, ppr orig_fun_ty )	-- Zero case gives infnite loop!
500
501
502
503
504
505
    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     
506
\end{code}
507

508

509
510
%************************************************************************
%*									*
511
\subsection{Source types}
512
513
%*									*
%************************************************************************
514

515
516
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.
517

518
Source types are always lifted.
519

520
The key function is predTypeRep which gives the representation of a source type:
521
522

\begin{code}
523
mkPredTy :: PredType -> Type
524
mkPredTy pred = PredTy pred
525
526

mkPredTys :: ThetaType -> [Type]
527
528
529
530
531
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.
532
-- Unwraps only the outermost level; for example, the result might
533
-- be a newtype application
534
535
predTypeRep (IParam _ ty)     = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
536
	-- Result might be a newtype application, but the consumer will
537
538
	-- look through that too if necessary
\end{code}
539
540


541
542
543
544
545
%************************************************************************
%*									*
		NewTypes
%*									*
%************************************************************************
546

547
548
549
\begin{code}
splitRecNewType_maybe :: Type -> Maybe Type
-- Sometimes we want to look through a recursive newtype, and that's what happens here
550
-- It only strips *one layer* off, so the caller will usually call itself recursively
551
-- Only applied to types of kind *, hence the newtype is always saturated
552
553
554
555
556
557
558
splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
splitRecNewType_maybe (TyConApp tc tys)
  | isNewTyCon tc
  = ASSERT( tys `lengthIs` tyConArity tc )	-- splitRecNewType_maybe only be applied 
						-- 	to *types* (of kind *)
    ASSERT( isRecursiveTyCon tc ) 		-- Guaranteed by coreView
    case newTyConRhs tc of
559
560
561
	(tvs, rep_ty) -> ASSERT( length tvs == length tys )
			 Just (substTyWith tvs tys rep_ty)
	
562
splitRecNewType_maybe other = Nothing
563
564
\end{code}

565

566
567
568
569
570
571
572
573
574
%************************************************************************
%*									*
\subsection{Kinds and free variables}
%*									*
%************************************************************************

---------------------------------------------------------------------
		Finding the kind of a type
		~~~~~~~~~~~~~~~~~~~~~~~~~~
575
\begin{code}
576
typeKind :: Type -> Kind
577

578
typeKind (TyVarTy tyvar)	= tyVarKind tyvar
579
typeKind (TyConApp tycon tys)	= foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
580
typeKind (NoteTy _ ty)		= typeKind ty
581
typeKind (PredTy _)		= liftedTypeKind -- Predicates are always 
582
						 -- represented by lifted types
583
584
typeKind (AppTy fun arg)	= kindFunResult (typeKind fun)
typeKind (FunTy arg res)	= liftedTypeKind
585
typeKind (ForAllTy tv ty)	= typeKind ty
586
587
588
\end{code}


589
590
591
---------------------------------------------------------------------
		Free variables of a type
		~~~~~~~~~~~~~~~~~~~~~~~~
592
\begin{code}
593
tyVarsOfType :: Type -> TyVarSet
594
-- NB: for type synonyms tyVarsOfType does *not* expand the synonym
595
tyVarsOfType (TyVarTy tv)		= unitVarSet tv
596
tyVarsOfType (TyConApp tycon tys)	= tyVarsOfTypes tys
597
tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
598
tyVarsOfType (PredTy sty)		= tyVarsOfPred sty
599
600
tyVarsOfType (FunTy arg res)		= tyVarsOfType arg `unionVarSet` tyVarsOfType res
tyVarsOfType (AppTy fun arg)		= tyVarsOfType fun `unionVarSet` tyVarsOfType arg
601
tyVarsOfType (ForAllTy tyvar ty)	= delVarSet (tyVarsOfType ty) tyvar
602

603
tyVarsOfTypes :: [Type] -> TyVarSet
604
605
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys

606
tyVarsOfPred :: PredType -> TyVarSet
607
608
tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
609
610

tyVarsOfTheta :: ThetaType -> TyVarSet
611
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
612

613
-- Add a Note with the free tyvars to the top of the type
614
addFreeTyVars :: Type -> Type
615
616
addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
addFreeTyVars ty			     = NoteTy (FTVNote (tyVarsOfType ty)) ty
617
\end{code}
618

619

620
621
622
623
624
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
625

626
627
tidyTy tidies up a type for printing in an error message, or in
an interface file.
628

629
It doesn't change the uniques at all, just the print names.
630
631

\begin{code}
632
633
634
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidyTyVarBndr (tidy_env, subst) tyvar
  = case tidyOccName tidy_env (getOccName name) of
635
      (tidy', occ') -> 	((tidy', subst'), tyvar')
636
637
638
		    where
			subst' = extendVarEnv subst tyvar tyvar'
			tyvar' = setTyVarName tyvar name'
639
			name'  = tidyNameOcc name occ'
640
641
  where
    name = tyVarName tyvar
642

643
644
645
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
646
647
648
649
650
651
652
653
654
655
656
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
657

658
659
660
tidyType :: TidyEnv -> Type -> Type
tidyType env@(tidy_env, subst) ty
  = go ty
661
  where
662
663
664
    go (TyVarTy tv)	    = case lookupVarEnv subst tv of
				Nothing  -> TyVarTy tv
				Just tv' -> TyVarTy tv'
665
666
    go (TyConApp tycon tys) = let args = map go tys
			      in args `seqList` TyConApp tycon args
sof's avatar
sof committed
667
    go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
668
    go (PredTy sty)	    = PredTy (tidyPred env sty)
sof's avatar
sof committed
669
670
671
    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)
672
			      where
673
			        (envp, tvp) = tidyTyVarBndr env tv
674
675
676

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

677
tidyTypes env tys = map (tidyType env) tys
678

679
680
681
tidyPred :: TidyEnv -> PredType -> PredType
tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
682
683
684
\end{code}


685
@tidyOpenType@ grabs the free type variables, tidies them
686
687
688
689
690
691
692
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
693
    env' = tidyFreeTyVars env (tyVarsOfType ty)
694
695
696
697
698
699

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

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
700
701
\end{code}

702

703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
%************************************************************************
%*									*
		Tidying Kinds
%*									*
%************************************************************************

We use a grevious hack for tidying KindVars.  A TidyEnv contains
a (VarEnv Var) substitution, to express the renaming; but
KindVars are not Vars.  The Right Thing ultimately is to make them
into Vars (and perhaps make Kinds into Types), but I just do a hack
here: I make up a TyVar just to remember the new OccName for the
renamed KindVar

\begin{code}
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
tidyKind env@(tidy_env, subst) (KindVar kvar)
  | Just tv <- lookupVarEnv_Directly subst uniq
  = (env, KindVar (setKindVarOcc kvar (getOccName tv)))
  | otherwise
  = ((tidy', subst'), KindVar kvar')
  where
    uniq = kindVarUniq kvar
    (tidy', occ') = tidyOccName tidy_env (kindVarOcc kvar)
    kvar'   = setKindVarOcc kvar occ'
    fake_tv = mkTyVar tv_name (panic "tidyKind:fake tv kind")
    tv_name = mkInternalName uniq occ' noSrcLoc
    subst'  = extendVarEnv subst fake_tv fake_tv

tidyKind env (FunKind k1 k2) 
  = (env2, FunKind k1' k2')
  where
    (env1, k1') = tidyKind env  k1
    (env2, k2') = tidyKind env1 k2

tidyKind env k = (env, k)	-- Atomic kinds
\end{code}

740

741
742
%************************************************************************
%*									*
743
\subsection{Liftedness}
744
745
746
%*									*
%************************************************************************

747
\begin{code}
748
isUnLiftedType :: Type -> Bool
749
750
751
752
753
754
	-- 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

755
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
756
757
758
isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
isUnLiftedType other		 = False	
759

760
isUnboxedTupleType :: Type -> Bool
761
762
763
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
			   Just (tc, ty_args) -> isUnboxedTupleTyCon tc
			   other	      -> False
764

765
-- Should only be applied to *types*; hence the assert
766
isAlgType :: Type -> Bool
767
isAlgType ty = case splitTyConApp_maybe ty of
sof's avatar
sof committed
768
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
769
770
					      isAlgTyCon tc
			other		   -> False
771
772
\end{code}

773
774
775
776
777
778
779
780
@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}
781
782
isStrictType (PredTy pred)     = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
783
784
785
786
787
788
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
789
790
791
792
793
794
795
796
797
798
799
800
	-- 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
801
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
802
803
804
805
					      isPrimTyCon tc
			other		   -> False
\end{code}

806

807
808
809
810
811
812
813
814
815
816
817
818
%************************************************************************
%*									*
\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
819
seqType (PredTy p) 	  = seqPred p
820
821
822
823
824
825
826
827
828
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` ()
829

830
seqPred :: PredType -> ()
831
832
seqPred (ClassP c tys) = c  `seq` seqTypes tys
seqPred (IParam n ty)  = n  `seq` seqType ty
833
834
835
836
837
\end{code}


%************************************************************************
%*									*
838
		Equality for Core types 
839
	(We don't use instances so that we know where it happens)
840
841
842
%*									*
%************************************************************************

843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
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
    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
		 | Just t2' <- coreView t2 = eq env t1 t2'

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

877

878
879
880
881
882
883
%************************************************************************
%*									*
		Comparision for source types 
	(We don't use instances so that we know where it happens)
%*									*
%************************************************************************
884

885
886
887
Note that 
	tcEqType, tcCmpType 
do *not* look through newtypes, PredTypes
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913

\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

914
\begin{code}
915
916
917
918
919
920
921
922
923
924
925
926
927
928
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))
929

930
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
931
932
cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
		   | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
933

934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
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
    
cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
    
cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
    
cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT

cmpTypeX env (PredTy _)   t2		= GT

cmpTypeX env _ _ = LT

-------------
cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
cmpTypesX env []        []        = EQ
964
cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
965
966
967
968
969
970
971
972
973
974
cmpTypesX env []        tys       = LT
cmpTypesX env ty        []        = GT

-------------
cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
	-- Compare types as well as names for implicit parameters
	-- This comparison is used exclusively (I think) for the
	-- finite map built in TcSimplify
cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
975
cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
976
977
978
979
980
981
982
983
984
cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
\end{code}

PredTypes are used as a FM key in TcSimplify, 
so we take the easy path and make them an instance of Ord

\begin{code}
instance Eq  PredType where { (==)    = tcEqPred }
instance Ord PredType where { compare = tcCmpPred }
985
986
\end{code}

987
988
989
990
991
992
993
994
995
996

%************************************************************************
%*									*
		Type substitutions
%*									*
%************************************************************************

\begin{code}
data TvSubst 		
  = TvSubst InScopeSet 	-- The in-scope type variables
997
	    TvSubstEnv	-- The substitution itself
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
			-- See Note [Apply Once]

{- ----------------------------------------------------------
	 	Note [Apply Once]

We use TvSubsts to instantiate things, and we might instantiate
	forall a b. ty
\with the types
	[a, b], or [b, a].
So the substition might go [a->b, b->a].  A similar situation arises in Core
when we find a beta redex like
	(/\ a /\ b -> e) b a
Then we also end up with a substition that permutes type variables. Other
variations happen to; for example [a -> (a, b)].  

	***************************************************
	*** So a TvSubst must be applied precisely once ***
	***************************************************

A TvSubst is not idempotent, but, unlike the non-idempotent substitution
we use during unifications, it must not be repeatedly applied.
-------------------------------------------------------------- -}


type TvSubstEnv = TyVarEnv Type
	-- A TvSubstEnv is used both inside a TvSubst (with the apply-once
	-- invariant discussed in Note [Apply Once]), and also independently
	-- in the middle of matching, and unification (see Types.Unify)
	-- So you have to look at the context to know if it's idempotent or
	-- apply-once or whatever
1028
1029
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = emptyVarEnv
1030

1031
1032
1033
composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
-- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
-- It assumes that both are idempotent
1034
-- Typically, env1 is the refinement to a base substitution env2
1035
1036
1037
1038
1039
composeTvSubst in_scope env1 env2
  = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
	-- First apply env1 to the range of env2
	-- Then combine the two, making sure that env1 loses if
	-- both bind the same variable; that's why env1 is the
1040
	--  *left* argument to plusVarEnv, because the right arg wins
1041
1042
1043
  where
    subst1 = TvSubst in_scope env1

1044
emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1045

1046
1047
1048
isEmptyTvSubst :: TvSubst -> Bool
isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env

1049
1050
1051
mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
mkTvSubst = TvSubst

1052
1053
1054
1055
1056
1057
1058
1059
1060
getTvSubstEnv :: TvSubst -> TvSubstEnv
getTvSubstEnv (TvSubst _ env) = env

getTvInScope :: TvSubst -> InScopeSet
getTvInScope (TvSubst in_scope _) = in_scope

isInScope :: Var -> TvSubst -> Bool
isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope

1061
1062
1063
notElemTvSubst :: TyVar -> TvSubst -> Bool
notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)

1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env

extendTvInScope :: TvSubst -> [Var] -> TvSubst
extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env

extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)

extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
extendTvSubstList (TvSubst in_scope env) tvs tys 
  = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))

1077
-- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1078
1079
1080
-- the types given; but it's just a thunk so with a bit of luck
-- it'll never be evaluated

1081
1082
mkOpenTvSubst :: TvSubstEnv -> TvSubst
mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1083

1084
1085
zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
zipOpenTvSubst tyvars tys 
1086
1087
1088
1089
1090
#ifdef DEBUG
  | length tyvars /= length tys
  = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
  | otherwise
#endif
1091
1092
1093
1094
1095
1096
1097
1098
1099
  = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)

-- mkTopTvSubst is called when doing top-level substitutions.
-- Here we expect that the free vars of the range of the
-- substitution will be empty.
mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)

zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1100
1101
1102
1103
1104
1105
1106
zipTopTvSubst tyvars tys 
#ifdef DEBUG
  | length tyvars /= length tys
  = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
  | otherwise
#endif
  = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132

zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv tyvars tys
#ifdef DEBUG
  | length tyvars /= length tys
  = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
  | otherwise
#endif
  = zip_ty_env tyvars tys emptyVarEnv

-- Later substitutions in the list over-ride earlier ones, 
-- but there should be no loops
zip_ty_env []       []       env = env
zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
	-- There used to be a special case for when 
	--	ty == TyVarTy tv
	-- (a not-uncommon case) in which case the substitution was dropped.
	-- But the type-tidier changes the print-name of a type variable without
	-- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had 
	-- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
	-- And it happened that t was the type variable of the class.  Post-tiding, 
	-- it got turned into {Foo t2}.  The ext-core printer expanded this using
	-- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
	-- and so generated a rep type mentioning t not t2.  
	--
	-- Simplest fix is to nuke the "optimisation"
1133
1134
zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
-- zip_ty_env _ _ env = env
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150

instance Outputable TvSubst where
  ppr (TvSubst ins env) 
    = sep[ ptext SLIT("<TvSubst"),
	   nest 2 (ptext SLIT("In scope:") <+> ppr ins), 
	   nest 2 (ptext SLIT("Env:") <+> ppr env) ]
\end{code}

%************************************************************************
%*									*
		Performing type substitutions
%*									*
%************************************************************************

\begin{code}
substTyWith :: [TyVar] -> [Type] -> Type -> Type
1151
1152
substTyWith tvs tys = ASSERT( length tvs == length tys )
		      substTy (zipOpenTvSubst tvs tys)
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170

substTy :: TvSubst -> Type  -> Type
substTy subst ty | isEmptyTvSubst subst = ty
		 | otherwise	        = subst_ty subst ty

substTys :: TvSubst -> [Type] -> [Type]
substTys subst tys | isEmptyTvSubst subst = tys
	           | otherwise	          = map (subst_ty subst) tys

substTheta :: TvSubst -> ThetaType -> ThetaType
substTheta subst theta
  | isEmptyTvSubst subst = theta
  | otherwise	         = map (substPred subst) theta

substPred :: TvSubst -> PredType -> PredType
substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)

1171
1172
1173
1174
1175
1176
deShadowTy :: TyVarSet -> Type -> Type	-- Remove any nested binders mentioning tvs
deShadowTy tvs ty 
  = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
  where
    in_scope = mkInScopeSet tvs

1177
1178
-- Note that the in_scope set is poked only if we hit a forall
-- so it may often never be fully computed 
1179
subst_ty subst ty
1180
1181
   = go ty
  where
1182
    go (TyVarTy tv)   		   = substTyVar subst tv
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
    go (TyConApp tc tys)	   = let args = map go tys
				     in  args `seqList` TyConApp tc args

    go (PredTy p)  		   = PredTy $! (substPred subst p)

    go (NoteTy (FTVNote _) ty2)    = go ty2		-- Discard the free tyvar note

    go (FunTy arg res)   	   = (FunTy $! (go arg)) $! (go res)
    go (AppTy fun arg)   	   = mkAppTy (go fun) $! (go arg)
		-- The mkAppTy smart constructor is important
		-- we might be replacing (a Int), represented with App
		-- by [Int], represented with TyConApp
1195
    go (ForAllTy tv ty)		   = case substTyVarBndr subst tv of
1196
1197
					(subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)

1198
substTyVar :: TvSubst -> TyVar  -> Type
1199
1200
substTyVar subst tv
  = case lookupTyVar subst tv of
1201
1202
1203
	Nothing  -> TyVarTy tv
       	Just ty' -> ty'	-- See Note [Apply Once]

1204
1205
1206
lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv

1207
1208
substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)	
substTyVarBndr subst@(TvSubst in_scope env) old_var
1209
1210
1211
1212
1213
1214
1215
1216
  | old_var == new_var	-- No need to clone
			-- But we *must* zap any current substitution for the variable.
			--  For example:
			--	(\x.e) with id_subst = [x |-> e']
			-- Here we must simply zap the substitution for x
			--
			-- The new_id isn't cloned, but it may have a different type
			-- etc, so we must return it, not the old id
1217
1218
  = (TvSubst (in_scope `extendInScopeSet` new_var) 
	     (delVarEnv env old_var),
1219
1220
1221
1222
1223
1224
1225
     new_var)

  | otherwise	-- The new binder is in scope so
		-- we'd better rename it away from the in-scope variables
		-- Extending the substitution to do this renaming also
		-- has the (correct) effect of discarding any existing
		-- substitution for that variable
1226
1227
  = (TvSubst (in_scope `extendInScopeSet` new_var) 
	     (extendVarEnv env old_var (TyVarTy new_var)),
1228
1229
1230
1231
1232
     new_var)
  where
    new_var = uniqAway in_scope old_var
	-- The uniqAway part makes sure the new variable is not already in scope
\end{code}