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

6
Type - public interface
7

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

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

        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
        argTypeKindTyCon, ubxTupleKindTyCon,

        liftedTypeKind, unliftedTypeKind, openTypeKind,
        argTypeKind, ubxTupleKind,

        tySuperKind, coSuperKind, 

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

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

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

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

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

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

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

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

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

56
	-- Source types
57
	predTypeRep, mkPredTy, mkPredTys,
58
	tyConOrigHead, pprSourceTyCon,
59

60
	-- Newtypes
61
	splitRecNewType_maybe, newTyConInstRhs,
62

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

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

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

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

83
	-- Seq
84
	seqType, seqTypes,
85

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

	-- Performing substitution on types
95
	substTy, substTys, substTyWith, substTheta, 
96
	substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
97

98
	-- Pretty-printing
99
	pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprForAll,
100
	pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
101
    ) where
102

103
104
#include "HsVersions.h"

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

import TypeRep

110
-- friends:
111
import Var
112
113
114
import VarEnv
import VarSet

115
116
117
118
import Name
import Class
import PrelNames
import TyCon
119

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

126
import Data.Maybe	( isJust )
127
128
\end{code}

129

130
131
132
133
134
135
136
137
138
139
140
%************************************************************************
%*									*
		Type representation
%*									*
%************************************************************************

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

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

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
161
162
163
coreView (PredTy p)
  | isEqPred p             = Nothing
  | otherwise    	   = Just (predTypeRep p)
164
165
166
167
168
169
170
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

171
172


173
174
175
176
177
178
179
180
-----------------------------------------------
{-# 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
181
182
183
184
185
186
187
188

-----------------------------------------------
{-# 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
189
190
191
\end{code}


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


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

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

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

214
isTyVarTy :: Type -> Bool
215
216
217
isTyVarTy ty = isJust (getTyVar_maybe ty)

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

222
223
224
\end{code}


225
226
227
228
229
230
---------------------------------------------------------------------
				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.
231

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

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

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

269
270
271
272
273
274
275
276
277
278
-------------
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
-------------
279
splitAppTy :: Type -> (Type, Type)
280
281
282
splitAppTy ty = case splitAppTy_maybe ty of
			Just pr -> pr
			Nothing -> panic "splitAppTy"
283

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

295
296
\end{code}

297
298
299
300
301

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

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

307
mkFunTys :: [Type] -> Type -> Type
308
mkFunTys tys ty = foldr mkFunTy ty tys
309

310
311
312
isFunTy :: Type -> Bool 
isFunTy ty = isJust (splitFunTy_maybe ty)

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

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

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

330
331
332
333
334
335
336
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) }}

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

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


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

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

370
  | otherwise
371
  = TyConApp tycon tys
372

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

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

380
tyConAppTyCon :: Type -> TyCon
381
tyConAppTyCon ty = fst (splitTyConApp ty)
382
383

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

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

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

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

410
411
412
413
414
-- 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
415
\end{code}
416

417

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

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

427
428
429
430
431
432
433
434
	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.
435
436


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

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

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


471
472
473
474
475
-- 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
476

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

492
493
494
\end{code}


495
496
497
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
498
499

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

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

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

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

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

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

530
-- (mkPiType now in CoreUtils)
531

532
533
534
535
536
537
538
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. 
539

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

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

575

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

582
583
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.
584

585
Source types are always lifted.
586

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

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

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

-- The original head is the tycon and its variables for a vanilla tycon and it
-- is the family tycon and its type indexes for a family instance.
tyConOrigHead :: TyCon -> (TyCon, [Type])
tyConOrigHead tycon = case tyConFamInst_maybe tycon of
		        Nothing      -> (tycon, mkTyVarTys (tyConTyVars tycon))
			Just famInst -> famInst
613
614

-- Pretty prints a tycon, using the family instance in case of a
615
616
617
618
619
620
621
622
-- representation tycon.  For example
--  	e.g.  data T [a] = ...
-- In that case we want to print `T [a]', where T is the family TyCon
pprSourceTyCon tycon 
  | Just (repTyCon, tys) <- tyConFamInst_maybe tycon
  = ppr $ repTyCon `TyConApp` tys	       -- can't be FunTyCon
  | otherwise
  = ppr tycon
623
\end{code}
624
625


626
627
628
629
630
%************************************************************************
%*									*
		NewTypes
%*									*
%************************************************************************
631

632
633
634
\begin{code}
splitRecNewType_maybe :: Type -> Maybe Type
-- Sometimes we want to look through a recursive newtype, and that's what happens here
635
-- It only strips *one layer* off, so the caller will usually call itself recursively
636
-- Only applied to types of kind *, hence the newtype is always saturated
637
638
splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
splitRecNewType_maybe (TyConApp tc tys)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
639
  | isClosedNewTyCon tc
640
641
642
643
  = ASSERT( tys `lengthIs` tyConArity tc )	-- splitRecNewType_maybe only be applied 
						-- 	to *types* (of kind *)
    ASSERT( isRecursiveTyCon tc ) 		-- Guaranteed by coreView
    case newTyConRhs tc of
644
645
646
	(tvs, rep_ty) -> ASSERT( length tvs == length tys )
			 Just (substTyWith tvs tys rep_ty)
	
647
splitRecNewType_maybe other = Nothing
648
649
650



651
652
\end{code}

653

654
655
656
657
658
659
660
661
662
%************************************************************************
%*									*
\subsection{Kinds and free variables}
%*									*
%************************************************************************

---------------------------------------------------------------------
		Finding the kind of a type
		~~~~~~~~~~~~~~~~~~~~~~~~~~
663
\begin{code}
664
typeKind :: Type -> Kind
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
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
689
690
691
\end{code}


692
693
694
---------------------------------------------------------------------
		Free variables of a type
		~~~~~~~~~~~~~~~~~~~~~~~~
695
\begin{code}
696
tyVarsOfType :: Type -> TyVarSet
697
-- NB: for type synonyms tyVarsOfType does *not* expand the synonym
698
tyVarsOfType (TyVarTy tv)		= unitVarSet tv
699
tyVarsOfType (TyConApp tycon tys)	= tyVarsOfTypes tys
700
tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
701
tyVarsOfType (PredTy sty)		= tyVarsOfPred sty
702
703
tyVarsOfType (FunTy arg res)		= tyVarsOfType arg `unionVarSet` tyVarsOfType res
tyVarsOfType (AppTy fun arg)		= tyVarsOfType fun `unionVarSet` tyVarsOfType arg
704
tyVarsOfType (ForAllTy tyvar ty)	= delVarSet (tyVarsOfType ty) tyvar
705

706
tyVarsOfTypes :: [Type] -> TyVarSet
707
708
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys

709
tyVarsOfPred :: PredType -> TyVarSet
710
711
712
tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
713
714

tyVarsOfTheta :: ThetaType -> TyVarSet
715
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
716

717
-- Add a Note with the free tyvars to the top of the type
718
addFreeTyVars :: Type -> Type
719
720
addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
addFreeTyVars ty			     = NoteTy (FTVNote (tyVarsOfType ty)) ty
721
\end{code}
722

723

724
725
726
727
728
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
729

730
731
tidyTy tidies up a type for printing in an error message, or in
an interface file.
732

733
It doesn't change the uniques at all, just the print names.
734
735

\begin{code}
736
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
737
tidyTyVarBndr env@(tidy_env, subst) tyvar
738
  = case tidyOccName tidy_env (getOccName name) of
739
740
741
742
743
744
745
746
747
      (tidy', occ') -> ((tidy', subst'), tyvar'')
	where
	  subst' = extendVarEnv subst tyvar tyvar''
	  tyvar' = setTyVarName tyvar name'
	  name'  = tidyNameOcc name occ'
		-- Don't forget to tidy the kind for coercions!
	  tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
		  | otherwise	  = tyvar'
	  kind'  = tidyType env (tyVarKind tyvar)
748
749
  where
    name = tyVarName tyvar
750

751
752
753
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
754
755
756
757
758
759
760
761
762
763
764
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
765

766
767
768
tidyType :: TidyEnv -> Type -> Type
tidyType env@(tidy_env, subst) ty
  = go ty
769
  where
770
771
772
    go (TyVarTy tv)	    = case lookupVarEnv subst tv of
				Nothing  -> TyVarTy tv
				Just tv' -> TyVarTy tv'
773
774
    go (TyConApp tycon tys) = let args = map go tys
			      in args `seqList` TyConApp tycon args
sof's avatar
sof committed
775
    go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
776
    go (PredTy sty)	    = PredTy (tidyPred env sty)
sof's avatar
sof committed
777
778
779
    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)
780
			      where
781
			        (envp, tvp) = tidyTyVarBndr env tv
782
783
784

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

785
tidyTypes env tys = map (tidyType env) tys
786

787
788
789
tidyPred :: TidyEnv -> PredType -> PredType
tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
790
tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
791
792
793
\end{code}


794
@tidyOpenType@ grabs the free type variables, tidies them
795
796
797
798
799
800
801
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
802
    env' = tidyFreeTyVars env (tyVarsOfType ty)
803
804
805
806
807
808

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

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
809
810
\end{code}

811
\begin{code}
812

813
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
814
tidyKind env k = tidyOpenType env k
815
816
817

\end{code}

818

819
820
%************************************************************************
%*									*
821
\subsection{Liftedness}
822
823
824
%*									*
%************************************************************************

825
\begin{code}
826
isUnLiftedType :: Type -> Bool
827
828
829
830
831
832
	-- 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

833
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
834
835
836
isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
isUnLiftedType other		 = False	
837

838
isUnboxedTupleType :: Type -> Bool
839
840
841
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
			   Just (tc, ty_args) -> isUnboxedTupleTyCon tc
			   other	      -> False
842

843
-- Should only be applied to *types*; hence the assert
844
isAlgType :: Type -> Bool
845
isAlgType ty = case splitTyConApp_maybe ty of
sof's avatar
sof committed
846
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
847
848
					      isAlgTyCon tc
			other		   -> False
849
850
\end{code}

851
852
853
854
855
856
857
858
@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}
859
860
isStrictType (PredTy pred)     = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
861
862
863
864
865
866
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
867
868
869
870
871
872
873
874
875
876
877
878
	-- 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
879
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
880
881
882
883
					      isPrimTyCon tc
			other		   -> False
\end{code}

884

885
886
887
888
889
890
891
892
893
894
895
896
%************************************************************************
%*									*
\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
897
seqType (PredTy p) 	  = seqPred p
898
899
900
901
902
903
904
905
906
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` ()
907

908
seqPred :: PredType -> ()
909
910
911
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
912
913
914
915
916
\end{code}


%************************************************************************
%*									*
917
		Equality for Core types 
918
	(We don't use instances so that we know where it happens)
919
920
921
%*									*
%************************************************************************

922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
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
949
950
    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
		 | Just t2' <- coreView t2 = eq env t1 t2' 
951
952
953
954

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

956

957
958
959
960
961
962
%************************************************************************
%*									*
		Comparision for source types 
	(We don't use instances so that we know where it happens)
%*									*
%************************************************************************
963

964
965
966
Note that 
	tcEqType, tcCmpType 
do *not* look through newtypes, PredTypes
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992

\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

993
\begin{code}
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
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))
1008

1009
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
1010
1011
cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
		   | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
1012

1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
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
1043
cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1044
1045
1046
1047
1048
1049
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
1050
1051
1052
1053
1054
1055
	-- Compare names only for implicit parameters
	-- This comparison is used exclusively (I believe) 
	-- for the Avails finite map built in TcSimplify
	-- If the types differ we keep them distinct so that we see 
	-- a distinct pair to run improvement on 
cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1056
cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1057
1058
1059
1060
1061
1062

-- Constructor order: IParam < ClassP < EqPred
cmpPredX env (IParam {})     _		    = LT
cmpPredX env (ClassP {})    (IParam {})     = GT
cmpPredX env (ClassP {})    (EqPred {})     = LT
cmpPredX env (EqPred {})    _		    = GT
1063
1064
1065
1066
1067
1068
1069
1070
\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 }
1071
1072
\end{code}

1073
1074
1075
1076
1077
1078
1079
1080
1081
1082

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

\begin{code}
data TvSubst 		
  = TvSubst InScopeSet 	-- The in-scope type variables
1083
	    TvSubstEnv	-- The substitution itself
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1084
1085
	-- See Note [Apply Once]
	-- and Note [Extending the TvSubstEnv]
1086
1087
1088

{- ----------------------------------------------------------

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1089
1090
Note [Apply Once]
~~~~~~~~~~~~~~~~~
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
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.
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
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
1133
1134
1135
1136
1137
1138

Note [Extending the TvSubst]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The following invariant should hold of a TvSubst

	The in-scope set is needed *only* to
	guide the generation of fresh uniques

	In particular, the *kind* of the type variables in 
	the in-scope set is not relevant

This invariant allows a short-cut when the TvSubstEnv is empty:
if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
then (substTy subst ty) does nothing.

For example, consider:
	(/\a. /\b:(a~Int). ...b..) Int
We substitute Int for 'a'.  The Unique of 'b' does not change, but
nevertheless we add 'b' to the TvSubstEnv, because b's type does change

This invariant has several crucial consequences:

* In substTyVarBndr, we need extend the TvSubstEnv 
	- if the unique has changed
	- or if the kind has changed

* In substTyVar, we do not need to consult the in-scope set;
  the TvSubstEnv is enough

* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
  

1139
1140
1141
1142
1143
1144
1145
1146
1147
-------------------------------------------------------------- -}


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
1148
1149
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = emptyVarEnv
1150

1151
1152
1153
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
1154
-- Typically, env1 is the refinement to a base substitution env2
1155
1156
1157
1158
1159
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
1160
	--  *left* argument to plusVarEnv, because the right arg wins
1161
1162
1163
  where
    subst1 = TvSubst in_scope env1

1164
emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1165

1166
isEmptyTvSubst :: TvSubst -> Bool
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1167
	 -- See Note [Extending the TvSubstEnv]
1168
1169
isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env

1170
1171
1172
mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
mkTvSubst = TvSubst

1173
1174
1175
1176
1177
1178
1179
1180
1181
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

1182
1183
1184
notElemTvSubst :: TyVar -> TvSubst -> Bool
notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)

1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
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))

1198
-- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1199
1200
12