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

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

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

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

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

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

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

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

30
	mkSynTy, 
31

32
	repType, typePrimRep, coreView, deepCoreView,
33

34
	mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
35
	applyTy, applyTys, isForAllTy, dropForAlls,
36

37
	-- Source types
38
	predTypeRep, mkPredTy, mkPredTys,
39

40
	-- Newtypes
41
	splitRecNewType_maybe,
42

43
	-- Lifting and boxity
44
45
	isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
	isStrictType, isStrictPred, 
46

47
	-- Free variables
48
	tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
49
	typeKind, addFreeTyVars,
50

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

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

62
	-- Seq
63
	seqType, seqTypes,
64

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

	-- Performing substitution on types
73
	substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
74
	deShadowTy, 
75

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

81
82
#include "HsVersions.h"

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

import TypeRep

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

94
import Name	( NamedThing(..), mkInternalName, tidyOccName )
95
import Class	( Class, classTyCon )
96
import TyCon	( TyCon, isRecursiveTyCon, isPrimTyCon,
97
		  isUnboxedTupleTyCon, isUnLiftedTyCon,
98
		  isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
99
		  isAlgTyCon, isSynTyCon, tyConArity, newTyConRhs_maybe,
100
	          tyConKind, getSynTyConDefn, PrimRep(..), tyConPrimRep,
101
102
		)

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

113

114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
%************************************************************************
%*									*
		Type representation
%*									*
%************************************************************************

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

\begin{code}
{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
-- Srips off the *top layer only* of a type to give 
-- its underlying representation type. 
-- Returns Nothing if there is nothing to look through.
--
-- By being non-recursive and inlined, this case analysis gets efficiently
-- joined onto the case analysis that the caller is already doing
coreView (NoteTy _ ty) 	   = Just ty
coreView (PredTy p)    	   = Just (predTypeRep p)
coreView (TyConApp tc tys) = expandNewTcApp tc tys
coreView ty		   = Nothing

136
137
138
139
140
141
142
143
144
145
146
deepCoreView :: Type -> Type
-- Apply coreView recursively
deepCoreView ty
  | Just ty' <- coreView ty    = deepCoreView ty'
deepCoreView (TyVarTy tv)      = TyVarTy tv
deepCoreView (TyConApp tc tys) = TyConApp tc (map deepCoreView tys)
deepCoreView (AppTy t1 t2)     = AppTy (deepCoreView t1) (deepCoreView t2)
deepCoreView (FunTy t1 t2)     = FunTy (deepCoreView t1) (deepCoreView t2)
deepCoreView (ForAllTy tv ty)  = ForAllTy tv (deepCoreView ty)
	-- No NoteTy, no PredTy

147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
expandNewTcApp :: TyCon -> [Type] -> Maybe Type
-- A local helper function (not exported)
-- Expands *the outermoset level of* a newtype application to 
--	*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)

expandNewTcApp tc tys = case newTyConRhs_maybe tc tys of
			  Nothing          -> Nothing
			  Just (tenv, rhs) -> Just (substTy (mkTopTvSubst tenv) rhs)
\end{code}


168
169
170
171
172
%************************************************************************
%*									*
\subsection{Constructor-specific functions}
%*									*
%************************************************************************
sof's avatar
sof committed
173
174


175
176
177
---------------------------------------------------------------------
				TyVarTy
				~~~~~~~
178
\begin{code}
179
mkTyVarTy  :: TyVar   -> Type
180
mkTyVarTy  = TyVarTy
181

182
mkTyVarTys :: [TyVar] -> [Type]
183
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
184

185
getTyVar :: String -> Type -> TyVar
186
187
188
getTyVar msg ty = case getTyVar_maybe ty of
		    Just tv -> tv
		    Nothing -> panic ("getTyVar: " ++ msg)
189

190
isTyVarTy :: Type -> Bool
191
192
193
isTyVarTy ty = isJust (getTyVar_maybe ty)

getTyVar_maybe :: Type -> Maybe TyVar
194
195
196
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
getTyVar_maybe (TyVarTy tv) 	 	    = Just tv  
getTyVar_maybe other	         	    = Nothing
197
198
199
\end{code}


200
201
202
203
204
205
---------------------------------------------------------------------
				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.
206

207
\begin{code}
208
mkAppTy orig_ty1 orig_ty2
209
  = mk_app orig_ty1
210
  where
211
    mk_app (NoteTy _ ty1)    = mk_app ty1
212
    mk_app (TyConApp tc tys) = mkGenTyConApp tc (tys ++ [orig_ty2])
213
    mk_app ty1		     = AppTy orig_ty1 orig_ty2
214
215
216
217
218
219
220
221
	-- We call mkGenTyConApp because the TyConApp could be an 
	-- 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
222

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

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

247
splitAppTy :: Type -> (Type, Type)
248
249
250
splitAppTy ty = case splitAppTy_maybe ty of
			Just pr -> pr
			Nothing -> panic "splitAppTy"
251

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

263
264
265
266
267

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

268
\begin{code}
269
mkFunTy :: Type -> Type -> Type
270
mkFunTy arg res = FunTy arg res
271

272
mkFunTys :: [Type] -> Type -> Type
273
mkFunTys tys ty = foldr FunTy ty tys
274

275
276
277
isFunTy :: Type -> Bool 
isFunTy ty = isJust (splitFunTy_maybe ty)

278
splitFunTy :: Type -> (Type, Type)
279
splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
280
splitFunTy (FunTy arg res)   = (arg, res)
281
splitFunTy other	     = pprPanic "splitFunTy" (ppr other)
282

283
splitFunTy_maybe :: Type -> Maybe (Type, Type)
284
splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
285
286
splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
splitFunTy_maybe other	           = Nothing
287

288
splitFunTys :: Type -> ([Type], Type)
289
splitFunTys ty = split [] ty ty
290
  where
291
    split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
292
293
    split args orig_ty (FunTy arg res) 	 = split (arg:args) res res
    split args orig_ty ty                = (reverse args, orig_ty)
294

295
296
297
298
299
300
301
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) }}

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

funArgTy :: Type -> Type
317
funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
318
funArgTy (FunTy arg res)   = arg
319
funArgTy ty		   = pprPanic "funArgTy" (ppr ty)
320
321
322
\end{code}


323
324
325
---------------------------------------------------------------------
				TyConApp
				~~~~~~~~
326
@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
327
as apppropriate.
328

329
\begin{code}
330
331
332
333
334
mkGenTyConApp :: TyCon -> [Type] -> Type
mkGenTyConApp tc tys
  | isSynTyCon tc = mkSynTy tc tys
  | otherwise     = mkTyConApp tc tys

335
mkTyConApp :: TyCon -> [Type] -> Type
336
-- Assumes TyCon is not a SynTyCon; use mkSynTy instead for those
337
mkTyConApp tycon tys
338
  | isFunTyCon tycon, [ty1,ty2] <- tys
339
  = FunTy ty1 ty2
340

341
342
343
344
  | otherwise
  = ASSERT(not (isSynTyCon tycon))
    TyConApp tycon tys

345
mkTyConTy :: TyCon -> Type
346
mkTyConTy tycon = mkTyConApp tycon []
347
348
349
350
351

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

352
tyConAppTyCon :: Type -> TyCon
353
tyConAppTyCon ty = fst (splitTyConApp ty)
354
355

tyConAppArgs :: Type -> [Type]
356
tyConAppArgs ty = snd (splitTyConApp ty)
357
358
359
360

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

363
splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
364
splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
365
splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
366
splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
367
splitTyConApp_maybe other	      = Nothing
sof's avatar
sof committed
368
\end{code}
369

370

371
372
373
374
---------------------------------------------------------------------
				SynTy
				~~~~~

375
\begin{code}
376
377
378
379
mkSynTy tycon tys
  | n_args == arity	-- Exactly saturated
  = mk_syn tys
  | n_args >  arity	-- Over-saturated
380
381
382
383
  = case splitAt arity tys of { (as,bs) -> mkAppTys (mk_syn as) bs }
	-- Its important to use mkAppTys, rather than (foldl AppTy),
	-- because (mk_syn as) might well return a partially-applied
	-- type constructor; indeed, usually will!
384
385
386
387
388
389
390
391
  | otherwise		-- Un-saturated
  = TyConApp tycon tys
	-- For the un-saturated case we build TyConApp directly
	-- (mkTyConApp ASSERTs that the tc isn't a SynTyCon).
	-- Here we are relying on checkValidType to find
	-- the error.  What we can't do is use mkSynTy with
	-- too few arg tys, because that is utterly bogus.

392
  where
393
394
395
396
397
398
    mk_syn tys = NoteTy (SynNote (TyConApp tycon tys))
			(substTyWith tyvars tys body)

    (tyvars, body) = ASSERT( isSynTyCon tycon ) getSynTyConDefn tycon
    arity 	   = tyConArity tycon
    n_args	   = length tys
399
400
\end{code}

401
402
403
404
Notes on type synonyms
~~~~~~~~~~~~~~~~~~~~~~
The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
to return type synonyms whereever possible. Thus
405

406
407
408
409
410
411
412
413
	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.
414
415


416
417
		Representation types
		~~~~~~~~~~~~~~~~~~~~
418
419
repType looks through 
	(a) for-alls, and
420
421
422
	(b) synonyms
	(c) predicates
	(d) usage annotations
423
	(e) all newtypes, including recursive ones
424
It's useful in the back end.
425
426
427

\begin{code}
repType :: Type -> Type
428
-- Only applied to types of kind *; hence tycons are saturated
429
430
repType (ForAllTy _ ty)   = repType ty
repType (NoteTy   _ ty)   = repType ty
431
repType (PredTy  p)       = repType (predTypeRep p)
432
433
repType (TyConApp tc tys) 
  | isNewTyCon tc 	  = ASSERT( tys `lengthIs` tyConArity tc )
434
			    repType (new_type_rep tc tys)
435
repType ty	 	  = ty
436

437
438
-- ToDo: this could be moved to the code generator, using splitTyConApp instead
-- of inspecting the type directly.
439
440
441
442
typePrimRep :: Type -> PrimRep
typePrimRep ty = case repType ty of
		   TyConApp tc _ -> tyConPrimRep tc
		   FunTy _ _	 -> PtrRep
443
		   AppTy _ _	 -> PtrRep	-- See note below
444
		   TyVarTy _	 -> PtrRep
445
		   other	 -> pprPanic "typePrimRep" (ppr ty)
446
447
448
449
450
	-- 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.
451
452
453
454
455
456

-- 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
457
458
459
\end{code}


460
461
462
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
463
464

\begin{code}
465
mkForAllTy :: TyVar -> Type -> Type
466
467
mkForAllTy tyvar ty
  = mkForAllTys [tyvar] ty
468

469
mkForAllTys :: [TyVar] -> Type -> Type
470
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
471
472
473
474
475

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

477
splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
478
splitForAllTy_maybe ty = splitFAT_m ty
479
  where
480
481
482
    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
483

484
splitForAllTys :: Type -> ([TyVar], Type)
485
splitForAllTys ty = split ty ty []
486
   where
487
     split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
488
489
     split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
     split orig_ty t		     tvs = (reverse tvs, orig_ty)
490
491
492

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

495
-- (mkPiType now in CoreUtils)
496

497
498
499
500
501
502
503
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. 
504

505
\begin{code}
506
applyTy :: Type -> Type -> Type
507
508
509
applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
applyTy other		 arg = panic "applyTy"
510

511
applyTys :: Type -> [Type] -> Type
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
-- 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
531
  = ASSERT2( n_tvs > 0, ppr orig_fun_ty )	-- Zero case gives infnite loop!
532
533
534
535
536
537
    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     
538
\end{code}
539

540

541
542
%************************************************************************
%*									*
543
\subsection{Source types}
544
545
%*									*
%************************************************************************
546

547
548
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.
549

550
Source types are always lifted.
551

552
The key function is predTypeRep which gives the representation of a source type:
553
554

\begin{code}
555
mkPredTy :: PredType -> Type
556
mkPredTy pred = PredTy pred
557
558

mkPredTys :: ThetaType -> [Type]
559
560
561
562
563
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.
564
-- Unwraps only the outermost level; for example, the result might
565
-- be a newtype application
566
567
predTypeRep (IParam _ ty)     = ty
predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
568
	-- Result might be a newtype application, but the consumer will
569
570
	-- look through that too if necessary
\end{code}
571
572


573
574
575
576
577
%************************************************************************
%*									*
		NewTypes
%*									*
%************************************************************************
578

579
580
581
\begin{code}
splitRecNewType_maybe :: Type -> Maybe Type
-- Sometimes we want to look through a recursive newtype, and that's what happens here
582
-- It only strips *one layer* off, so the caller will usually call itself recursively
583
-- Only applied to types of kind *, hence the newtype is always saturated
584
585
586
587
588
589
590
591
592
splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
splitRecNewType_maybe (TyConApp tc tys)
  | isNewTyCon tc
  = ASSERT( tys `lengthIs` tyConArity tc )	-- splitRecNewType_maybe only be applied 
						-- 	to *types* (of kind *)
    ASSERT( isRecursiveTyCon tc ) 		-- Guaranteed by coreView
    case newTyConRhs tc of
	(tvs, rep_ty) -> Just (substTyWith tvs tys rep_ty)

593
splitRecNewType_maybe other = Nothing
594
595
\end{code}

596

597
598
599
600
601
602
603
604
605
%************************************************************************
%*									*
\subsection{Kinds and free variables}
%*									*
%************************************************************************

---------------------------------------------------------------------
		Finding the kind of a type
		~~~~~~~~~~~~~~~~~~~~~~~~~~
606
\begin{code}
607
typeKind :: Type -> Kind
608

609
typeKind (TyVarTy tyvar)	= tyVarKind tyvar
610
typeKind (TyConApp tycon tys)	= foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
611
typeKind (NoteTy _ ty)		= typeKind ty
612
typeKind (PredTy _)		= liftedTypeKind -- Predicates are always 
613
						 -- represented by lifted types
614
615
typeKind (AppTy fun arg)	= kindFunResult (typeKind fun)
typeKind (FunTy arg res)	= liftedTypeKind
616
typeKind (ForAllTy tv ty)	= typeKind ty
617
618
619
\end{code}


620
621
622
---------------------------------------------------------------------
		Free variables of a type
		~~~~~~~~~~~~~~~~~~~~~~~~
623
\begin{code}
624
tyVarsOfType :: Type -> TyVarSet
625
tyVarsOfType (TyVarTy tv)		= unitVarSet tv
626
tyVarsOfType (TyConApp tycon tys)	= tyVarsOfTypes tys
627
tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
628
tyVarsOfType (NoteTy (SynNote ty1) ty2)	= tyVarsOfType ty2	-- See note [Syn] below
629
tyVarsOfType (PredTy sty)		= tyVarsOfPred sty
630
631
632
tyVarsOfType (FunTy arg res)		= tyVarsOfType arg `unionVarSet` tyVarsOfType res
tyVarsOfType (AppTy fun arg)		= tyVarsOfType fun `unionVarSet` tyVarsOfType arg
tyVarsOfType (ForAllTy tyvar ty)	= tyVarsOfType ty `minusVarSet` unitVarSet tyvar
633

634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
-- 			Note [Syn]
-- Consider
--	type T a = Int
-- What are the free tyvars of (T x)?  Empty, of course!  
-- Here's the example that Ralf Laemmel showed me:
--	foo :: (forall a. C u a -> C u a) -> u
--	mappend :: Monoid u => u -> u -> u
--
--	bar :: Monoid u => u
--	bar = foo (\t -> t `mappend` t)
-- We have to generalise at the arg to f, and we don't
-- want to capture the constraint (Monad (C u a)) because
-- it appears to mention a.  Pretty silly, but it was useful to him.


649
tyVarsOfTypes :: [Type] -> TyVarSet
650
651
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys

652
tyVarsOfPred :: PredType -> TyVarSet
653
654
tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
655
656

tyVarsOfTheta :: ThetaType -> TyVarSet
657
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
658

659
-- Add a Note with the free tyvars to the top of the type
660
addFreeTyVars :: Type -> Type
661
662
addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
addFreeTyVars ty			     = NoteTy (FTVNote (tyVarsOfType ty)) ty
663
\end{code}
664

665
666
667
668
669
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
670

671
672
tidyTy tidies up a type for printing in an error message, or in
an interface file.
673

674
It doesn't change the uniques at all, just the print names.
675
676

\begin{code}
677
678
679
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidyTyVarBndr (tidy_env, subst) tyvar
  = case tidyOccName tidy_env (getOccName name) of
680
      (tidy', occ') -> 	((tidy', subst'), tyvar')
681
682
683
		    where
			subst' = extendVarEnv subst tyvar tyvar'
			tyvar' = setTyVarName tyvar name'
684
			name'  = mkInternalName (getUnique name) occ' noSrcLoc
685
686
				-- Note: make a *user* tyvar, so it printes nicely
				-- Could extract src loc, but no need.
687
688
  where
    name = tyVarName tyvar
689

690
691
692
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
693
694
695
696
697
698
699
700
701
702
703
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
704

705
706
707
tidyType :: TidyEnv -> Type -> Type
tidyType env@(tidy_env, subst) ty
  = go ty
708
  where
709
710
711
    go (TyVarTy tv)	    = case lookupVarEnv subst tv of
				Nothing  -> TyVarTy tv
				Just tv' -> TyVarTy tv'
712
713
    go (TyConApp tycon tys) = let args = map go tys
			      in args `seqList` TyConApp tycon args
sof's avatar
sof committed
714
    go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
715
    go (PredTy sty)	    = PredTy (tidyPred env sty)
sof's avatar
sof committed
716
717
718
    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)
719
			      where
720
			        (envp, tvp) = tidyTyVarBndr env tv
721

sof's avatar
sof committed
722
    go_note (SynNote ty)        = SynNote $! (go ty)
723
724
    go_note note@(FTVNote ftvs) = note	-- No need to tidy the free tyvars

725
tidyTypes env tys = map (tidyType env) tys
726

727
728
729
tidyPred :: TidyEnv -> PredType -> PredType
tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
730
731
732
\end{code}


733
@tidyOpenType@ grabs the free type variables, tidies them
734
735
736
737
738
739
740
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
741
    env' = tidyFreeTyVars env (tyVarsOfType ty)
742
743
744
745
746
747

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

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
748
749
\end{code}

750

751

752
753
%************************************************************************
%*									*
754
\subsection{Liftedness}
755
756
757
%*									*
%************************************************************************

758
\begin{code}
759
isUnLiftedType :: Type -> Bool
760
761
762
763
764
765
	-- 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

766
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
767
768
769
isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
isUnLiftedType other		 = False	
770

771
isUnboxedTupleType :: Type -> Bool
772
773
774
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
			   Just (tc, ty_args) -> isUnboxedTupleTyCon tc
			   other	      -> False
775

776
-- Should only be applied to *types*; hence the assert
777
isAlgType :: Type -> Bool
778
isAlgType ty = case splitTyConApp_maybe ty of
sof's avatar
sof committed
779
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
780
781
					      isAlgTyCon tc
			other		   -> False
782
783
\end{code}

784
785
786
787
788
789
790
791
@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}
792
793
isStrictType (PredTy pred)     = isStrictPred pred
isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
794
795
796
797
798
799
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
800
801
802
803
804
805
806
807
808
809
810
811
	-- 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
812
			Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
813
814
815
816
					      isPrimTyCon tc
			other		   -> False
\end{code}

817

818
819
820
821
822
823
824
825
826
827
828
829
%************************************************************************
%*									*
\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
830
seqType (PredTy p) 	  = seqPred p
831
832
833
834
835
836
837
838
839
840
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 (SynNote ty)  = seqType ty
seqNote (FTVNote set) = sizeUniqSet set `seq` ()
841

842
seqPred :: PredType -> ()
843
844
seqPred (ClassP c tys) = c  `seq` seqTypes tys
seqPred (IParam n ty)  = n  `seq` seqType ty
845
846
847
848
849
\end{code}


%************************************************************************
%*									*
850
851
		Comparison of types
	(We don't use instances so that we know where it happens)
852
853
854
%*									*
%************************************************************************

855
856
857
858
Two flavours:

* tcEqType, tcCmpType do *not* look through newtypes, PredTypes
* coreEqType *does* look through them
859

860
861
862
863
864
865
866
867
Note that eqType can respond 'False' for partial applications of newtypes.
Consider
	newtype Parser m a = MkParser (Foogle m a)
Does 	
	Monad (Parser m) `eqType` Monad (Foogle m)
Well, yes, but eqType won't see that they are the same. 
I don't think this is harmful, but it's soemthing to watch out for.

868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
First, the external interface

\begin{code}
coreEqType :: Type -> Type -> Bool
coreEqType t1 t2 = isEqual $ cmpType (deepCoreView t1) (deepCoreView t2)

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

898
\begin{code}
899
900
901
902
903
904
905
906
907
908
909
910
911
912
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))
913

914
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
915
916

-- NB: we *cannot* short-cut the newtype comparison thus:
917
918
-- eqTypeX env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) 
--	| (tc1 == tc2) = (eqTypeXs env tys1 tys2)
919
920
921
922
923
924
925
926
927
928
929
930
931
932
--
-- Consider:
--	newtype T a = MkT [a]
--	newtype Foo m = MkFoo (forall a. m a -> Int)
--	w1 :: Foo []
--	w1 = ...
--	
--	w2 :: Foo T
--	w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
--
-- We end up with w2 = w1; so we need that Foo T = Foo []
-- but we can only expand saturated newtypes, so just comparing
-- T with [] won't do. 

933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
cmpTypeX env (NoteTy _ t1)	t2		     = cmpTypeX env t1 t2
cmpTypeX env t1			(NoteTy _ t2)	     = cmpTypeX env t1 t2

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

cmpTypeX env (PredTy _)   t2		= GT

cmpTypeX env _ _ = LT

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

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

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

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

987
988
989
990
991
992
993
994
995
996

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

\begin{code}
data TvSubst 		
  = TvSubst InScopeSet 	-- The in-scope type variables
997
	    TvSubstEnv	-- The substitution itself
998
999
1000
			-- See Note [Apply Once]

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