Check category of type instances and some newtype family fixes
[ghc.git] / compiler / types / Type.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
3 %
4 \section[Type]{Type - public interface}
5
6
7 \begin{code}
8 module Type (
9         -- re-exports from TypeRep
10         TyThing(..), Type, PredType(..), ThetaType, 
11         funTyCon,
12
13         -- Kinds
14         Kind, SimpleKind, KindVar,
15         kindFunResult, splitKindFunTys, splitKindFunTysN,
16
17         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
18         argTypeKindTyCon, ubxTupleKindTyCon,
19
20         liftedTypeKind, unliftedTypeKind, openTypeKind,
21         argTypeKind, ubxTupleKind,
22
23         tySuperKind, coSuperKind, 
24
25         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
26         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind, 
27         isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
28         mkArrowKind, mkArrowKinds,
29
30         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
31         isSubKindCon,
32
33         -- Re-exports from TyCon
34         PrimRep(..),
35
36         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
37
38         mkAppTy, mkAppTys, splitAppTy, splitAppTys, 
39         splitAppTy_maybe, repSplitAppTy_maybe,
40
41         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, 
42         splitFunTys, splitFunTysN,
43         funResultTy, funArgTy, zipFunTys, isFunTy,
44
45         mkTyConApp, mkTyConTy, 
46         tyConAppTyCon, tyConAppArgs, 
47         splitTyConApp_maybe, splitTyConApp, 
48         splitNewTyConApp_maybe, splitNewTyConApp,
49
50         repType, typePrimRep, coreView, tcView, kindView,
51
52         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, 
53         applyTy, applyTys, isForAllTy, dropForAlls,
54
55         -- Source types
56         predTypeRep, mkPredTy, mkPredTys,
57
58         -- Newtypes
59         splitRecNewType_maybe, newTyConInstRhs,
60
61         -- Lifting and boxity
62         isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
63         isStrictType, isStrictPred, 
64
65         -- Free variables
66         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
67         typeKind, addFreeTyVars,
68
69         -- Tidying up for printing
70         tidyType,      tidyTypes,
71         tidyOpenType,  tidyOpenTypes,
72         tidyTyVarBndr, tidyFreeTyVars,
73         tidyOpenTyVar, tidyOpenTyVars,
74         tidyTopType,   tidyPred,
75         tidyKind,
76
77         -- Comparison
78         coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
79         tcEqPred, tcCmpPred, tcEqTypeX, 
80
81         -- Seq
82         seqType, seqTypes,
83
84         -- Type substitutions
85         TvSubstEnv, emptyTvSubstEnv,    -- Representation widely visible
86         TvSubst(..), emptyTvSubst,      -- Representation visible to a few friends
87         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
88         getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
89         extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
90
91         -- Performing substitution on types
92         substTy, substTys, substTyWith, substTheta, 
93         substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
94
95         -- Pretty-printing
96         pprType, pprParendType, pprTyThingCategory,
97         pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
98     ) where
99
100 #include "HsVersions.h"
101
102 -- We import the representation and primitive functions from TypeRep.
103 -- Many things are reexported, but not the representation!
104
105 import TypeRep
106
107 -- friends:
108 import Var      ( Var, TyVar, tyVarKind, tyVarName, 
109                   setTyVarName, setTyVarKind, mkWildCoVar )
110 import VarEnv
111 import VarSet
112
113 import OccName  ( tidyOccName )
114 import Name     ( NamedThing(..), tidyNameOcc )
115 import Class    ( Class, classTyCon )
116 import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey, 
117                   ubxTupleKindTyConKey, argTypeKindTyConKey )
118 import TyCon    ( TyCon, isRecursiveTyCon, isPrimTyCon,
119                   isUnboxedTupleTyCon, isUnLiftedTyCon,
120                   isFunTyCon, isNewTyCon, isOpenTyCon, newTyConRep,
121                   newTyConRhs, 
122                   isAlgTyCon, tyConArity, isSuperKindTyCon,
123                   tcExpandTyCon_maybe, coreExpandTyCon_maybe,
124                   tyConKind, PrimRep(..), tyConPrimRep, tyConUnique,
125                   isCoercionTyCon_maybe, isCoercionTyCon
126                 )
127
128 -- others
129 import StaticFlags      ( opt_DictsStrict )
130 import Util             ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
131 import Outputable
132 import UniqSet          ( sizeUniqSet )         -- Should come via VarSet
133 import Maybe            ( isJust )
134 \end{code}
135
136
137 %************************************************************************
138 %*                                                                      *
139                 Type representation
140 %*                                                                      *
141 %************************************************************************
142
143 In Core, we "look through" non-recursive newtypes and PredTypes.
144
145 \begin{code}
146 {-# INLINE coreView #-}
147 coreView :: Type -> Maybe Type
148 -- Strips off the *top layer only* of a type to give 
149 -- its underlying representation type. 
150 -- Returns Nothing if there is nothing to look through.
151 --
152 -- In the case of newtypes, it returns
153 --      *either* a vanilla TyConApp (recursive newtype, or non-saturated)
154 --      *or*     the newtype representation (otherwise), meaning the
155 --                      type written in the RHS of the newtype decl,
156 --                      which may itself be a newtype
157 --
158 -- Example: newtype R = MkR S
159 --          newtype S = MkS T
160 --          newtype T = MkT (T -> T)
161 --   expandNewTcApp on R gives Just S
162 --                  on S gives Just T
163 --                  on T gives Nothing   (no expansion)
164
165 -- By being non-recursive and inlined, this case analysis gets efficiently
166 -- joined onto the case analysis that the caller is already doing
167 coreView (NoteTy _ ty)     = Just ty
168 coreView (PredTy p)
169   | isEqPred p             = Nothing
170   | otherwise              = Just (predTypeRep p)
171 coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- coreExpandTyCon_maybe tc tys 
172                            = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
173                                 -- Its important to use mkAppTys, rather than (foldl AppTy),
174                                 -- because the function part might well return a 
175                                 -- partially-applied type constructor; indeed, usually will!
176 coreView ty                = Nothing
177
178
179
180 -----------------------------------------------
181 {-# INLINE tcView #-}
182 tcView :: Type -> Maybe Type
183 -- Same, but for the type checker, which just looks through synonyms
184 tcView (NoteTy _ ty)     = Just ty
185 tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys 
186                          = Just (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
187 tcView ty                = Nothing
188
189 -----------------------------------------------
190 {-# INLINE kindView #-}
191 kindView :: Kind -> Maybe Kind
192 -- C.f. coreView, tcView
193 -- For the moment, we don't even handle synonyms in kinds
194 kindView (NoteTy _ k) = Just k
195 kindView other        = Nothing
196 \end{code}
197
198
199 %************************************************************************
200 %*                                                                      *
201 \subsection{Constructor-specific functions}
202 %*                                                                      *
203 %************************************************************************
204
205
206 ---------------------------------------------------------------------
207                                 TyVarTy
208                                 ~~~~~~~
209 \begin{code}
210 mkTyVarTy  :: TyVar   -> Type
211 mkTyVarTy  = TyVarTy
212
213 mkTyVarTys :: [TyVar] -> [Type]
214 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
215
216 getTyVar :: String -> Type -> TyVar
217 getTyVar msg ty = case getTyVar_maybe ty of
218                     Just tv -> tv
219                     Nothing -> panic ("getTyVar: " ++ msg)
220
221 isTyVarTy :: Type -> Bool
222 isTyVarTy ty = isJust (getTyVar_maybe ty)
223
224 getTyVar_maybe :: Type -> Maybe TyVar
225 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
226 getTyVar_maybe (TyVarTy tv)                 = Just tv  
227 getTyVar_maybe other                        = Nothing
228
229 \end{code}
230
231
232 ---------------------------------------------------------------------
233                                 AppTy
234                                 ~~~~~
235 We need to be pretty careful with AppTy to make sure we obey the 
236 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
237 invariant: use it.
238
239 \begin{code}
240 mkAppTy orig_ty1 orig_ty2
241   = mk_app orig_ty1
242   where
243     mk_app (NoteTy _ ty1)    = mk_app ty1
244     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ [orig_ty2])
245     mk_app ty1               = AppTy orig_ty1 orig_ty2
246         -- Note that the TyConApp could be an 
247         -- under-saturated type synonym.  GHC allows that; e.g.
248         --      type Foo k = k a -> k a
249         --      type Id x = x
250         --      foo :: Foo Id -> Foo Id
251         --
252         -- Here Id is partially applied in the type sig for Foo,
253         -- but once the type synonyms are expanded all is well
254
255 mkAppTys :: Type -> [Type] -> Type
256 mkAppTys orig_ty1 []        = orig_ty1
257         -- This check for an empty list of type arguments
258         -- avoids the needless loss of a type synonym constructor.
259         -- For example: mkAppTys Rational []
260         --   returns to (Ratio Integer), which has needlessly lost
261         --   the Rational part.
262 mkAppTys orig_ty1 orig_tys2
263   = mk_app orig_ty1
264   where
265     mk_app (NoteTy _ ty1)    = mk_app ty1
266     mk_app (TyConApp tc tys) = mkTyConApp tc (tys ++ orig_tys2)
267                                 -- mkTyConApp: see notes with mkAppTy
268     mk_app ty1               = foldl AppTy orig_ty1 orig_tys2
269
270 -------------
271 splitAppTy_maybe :: Type -> Maybe (Type, Type)
272 splitAppTy_maybe ty | Just ty' <- coreView ty
273                     = splitAppTy_maybe ty'
274 splitAppTy_maybe ty = repSplitAppTy_maybe ty
275
276 -------------
277 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
278 -- Does the AppTy split, but assumes that any view stuff is already done
279 repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
280 repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
281 repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
282                                                 Just (tys', ty') -> Just (TyConApp tc tys', ty')
283                                                 Nothing          -> Nothing
284 repSplitAppTy_maybe other = Nothing
285 -------------
286 splitAppTy :: Type -> (Type, Type)
287 splitAppTy ty = case splitAppTy_maybe ty of
288                         Just pr -> pr
289                         Nothing -> panic "splitAppTy"
290
291 -------------
292 splitAppTys :: Type -> (Type, [Type])
293 splitAppTys ty = split ty ty []
294   where
295     split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
296     split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
297     split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
298     split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
299                                                (TyConApp funTyCon [], [ty1,ty2])
300     split orig_ty ty                    args = (orig_ty, args)
301
302 \end{code}
303
304
305 ---------------------------------------------------------------------
306                                 FunTy
307                                 ~~~~~
308
309 \begin{code}
310 mkFunTy :: Type -> Type -> Type
311 mkFunTy (PredTy (EqPred ty1 ty2)) res = mkForAllTy (mkWildCoVar (PredTy (EqPred ty1 ty2))) res
312 mkFunTy arg res = FunTy arg res
313
314 mkFunTys :: [Type] -> Type -> Type
315 mkFunTys tys ty = foldr mkFunTy ty tys
316
317 isFunTy :: Type -> Bool 
318 isFunTy ty = isJust (splitFunTy_maybe ty)
319
320 splitFunTy :: Type -> (Type, Type)
321 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
322 splitFunTy (FunTy arg res)   = (arg, res)
323 splitFunTy other             = pprPanic "splitFunTy" (ppr other)
324
325 splitFunTy_maybe :: Type -> Maybe (Type, Type)
326 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
327 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
328 splitFunTy_maybe other             = Nothing
329
330 splitFunTys :: Type -> ([Type], Type)
331 splitFunTys ty = split [] ty ty
332   where
333     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
334     split args orig_ty (FunTy arg res)   = split (arg:args) res res
335     split args orig_ty ty                = (reverse args, orig_ty)
336
337 splitFunTysN :: Int -> Type -> ([Type], Type)
338 -- Split off exactly n arg tys
339 splitFunTysN 0 ty = ([], ty)
340 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
341                     case splitFunTysN (n-1) res of { (args, res) ->
342                     (arg:args, res) }}
343
344 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
345 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
346   where
347     split acc []     nty ty                = (reverse acc, nty)
348     split acc xs     nty ty 
349           | Just ty' <- coreView ty        = split acc xs nty ty'
350     split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
351     split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
352     
353 funResultTy :: Type -> Type
354 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
355 funResultTy (FunTy arg res)   = res
356 funResultTy ty                = pprPanic "funResultTy" (ppr ty)
357
358 funArgTy :: Type -> Type
359 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
360 funArgTy (FunTy arg res)   = arg
361 funArgTy ty                = pprPanic "funArgTy" (ppr ty)
362 \end{code}
363
364
365 ---------------------------------------------------------------------
366                                 TyConApp
367                                 ~~~~~~~~
368 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
369 as apppropriate.
370
371 \begin{code}
372 mkTyConApp :: TyCon -> [Type] -> Type
373 mkTyConApp tycon tys
374   | isFunTyCon tycon, [ty1,ty2] <- tys
375   = FunTy ty1 ty2
376
377   | otherwise
378   = TyConApp tycon tys
379
380 mkTyConTy :: TyCon -> Type
381 mkTyConTy tycon = mkTyConApp tycon []
382
383 -- splitTyConApp "looks through" synonyms, because they don't
384 -- mean a distinct type, but all other type-constructor applications
385 -- including functions are returned as Just ..
386
387 tyConAppTyCon :: Type -> TyCon
388 tyConAppTyCon ty = fst (splitTyConApp ty)
389
390 tyConAppArgs :: Type -> [Type]
391 tyConAppArgs ty = snd (splitTyConApp ty)
392
393 splitTyConApp :: Type -> (TyCon, [Type])
394 splitTyConApp ty = case splitTyConApp_maybe ty of
395                         Just stuff -> stuff
396                         Nothing    -> pprPanic "splitTyConApp" (ppr ty)
397
398 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
399 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
400 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
401 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
402 splitTyConApp_maybe other             = Nothing
403
404 -- Sometimes we do NOT want to look throught a newtype.  When case matching
405 -- on a newtype we want a convenient way to access the arguments of a newty
406 -- constructor so as to properly form a coercion.
407 splitNewTyConApp :: Type -> (TyCon, [Type])
408 splitNewTyConApp ty = case splitNewTyConApp_maybe ty of
409                         Just stuff -> stuff
410                         Nothing    -> pprPanic "splitNewTyConApp" (ppr ty)
411 splitNewTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
412 splitNewTyConApp_maybe ty | Just ty' <- tcView ty = splitNewTyConApp_maybe ty'
413 splitNewTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
414 splitNewTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
415 splitNewTyConApp_maybe other          = Nothing
416
417 -- get instantiated newtype rhs, the arguments had better saturate 
418 -- the constructor
419 newTyConInstRhs :: TyCon -> [Type] -> Type
420 newTyConInstRhs tycon tys =
421     let (tvs, ty) = newTyConRhs tycon in substTyWith tvs tys ty
422
423 \end{code}
424
425
426 ---------------------------------------------------------------------
427                                 SynTy
428                                 ~~~~~
429
430 Notes on type synonyms
431 ~~~~~~~~~~~~~~~~~~~~~~
432 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
433 to return type synonyms whereever possible. Thus
434
435         type Foo a = a -> a
436
437 we want 
438         splitFunTys (a -> Foo a) = ([a], Foo a)
439 not                                ([a], a -> a)
440
441 The reason is that we then get better (shorter) type signatures in 
442 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
443
444
445                 Representation types
446                 ~~~~~~~~~~~~~~~~~~~~
447 repType looks through 
448         (a) for-alls, and
449         (b) synonyms
450         (c) predicates
451         (d) usage annotations
452         (e) all newtypes, including recursive ones, but not newtype families
453 It's useful in the back end.
454
455 \begin{code}
456 repType :: Type -> Type
457 -- Only applied to types of kind *; hence tycons are saturated
458 repType ty | Just ty' <- coreView ty = repType ty'
459 repType (ForAllTy _ ty)  = repType ty
460 repType (TyConApp tc tys)
461   | isNewTyCon tc &&
462     not (isOpenTyCon tc) = -- Recursive newtypes are opaque to coreView
463                            -- but we must expand them here.  Sure to
464                            -- be saturated because repType is only applied
465                            -- to types of kind *
466                            ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
467                            repType (new_type_rep tc tys)
468 repType ty = ty
469
470 -- new_type_rep doesn't ask any questions: 
471 -- it just expands newtype, whether recursive or not
472 new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
473                              case newTyConRep new_tycon of
474                                  (tvs, rep_ty) -> substTyWith tvs tys rep_ty
475
476 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
477 -- of inspecting the type directly.
478 typePrimRep :: Type -> PrimRep
479 typePrimRep ty = case repType ty of
480                    TyConApp tc _ -> tyConPrimRep tc
481                    FunTy _ _     -> PtrRep
482                    AppTy _ _     -> PtrRep      -- See note below
483                    TyVarTy _     -> PtrRep
484                    other         -> pprPanic "typePrimRep" (ppr ty)
485         -- Types of the form 'f a' must be of kind *, not *#, so
486         -- we are guaranteed that they are represented by pointers.
487         -- The reason is that f must have kind *->*, not *->*#, because
488         -- (we claim) there is no way to constrain f's kind any other
489         -- way.
490
491 \end{code}
492
493
494 ---------------------------------------------------------------------
495                                 ForAllTy
496                                 ~~~~~~~~
497
498 \begin{code}
499 mkForAllTy :: TyVar -> Type -> Type
500 mkForAllTy tyvar ty
501   = mkForAllTys [tyvar] ty
502
503 mkForAllTys :: [TyVar] -> Type -> Type
504 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
505
506 isForAllTy :: Type -> Bool
507 isForAllTy (NoteTy _ ty)  = isForAllTy ty
508 isForAllTy (ForAllTy _ _) = True
509 isForAllTy other_ty       = False
510
511 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
512 splitForAllTy_maybe ty = splitFAT_m ty
513   where
514     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
515     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
516     splitFAT_m _                            = Nothing
517
518 splitForAllTys :: Type -> ([TyVar], Type)
519 splitForAllTys ty = split ty ty []
520    where
521      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
522      split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
523      split orig_ty t                 tvs = (reverse tvs, orig_ty)
524
525 dropForAlls :: Type -> Type
526 dropForAlls ty = snd (splitForAllTys ty)
527 \end{code}
528
529 -- (mkPiType now in CoreUtils)
530
531 applyTy, applyTys
532 ~~~~~~~~~~~~~~~~~
533 Instantiate a for-all type with one or more type arguments.
534 Used when we have a polymorphic function applied to type args:
535         f t1 t2
536 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
537 the expression. 
538
539 \begin{code}
540 applyTy :: Type -> Type -> Type
541 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
542 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
543 applyTy other            arg = panic "applyTy"
544
545 applyTys :: Type -> [Type] -> Type
546 -- This function is interesting because 
547 --      a) the function may have more for-alls than there are args
548 --      b) less obviously, it may have fewer for-alls
549 -- For case (b) think of 
550 --      applyTys (forall a.a) [forall b.b, Int]
551 -- This really can happen, via dressing up polymorphic types with newtype
552 -- clothing.  Here's an example:
553 --      newtype R = R (forall a. a->a)
554 --      foo = case undefined :: R of
555 --              R f -> f ()
556
557 applyTys orig_fun_ty []      = orig_fun_ty
558 applyTys orig_fun_ty arg_tys 
559   | n_tvs == n_args     -- The vastly common case
560   = substTyWith tvs arg_tys rho_ty
561   | n_tvs > n_args      -- Too many for-alls
562   = substTyWith (take n_args tvs) arg_tys 
563                 (mkForAllTys (drop n_args tvs) rho_ty)
564   | otherwise           -- Too many type args
565   = ASSERT2( n_tvs > 0, ppr orig_fun_ty )       -- Zero case gives infnite loop!
566     applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
567              (drop n_tvs arg_tys)
568   where
569     (tvs, rho_ty) = splitForAllTys orig_fun_ty 
570     n_tvs = length tvs
571     n_args = length arg_tys     
572 \end{code}
573
574
575 %************************************************************************
576 %*                                                                      *
577 \subsection{Source types}
578 %*                                                                      *
579 %************************************************************************
580
581 A "source type" is a type that is a separate type as far as the type checker is
582 concerned, but which has low-level representation as far as the back end is concerned.
583
584 Source types are always lifted.
585
586 The key function is predTypeRep which gives the representation of a source type:
587
588 \begin{code}
589 mkPredTy :: PredType -> Type
590 mkPredTy pred = PredTy pred
591
592 mkPredTys :: ThetaType -> [Type]
593 mkPredTys preds = map PredTy preds
594
595 predTypeRep :: PredType -> Type
596 -- Convert a PredType to its "representation type";
597 -- the post-type-checking type used by all the Core passes of GHC.
598 -- Unwraps only the outermost level; for example, the result might
599 -- be a newtype application
600 predTypeRep (IParam _ ty)     = ty
601 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
602         -- Result might be a newtype application, but the consumer will
603         -- look through that too if necessary
604 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
605 \end{code}
606
607
608 %************************************************************************
609 %*                                                                      *
610                 NewTypes
611 %*                                                                      *
612 %************************************************************************
613
614 \begin{code}
615 splitRecNewType_maybe :: Type -> Maybe Type
616 -- Sometimes we want to look through a recursive newtype, and that's what happens here
617 -- It only strips *one layer* off, so the caller will usually call itself recursively
618 -- Only applied to types of kind *, hence the newtype is always saturated
619 splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
620 splitRecNewType_maybe (TyConApp tc tys)
621   | isNewTyCon tc
622   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitRecNewType_maybe only be applied 
623                                                 --      to *types* (of kind *)
624     ASSERT( isRecursiveTyCon tc )               -- Guaranteed by coreView
625     case newTyConRhs tc of
626         (tvs, rep_ty) -> ASSERT( length tvs == length tys )
627                          Just (substTyWith tvs tys rep_ty)
628         
629 splitRecNewType_maybe other = Nothing
630
631
632
633 \end{code}
634
635
636 %************************************************************************
637 %*                                                                      *
638 \subsection{Kinds and free variables}
639 %*                                                                      *
640 %************************************************************************
641
642 ---------------------------------------------------------------------
643                 Finding the kind of a type
644                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
645 \begin{code}
646 typeKind :: Type -> Kind
647 typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
648                                    -- We should be looking for the coercion kind,
649                                    -- not the type kind
650                                 foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
651 typeKind (NoteTy _ ty)        = typeKind ty
652 typeKind (PredTy pred)        = predKind pred
653 typeKind (AppTy fun arg)      = kindFunResult (typeKind fun)
654 typeKind (ForAllTy tv ty)     = typeKind ty
655 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
656 typeKind (FunTy arg res)
657     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*), 
658     --              not unliftedTypKind (#)
659     -- The only things that can be after a function arrow are
660     --   (a) types (of kind openTypeKind or its sub-kinds)
661     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
662     | isTySuperKind k         = k
663     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind 
664     where
665       k = typeKind res
666
667 predKind :: PredType -> Kind
668 predKind (EqPred {}) = coSuperKind      -- A coercion kind!
669 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
670 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
671 \end{code}
672
673
674 ---------------------------------------------------------------------
675                 Free variables of a type
676                 ~~~~~~~~~~~~~~~~~~~~~~~~
677 \begin{code}
678 tyVarsOfType :: Type -> TyVarSet
679 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
680 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
681 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
682 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
683 tyVarsOfType (PredTy sty)               = tyVarsOfPred sty
684 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
685 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
686 tyVarsOfType (ForAllTy tyvar ty)        = delVarSet (tyVarsOfType ty) tyvar
687
688 tyVarsOfTypes :: [Type] -> TyVarSet
689 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
690
691 tyVarsOfPred :: PredType -> TyVarSet
692 tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
693 tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
694 tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
695
696 tyVarsOfTheta :: ThetaType -> TyVarSet
697 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
698
699 -- Add a Note with the free tyvars to the top of the type
700 addFreeTyVars :: Type -> Type
701 addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
702 addFreeTyVars ty                             = NoteTy (FTVNote (tyVarsOfType ty)) ty
703 \end{code}
704
705
706 %************************************************************************
707 %*                                                                      *
708 \subsection{TidyType}
709 %*                                                                      *
710 %************************************************************************
711
712 tidyTy tidies up a type for printing in an error message, or in
713 an interface file.
714
715 It doesn't change the uniques at all, just the print names.
716
717 \begin{code}
718 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
719 tidyTyVarBndr (tidy_env, subst) tyvar
720   = case tidyOccName tidy_env (getOccName name) of
721       (tidy', occ') ->  ((tidy', subst'), tyvar')
722                     where
723                         subst' = extendVarEnv subst tyvar tyvar'
724                         tyvar' = setTyVarName tyvar name'
725                         name'  = tidyNameOcc name occ'
726   where
727     name = tyVarName tyvar
728
729 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
730 -- Add the free tyvars to the env in tidy form,
731 -- so that we can tidy the type they are free in
732 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
733
734 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
735 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
736
737 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
738 -- Treat a new tyvar as a binder, and give it a fresh tidy name
739 tidyOpenTyVar env@(tidy_env, subst) tyvar
740   = case lookupVarEnv subst tyvar of
741         Just tyvar' -> (env, tyvar')            -- Already substituted
742         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
743
744 tidyType :: TidyEnv -> Type -> Type
745 tidyType env@(tidy_env, subst) ty
746   = go ty
747   where
748     go (TyVarTy tv)         = case lookupVarEnv subst tv of
749                                 Nothing  -> TyVarTy tv
750                                 Just tv' -> TyVarTy tv'
751     go (TyConApp tycon tys) = let args = map go tys
752                               in args `seqList` TyConApp tycon args
753     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
754     go (PredTy sty)         = PredTy (tidyPred env sty)
755     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
756     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
757     go (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
758                               where
759                                 (envp, tvp) = tidyTyVarBndr env tv
760
761     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
762
763 tidyTypes env tys = map (tidyType env) tys
764
765 tidyPred :: TidyEnv -> PredType -> PredType
766 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
767 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
768 tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
769 \end{code}
770
771
772 @tidyOpenType@ grabs the free type variables, tidies them
773 and then uses @tidyType@ to work over the type itself
774
775 \begin{code}
776 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
777 tidyOpenType env ty
778   = (env', tidyType env' ty)
779   where
780     env' = tidyFreeTyVars env (tyVarsOfType ty)
781
782 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
783 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
784
785 tidyTopType :: Type -> Type
786 tidyTopType ty = tidyType emptyTidyEnv ty
787 \end{code}
788
789 \begin{code}
790
791 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
792 tidyKind env k = tidyOpenType env k
793
794 \end{code}
795
796
797 %************************************************************************
798 %*                                                                      *
799 \subsection{Liftedness}
800 %*                                                                      *
801 %************************************************************************
802
803 \begin{code}
804 isUnLiftedType :: Type -> Bool
805         -- isUnLiftedType returns True for forall'd unlifted types:
806         --      x :: forall a. Int#
807         -- I found bindings like these were getting floated to the top level.
808         -- They are pretty bogus types, mind you.  It would be better never to
809         -- construct them
810
811 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
812 isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
813 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
814 isUnLiftedType other             = False        
815
816 isUnboxedTupleType :: Type -> Bool
817 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
818                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
819                            other              -> False
820
821 -- Should only be applied to *types*; hence the assert
822 isAlgType :: Type -> Bool
823 isAlgType ty = case splitTyConApp_maybe ty of
824                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
825                                               isAlgTyCon tc
826                         other              -> False
827 \end{code}
828
829 @isStrictType@ computes whether an argument (or let RHS) should
830 be computed strictly or lazily, based only on its type.
831 Works just like isUnLiftedType, except that it has a special case 
832 for dictionaries.  Since it takes account of ClassP, you might think
833 this function should be in TcType, but isStrictType is used by DataCon,
834 which is below TcType in the hierarchy, so it's convenient to put it here.
835
836 \begin{code}
837 isStrictType (PredTy pred)     = isStrictPred pred
838 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
839 isStrictType (ForAllTy tv ty)  = isStrictType ty
840 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
841 isStrictType other             = False  
842
843 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
844 isStrictPred other           = False
845         -- We may be strict in dictionary types, but only if it 
846         -- has more than one component.
847         -- [Being strict in a single-component dictionary risks
848         --  poking the dictionary component, which is wrong.]
849 \end{code}
850
851 \begin{code}
852 isPrimitiveType :: Type -> Bool
853 -- Returns types that are opaque to Haskell.
854 -- Most of these are unlifted, but now that we interact with .NET, we
855 -- may have primtive (foreign-imported) types that are lifted
856 isPrimitiveType ty = case splitTyConApp_maybe ty of
857                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
858                                               isPrimTyCon tc
859                         other              -> False
860 \end{code}
861
862
863 %************************************************************************
864 %*                                                                      *
865 \subsection{Sequencing on types
866 %*                                                                      *
867 %************************************************************************
868
869 \begin{code}
870 seqType :: Type -> ()
871 seqType (TyVarTy tv)      = tv `seq` ()
872 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
873 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
874 seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
875 seqType (PredTy p)        = seqPred p
876 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
877 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
878
879 seqTypes :: [Type] -> ()
880 seqTypes []       = ()
881 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
882
883 seqNote :: TyNote -> ()
884 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
885
886 seqPred :: PredType -> ()
887 seqPred (ClassP c tys)   = c `seq` seqTypes tys
888 seqPred (IParam n ty)    = n `seq` seqType ty
889 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
890 \end{code}
891
892
893 %************************************************************************
894 %*                                                                      *
895                 Equality for Core types 
896         (We don't use instances so that we know where it happens)
897 %*                                                                      *
898 %************************************************************************
899
900 Note that eqType works right even for partial applications of newtypes.
901 See Note [Newtype eta] in TyCon.lhs
902
903 \begin{code}
904 coreEqType :: Type -> Type -> Bool
905 coreEqType t1 t2
906   = eq rn_env t1 t2
907   where
908     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
909
910     eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
911     eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
912     eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
913     eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
914     eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
915         | tc1 == tc2, all2 (eq env) tys1 tys2 = True
916                         -- The lengths should be equal because
917                         -- the two types have the same kind
918         -- NB: if the type constructors differ that does not 
919         --     necessarily mean that the types aren't equal
920         --     (synonyms, newtypes)
921         -- Even if the type constructors are the same, but the arguments
922         -- differ, the two types could be the same (e.g. if the arg is just
923         -- ignored in the RHS).  In both these cases we fall through to an 
924         -- attempt to expand one side or the other.
925
926         -- Now deal with newtypes, synonyms, pred-tys
927     eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2 
928                  | Just t2' <- coreView t2 = eq env t1 t2' 
929
930         -- Fall through case; not equal!
931     eq env t1 t2 = False
932 \end{code}
933
934
935 %************************************************************************
936 %*                                                                      *
937                 Comparision for source types 
938         (We don't use instances so that we know where it happens)
939 %*                                                                      *
940 %************************************************************************
941
942 Note that 
943         tcEqType, tcCmpType 
944 do *not* look through newtypes, PredTypes
945
946 \begin{code}
947 tcEqType :: Type -> Type -> Bool
948 tcEqType t1 t2 = isEqual $ cmpType t1 t2
949
950 tcEqTypes :: [Type] -> [Type] -> Bool
951 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
952
953 tcCmpType :: Type -> Type -> Ordering
954 tcCmpType t1 t2 = cmpType t1 t2
955
956 tcCmpTypes :: [Type] -> [Type] -> Ordering
957 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
958
959 tcEqPred :: PredType -> PredType -> Bool
960 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
961
962 tcCmpPred :: PredType -> PredType -> Ordering
963 tcCmpPred p1 p2 = cmpPred p1 p2
964
965 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
966 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
967 \end{code}
968
969 Now here comes the real worker
970
971 \begin{code}
972 cmpType :: Type -> Type -> Ordering
973 cmpType t1 t2 = cmpTypeX rn_env t1 t2
974   where
975     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
976
977 cmpTypes :: [Type] -> [Type] -> Ordering
978 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
979   where
980     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
981
982 cmpPred :: PredType -> PredType -> Ordering
983 cmpPred p1 p2 = cmpPredX rn_env p1 p2
984   where
985     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
986
987 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
988 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
989                    | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
990
991 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
992 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
993 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
994 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
995 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
996 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
997 cmpTypeX env t1                 (NoteTy _ t2)        = cmpTypeX env t1 t2
998
999     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1000 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
1001     
1002 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
1003 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
1004     
1005 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
1006 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
1007 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
1008     
1009 cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
1010 cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
1011 cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
1012 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
1013
1014 cmpTypeX env (PredTy _)   t2            = GT
1015
1016 cmpTypeX env _ _ = LT
1017
1018 -------------
1019 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1020 cmpTypesX env []        []        = EQ
1021 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1022 cmpTypesX env []        tys       = LT
1023 cmpTypesX env ty        []        = GT
1024
1025 -------------
1026 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1027 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1028         -- Compare types as well as names for implicit parameters
1029         -- This comparison is used exclusively (I think) for the
1030         -- finite map built in TcSimplify
1031 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
1032 cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
1033 cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
1034 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1035 \end{code}
1036
1037 PredTypes are used as a FM key in TcSimplify, 
1038 so we take the easy path and make them an instance of Ord
1039
1040 \begin{code}
1041 instance Eq  PredType where { (==)    = tcEqPred }
1042 instance Ord PredType where { compare = tcCmpPred }
1043 \end{code}
1044
1045
1046 %************************************************************************
1047 %*                                                                      *
1048                 Type substitutions
1049 %*                                                                      *
1050 %************************************************************************
1051
1052 \begin{code}
1053 data TvSubst            
1054   = TvSubst InScopeSet  -- The in-scope type variables
1055             TvSubstEnv  -- The substitution itself
1056                         -- See Note [Apply Once]
1057
1058 {- ----------------------------------------------------------
1059                 Note [Apply Once]
1060
1061 We use TvSubsts to instantiate things, and we might instantiate
1062         forall a b. ty
1063 \with the types
1064         [a, b], or [b, a].
1065 So the substition might go [a->b, b->a].  A similar situation arises in Core
1066 when we find a beta redex like
1067         (/\ a /\ b -> e) b a
1068 Then we also end up with a substition that permutes type variables. Other
1069 variations happen to; for example [a -> (a, b)].  
1070
1071         ***************************************************
1072         *** So a TvSubst must be applied precisely once ***
1073         ***************************************************
1074
1075 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1076 we use during unifications, it must not be repeatedly applied.
1077 -------------------------------------------------------------- -}
1078
1079
1080 type TvSubstEnv = TyVarEnv Type
1081         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1082         -- invariant discussed in Note [Apply Once]), and also independently
1083         -- in the middle of matching, and unification (see Types.Unify)
1084         -- So you have to look at the context to know if it's idempotent or
1085         -- apply-once or whatever
1086 emptyTvSubstEnv :: TvSubstEnv
1087 emptyTvSubstEnv = emptyVarEnv
1088
1089 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1090 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1091 -- It assumes that both are idempotent
1092 -- Typically, env1 is the refinement to a base substitution env2
1093 composeTvSubst in_scope env1 env2
1094   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1095         -- First apply env1 to the range of env2
1096         -- Then combine the two, making sure that env1 loses if
1097         -- both bind the same variable; that's why env1 is the
1098         --  *left* argument to plusVarEnv, because the right arg wins
1099   where
1100     subst1 = TvSubst in_scope env1
1101
1102 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1103
1104 isEmptyTvSubst :: TvSubst -> Bool
1105 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1106
1107 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1108 mkTvSubst = TvSubst
1109
1110 getTvSubstEnv :: TvSubst -> TvSubstEnv
1111 getTvSubstEnv (TvSubst _ env) = env
1112
1113 getTvInScope :: TvSubst -> InScopeSet
1114 getTvInScope (TvSubst in_scope _) = in_scope
1115
1116 isInScope :: Var -> TvSubst -> Bool
1117 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1118
1119 notElemTvSubst :: TyVar -> TvSubst -> Bool
1120 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1121
1122 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1123 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1124
1125 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1126 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1127
1128 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1129 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1130
1131 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1132 extendTvSubstList (TvSubst in_scope env) tvs tys 
1133   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1134
1135 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1136 -- the types given; but it's just a thunk so with a bit of luck
1137 -- it'll never be evaluated
1138
1139 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1140 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1141
1142 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1143 zipOpenTvSubst tyvars tys 
1144 #ifdef DEBUG
1145   | length tyvars /= length tys
1146   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1147   | otherwise
1148 #endif
1149   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1150
1151 -- mkTopTvSubst is called when doing top-level substitutions.
1152 -- Here we expect that the free vars of the range of the
1153 -- substitution will be empty.
1154 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1155 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1156
1157 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1158 zipTopTvSubst tyvars tys 
1159 #ifdef DEBUG
1160   | length tyvars /= length tys
1161   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1162   | otherwise
1163 #endif
1164   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1165
1166 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1167 zipTyEnv tyvars tys
1168 #ifdef DEBUG
1169   | length tyvars /= length tys
1170   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1171   | otherwise
1172 #endif
1173   = zip_ty_env tyvars tys emptyVarEnv
1174
1175 -- Later substitutions in the list over-ride earlier ones, 
1176 -- but there should be no loops
1177 zip_ty_env []       []       env = env
1178 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1179         -- There used to be a special case for when 
1180         --      ty == TyVarTy tv
1181         -- (a not-uncommon case) in which case the substitution was dropped.
1182         -- But the type-tidier changes the print-name of a type variable without
1183         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had 
1184         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1185         -- And it happened that t was the type variable of the class.  Post-tiding, 
1186         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1187         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1188         -- and so generated a rep type mentioning t not t2.  
1189         --
1190         -- Simplest fix is to nuke the "optimisation"
1191 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1192 -- zip_ty_env _ _ env = env
1193
1194 instance Outputable TvSubst where
1195   ppr (TvSubst ins env) 
1196     = brackets $ sep[ ptext SLIT("TvSubst"),
1197                       nest 2 (ptext SLIT("In scope:") <+> ppr ins), 
1198                       nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1199 \end{code}
1200
1201 %************************************************************************
1202 %*                                                                      *
1203                 Performing type substitutions
1204 %*                                                                      *
1205 %************************************************************************
1206
1207 \begin{code}
1208 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1209 substTyWith tvs tys = ASSERT( length tvs == length tys )
1210                       substTy (zipOpenTvSubst tvs tys)
1211
1212 substTy :: TvSubst -> Type  -> Type
1213 substTy subst ty | isEmptyTvSubst subst = ty
1214                  | otherwise            = subst_ty subst ty
1215
1216 substTys :: TvSubst -> [Type] -> [Type]
1217 substTys subst tys | isEmptyTvSubst subst = tys
1218                    | otherwise            = map (subst_ty subst) tys
1219
1220 substTheta :: TvSubst -> ThetaType -> ThetaType
1221 substTheta subst theta
1222   | isEmptyTvSubst subst = theta
1223   | otherwise            = map (substPred subst) theta
1224
1225 substPred :: TvSubst -> PredType -> PredType
1226 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1227 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1228 substPred subst (EqPred ty1 ty2)  = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1229
1230 deShadowTy :: TyVarSet -> Type -> Type  -- Remove any nested binders mentioning tvs
1231 deShadowTy tvs ty 
1232   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1233   where
1234     in_scope = mkInScopeSet tvs
1235
1236 subst_ty :: TvSubst -> Type -> Type
1237 -- subst_ty is the main workhorse for type substitution
1238 --
1239 -- Note that the in_scope set is poked only if we hit a forall
1240 -- so it may often never be fully computed 
1241 subst_ty subst ty
1242    = go ty
1243   where
1244     go (TyVarTy tv)                = substTyVar subst tv
1245     go (TyConApp tc tys)           = let args = map go tys
1246                                      in  args `seqList` TyConApp tc args
1247
1248     go (PredTy p)                  = PredTy $! (substPred subst p)
1249
1250     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
1251
1252     go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
1253     go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
1254                 -- The mkAppTy smart constructor is important
1255                 -- we might be replacing (a Int), represented with App
1256                 -- by [Int], represented with TyConApp
1257     go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
1258                                         (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1259
1260 substTyVar :: TvSubst -> TyVar  -> Type
1261 substTyVar subst@(TvSubst in_scope env) tv
1262   = case lookupTyVar subst tv of {
1263         Nothing  -> TyVarTy tv;
1264         Just ty -> ty   -- See Note [Apply Once]
1265     } 
1266
1267 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1268 lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
1269
1270 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)  
1271 substTyVarBndr subst@(TvSubst in_scope env) old_var
1272   = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1273   where
1274
1275     new_env | no_change = delVarEnv env old_var
1276             | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1277
1278     no_change = new_var == old_var && not is_co_var
1279         -- no_change means that the new_var is identical in
1280         -- all respects to the old_var (same unique, same kind)
1281         --
1282         -- In that case we don't need to extend the substitution
1283         -- to map old to new.  But instead we must zap any 
1284         -- current substitution for the variable. For example:
1285         --      (\x.e) with id_subst = [x |-> e']
1286         -- Here we must simply zap the substitution for x
1287
1288     new_var = uniqAway in_scope subst_old_var
1289         -- The uniqAway part makes sure the new variable is not already in scope
1290
1291     subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1292                  -- It's only worth doing the substitution for coercions,
1293                  -- becuase only they can have free type variables
1294         | is_co_var = setTyVarKind old_var (substTy subst kind)
1295         | otherwise = old_var
1296     kind = tyVarKind old_var
1297     is_co_var = isCoercionKind kind
1298 \end{code}
1299
1300 ----------------------------------------------------
1301 -- Kind Stuff
1302
1303 Kinds
1304 ~~~~~
1305 There's a little subtyping at the kind level:  
1306
1307                  ?
1308                 / \
1309                /   \
1310               ??   (#)
1311              /  \
1312             *   #
1313
1314 where   *    [LiftedTypeKind]   means boxed type
1315         #    [UnliftedTypeKind] means unboxed type
1316         (#)  [UbxTupleKind]     means unboxed tuple
1317         ??   [ArgTypeKind]      is the lub of *,#
1318         ?    [OpenTypeKind]     means any type at all
1319
1320 In particular:
1321
1322         error :: forall a:?. String -> a
1323         (->)  :: ?? -> ? -> *
1324         (\(x::t) -> ...)        Here t::?? (i.e. not unboxed tuple)
1325
1326 \begin{code}
1327 type KindVar = TyVar  -- invariant: KindVar will always be a 
1328                       -- TcTyVar with details MetaTv TauTv ...
1329 -- kind var constructors and functions are in TcType
1330
1331 type SimpleKind = Kind
1332 \end{code}
1333
1334 Kind inference
1335 ~~~~~~~~~~~~~~
1336 During kind inference, a kind variable unifies only with 
1337 a "simple kind", sk
1338         sk ::= * | sk1 -> sk2
1339 For example 
1340         data T a = MkT a (T Int#)
1341 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1342 with # (the kind of Int#).
1343
1344 Type inference
1345 ~~~~~~~~~~~~~~
1346 When creating a fresh internal type variable, we give it a kind to express 
1347 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x, 
1348 with kind ??.  
1349
1350 During unification we only bind an internal type variable to a type
1351 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1352
1353 When unifying two internal type variables, we collect their kind constraints by
1354 finding the GLB of the two.  Since the partial order is a tree, they only
1355 have a glb if one is a sub-kind of the other.  In that case, we bind the
1356 less-informative one to the more informative one.  Neat, eh?
1357
1358
1359 \begin{code}
1360
1361 \end{code}
1362
1363 %************************************************************************
1364 %*                                                                      *
1365         Functions over Kinds            
1366 %*                                                                      *
1367 %************************************************************************
1368
1369 \begin{code}
1370 kindFunResult :: Kind -> Kind
1371 kindFunResult k = funResultTy k
1372
1373 splitKindFunTys :: Kind -> ([Kind],Kind)
1374 splitKindFunTys k = splitFunTys k
1375
1376 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1377 splitKindFunTysN k = splitFunTysN k
1378
1379 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1380
1381 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
1382
1383 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1384 isOpenTypeKind other           = False
1385
1386 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1387
1388 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1389 isUbxTupleKind other           = False
1390
1391 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1392
1393 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1394 isArgTypeKind other = False
1395
1396 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1397
1398 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1399 isUnliftedTypeKind other           = False
1400
1401 isSubOpenTypeKind :: Kind -> Bool
1402 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1403 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) ) 
1404                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) ) 
1405                                      False
1406 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1407 isSubOpenTypeKind other            = ASSERT( isKind other ) False
1408          -- This is a conservative answer
1409          -- It matters in the call to isSubKind in
1410          -- checkExpectedKind.
1411
1412 isSubArgTypeKindCon kc
1413   | isUnliftedTypeKindCon kc = True
1414   | isLiftedTypeKindCon kc   = True
1415   | isArgTypeKindCon kc      = True
1416   | otherwise                = False
1417
1418 isSubArgTypeKind :: Kind -> Bool
1419 -- True of any sub-kind of ArgTypeKind 
1420 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1421 isSubArgTypeKind other            = False
1422
1423 isSuperKind :: Type -> Bool
1424 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1425 isSuperKind other = False
1426
1427 isKind :: Kind -> Bool
1428 isKind k = isSuperKind (typeKind k)
1429
1430
1431
1432 isSubKind :: Kind -> Kind -> Bool
1433 -- (k1 `isSubKind` k2) checks that k1 <: k2
1434 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc1
1435 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1436 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2')) 
1437   = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1438 isSubKind k1            k2                    = False
1439
1440 eqKind :: Kind -> Kind -> Bool
1441 eqKind = tcEqType
1442
1443 isSubKindCon :: TyCon -> TyCon -> Bool
1444 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1445 isSubKindCon kc1 kc2
1446   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
1447   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1448   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
1449   | isOpenTypeKindCon kc2                                  = True 
1450                            -- we already know kc1 is not a fun, its a TyCon
1451   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
1452   | otherwise                                              = False
1453
1454 defaultKind :: Kind -> Kind
1455 -- Used when generalising: default kind '?' and '??' to '*'
1456 -- 
1457 -- When we generalise, we make generic type variables whose kind is
1458 -- simple (* or *->* etc).  So generic type variables (other than
1459 -- built-in constants like 'error') always have simple kinds.  This is important;
1460 -- consider
1461 --      f x = True
1462 -- We want f to get type
1463 --      f :: forall (a::*). a -> Bool
1464 -- Not 
1465 --      f :: forall (a::??). a -> Bool
1466 -- because that would allow a call like (f 3#) as well as (f True),
1467 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
1468 defaultKind k 
1469   | isSubOpenTypeKind k = liftedTypeKind
1470   | isSubArgTypeKind k  = liftedTypeKind
1471   | otherwise        = k
1472
1473 isCoercionKind :: Kind -> Bool
1474 -- All coercions are of form (ty1 :=: ty2)
1475 -- This function is here rather than in Coercion, 
1476 -- because it's used by substTy
1477 isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
1478 isCoercionKind (PredTy (EqPred {}))      = True
1479 isCoercionKind other                     = False
1480
1481 isEqPred :: PredType -> Bool
1482 isEqPred (EqPred _ _) = True
1483 isEqPred other        = False
1484 \end{code}