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