Type.lhs 53.6 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
\begin{code}
9
{-# OPTIONS -w #-}
10
11
12
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
Ian Lynagh's avatar
Ian Lynagh committed
13
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
14
15
-- for details

16
module Type (
17
        -- re-exports from TypeRep
18
	TyThing(..), Type, PredType(..), ThetaType, 
19
	funTyCon,
20

21
22
	-- Kinds
        Kind, SimpleKind, KindVar,
23
        kindFunResult, splitKindFunTys, splitKindFunTysN,
24
25
26
27
28
29
30
31
32
33
34

        liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
        argTypeKindTyCon, ubxTupleKindTyCon,

        liftedTypeKind, unliftedTypeKind, openTypeKind,
        argTypeKind, ubxTupleKind,

        tySuperKind, coSuperKind, 

        isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
        isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
35
        isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
36
37
38
39
	mkArrowKind, mkArrowKinds,

        isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
        isSubKindCon,
40

41
42
	-- Re-exports from TyCon
	PrimRep(..),
43

44
45
	mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,

46
47
	mkAppTy, mkAppTys, splitAppTy, splitAppTys, 
	splitAppTy_maybe, repSplitAppTy_maybe,
48

49
50
	mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
	splitFunTys, splitFunTysN,
51
	funResultTy, funArgTy, zipFunTys, isFunTy,
52

53
	mkTyConApp, mkTyConTy, 
54
	tyConAppTyCon, tyConAppArgs, 
55
56
	splitTyConApp_maybe, splitTyConApp, 
        splitNewTyConApp_maybe, splitNewTyConApp,
57

mnislaih's avatar
mnislaih committed
58
	repType, repType', typePrimRep, coreView, tcView, kindView,
59

60
	mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
61
	applyTy, applyTys, isForAllTy, dropForAlls,
62

63
	-- Source types
64
	predTypeRep, mkPredTy, mkPredTys, pprSourceTyCon, mkFamilyTyConApp,
65

66
	-- Newtypes
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
67
	newTyConInstRhs,
68

69
	-- Lifting and boxity
70
71
	isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
	isStrictType, isStrictPred, 
72

73
	-- Free variables
74
	tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
75
	typeKind, addFreeTyVars,
76

77
78
79
        -- Type families
        tyFamInsts,

80
	-- Tidying up for printing
81
82
83
84
85
	tidyType,      tidyTypes,
	tidyOpenType,  tidyOpenTypes,
	tidyTyVarBndr, tidyFreeTyVars,
	tidyOpenTyVar, tidyOpenTyVars,
	tidyTopType,   tidyPred,
86
	tidyKind,
87

88
	-- Comparison
89
	coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
90
	tcEqPred, tcCmpPred, tcEqTypeX, tcPartOfType, tcPartOfPred,
91

92
	-- Seq
93
	seqType, seqTypes,
94

95
	-- Type substitutions
96
97
	TvSubstEnv, emptyTvSubstEnv,	-- Representation widely visible
	TvSubst(..), emptyTvSubst,	-- Representation visible to a few friends
98
	mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
99
	getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
100
 	extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
101
        isEmptyTvSubst,
102
103

	-- Performing substitution on types
104
	substTy, substTys, substTyWith, substTheta, 
105
	substPred, substTyVar, substTyVars, substTyVarBndr, deShadowTy, lookupTyVar,
106

107
	-- Pretty-printing
108
	pprType, pprParendType, pprTypeApp, pprTyThingCategory, pprTyThing, pprForAll,
109
	pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
110
    ) where
111

112
113
#include "HsVersions.h"

114
115
116
117
118
-- We import the representation and primitive functions from TypeRep.
-- Many things are reexported, but not the representation!

import TypeRep

119
-- friends:
120
import Var
121
122
123
import VarEnv
import VarSet

124
125
126
127
import Name
import Class
import PrelNames
import TyCon
128

129
-- others
130
131
import StaticFlags
import Util
132
import Outputable
133
import UniqSet
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
134

135
import Data.List
136
import Data.Maybe	( isJust )
137
138
\end{code}

139

140
141
142
143
144
145
146
147
148
149
150
%************************************************************************
%*									*
		Type representation
%*									*
%************************************************************************

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

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

168
169
170
-- 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
171
172
173
coreView (PredTy p)
  | isEqPred p             = Nothing
  | otherwise    	   = Just (predTypeRep p)
174
175
176
177
178
179
180
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

181
182


183
184
185
186
187
188
189
190
-----------------------------------------------
{-# 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
191
192
193
194
195
196
197
198

-----------------------------------------------
{-# 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
199
200
201
\end{code}


202
203
204
205
206
%************************************************************************
%*									*
\subsection{Constructor-specific functions}
%*									*
%************************************************************************
sof's avatar
sof committed
207
208


209
210
211
---------------------------------------------------------------------
				TyVarTy
				~~~~~~~
212
\begin{code}
213
mkTyVarTy  :: TyVar   -> Type
214
mkTyVarTy  = TyVarTy
215

216
mkTyVarTys :: [TyVar] -> [Type]
217
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
218

219
getTyVar :: String -> Type -> TyVar
220
221
222
getTyVar msg ty = case getTyVar_maybe ty of
		    Just tv -> tv
		    Nothing -> panic ("getTyVar: " ++ msg)
223

224
isTyVarTy :: Type -> Bool
225
226
227
isTyVarTy ty = isJust (getTyVar_maybe ty)

getTyVar_maybe :: Type -> Maybe TyVar
228
229
230
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) 	 	    = Just tv  
getTyVar_maybe other	         	    = Nothing
231

232
233
234
\end{code}


235
236
237
238
239
240
---------------------------------------------------------------------
				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.
241

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

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

273
-------------
274
splitAppTy_maybe :: Type -> Maybe (Type, Type)
275
276
277
splitAppTy_maybe ty | Just ty' <- coreView ty
		    = splitAppTy_maybe ty'
splitAppTy_maybe ty = repSplitAppTy_maybe ty
278

279
280
281
282
283
-------------
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)
284
285
286
287
288
289
repSplitAppTy_maybe (TyConApp tc tys) 
  | not (isOpenSynTyCon tc) || length tys > tyConArity tc 
  = case snocView tys of       -- never create unsaturated type family apps
      Just (tys', ty') -> Just (TyConApp tc tys', ty')
      Nothing	       -> Nothing
repSplitAppTy_maybe _other = Nothing
290
-------------
291
splitAppTy :: Type -> (Type, Type)
292
293
294
splitAppTy ty = case splitAppTy_maybe ty of
			Just pr -> pr
			Nothing -> panic "splitAppTy"
295

296
-------------
297
splitAppTys :: Type -> (Type, [Type])
298
splitAppTys ty = split ty ty []
299
  where
300
    split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
301
    split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
302
303
304
305
306
307
308
    split orig_ty (TyConApp tc tc_args) args 
      = let -- keep type families saturated
            n | isOpenSynTyCon tc = tyConArity tc
              | otherwise         = 0
            (tc_args1, tc_args2)  = splitAt n tc_args
        in
        (TyConApp tc tc_args1, tc_args2 ++ args)
309
    split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
310
					       (TyConApp funTyCon [], [ty1,ty2])
311
    split orig_ty ty		        args = (orig_ty, args)
312

313
314
\end{code}

315
316
317
318
319

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

320
\begin{code}
321
mkFunTy :: Type -> Type -> Type
322
mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
323
mkFunTy arg res = FunTy arg res
324

325
mkFunTys :: [Type] -> Type -> Type
326
mkFunTys tys ty = foldr mkFunTy ty tys
327

328
329
330
isFunTy :: Type -> Bool 
isFunTy ty = isJust (splitFunTy_maybe ty)

331
splitFunTy :: Type -> (Type, Type)
332
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
333
splitFunTy (FunTy arg res)   = (arg, res)
334
splitFunTy other	     = pprPanic "splitFunTy" (ppr other)
335

336
splitFunTy_maybe :: Type -> Maybe (Type, Type)
337
splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
338
339
splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
splitFunTy_maybe other	           = Nothing
340

341
splitFunTys :: Type -> ([Type], Type)
342
splitFunTys ty = split [] ty ty
343
  where
344
    split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
345
346
    split args orig_ty (FunTy arg res) 	 = split (arg:args) res res
    split args orig_ty ty                = (reverse args, orig_ty)
347

348
349
350
351
352
353
354
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) }}

355
356
357
zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
  where
358
    split acc []     nty ty  	           = (reverse acc, nty)
359
360
    split acc xs     nty ty 
	  | Just ty' <- coreView ty 	   = split acc xs nty ty'
361
    split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
362
    split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
363
364
    
funResultTy :: Type -> Type
365
funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
366
funResultTy (FunTy arg res)   = res
367
funResultTy ty		      = pprPanic "funResultTy" (ppr ty)
368
369

funArgTy :: Type -> Type
370
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
371
funArgTy (FunTy arg res)   = arg
372
funArgTy ty		   = pprPanic "funArgTy" (ppr ty)
373
374
375
\end{code}


376
377
378
---------------------------------------------------------------------
				TyConApp
				~~~~~~~~
379
@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
380
as apppropriate.
381

382
\begin{code}
383
mkTyConApp :: TyCon -> [Type] -> Type
384
mkTyConApp tycon tys
385
  | isFunTyCon tycon, [ty1,ty2] <- tys
386
  = FunTy ty1 ty2
387

388
  | otherwise
389
  = TyConApp tycon tys
390

391
mkTyConTy :: TyCon -> Type
392
mkTyConTy tycon = mkTyConApp tycon []
393
394
395
396
397

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

398
tyConAppTyCon :: Type -> TyCon
399
tyConAppTyCon ty = fst (splitTyConApp ty)
400
401

tyConAppArgs :: Type -> [Type]
402
tyConAppArgs ty = snd (splitTyConApp ty)
403
404
405
406

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

409
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
410
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
411
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
412
splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
413
splitTyConApp_maybe other	      = Nothing
414
415
416
417
418
419
420
421
422
423
424
425
426
427

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

428
newTyConInstRhs :: TyCon -> [Type] -> Type
429
430
431
432
433
434
435
436
-- Unwrap one 'layer' of newtype
-- Use the eta'd version if possible
newTyConInstRhs tycon tys 
    = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs )
      mkAppTys (substTyWith tvs tys1 ty) tys2
  where
    (tvs, ty)    = newTyConEtadRhs tycon
    (tys1, tys2) = splitAtList tvs tys
sof's avatar
sof committed
437
\end{code}
438

439

440
441
442
443
444
445
446
447
---------------------------------------------------------------------
				SynTy
				~~~~~

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

449
450
451
452
453
454
455
456
	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.
457
458


459
460
		Representation types
		~~~~~~~~~~~~~~~~~~~~
461
462
repType looks through 
	(a) for-alls, and
463
464
465
	(b) synonyms
	(c) predicates
	(d) usage annotations
466
	(e) all newtypes, including recursive ones, but not newtype families
467
It's useful in the back end.
468
469
470

\begin{code}
repType :: Type -> Type
471
-- Only applied to types of kind *; hence tycons are saturated
472
repType ty | Just ty' <- coreView ty = repType ty'
473
474
repType (ForAllTy _ ty)  = repType ty
repType (TyConApp tc tys)
475
476
477
478
479
480
481
482
483
  | isNewTyCon tc
  , (tvs, rep_ty) <- newTyConRep tc
  = -- Recursive newtypes are opaque to coreView
    -- but we must expand them here.  Sure to
    -- be saturated because repType is only applied
    -- to types of kind *
    ASSERT( tys `lengthIs` tyConArity tc )
    repType (substTyWith tvs tys rep_ty)

484
485
repType ty = ty

mnislaih's avatar
mnislaih committed
486
487
488
489
490
491
492
493
494
495
-- 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


496
497
-- ToDo: this could be moved to the code generator, using splitTyConApp instead
-- of inspecting the type directly.
498
499
500
501
typePrimRep :: Type -> PrimRep
typePrimRep ty = case repType ty of
		   TyConApp tc _ -> tyConPrimRep tc
		   FunTy _ _	 -> PtrRep
502
		   AppTy _ _	 -> PtrRep	-- See note below
503
		   TyVarTy _	 -> PtrRep
504
		   other	 -> pprPanic "typePrimRep" (ppr ty)
505
506
507
508
509
	-- 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.
510
511
512
\end{code}


513
514
515
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
516
517

\begin{code}
518
mkForAllTy :: TyVar -> Type -> Type
519
520
mkForAllTy tyvar ty
  = mkForAllTys [tyvar] ty
521

522
mkForAllTys :: [TyVar] -> Type -> Type
523
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
524
525
526
527
528

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

530
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
531
splitForAllTy_maybe ty = splitFAT_m ty
532
  where
533
534
535
    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
536

537
splitForAllTys :: Type -> ([TyVar], Type)
538
splitForAllTys ty = split ty ty []
539
   where
540
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
541
542
     split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
     split orig_ty t		     tvs = (reverse tvs, orig_ty)
543
544
545

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

548
-- (mkPiType now in CoreUtils)
549

550
551
552
553
554
555
556
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. 
557

558
\begin{code}
559
applyTy :: Type -> Type -> Type
560
561
562
applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
applyTy other		 arg = panic "applyTy"
563

564
applyTys :: Type -> [Type] -> Type
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
-- 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
584
  = ASSERT2( n_tvs > 0, ppr orig_fun_ty )	-- Zero case gives infnite loop!
585
586
587
588
589
590
    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     
591
\end{code}
592

593

594
595
%************************************************************************
%*									*
596
\subsection{Source types}
597
598
%*									*
%************************************************************************
599

600
601
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.
602

603
Source types are always lifted.
604

605
The key function is predTypeRep which gives the representation of a source type:
606
607

\begin{code}
608
mkPredTy :: PredType -> Type
609
mkPredTy pred = PredTy pred
610
611

mkPredTys :: ThetaType -> [Type]
612
613
614
615
616
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.
617
-- Unwraps only the outermost level; for example, the result might
618
-- be a newtype application
619
620
predTypeRep (IParam _ ty)     = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
621
	-- Result might be a newtype application, but the consumer will
622
	-- look through that too if necessary
623
predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
624

625
626
627
628
629
630
631
632
633
634
635
636
637
638
mkFamilyTyConApp :: TyCon -> [Type] -> Type
-- Given a family instance TyCon and its arg types, return the
-- corresponding family type.  E.g.
--	data family T a
--	data instance T (Maybe b) = MkT b	-- Instance tycon :RTL
-- Then 
--	mkFamilyTyConApp :RTL Int  =  T (Maybe Int)
mkFamilyTyConApp tc tys
  | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
  , let fam_subst = zipTopTvSubst (tyConTyVars tc) tys
  = mkTyConApp fam_tc (substTys fam_subst fam_tys)
  | otherwise
  = mkTyConApp tc tys

639
-- Pretty prints a tycon, using the family instance in case of a
640
641
642
643
-- 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 
644
645
  | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
  = ppr $ fam_tc `TyConApp` tys	       -- can't be FunTyCon
646
647
  | otherwise
  = ppr tycon
648
\end{code}
649
650


651
652
653
654
655
656
657
658
659
%************************************************************************
%*									*
\subsection{Kinds and free variables}
%*									*
%************************************************************************

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


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

703
tyVarsOfTypes :: [Type] -> TyVarSet
704
705
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys

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

tyVarsOfTheta :: ThetaType -> TyVarSet
712
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
713

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

720

721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
%************************************************************************
%*									*
\subsection{Type families}
%*									*
%************************************************************************

Type family instances occuring in a type after expanding synonyms.

\begin{code}
tyFamInsts :: Type -> [(TyCon, [Type])]
tyFamInsts ty 
  | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
tyFamInsts (TyVarTy _)          = []
tyFamInsts (TyConApp tc tys) 
  | isOpenSynTyCon tc           = [(tc, tys)]
  | otherwise                   = concat (map tyFamInsts tys)
tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
\end{code}


743
744
745
746
747
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
748

749
750
tidyTy tidies up a type for printing in an error message, or in
an interface file.
751

752
It doesn't change the uniques at all, just the print names.
753
754

\begin{code}
755
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
756
tidyTyVarBndr env@(tidy_env, subst) tyvar
757
  = case tidyOccName tidy_env (getOccName name) of
758
759
760
761
762
763
764
765
766
      (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)
767
768
  where
    name = tyVarName tyvar
769

770
771
772
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
773
774
775
776
777
778
779
780
781
782
783
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
784

785
786
787
tidyType :: TidyEnv -> Type -> Type
tidyType env@(tidy_env, subst) ty
  = go ty
788
  where
789
790
791
    go (TyVarTy tv)	    = case lookupVarEnv subst tv of
				Nothing  -> TyVarTy tv
				Just tv' -> TyVarTy tv'
792
793
    go (TyConApp tycon tys) = let args = map go tys
			      in args `seqList` TyConApp tycon args
sof's avatar
sof committed
794
    go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
795
    go (PredTy sty)	    = PredTy (tidyPred env sty)
sof's avatar
sof committed
796
797
798
    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)
799
			      where
800
			        (envp, tvp) = tidyTyVarBndr env tv
801
802
803

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

804
tidyTypes env tys = map (tidyType env) tys
805

806
807
808
tidyPred :: TidyEnv -> PredType -> PredType
tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
809
tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
810
811
812
\end{code}


813
@tidyOpenType@ grabs the free type variables, tidies them
814
815
816
817
818
819
820
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
821
    env' = tidyFreeTyVars env (tyVarsOfType ty)
822
823
824
825
826
827

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

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
828
829
\end{code}

830
\begin{code}
831

832
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
833
tidyKind env k = tidyOpenType env k
834
835
836

\end{code}

837

838
839
%************************************************************************
%*									*
840
\subsection{Liftedness}
841
842
843
%*									*
%************************************************************************

844
\begin{code}
845
isUnLiftedType :: Type -> Bool
846
847
848
849
850
851
	-- 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

852
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
853
854
855
isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
isUnLiftedType other		 = False	
856

857
isUnboxedTupleType :: Type -> Bool
858
859
860
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
			   Just (tc, ty_args) -> isUnboxedTupleTyCon tc
			   other	      -> False
861

862
-- Should only be applied to *types*; hence the assert
863
isAlgType :: Type -> Bool
864
isAlgType ty = case splitTyConApp_maybe ty of
sof's avatar
sof committed
865
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
866
867
					      isAlgTyCon tc
			other		   -> False
868
869
\end{code}

870
871
872
873
874
875
876
877
@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}
878
879
isStrictType (PredTy pred)     = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
880
881
882
883
884
885
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
886
887
888
889
890
891
892
893
894
895
896
897
	-- 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
898
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
899
900
901
902
					      isPrimTyCon tc
			other		   -> False
\end{code}

903

904
905
906
907
908
909
910
911
912
913
914
915
%************************************************************************
%*									*
\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
916
seqType (PredTy p) 	  = seqPred p
917
918
919
920
921
922
923
924
925
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` ()
926

927
seqPred :: PredType -> ()
928
929
930
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
931
932
933
934
935
\end{code}


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

941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
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
968
969
    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
		 | Just t2' <- coreView t2 = eq env t1 t2' 
970
971
972
973

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

975

976
977
978
979
980
981
%************************************************************************
%*									*
		Comparision for source types 
	(We don't use instances so that we know where it happens)
%*									*
%************************************************************************
982

983
984
985
Note that 
	tcEqType, tcCmpType 
do *not* look through newtypes, PredTypes
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009

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

1010
1011
1012
1013
1014
Checks whether the second argument is a subterm of the first.  (We don't care
about binders, as we are only interested in syntactic subterms.)

\begin{code}
tcPartOfType :: Type -> Type -> Bool
1015
1016
tcPartOfType t1              t2 
  | tcEqType t1 t2              = True
1017
1018
tcPartOfType t1              t2 
  | Just t2' <- tcView t2       = tcPartOfType t1 t2'
1019
tcPartOfType _  (TyVarTy _)     = False
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
tcPartOfType t1 (AppTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
tcPartOfType t1 (FunTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
tcPartOfType t1 (PredTy p2)     = tcPartOfPred t1 p2
tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
tcPartOfType t1 (NoteTy _ t2)   = tcPartOfType t1 t2

tcPartOfPred :: Type -> PredType -> Bool
tcPartOfPred t1 (IParam _ t2)  = tcPartOfType t1 t2
tcPartOfPred t1 (ClassP _ ts)  = any (tcPartOfType t1) ts
tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
\end{code}

1033
1034
Now here comes the real worker

1035
\begin{code}
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
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))
1050

1051
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
1052
1053
cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
		   | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
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
1083
1084
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
1085
cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1086
1087
1088
1089
1090
1091
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
1092
1093
1094
1095
1096
1097
	-- 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)
1098
cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1099
1100
1101
1102
1103
1104

-- Constructor order: IParam < ClassP < EqPred
cmpPredX env (IParam {})     _		    = LT
cmpPredX env (ClassP {})    (IParam {})     = GT
cmpPredX env (ClassP {})    (EqPred {})     = LT
cmpPredX env (EqPred {})    _		    = GT
1105
1106
1107
1108
1109
1110
1111
1112
\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 }
1113
1114
\end{code}

1115
1116
1117
1118
1119
1120
1121
1122
1123
1124

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

\begin{code}
data TvSubst 		
  = TvSubst InScopeSet 	-- The in-scope type variables
1125
	    TvSubstEnv	-- The substitution itself
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1126
1127
	-- See Note [Apply Once]
	-- and Note [Extending the TvSubstEnv]
1128
1129
1130

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

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1131
1132
Note [Apply Once]
~~~~~~~~~~~~~~~~~
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
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
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180

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
  

1181
1182
1183
1184
1185
1186
1187
1188
1189
-------------------------------------------------------------- -}


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
1190
1191
emptyTvSubstEnv :: TvSubstEnv
emptyTvSubstEnv = emptyVarEnv
1192

1193
1194
1195
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
1196
-- Typically, env1 is the refinement to a base substitution env2
1197
1198
1199
1200
1201
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
1202
	--  *left* argument to plusVarEnv, because the right arg wins
1203
1204
1205
  where
    subst1 = TvSubst in_scope env1

1206
emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1207

1208
isEmptyTvSubst :: TvSubst -> Bool
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1209
	 -- See Note [Extending the TvSubstEnv]
1210
1211
isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env