[project @ 2005-05-16 12:39:15 by simonpj]
[ghc-hetmet.git] / ghc / compiler / types / Type.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
3 %
4 \section[Type]{Type - public interface}
5
6 \begin{code}
7 module Type (
8         -- re-exports from TypeRep
9         TyThing(..), Type, PredType(..), ThetaType, 
10         funTyCon,
11
12         -- Re-exports from Kind
13         module Kind,
14
15         -- Re-exports from TyCon
16         PrimRep(..),
17
18         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
19
20         mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
21
22         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
23         splitFunTys, splitFunTysN,
24         funResultTy, funArgTy, zipFunTys, isFunTy,
25
26         mkGenTyConApp, mkTyConApp, mkTyConTy, 
27         tyConAppTyCon, tyConAppArgs, 
28         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         isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
45         isStrictType, isStrictPred, 
46
47         -- Free variables
48         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
49         typeKind, addFreeTyVars,
50
51         -- Tidying up for printing
52         tidyType,      tidyTypes,
53         tidyOpenType,  tidyOpenTypes,
54         tidyTyVarBndr, tidyFreeTyVars,
55         tidyOpenTyVar, tidyOpenTyVars,
56         tidyTopType,   tidyPred,
57
58         -- Comparison
59         coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
60         tcEqPred, tcCmpPred, tcEqTypeX, 
61
62         -- Seq
63         seqType, seqTypes,
64
65         -- Type substitutions
66         TvSubstEnv, emptyTvSubstEnv,    -- Representation widely visible
67         TvSubst(..), emptyTvSubst,      -- Representation visible to a few friends
68         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, 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 #include "HsVersions.h"
82
83 -- We import the representation and primitive functions from TypeRep.
84 -- Many things are reexported, but not the representation!
85
86 import TypeRep
87
88 -- friends:
89 import Kind
90 import Var      ( Var, TyVar, tyVarKind, tyVarName, setTyVarName )
91 import VarEnv
92 import VarSet
93
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 StaticFlags      ( opt_DictsStrict )
105 import SrcLoc           ( noSrcLoc )
106 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 \end{code}
112
113
114 %************************************************************************
115 %*                                                                      *
116                 Type representation
117 %*                                                                      *
118 %************************************************************************
119
120 In Core, we "look through" non-recursive newtypes and PredTypes.
121
122 \begin{code}
123 {-# INLINE coreView #-}
124 coreView :: Type -> Maybe Type
125 -- Srips off the *top layer only* of a type to give 
126 -- its underlying representation type. 
127 -- Returns Nothing if there is nothing to look through.
128 --
129 -- By being non-recursive and inlined, this case analysis gets efficiently
130 -- joined onto the case analysis that the caller is already doing
131 coreView (NoteTy _ ty)     = Just ty
132 coreView (PredTy p)        = Just (predTypeRep p)
133 coreView (TyConApp tc tys) = expandNewTcApp tc tys
134 coreView ty                = Nothing
135
136 deepCoreView :: Type -> Type
137 -- Apply coreView recursively
138 deepCoreView ty
139   | Just ty' <- coreView ty    = deepCoreView ty'
140 deepCoreView (TyVarTy tv)      = TyVarTy tv
141 deepCoreView (TyConApp tc tys) = TyConApp tc (map deepCoreView tys)
142 deepCoreView (AppTy t1 t2)     = AppTy (deepCoreView t1) (deepCoreView t2)
143 deepCoreView (FunTy t1 t2)     = FunTy (deepCoreView t1) (deepCoreView t2)
144 deepCoreView (ForAllTy tv ty)  = ForAllTy tv (deepCoreView ty)
145         -- No NoteTy, no PredTy
146
147 expandNewTcApp :: TyCon -> [Type] -> Maybe Type
148 -- A local helper function (not exported)
149 -- Expands *the outermoset level of* a newtype application to 
150 --      *either* a vanilla TyConApp (recursive newtype, or non-saturated)
151 --      *or*     the newtype representation (otherwise), meaning the
152 --                      type written in the RHS of the newtype decl,
153 --                      which may itself be a newtype
154 --
155 -- Example: newtype R = MkR S
156 --          newtype S = MkS T
157 --          newtype T = MkT (T -> T)
158 --   expandNewTcApp on R gives Just S
159 --                  on S gives Just T
160 --                  on T gives Nothing   (no expansion)
161
162 expandNewTcApp tc tys = case newTyConRhs_maybe tc tys of
163                           Nothing          -> Nothing
164                           Just (tenv, rhs) -> Just (substTy (mkTopTvSubst tenv) rhs)
165 \end{code}
166
167
168 %************************************************************************
169 %*                                                                      *
170 \subsection{Constructor-specific functions}
171 %*                                                                      *
172 %************************************************************************
173
174
175 ---------------------------------------------------------------------
176                                 TyVarTy
177                                 ~~~~~~~
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 getTyVar msg ty = case getTyVar_maybe ty of
187                     Just tv -> tv
188                     Nothing -> panic ("getTyVar: " ++ msg)
189
190 isTyVarTy :: Type -> Bool
191 isTyVarTy ty = isJust (getTyVar_maybe ty)
192
193 getTyVar_maybe :: Type -> Maybe TyVar
194 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
195 getTyVar_maybe (TyVarTy tv)                 = Just tv  
196 getTyVar_maybe other                        = Nothing
197 \end{code}
198
199
200 ---------------------------------------------------------------------
201                                 AppTy
202                                 ~~~~~
203 We need to be pretty careful with AppTy to make sure we obey the 
204 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
205 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         -- We call mkGenTyConApp because the TyConApp could be an 
215         -- under-saturated type synonym.  GHC allows that; e.g.
216         --      type Foo k = k a -> k a
217         --      type Id x = x
218         --      foo :: Foo Id -> Foo Id
219         --
220         -- Here Id is partially applied in the type sig for Foo,
221         -- but once the type synonyms are expanded all is well
222
223 mkAppTys :: Type -> [Type] -> Type
224 mkAppTys orig_ty1 []        = orig_ty1
225         -- This check for an empty list of type arguments
226         -- avoids the needless loss of a type synonym constructor.
227         -- For example: mkAppTys Rational []
228         --   returns to (Ratio Integer), which has needlessly lost
229         --   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     mk_app (TyConApp tc tys) = mkGenTyConApp tc (tys ++ orig_tys2)
235                                 -- 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                                         Nothing         -> Nothing
244                                         Just (tys',ty') -> Just (TyConApp tc tys', ty')
245 splitAppTy_maybe other             = Nothing
246
247 splitAppTy :: Type -> (Type, Type)
248 splitAppTy ty = case splitAppTy_maybe ty of
249                         Just pr -> pr
250                         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 \end{code}
262
263
264 ---------------------------------------------------------------------
265                                 FunTy
266                                 ~~~~~
267
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 isFunTy :: Type -> Bool 
276 isFunTy ty = isJust (splitFunTy_maybe ty)
277
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 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
286 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     split args orig_ty (FunTy arg res)   = split (arg:args) res res
293     split args orig_ty ty                = (reverse args, orig_ty)
294
295 splitFunTysN :: Int -> Type -> ([Type], Type)
296 -- Split off exactly n arg tys
297 splitFunTysN 0 ty = ([], ty)
298 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
299                     case splitFunTysN (n-1) res of { (args, res) ->
300                     (arg:args, res) }}
301
302 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
303 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
304   where
305     split acc []     nty ty                = (reverse acc, nty)
306     split acc xs     nty ty 
307           | 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 \end{code}
321
322
323 ---------------------------------------------------------------------
324                                 TyConApp
325                                 ~~~~~~~~
326 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
327 as apppropriate.
328
329 \begin{code}
330 mkGenTyConApp :: TyCon -> [Type] -> Type
331 mkGenTyConApp tc tys
332   | isSynTyCon tc = mkSynTy tc tys
333   | otherwise     = mkTyConApp tc tys
334
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   | otherwise
342   = ASSERT(not (isSynTyCon tycon))
343     TyConApp tycon tys
344
345 mkTyConTy :: TyCon -> Type
346 mkTyConTy tycon = mkTyConApp tycon []
347
348 -- splitTyConApp "looks through" synonyms, because they don't
349 -- mean a distinct type, but all other type-constructor applications
350 -- including functions are returned as Just ..
351
352 tyConAppTyCon :: Type -> TyCon
353 tyConAppTyCon ty = fst (splitTyConApp ty)
354
355 tyConAppArgs :: Type -> [Type]
356 tyConAppArgs ty = snd (splitTyConApp ty)
357
358 splitTyConApp :: Type -> (TyCon, [Type])
359 splitTyConApp ty = case splitTyConApp_maybe ty of
360                         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
368 \end{code}
369
370
371 ---------------------------------------------------------------------
372                                 SynTy
373                                 ~~~~~
374
375 \begin{code}
376 mkSynTy tycon tys
377   | n_args == arity     -- Exactly saturated
378   = mk_syn tys
379   | n_args >  arity     -- Over-saturated
380   = case splitAt arity tys of { (as,bs) -> mkAppTys (mk_syn as) bs }
381         -- Its important to use mkAppTys, rather than (foldl AppTy),
382         -- because (mk_syn as) might well return a partially-applied
383         -- type constructor; indeed, usually will!
384   | otherwise           -- Un-saturated
385   = TyConApp tycon tys
386         -- For the un-saturated case we build TyConApp directly
387         -- (mkTyConApp ASSERTs that the tc isn't a SynTyCon).
388         -- Here we are relying on checkValidType to find
389         -- the error.  What we can't do is use mkSynTy with
390         -- too few arg tys, because that is utterly bogus.
391
392   where
393     mk_syn tys = NoteTy (SynNote (TyConApp tycon tys))
394                         (substTyWith tyvars tys body)
395
396     (tyvars, body) = ASSERT( isSynTyCon tycon ) getSynTyConDefn tycon
397     arity          = tyConArity tycon
398     n_args         = length tys
399 \end{code}
400
401 Notes on type synonyms
402 ~~~~~~~~~~~~~~~~~~~~~~
403 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
404 to return type synonyms whereever possible. Thus
405
406         type Foo a = a -> a
407
408 we want 
409         splitFunTys (a -> Foo a) = ([a], Foo a)
410 not                                ([a], a -> a)
411
412 The reason is that we then get better (shorter) type signatures in 
413 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
414
415
416                 Representation types
417                 ~~~~~~~~~~~~~~~~~~~~
418 repType looks through 
419         (a) for-alls, and
420         (b) synonyms
421         (c) predicates
422         (d) usage annotations
423         (e) all newtypes, including recursive ones
424 It's useful in the back end.
425
426 \begin{code}
427 repType :: Type -> Type
428 -- Only applied to types of kind *; hence tycons are saturated
429 repType (ForAllTy _ ty)   = repType ty
430 repType (NoteTy   _ ty)   = repType ty
431 repType (PredTy  p)       = repType (predTypeRep p)
432 repType (TyConApp tc tys) 
433   | isNewTyCon tc         = ASSERT( tys `lengthIs` tyConArity tc )
434                             repType (new_type_rep tc tys)
435 repType ty                = ty
436
437 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
438 -- of inspecting the type directly.
439 typePrimRep :: Type -> PrimRep
440 typePrimRep ty = case repType ty of
441                    TyConApp tc _ -> tyConPrimRep tc
442                    FunTy _ _     -> PtrRep
443                    AppTy _ _     -> PtrRep      -- See note below
444                    TyVarTy _     -> PtrRep
445                    other         -> pprPanic "typePrimRep" (ppr ty)
446         -- Types of the form 'f a' must be of kind *, not *#, so
447         -- we are guaranteed that they are represented by pointers.
448         -- The reason is that f must have kind *->*, not *->*#, because
449         -- (we claim) there is no way to constrain f's kind any other
450         -- way.
451
452 -- new_type_rep doesn't ask any questions: 
453 -- it just expands newtype, whether recursive or not
454 new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
455                              case newTyConRep new_tycon of
456                                  (tvs, rep_ty) -> substTyWith tvs tys rep_ty
457 \end{code}
458
459
460 ---------------------------------------------------------------------
461                                 ForAllTy
462                                 ~~~~~~~~
463
464 \begin{code}
465 mkForAllTy :: TyVar -> Type -> Type
466 mkForAllTy tyvar ty
467   = mkForAllTys [tyvar] ty
468
469 mkForAllTys :: [TyVar] -> Type -> Type
470 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
471
472 isForAllTy :: Type -> Bool
473 isForAllTy (NoteTy _ ty)  = isForAllTy ty
474 isForAllTy (ForAllTy _ _) = True
475 isForAllTy other_ty       = False
476
477 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
478 splitForAllTy_maybe ty = splitFAT_m ty
479   where
480     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
481     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
482     splitFAT_m _                            = Nothing
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      split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
489      split orig_ty t                 tvs = (reverse tvs, orig_ty)
490
491 dropForAlls :: Type -> Type
492 dropForAlls ty = snd (splitForAllTys ty)
493 \end{code}
494
495 -- (mkPiType now in CoreUtils)
496
497 applyTy, applyTys
498 ~~~~~~~~~~~~~~~~~
499 Instantiate a for-all type with one or more type arguments.
500 Used when we have a polymorphic function applied to type args:
501         f t1 t2
502 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
503 the expression. 
504
505 \begin{code}
506 applyTy :: Type -> Type -> Type
507 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
508 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
509 applyTy other            arg = panic "applyTy"
510
511 applyTys :: Type -> [Type] -> Type
512 -- This function is interesting because 
513 --      a) the function may have more for-alls than there are args
514 --      b) less obviously, it may have fewer for-alls
515 -- For case (b) think of 
516 --      applyTys (forall a.a) [forall b.b, Int]
517 -- This really can happen, via dressing up polymorphic types with newtype
518 -- clothing.  Here's an example:
519 --      newtype R = R (forall a. a->a)
520 --      foo = case undefined :: R of
521 --              R f -> f ()
522
523 applyTys orig_fun_ty []      = orig_fun_ty
524 applyTys orig_fun_ty arg_tys 
525   | n_tvs == n_args     -- The vastly common case
526   = substTyWith tvs arg_tys rho_ty
527   | n_tvs > n_args      -- Too many for-alls
528   = substTyWith (take n_args tvs) arg_tys 
529                 (mkForAllTys (drop n_args tvs) rho_ty)
530   | otherwise           -- Too many type args
531   = ASSERT2( n_tvs > 0, ppr orig_fun_ty )       -- Zero case gives infnite loop!
532     applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
533              (drop n_tvs arg_tys)
534   where
535     (tvs, rho_ty) = splitForAllTys orig_fun_ty 
536     n_tvs = length tvs
537     n_args = length arg_tys     
538 \end{code}
539
540
541 %************************************************************************
542 %*                                                                      *
543 \subsection{Source types}
544 %*                                                                      *
545 %************************************************************************
546
547 A "source type" is a type that is a separate type as far as the type checker is
548 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 mkPredTys preds = map PredTy preds
560
561 predTypeRep :: PredType -> Type
562 -- Convert a PredType to its "representation type";
563 -- 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 predTypeRep (IParam _ ty)     = ty
567 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
568         -- Result might be a newtype application, but the consumer will
569         -- look through that too if necessary
570 \end{code}
571
572
573 %************************************************************************
574 %*                                                                      *
575                 NewTypes
576 %*                                                                      *
577 %************************************************************************
578
579 \begin{code}
580 splitRecNewType_maybe :: Type -> Maybe Type
581 -- 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 splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
585 splitRecNewType_maybe (TyConApp tc tys)
586   | isNewTyCon tc
587   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitRecNewType_maybe only be applied 
588                                                 --      to *types* (of kind *)
589     ASSERT( isRecursiveTyCon tc )               -- Guaranteed by coreView
590     case newTyConRhs tc of
591         (tvs, rep_ty) -> ASSERT( length tvs == length tys )
592                          Just (substTyWith tvs tys rep_ty)
593         
594 splitRecNewType_maybe other = Nothing
595 \end{code}
596
597
598 %************************************************************************
599 %*                                                                      *
600 \subsection{Kinds and free variables}
601 %*                                                                      *
602 %************************************************************************
603
604 ---------------------------------------------------------------------
605                 Finding the kind of a type
606                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
607 \begin{code}
608 typeKind :: Type -> Kind
609
610 typeKind (TyVarTy tyvar)        = tyVarKind tyvar
611 typeKind (TyConApp tycon tys)   = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
612 typeKind (NoteTy _ ty)          = typeKind ty
613 typeKind (PredTy _)             = liftedTypeKind -- Predicates are always 
614                                                  -- represented by lifted types
615 typeKind (AppTy fun arg)        = kindFunResult (typeKind fun)
616 typeKind (FunTy arg res)        = liftedTypeKind
617 typeKind (ForAllTy tv ty)       = typeKind ty
618 \end{code}
619
620
621 ---------------------------------------------------------------------
622                 Free variables of a type
623                 ~~~~~~~~~~~~~~~~~~~~~~~~
624 \begin{code}
625 tyVarsOfType :: Type -> TyVarSet
626 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
627 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
628 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
629 tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty2      -- See note [Syn] below
630 tyVarsOfType (PredTy sty)               = tyVarsOfPred sty
631 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
632 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
633 tyVarsOfType (ForAllTy tyvar ty)        = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
634
635 --                      Note [Syn]
636 -- Consider
637 --      type T a = Int
638 -- What are the free tyvars of (T x)?  Empty, of course!  
639 -- Here's the example that Ralf Laemmel showed me:
640 --      foo :: (forall a. C u a -> C u a) -> u
641 --      mappend :: Monoid u => u -> u -> u
642 --
643 --      bar :: Monoid u => u
644 --      bar = foo (\t -> t `mappend` t)
645 -- We have to generalise at the arg to f, and we don't
646 -- want to capture the constraint (Monad (C u a)) because
647 -- it appears to mention a.  Pretty silly, but it was useful to him.
648
649
650 tyVarsOfTypes :: [Type] -> TyVarSet
651 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
652
653 tyVarsOfPred :: PredType -> TyVarSet
654 tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
655 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
656
657 tyVarsOfTheta :: ThetaType -> TyVarSet
658 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
659
660 -- Add a Note with the free tyvars to the top of the type
661 addFreeTyVars :: Type -> Type
662 addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
663 addFreeTyVars ty                             = NoteTy (FTVNote (tyVarsOfType ty)) ty
664 \end{code}
665
666 %************************************************************************
667 %*                                                                      *
668 \subsection{TidyType}
669 %*                                                                      *
670 %************************************************************************
671
672 tidyTy tidies up a type for printing in an error message, or in
673 an interface file.
674
675 It doesn't change the uniques at all, just the print names.
676
677 \begin{code}
678 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
679 tidyTyVarBndr (tidy_env, subst) tyvar
680   = case tidyOccName tidy_env (getOccName name) of
681       (tidy', occ') ->  ((tidy', subst'), tyvar')
682                     where
683                         subst' = extendVarEnv subst tyvar tyvar'
684                         tyvar' = setTyVarName tyvar name'
685                         name'  = mkInternalName (getUnique name) occ' noSrcLoc
686                                 -- Note: make a *user* tyvar, so it printes nicely
687                                 -- Could extract src loc, but no need.
688   where
689     name = tyVarName tyvar
690
691 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
692 -- Add the free tyvars to the env in tidy form,
693 -- so that we can tidy the type they are free in
694 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
695
696 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
697 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
698
699 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
700 -- Treat a new tyvar as a binder, and give it a fresh tidy name
701 tidyOpenTyVar env@(tidy_env, subst) tyvar
702   = case lookupVarEnv subst tyvar of
703         Just tyvar' -> (env, tyvar')            -- Already substituted
704         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
705
706 tidyType :: TidyEnv -> Type -> Type
707 tidyType env@(tidy_env, subst) ty
708   = go ty
709   where
710     go (TyVarTy tv)         = case lookupVarEnv subst tv of
711                                 Nothing  -> TyVarTy tv
712                                 Just tv' -> TyVarTy tv'
713     go (TyConApp tycon tys) = let args = map go tys
714                               in args `seqList` TyConApp tycon args
715     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
716     go (PredTy sty)         = PredTy (tidyPred env sty)
717     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
718     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
719     go (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
720                               where
721                                 (envp, tvp) = tidyTyVarBndr env tv
722
723     go_note (SynNote ty)        = SynNote $! (go ty)
724     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
725
726 tidyTypes env tys = map (tidyType env) tys
727
728 tidyPred :: TidyEnv -> PredType -> PredType
729 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
730 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
731 \end{code}
732
733
734 @tidyOpenType@ grabs the free type variables, tidies them
735 and then uses @tidyType@ to work over the type itself
736
737 \begin{code}
738 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
739 tidyOpenType env ty
740   = (env', tidyType env' ty)
741   where
742     env' = tidyFreeTyVars env (tyVarsOfType ty)
743
744 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
745 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
746
747 tidyTopType :: Type -> Type
748 tidyTopType ty = tidyType emptyTidyEnv ty
749 \end{code}
750
751
752
753 %************************************************************************
754 %*                                                                      *
755 \subsection{Liftedness}
756 %*                                                                      *
757 %************************************************************************
758
759 \begin{code}
760 isUnLiftedType :: Type -> Bool
761         -- isUnLiftedType returns True for forall'd unlifted types:
762         --      x :: forall a. Int#
763         -- I found bindings like these were getting floated to the top level.
764         -- They are pretty bogus types, mind you.  It would be better never to
765         -- construct them
766
767 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
768 isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
769 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
770 isUnLiftedType other             = False        
771
772 isUnboxedTupleType :: Type -> Bool
773 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
774                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
775                            other              -> False
776
777 -- Should only be applied to *types*; hence the assert
778 isAlgType :: Type -> Bool
779 isAlgType ty = case splitTyConApp_maybe ty of
780                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
781                                               isAlgTyCon tc
782                         other              -> False
783 \end{code}
784
785 @isStrictType@ computes whether an argument (or let RHS) should
786 be computed strictly or lazily, based only on its type.
787 Works just like isUnLiftedType, except that it has a special case 
788 for dictionaries.  Since it takes account of ClassP, you might think
789 this function should be in TcType, but isStrictType is used by DataCon,
790 which is below TcType in the hierarchy, so it's convenient to put it here.
791
792 \begin{code}
793 isStrictType (PredTy pred)     = isStrictPred pred
794 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
795 isStrictType (ForAllTy tv ty)  = isStrictType ty
796 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
797 isStrictType other             = False  
798
799 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
800 isStrictPred other           = False
801         -- We may be strict in dictionary types, but only if it 
802         -- has more than one component.
803         -- [Being strict in a single-component dictionary risks
804         --  poking the dictionary component, which is wrong.]
805 \end{code}
806
807 \begin{code}
808 isPrimitiveType :: Type -> Bool
809 -- Returns types that are opaque to Haskell.
810 -- Most of these are unlifted, but now that we interact with .NET, we
811 -- may have primtive (foreign-imported) types that are lifted
812 isPrimitiveType ty = case splitTyConApp_maybe ty of
813                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
814                                               isPrimTyCon tc
815                         other              -> False
816 \end{code}
817
818
819 %************************************************************************
820 %*                                                                      *
821 \subsection{Sequencing on types
822 %*                                                                      *
823 %************************************************************************
824
825 \begin{code}
826 seqType :: Type -> ()
827 seqType (TyVarTy tv)      = tv `seq` ()
828 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
829 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
830 seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
831 seqType (PredTy p)        = seqPred p
832 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
833 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
834
835 seqTypes :: [Type] -> ()
836 seqTypes []       = ()
837 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
838
839 seqNote :: TyNote -> ()
840 seqNote (SynNote ty)  = seqType ty
841 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
842
843 seqPred :: PredType -> ()
844 seqPred (ClassP c tys) = c  `seq` seqTypes tys
845 seqPred (IParam n ty)  = n  `seq` seqType ty
846 \end{code}
847
848
849 %************************************************************************
850 %*                                                                      *
851                 Comparison of types
852         (We don't use instances so that we know where it happens)
853 %*                                                                      *
854 %************************************************************************
855
856 Two flavours:
857
858 * tcEqType, tcCmpType do *not* look through newtypes, PredTypes
859 * coreEqType *does* look through them
860
861 Note that eqType can respond 'False' for partial applications of newtypes.
862 Consider
863         newtype Parser m a = MkParser (Foogle m a)
864 Does    
865         Monad (Parser m) `eqType` Monad (Foogle m)
866 Well, yes, but eqType won't see that they are the same. 
867 I don't think this is harmful, but it's soemthing to watch out for.
868
869 First, the external interface
870
871 \begin{code}
872 coreEqType :: Type -> Type -> Bool
873 coreEqType t1 t2 = isEqual $ cmpType (deepCoreView t1) (deepCoreView t2)
874
875 tcEqType :: Type -> Type -> Bool
876 tcEqType t1 t2 = isEqual $ cmpType t1 t2
877
878 tcEqTypes :: [Type] -> [Type] -> Bool
879 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
880
881 tcCmpType :: Type -> Type -> Ordering
882 tcCmpType t1 t2 = cmpType t1 t2
883
884 tcCmpTypes :: [Type] -> [Type] -> Ordering
885 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
886
887 tcEqPred :: PredType -> PredType -> Bool
888 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
889
890 tcCmpPred :: PredType -> PredType -> Ordering
891 tcCmpPred p1 p2 = cmpPred p1 p2
892
893 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
894 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
895 \end{code}
896
897 Now here comes the real worker
898
899 \begin{code}
900 cmpType :: Type -> Type -> Ordering
901 cmpType t1 t2 = cmpTypeX rn_env t1 t2
902   where
903     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
904
905 cmpTypes :: [Type] -> [Type] -> Ordering
906 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
907   where
908     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
909
910 cmpPred :: PredType -> PredType -> Ordering
911 cmpPred p1 p2 = cmpPredX rn_env p1 p2
912   where
913     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
914
915 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
916
917 -- NB: we *cannot* short-cut the newtype comparison thus:
918 -- eqTypeX env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) 
919 --      | (tc1 == tc2) = (eqTypeXs env tys1 tys2)
920 --
921 -- Consider:
922 --      newtype T a = MkT [a]
923 --      newtype Foo m = MkFoo (forall a. m a -> Int)
924 --      w1 :: Foo []
925 --      w1 = ...
926 --      
927 --      w2 :: Foo T
928 --      w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
929 --
930 -- We end up with w2 = w1; so we need that Foo T = Foo []
931 -- but we can only expand saturated newtypes, so just comparing
932 -- T with [] won't do. 
933
934 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
935 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
936 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
937 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
938 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
939 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
940 cmpTypeX env (NoteTy _ t1)      t2                   = cmpTypeX env t1 t2
941 cmpTypeX env t1                 (NoteTy _ t2)        = cmpTypeX env t1 t2
942
943     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
944 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
945     
946 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
947 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
948     
949 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
950 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
951 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
952     
953 cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
954 cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
955 cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
956 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
957
958 cmpTypeX env (PredTy _)   t2            = GT
959
960 cmpTypeX env _ _ = LT
961
962 -------------
963 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
964 cmpTypesX env []        []        = EQ
965 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
966 cmpTypesX env []        tys       = LT
967 cmpTypesX env ty        []        = GT
968
969 -------------
970 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
971 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
972         -- Compare types as well as names for implicit parameters
973         -- This comparison is used exclusively (I think) for the
974         -- finite map built in TcSimplify
975 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
976 cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
977 cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
978 \end{code}
979
980 PredTypes are used as a FM key in TcSimplify, 
981 so we take the easy path and make them an instance of Ord
982
983 \begin{code}
984 instance Eq  PredType where { (==)    = tcEqPred }
985 instance Ord PredType where { compare = tcCmpPred }
986 \end{code}
987
988
989 %************************************************************************
990 %*                                                                      *
991                 Type substitutions
992 %*                                                                      *
993 %************************************************************************
994
995 \begin{code}
996 data TvSubst            
997   = TvSubst InScopeSet  -- The in-scope type variables
998             TvSubstEnv  -- The substitution itself
999                         -- See Note [Apply Once]
1000
1001 {- ----------------------------------------------------------
1002                 Note [Apply Once]
1003
1004 We use TvSubsts to instantiate things, and we might instantiate
1005         forall a b. ty
1006 \with the types
1007         [a, b], or [b, a].
1008 So the substition might go [a->b, b->a].  A similar situation arises in Core
1009 when we find a beta redex like
1010         (/\ a /\ b -> e) b a
1011 Then we also end up with a substition that permutes type variables. Other
1012 variations happen to; for example [a -> (a, b)].  
1013
1014         ***************************************************
1015         *** So a TvSubst must be applied precisely once ***
1016         ***************************************************
1017
1018 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1019 we use during unifications, it must not be repeatedly applied.
1020 -------------------------------------------------------------- -}
1021
1022
1023 type TvSubstEnv = TyVarEnv Type
1024         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1025         -- invariant discussed in Note [Apply Once]), and also independently
1026         -- in the middle of matching, and unification (see Types.Unify)
1027         -- So you have to look at the context to know if it's idempotent or
1028         -- apply-once or whatever
1029 emptyTvSubstEnv :: TvSubstEnv
1030 emptyTvSubstEnv = emptyVarEnv
1031
1032 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1033 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1034 -- It assumes that both are idempotent
1035 -- Typically, env1 is the refinement to a base substitution env2
1036 composeTvSubst in_scope env1 env2
1037   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1038         -- First apply env1 to the range of env2
1039         -- Then combine the two, making sure that env1 loses if
1040         -- both bind the same variable; that's why env1 is the
1041         --  *left* argument to plusVarEnv, because the right arg wins
1042   where
1043     subst1 = TvSubst in_scope env1
1044
1045 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1046 isEmptyTvSubst :: TvSubst -> Bool
1047 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1048
1049 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1050 mkTvSubst = TvSubst
1051
1052 getTvSubstEnv :: TvSubst -> TvSubstEnv
1053 getTvSubstEnv (TvSubst _ env) = env
1054
1055 getTvInScope :: TvSubst -> InScopeSet
1056 getTvInScope (TvSubst in_scope _) = in_scope
1057
1058 isInScope :: Var -> TvSubst -> Bool
1059 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1060
1061 notElemTvSubst :: TyVar -> TvSubst -> Bool
1062 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1063
1064 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1065 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1066
1067 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1068 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1069
1070 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1071 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1072
1073 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1074 extendTvSubstList (TvSubst in_scope env) tvs tys 
1075   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1076
1077 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1078 -- the types given; but it's just a thunk so with a bit of luck
1079 -- it'll never be evaluated
1080
1081 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1082 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1083
1084 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1085 zipOpenTvSubst tyvars tys 
1086 #ifdef DEBUG
1087   | length tyvars /= length tys
1088   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1089   | otherwise
1090 #endif
1091   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1092
1093 -- mkTopTvSubst is called when doing top-level substitutions.
1094 -- Here we expect that the free vars of the range of the
1095 -- substitution will be empty.
1096 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1097 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1098
1099 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1100 zipTopTvSubst tyvars tys 
1101 #ifdef DEBUG
1102   | length tyvars /= length tys
1103   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1104   | otherwise
1105 #endif
1106   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1107
1108 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1109 zipTyEnv tyvars tys
1110 #ifdef DEBUG
1111   | length tyvars /= length tys
1112   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1113   | otherwise
1114 #endif
1115   = zip_ty_env tyvars tys emptyVarEnv
1116
1117 -- Later substitutions in the list over-ride earlier ones, 
1118 -- but there should be no loops
1119 zip_ty_env []       []       env = env
1120 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1121         -- There used to be a special case for when 
1122         --      ty == TyVarTy tv
1123         -- (a not-uncommon case) in which case the substitution was dropped.
1124         -- But the type-tidier changes the print-name of a type variable without
1125         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had 
1126         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1127         -- And it happened that t was the type variable of the class.  Post-tiding, 
1128         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1129         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1130         -- and so generated a rep type mentioning t not t2.  
1131         --
1132         -- Simplest fix is to nuke the "optimisation"
1133
1134 instance Outputable TvSubst where
1135   ppr (TvSubst ins env) 
1136     = sep[ ptext SLIT("<TvSubst"),
1137            nest 2 (ptext SLIT("In scope:") <+> ppr ins), 
1138            nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1139 \end{code}
1140
1141 %************************************************************************
1142 %*                                                                      *
1143                 Performing type substitutions
1144 %*                                                                      *
1145 %************************************************************************
1146
1147 \begin{code}
1148 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1149 substTyWith tvs tys = ASSERT( length tvs == length tys )
1150                       substTy (zipOpenTvSubst tvs tys)
1151
1152 substTy :: TvSubst -> Type  -> Type
1153 substTy subst ty | isEmptyTvSubst subst = ty
1154                  | otherwise            = subst_ty subst ty
1155
1156 substTys :: TvSubst -> [Type] -> [Type]
1157 substTys subst tys | isEmptyTvSubst subst = tys
1158                    | otherwise            = map (subst_ty subst) tys
1159
1160 deShadowTy :: Type -> Type              -- Remove any shadowing from the type
1161 deShadowTy ty = subst_ty emptyTvSubst ty
1162
1163 substTheta :: TvSubst -> ThetaType -> ThetaType
1164 substTheta subst theta
1165   | isEmptyTvSubst subst = theta
1166   | otherwise            = map (substPred subst) theta
1167
1168 substPred :: TvSubst -> PredType -> PredType
1169 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1170 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1171
1172 -- Note that the in_scope set is poked only if we hit a forall
1173 -- so it may often never be fully computed 
1174 subst_ty subst ty
1175    = go ty
1176   where
1177     go (TyVarTy tv)                = substTyVar subst tv
1178     go (TyConApp tc tys)           = let args = map go tys
1179                                      in  args `seqList` TyConApp tc args
1180
1181     go (PredTy p)                  = PredTy $! (substPred subst p)
1182
1183     go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote $! (go ty1)) $! (go ty2)
1184     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
1185
1186     go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
1187     go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
1188                 -- The mkAppTy smart constructor is important
1189                 -- we might be replacing (a Int), represented with App
1190                 -- by [Int], represented with TyConApp
1191     go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
1192                                         (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1193
1194 substTyVar :: TvSubst -> TyVar  -> Type
1195 substTyVar (TvSubst in_scope env) tv
1196   = case (lookupVarEnv env tv) of
1197         Nothing  -> TyVarTy tv
1198         Just ty' -> ty' -- See Note [Apply Once]
1199
1200 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)  
1201 substTyVarBndr subst@(TvSubst in_scope env) old_var
1202   | old_var == new_var  -- No need to clone
1203                         -- But we *must* zap any current substitution for the variable.
1204                         --  For example:
1205                         --      (\x.e) with id_subst = [x |-> e']
1206                         -- Here we must simply zap the substitution for x
1207                         --
1208                         -- The new_id isn't cloned, but it may have a different type
1209                         -- etc, so we must return it, not the old id
1210   = (TvSubst (in_scope `extendInScopeSet` new_var) 
1211              (delVarEnv env old_var),
1212      new_var)
1213
1214   | otherwise   -- The new binder is in scope so
1215                 -- we'd better rename it away from the in-scope variables
1216                 -- Extending the substitution to do this renaming also
1217                 -- has the (correct) effect of discarding any existing
1218                 -- substitution for that variable
1219   = (TvSubst (in_scope `extendInScopeSet` new_var) 
1220              (extendVarEnv env old_var (TyVarTy new_var)),
1221      new_var)
1222   where
1223     new_var = uniqAway in_scope old_var
1224         -- The uniqAway part makes sure the new variable is not already in scope
1225 \end{code}