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

6

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

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

        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
        argTypeKindTyCon, ubxTupleKindTyCon,

        liftedTypeKind, unliftedTypeKind, openTypeKind,
        argTypeKind, ubxTupleKind,

        tySuperKind, coSuperKind, 

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

        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
        isSubKindCon,
32

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

36
37
	mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,

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

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

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

50
	repType, typePrimRep, coreView, tcView, kindView,
51

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

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

58
	-- Newtypes
59
	splitRecNewType_maybe, newTyConInstRhs,
60

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

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

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

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

81
	-- Seq
82
	seqType, seqTypes,
83

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

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

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

100
101
#include "HsVersions.h"

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

import TypeRep

107
-- friends:
108
import Var	( Var, TyVar, tyVarKind, tyVarName, 
109
		  setTyVarName, setTyVarKind, mkWildTyVar )
110
111
112
import VarEnv
import VarSet

113
import OccName	( tidyOccName )
114
import Name	( NamedThing(..), tidyNameOcc )
115
import Class	( Class, classTyCon )
116
import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey, 
117
                  ubxTupleKindTyConKey, argTypeKindTyConKey )
118
import TyCon	( TyCon, isRecursiveTyCon, isPrimTyCon,
119
		  isUnboxedTupleTyCon, isUnLiftedTyCon,
120
		  isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
121
		  isAlgTyCon, tyConArity, isSuperKindTyCon,
122
		  tcExpandTyCon_maybe, coreExpandTyCon_maybe,
123
124
	          tyConKind, PrimRep(..), tyConPrimRep, tyConUnique,
                  isCoercionTyCon_maybe, isCoercionTyCon
125
126
		)

127
-- others
128
import StaticFlags	( opt_DictsStrict )
129
import Util		( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
130
import Outputable
131
import UniqSet		( sizeUniqSet )		-- Should come via VarSet
132
import Maybe		( isJust )
133
134
\end{code}

135

136
137
138
139
140
141
142
143
144
145
146
%************************************************************************
%*									*
		Type representation
%*									*
%************************************************************************

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

\begin{code}
{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
147
-- Strips off the *top layer only* of a type to give 
148
149
150
-- its underlying representation type. 
-- Returns Nothing if there is nothing to look through.
--
151
-- In the case of newtypes, it returns
152
153
154
155
156
157
158
159
160
161
162
163
--	*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)

164
165
166
-- 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
167
168
169
coreView (PredTy p)
  | isEqPred p             = Nothing
  | otherwise    	   = Just (predTypeRep p)
170
171
172
173
174
175
176
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

177
178


179
180
181
182
183
184
185
186
-----------------------------------------------
{-# 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
187
188
189
190
191
192
193
194

-----------------------------------------------
{-# 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
195
196
197
\end{code}


198
199
200
201
202
%************************************************************************
%*									*
\subsection{Constructor-specific functions}
%*									*
%************************************************************************
sof's avatar
sof committed
203
204


205
206
207
---------------------------------------------------------------------
				TyVarTy
				~~~~~~~
208
\begin{code}
209
mkTyVarTy  :: TyVar   -> Type
210
mkTyVarTy  = TyVarTy
211

212
mkTyVarTys :: [TyVar] -> [Type]
213
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
214

215
getTyVar :: String -> Type -> TyVar
216
217
218
getTyVar msg ty = case getTyVar_maybe ty of
		    Just tv -> tv
		    Nothing -> panic ("getTyVar: " ++ msg)
219

220
isTyVarTy :: Type -> Bool
221
222
223
isTyVarTy ty = isJust (getTyVar_maybe ty)

getTyVar_maybe :: Type -> Maybe TyVar
224
225
226
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) 	 	    = Just tv  
getTyVar_maybe other	         	    = Nothing
227

228
229
230
\end{code}


231
232
233
234
235
236
---------------------------------------------------------------------
				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.
237

238
\begin{code}
239
mkAppTy orig_ty1 orig_ty2
240
  = mk_app orig_ty1
241
  where
242
    mk_app (NoteTy _ ty1)    = mk_app ty1
243
    mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
244
    mk_app ty1		     = AppTy orig_ty1 orig_ty2
245
	-- Note that the TyConApp could be an 
246
247
248
249
250
251
252
	-- 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
253

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

269
-------------
270
splitAppTy_maybe :: Type -> Maybe (Type, Type)
271
272
273
splitAppTy_maybe ty | Just ty' <- coreView ty
		    = splitAppTy_maybe ty'
splitAppTy_maybe ty = repSplitAppTy_maybe ty
274

275
276
277
278
279
280
281
282
283
284
-------------
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
-------------
285
splitAppTy :: Type -> (Type, Type)
286
287
288
splitAppTy ty = case splitAppTy_maybe ty of
			Just pr -> pr
			Nothing -> panic "splitAppTy"
289

290
-------------
291
splitAppTys :: Type -> (Type, [Type])
292
splitAppTys ty = split ty ty []
293
  where
294
    split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
295
    split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
296
    split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
297
    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
298
					       (TyConApp funTyCon [], [ty1,ty2])
299
    split orig_ty ty		        args = (orig_ty, args)
300

301
302
\end{code}

303
304
305
306
307

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

308
\begin{code}
309
mkFunTy :: Type -> Type -> Type
310
mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildTyVar (PredTy (EqPred ty1 ty2))) res
311
mkFunTy arg res = FunTy arg res
312

313
mkFunTys :: [Type] -> Type -> Type
314
mkFunTys tys ty = foldr mkFunTy ty tys
315

316
317
318
isFunTy :: Type -> Bool 
isFunTy ty = isJust (splitFunTy_maybe ty)

319
splitFunTy :: Type -> (Type, Type)
320
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
321
splitFunTy (FunTy arg res)   = (arg, res)
322
splitFunTy other	     = pprPanic "splitFunTy" (ppr other)
323

324
splitFunTy_maybe :: Type -> Maybe (Type, Type)
325
splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
326
327
splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
splitFunTy_maybe other	           = Nothing
328

329
splitFunTys :: Type -> ([Type], Type)
330
splitFunTys ty = split [] ty ty
331
  where
332
    split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
333
334
    split args orig_ty (FunTy arg res) 	 = split (arg:args) res res
    split args orig_ty ty                = (reverse args, orig_ty)
335

336
337
338
339
340
341
342
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) }}

343
344
345
zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
  where
346
    split acc []     nty ty  	           = (reverse acc, nty)
347
348
    split acc xs     nty ty 
	  | Just ty' <- coreView ty 	   = split acc xs nty ty'
349
    split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
350
    split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
351
352
    
funResultTy :: Type -> Type
353
funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
354
funResultTy (FunTy arg res)   = res
355
funResultTy ty		      = pprPanic "funResultTy" (ppr ty)
356
357

funArgTy :: Type -> Type
358
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
359
funArgTy (FunTy arg res)   = arg
360
funArgTy ty		   = pprPanic "funArgTy" (ppr ty)
361
362
363
\end{code}


364
365
366
---------------------------------------------------------------------
				TyConApp
				~~~~~~~~
367
@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
368
as apppropriate.
369

370
\begin{code}
371
mkTyConApp :: TyCon -> [Type] -> Type
372
mkTyConApp tycon tys
373
  | isFunTyCon tycon, [ty1,ty2] <- tys
374
  = FunTy ty1 ty2
375

376
  | otherwise
377
  = TyConApp tycon tys
378

379
mkTyConTy :: TyCon -> Type
380
mkTyConTy tycon = mkTyConApp tycon []
381
382
383
384
385

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

386
tyConAppTyCon :: Type -> TyCon
387
tyConAppTyCon ty = fst (splitTyConApp ty)
388
389

tyConAppArgs :: Type -> [Type]
390
tyConAppArgs ty = snd (splitTyConApp ty)
391
392
393
394

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

397
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
398
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
399
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
400
splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
401
splitTyConApp_maybe other	      = Nothing
402
403
404
405
406
407
408
409
410
411
412
413
414
415

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

416
417
418
419
420
421
-- 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
422
\end{code}
423

424

425
426
427
428
429
430
431
432
---------------------------------------------------------------------
				SynTy
				~~~~~

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

434
435
436
437
438
439
440
441
	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.
442
443


444
445
		Representation types
		~~~~~~~~~~~~~~~~~~~~
446
447
repType looks through 
	(a) for-alls, and
448
449
450
	(b) synonyms
	(c) predicates
	(d) usage annotations
451
	(e) all newtypes, including recursive ones
452
It's useful in the back end.
453
454
455

\begin{code}
repType :: Type -> Type
456
-- Only applied to types of kind *; hence tycons are saturated
457
repType ty | Just ty' <- coreView ty = repType ty'
458
459
460
461
462
463
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 *
464
			   ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
465
466
467
468
469
470
471
472
			   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
473

474
475
-- ToDo: this could be moved to the code generator, using splitTyConApp instead
-- of inspecting the type directly.
476
477
478
479
typePrimRep :: Type -> PrimRep
typePrimRep ty = case repType ty of
		   TyConApp tc _ -> tyConPrimRep tc
		   FunTy _ _	 -> PtrRep
480
		   AppTy _ _	 -> PtrRep	-- See note below
481
		   TyVarTy _	 -> PtrRep
482
		   other	 -> pprPanic "typePrimRep" (ppr ty)
483
484
485
486
487
	-- 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.
488

489
490
491
\end{code}


492
493
494
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
495
496

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

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

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

509
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
510
splitForAllTy_maybe ty = splitFAT_m ty
511
  where
512
513
514
    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
515

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

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

527
-- (mkPiType now in CoreUtils)
528

529
530
531
532
533
534
535
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. 
536

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

543
applyTys :: Type -> [Type] -> Type
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
-- 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
563
  = ASSERT2( n_tvs > 0, ppr orig_fun_ty )	-- Zero case gives infnite loop!
564
565
566
567
568
569
    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     
570
\end{code}
571

572

573
574
%************************************************************************
%*									*
575
\subsection{Source types}
576
577
%*									*
%************************************************************************
578

579
580
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.
581

582
Source types are always lifted.
583

584
The key function is predTypeRep which gives the representation of a source type:
585
586

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

mkPredTys :: ThetaType -> [Type]
591
592
593
594
595
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.
596
-- Unwraps only the outermost level; for example, the result might
597
-- be a newtype application
598
599
predTypeRep (IParam _ ty)     = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
600
	-- Result might be a newtype application, but the consumer will
601
	-- look through that too if necessary
602
predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
603
\end{code}
604
605


606
607
608
609
610
%************************************************************************
%*									*
		NewTypes
%*									*
%************************************************************************
611

612
613
614
\begin{code}
splitRecNewType_maybe :: Type -> Maybe Type
-- Sometimes we want to look through a recursive newtype, and that's what happens here
615
-- It only strips *one layer* off, so the caller will usually call itself recursively
616
-- Only applied to types of kind *, hence the newtype is always saturated
617
618
619
620
621
622
623
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
624
625
626
	(tvs, rep_ty) -> ASSERT( length tvs == length tys )
			 Just (substTyWith tvs tys rep_ty)
	
627
splitRecNewType_maybe other = Nothing
628
629
630



631
632
\end{code}

633

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

---------------------------------------------------------------------
		Finding the kind of a type
		~~~~~~~~~~~~~~~~~~~~~~~~~~
643
\begin{code}
644
typeKind :: Type -> Kind
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
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
669
670
671
\end{code}


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

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

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

tyVarsOfTheta :: ThetaType -> TyVarSet
695
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
696

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

703

704
705
706
707
708
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
709

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

713
It doesn't change the uniques at all, just the print names.
714
715

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

727
728
729
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
730
731
732
733
734
735
736
737
738
739
740
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
741

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

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

761
tidyTypes env tys = map (tidyType env) tys
762

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


770
@tidyOpenType@ grabs the free type variables, tidies them
771
772
773
774
775
776
777
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
778
    env' = tidyFreeTyVars env (tyVarsOfType ty)
779
780
781
782
783
784

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

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
785
786
\end{code}

787
\begin{code}
788

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

\end{code}

794

795
796
%************************************************************************
%*									*
797
\subsection{Liftedness}
798
799
800
%*									*
%************************************************************************

801
\begin{code}
802
isUnLiftedType :: Type -> Bool
803
804
805
806
807
808
	-- 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

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

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

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

827
828
829
830
831
832
833
834
@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}
835
836
isStrictType (PredTy pred)     = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
837
838
839
840
841
842
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
843
844
845
846
847
848
849
850
851
852
853
854
	-- 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
855
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
856
857
858
859
					      isPrimTyCon tc
			other		   -> False
\end{code}

860

861
862
863
864
865
866
867
868
869
870
871
872
%************************************************************************
%*									*
\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
873
seqType (PredTy p) 	  = seqPred p
874
875
876
877
878
879
880
881
882
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` ()
883

884
seqPred :: PredType -> ()
885
886
887
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
888
889
890
891
892
\end{code}


%************************************************************************
%*									*
893
		Equality for Core types 
894
	(We don't use instances so that we know where it happens)
895
896
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
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
925
926
    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
		 | Just t2' <- coreView t2 = eq env t1 t2' 
927
928
929
930

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

932

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

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

\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

969
\begin{code}
970
971
972
973
974
975
976
977
978
979
980
981
982
983
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))
984

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

989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
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
1019
cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
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
1030
cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
1031
1032
1033
1034
1035
1036
1037
1038
1039
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 }
1040
1041
\end{code}

1042
1043
1044
1045
1046
1047
1048
1049
1050
1051

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

\begin{code}
data TvSubst 		
  = TvSubst InScopeSet 	-- The in-scope type variables
1052
	    TvSubstEnv	-- The substitution itself
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
			-- 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
1083
1084
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = emptyVarEnv
1085

1086
1087
1088
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
1089
-- Typically, env1 is the refinement to a base substitution env2
1090
1091
1092
1093
1094
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
1095
	--  *left* argument to plusVarEnv, because the right arg wins
1096
1097
1098
  where
    subst1 = TvSubst in_scope env1

1099
emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1100

1101
1102
1103
isEmptyTvSubst :: TvSubst -> Bool
isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env

1104
1105
1106
mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
mkTvSubst = TvSubst

1107
1108
1109
1110
1111
1112
1113
1114
1115
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

1116
1117
1118
notElemTvSubst :: TyVar -> TvSubst -> Bool
notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)

1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
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))

1132
-- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1133
1134
1135
-- the types given; but it's just a thunk so with a bit of luck
-- it'll never be evaluated

1136
1137
mkOpenTvSubst :: TvSubstEnv -> TvSubst
mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1138

1139
1140
zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
zipOpenTvSubst tyvars tys 
1141
1142
1143
1144
1145
#ifdef DEBUG
  | length tyvars /= length tys
  = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
  | otherwise
#endif
1146
1147
1148
1149
1150
1151
1152
1153
1154
  = 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
1155
1156
1157
1158
1159
1160
1161
zipTopTvSubst tyvars tys 
#ifdef DEBUG
  | length tyvars /= length tys
  = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
  | otherwise
#endif
  = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187

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"
1188
1189
zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
-- zip_ty_env _ _ env = env
1190
1191
1192

instance Outputable TvSubst where
  ppr (TvSubst ins env) 
1193
1194
1195
    = brackets $ sep[ ptext SLIT("TvSubst"),
		      nest 2 (ptext SLIT("In scope:") <+> ppr ins), 
		      nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
\end{code}

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

\begin{code}
substTyWith :: [TyVar]