Type.lhs 51 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, pprSourceTyCon, mkFamilyTyConApp,
58

59
	-- Newtypes
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
60
	newTyConInstRhs,
61

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

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

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

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

82
	-- Seq
83
	seqType, seqTypes,
84

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

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

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

102 103
#include "HsVersions.h"

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

import TypeRep

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

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

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

125
import Data.List
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
newTyConInstRhs :: TyCon -> [Type] -> Type
newTyConInstRhs tycon tys =
    let (tvs, ty) = newTyConRhs tycon in substTyWith tvs tys ty
sof's avatar
sof committed
413
\end{code}
414

415

416 417 418 419 420 421 422 423
---------------------------------------------------------------------
				SynTy
				~~~~~

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

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


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

\begin{code}
repType :: Type -> Type
447
-- Only applied to types of kind *; hence tycons are saturated
448
repType ty | Just ty' <- coreView ty = repType ty'
449 450
repType (ForAllTy _ ty)  = repType ty
repType (TyConApp tc tys)
451 452 453 454 455 456 457 458 459
  | 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)

460 461
repType ty = ty

mnislaih's avatar
mnislaih committed
462 463 464 465 466 467 468 469 470 471
-- 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


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


489 490 491
---------------------------------------------------------------------
				ForAllTy
				~~~~~~~~
492 493

\begin{code}
494
mkForAllTy :: TyVar -> Type -> Type
495 496
mkForAllTy tyvar ty
  = mkForAllTys [tyvar] ty
497

498
mkForAllTys :: [TyVar] -> Type -> Type
499
mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
500 501 502 503 504

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

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

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

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

524
-- (mkPiType now in CoreUtils)
525

526 527 528 529 530 531 532
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. 
533

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

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

569

570 571
%************************************************************************
%*									*
572
\subsection{Source types}
573 574
%*									*
%************************************************************************
575

576 577
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.
578

579
Source types are always lifted.
580

581
The key function is predTypeRep which gives the representation of a source type:
582 583

\begin{code}
584
mkPredTy :: PredType -> Type
585
mkPredTy pred = PredTy pred
586 587

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

601 602 603 604 605 606 607 608 609 610 611 612 613 614
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

615
-- Pretty prints a tycon, using the family instance in case of a
616 617 618 619
-- 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 
620 621
  | Just (fam_tc, tys) <- tyConFamInst_maybe tycon
  = ppr $ fam_tc `TyConApp` tys	       -- can't be FunTyCon
622 623
  | otherwise
  = ppr tycon
624
\end{code}
625 626


627 628 629 630 631 632 633 634 635
%************************************************************************
%*									*
\subsection{Kinds and free variables}
%*									*
%************************************************************************

---------------------------------------------------------------------
		Finding the kind of a type
		~~~~~~~~~~~~~~~~~~~~~~~~~~
636
\begin{code}
637
typeKind :: Type -> Kind
638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661
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
662 663 664
\end{code}


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

679
tyVarsOfTypes :: [Type] -> TyVarSet
680 681
tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys

682
tyVarsOfPred :: PredType -> TyVarSet
683 684 685
tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
686 687

tyVarsOfTheta :: ThetaType -> TyVarSet
688
tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
689

690
-- Add a Note with the free tyvars to the top of the type
691
addFreeTyVars :: Type -> Type
692 693
addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
addFreeTyVars ty			     = NoteTy (FTVNote (tyVarsOfType ty)) ty
694
\end{code}
695

696

697 698 699 700 701
%************************************************************************
%*									*
\subsection{TidyType}
%*									*
%************************************************************************
702

703 704
tidyTy tidies up a type for printing in an error message, or in
an interface file.
705

706
It doesn't change the uniques at all, just the print names.
707 708

\begin{code}
709
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
710
tidyTyVarBndr env@(tidy_env, subst) tyvar
711
  = case tidyOccName tidy_env (getOccName name) of
712 713 714 715 716 717 718 719 720
      (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)
721 722
  where
    name = tyVarName tyvar
723

724 725 726
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
727 728 729 730 731 732 733 734 735 736 737
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
738

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

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

758
tidyTypes env tys = map (tidyType env) tys
759

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


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

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

tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
782 783
\end{code}

784
\begin{code}
785

786
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
787
tidyKind env k = tidyOpenType env k
788 789 790

\end{code}

791

792 793
%************************************************************************
%*									*
794
\subsection{Liftedness}
795 796 797
%*									*
%************************************************************************

798
\begin{code}
799
isUnLiftedType :: Type -> Bool
800 801 802 803 804 805
	-- 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

806
isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
807 808 809
isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
isUnLiftedType other		 = False	
810

811
isUnboxedTupleType :: Type -> Bool
812 813 814
isUnboxedTupleType ty = case splitTyConApp_maybe ty of
			   Just (tc, ty_args) -> isUnboxedTupleTyCon tc
			   other	      -> False
815

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

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

857

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

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


%************************************************************************
%*									*
890
		Equality for Core types 
891
	(We don't use instances so that we know where it happens)
892 893 894
%*									*
%************************************************************************

895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921
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
922 923
    eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
		 | Just t2' <- coreView t2 = eq env t1 t2' 
924 925 926 927

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

929

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

937 938 939
Note that 
	tcEqType, tcCmpType 
do *not* look through newtypes, PredTypes
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

\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

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

982
cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering	-- Main workhorse
983 984
cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
		   | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
985

986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015
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 _ _) (TyCo