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,
  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 \end{code}
 752
 753
 754 %************************************************************************
 755 %*                                                                      *
 756 \subsection{Type families}
 757 %*                                                                      *
 758 %************************************************************************
 759
 760 Type family instances occuring in a type after expanding synonyms.
 761
 762 \begin{code}
 763 tyFamInsts :: Type -> [(TyCon, [Type])]
 764 tyFamInsts ty
 765   | Just exp_ty <- tcView ty    = tyFamInsts exp_ty
 766 tyFamInsts (TyVarTy _)          = []
 767 tyFamInsts (TyConApp tc tys)
 768   | isOpenSynTyCon tc           = [(tc, tys)]
 769   | otherwise                   = concat (map tyFamInsts tys)
 770 tyFamInsts (FunTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
 771 tyFamInsts (AppTy ty1 ty2)      = tyFamInsts ty1 ++ tyFamInsts ty2
 772 tyFamInsts (ForAllTy _ ty)      = tyFamInsts ty
 773 \end{code}
 774
 775
 776 %************************************************************************
 777 %*                                                                      *
 778 \subsection{TidyType}
 779 %*                                                                      *
 780 %************************************************************************
 781
 782 tidyTy tidies up a type for printing in an error message, or in
 783 an interface file.
 784
 785 It doesn't change the uniques at all, just the print names.
 786
 787 \begin{code}
 788 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 789 tidyTyVarBndr env@(tidy_env, subst) tyvar
 790   = case tidyOccName tidy_env (getOccName name) of
 791       (tidy', occ') -> ((tidy', subst'), tyvar'')
 792         where
 793           subst' = extendVarEnv subst tyvar tyvar''
 794           tyvar' = setTyVarName tyvar name'
 795           name'  = tidyNameOcc name occ'
 796                 -- Don't forget to tidy the kind for coercions!
 797           tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
 798                   | otherwise     = tyvar'
 799           kind'  = tidyType env (tyVarKind tyvar)
 800   where
 801     name = tyVarName tyvar
 802
 803 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
 804 -- Add the free tyvars to the env in tidy form,
 805 -- so that we can tidy the type they are free in
 806 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
 807
 808 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
 809 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
 810
 811 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 812 -- Treat a new tyvar as a binder, and give it a fresh tidy name
 813 tidyOpenTyVar env@(_, subst) tyvar
 814   = case lookupVarEnv subst tyvar of
 815         Just tyvar' -> (env, tyvar')            -- Already substituted
 816         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
 817
 818 tidyType :: TidyEnv -> Type -> Type
 819 tidyType env@(_, subst) ty
 820   = go ty
 821   where
 822     go (TyVarTy tv)         = case lookupVarEnv subst tv of
 823                                 Nothing  -> TyVarTy tv
 824                                 Just tv' -> TyVarTy tv'
 825     go (TyConApp tycon tys) = let args = map go tys
 826                               in args `seqList` TyConApp tycon args
 827     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
 828     go (PredTy sty)         = PredTy (tidyPred env sty)
 829     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
 830     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
 831     go (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
 832                               where
 833                                 (envp, tvp) = tidyTyVarBndr env tv
 834
 835     go_note note@(FTVNote _ftvs) = note -- No need to tidy the free tyvars
 836
 837 tidyTypes :: TidyEnv -> [Type] -> [Type]
 838 tidyTypes env tys = map (tidyType env) tys
 839
 840 tidyPred :: TidyEnv -> PredType -> PredType
 841 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
 842 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
 843 tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
 844 \end{code}
 845
 846
 847 @tidyOpenType@ grabs the free type variables, tidies them
 848 and then uses @tidyType@ to work over the type itself
 849
 850 \begin{code}
 851 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
 852 tidyOpenType env ty
 853   = (env', tidyType env' ty)
 854   where
 855     env' = tidyFreeTyVars env (tyVarsOfType ty)
 856
 857 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
 858 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
 859
 860 tidyTopType :: Type -> Type
 861 tidyTopType ty = tidyType emptyTidyEnv ty
 862 \end{code}
 863
 864 \begin{code}
 865
 866 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
 867 tidyKind env k = tidyOpenType env k
 868
 869 \end{code}
 870
 871
 872 %************************************************************************
 873 %*                                                                      *
 874 \subsection{Liftedness}
 875 %*                                                                      *
 876 %************************************************************************
 877
 878 \begin{code}
 879 isUnLiftedType :: Type -> Bool
 880         -- isUnLiftedType returns True for forall'd unlifted types:
 881         --      x :: forall a. Int#
 882         -- I found bindings like these were getting floated to the top level.
 883         -- They are pretty bogus types, mind you.  It would be better never to
 884         -- construct them
 885
 886 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
 887 isUnLiftedType (ForAllTy _ ty)   = isUnLiftedType ty
 888 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
 889 isUnLiftedType _                 = False
 890
 891 isUnboxedTupleType :: Type -> Bool
 892 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
 893                            Just (tc, _ty_args) -> isUnboxedTupleTyCon tc
 894                            _                   -> False
 895
 896 -- Should only be applied to *types*; hence the assert
 897 isAlgType :: Type -> Bool
 898 isAlgType ty
 899   = case splitTyConApp_maybe ty of
 900       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 901                             isAlgTyCon tc
 902       _other             -> False
 903
 904 -- Should only be applied to *types*; hence the assert
 905 isClosedAlgType :: Type -> Bool
 906 isClosedAlgType ty
 907   = case splitTyConApp_maybe ty of
 908       Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 909                             isAlgTyCon tc && not (isOpenTyCon tc)
 910       _other             -> False
 911 \end{code}
 912
 913 @isStrictType@ computes whether an argument (or let RHS) should
 914 be computed strictly or lazily, based only on its type.
 915 Works just like isUnLiftedType, except that it has a special case
 916 for dictionaries.  Since it takes account of ClassP, you might think
 917 this function should be in TcType, but isStrictType is used by DataCon,
 918 which is below TcType in the hierarchy, so it's convenient to put it here.
 919
 920 \begin{code}
 921 isStrictType :: Type -> Bool
 922 isStrictType (PredTy pred)     = isStrictPred pred
 923 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
 924 isStrictType (ForAllTy _ ty)   = isStrictType ty
 925 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
 926 isStrictType _                 = False
 927
 928 isStrictPred :: PredType -> Bool
 929 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
 930 isStrictPred _               = False
 931         -- We may be strict in dictionary types, but only if it
 932         -- has more than one component.
 933         -- [Being strict in a single-component dictionary risks
 934         --  poking the dictionary component, which is wrong.]
 935 \end{code}
 936
 937 \begin{code}
 938 isPrimitiveType :: Type -> Bool
 939 -- Returns types that are opaque to Haskell.
 940 -- Most of these are unlifted, but now that we interact with .NET, we
 941 -- may have primtive (foreign-imported) types that are lifted
 942 isPrimitiveType ty = case splitTyConApp_maybe ty of
 943                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 944                                               isPrimTyCon tc
 945                         _                  -> False
 946 \end{code}
 947
 948
 949 %************************************************************************
 950 %*                                                                      *
 951 \subsection{Sequencing on types
 952 %*                                                                      *
 953 %************************************************************************
 954
 955 \begin{code}
 956 seqType :: Type -> ()
 957 seqType (TyVarTy tv)      = tv `seq` ()
 958 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
 959 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
 960 seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
 961 seqType (PredTy p)        = seqPred p
 962 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 963 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
 964
 965 seqTypes :: [Type] -> ()
 966 seqTypes []       = ()
 967 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 968
 969 seqNote :: TyNote -> ()
 970 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 971
 972 seqPred :: PredType -> ()
 973 seqPred (ClassP c tys)   = c `seq` seqTypes tys
 974 seqPred (IParam n ty)    = n `seq` seqType ty
 975 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
 976 \end{code}
 977
 978
 979 %************************************************************************
 980 %*                                                                      *
 981                 Equality for Core types
 982         (We don't use instances so that we know where it happens)
 983 %*                                                                      *
 984 %************************************************************************
 985
 986 Note that eqType works right even for partial applications of newtypes.
 987 See Note [Newtype eta] in TyCon.lhs
 988
 989 \begin{code}
 990 coreEqType :: Type -> Type -> Bool
 991 coreEqType t1 t2
 992   = eq rn_env t1 t2
 993   where
 994     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
 995
 996     eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
 997     eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
 998     eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
 999     eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
1000     eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1001         | tc1 == tc2, all2 (eq env) tys1 tys2 = True
1002                         -- The lengths should be equal because
1003                         -- the two types have the same kind
1004         -- NB: if the type constructors differ that does not
1005         --     necessarily mean that the types aren't equal
1006         --     (synonyms, newtypes)
1007         -- Even if the type constructors are the same, but the arguments
1008         -- differ, the two types could be the same (e.g. if the arg is just
1009         -- ignored in the RHS).  In both these cases we fall through to an
1010         -- attempt to expand one side or the other.
1011
1012         -- Now deal with newtypes, synonyms, pred-tys
1013     eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
1014                  | Just t2' <- coreView t2 = eq env t1 t2'
1015
1016         -- Fall through case; not equal!
1017     eq _ _ _ = False
1018 \end{code}
1019
1020
1021 %************************************************************************
1022 %*                                                                      *
1023                 Comparision for source types
1024         (We don't use instances so that we know where it happens)
1025 %*                                                                      *
1026 %************************************************************************
1027
1028 Note that
1029         tcEqType, tcCmpType
1030 do *not* look through newtypes, PredTypes
1031
1032 \begin{code}
1033 tcEqType :: Type -> Type -> Bool
1034 tcEqType t1 t2 = isEqual $ cmpType t1 t2
1035
1036 tcEqTypes :: [Type] -> [Type] -> Bool
1037 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
1038
1039 tcCmpType :: Type -> Type -> Ordering
1040 tcCmpType t1 t2 = cmpType t1 t2
1041
1042 tcCmpTypes :: [Type] -> [Type] -> Ordering
1043 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
1044
1045 tcEqPred :: PredType -> PredType -> Bool
1046 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
1047
1048 tcCmpPred :: PredType -> PredType -> Ordering
1049 tcCmpPred p1 p2 = cmpPred p1 p2
1050
1051 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
1052 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
1053 \end{code}
1054
1055 Checks whether the second argument is a subterm of the first.  (We don't care
1056 about binders, as we are only interested in syntactic subterms.)
1057
1058 \begin{code}
1059 tcPartOfType :: Type -> Type -> Bool
1060 tcPartOfType t1              t2
1061   | tcEqType t1 t2              = True
1062 tcPartOfType t1              t2
1063   | Just t2' <- tcView t2       = tcPartOfType t1 t2'
1064 tcPartOfType _  (TyVarTy _)     = False
1065 tcPartOfType t1 (ForAllTy _ t2) = tcPartOfType t1 t2
1066 tcPartOfType t1 (AppTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
1067 tcPartOfType t1 (FunTy s2 t2)   = tcPartOfType t1 s2 || tcPartOfType t1 t2
1068 tcPartOfType t1 (PredTy p2)     = tcPartOfPred t1 p2
1069 tcPartOfType t1 (TyConApp _ ts) = any (tcPartOfType t1) ts
1070 tcPartOfType t1 (NoteTy _ t2)   = tcPartOfType t1 t2
1071
1072 tcPartOfPred :: Type -> PredType -> Bool
1073 tcPartOfPred t1 (IParam _ t2)  = tcPartOfType t1 t2
1074 tcPartOfPred t1 (ClassP _ ts)  = any (tcPartOfType t1) ts
1075 tcPartOfPred t1 (EqPred s2 t2) = tcPartOfType t1 s2 || tcPartOfType t1 t2
1076 \end{code}
1077
1078 Now here comes the real worker
1079
1080 \begin{code}
1081 cmpType :: Type -> Type -> Ordering
1082 cmpType t1 t2 = cmpTypeX rn_env t1 t2
1083   where
1084     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
1085
1086 cmpTypes :: [Type] -> [Type] -> Ordering
1087 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
1088   where
1089     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
1090
1091 cmpPred :: PredType -> PredType -> Ordering
1092 cmpPred p1 p2 = cmpPredX rn_env p1 p2
1093   where
1094     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
1095
1096 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
1097 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
1098                    | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
1099
1100 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
1101 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
1102 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1103 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
1104 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
1105 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
1106 cmpTypeX env t1                 (NoteTy _ t2)        = cmpTypeX env t1 t2
1107
1108     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1109 cmpTypeX _ (AppTy _ _)    (TyVarTy _)    = GT
1110
1111 cmpTypeX _ (FunTy _ _)    (TyVarTy _)    = GT
1112 cmpTypeX _ (FunTy _ _)    (AppTy _ _)    = GT
1113
1114 cmpTypeX _ (TyConApp _ _) (TyVarTy _)    = GT
1115 cmpTypeX _ (TyConApp _ _) (AppTy _ _)    = GT
1116 cmpTypeX _ (TyConApp _ _) (FunTy _ _)    = GT
1117
1118 cmpTypeX _ (ForAllTy _ _) (TyVarTy _)    = GT
1119 cmpTypeX _ (ForAllTy _ _) (AppTy _ _)    = GT
1120 cmpTypeX _ (ForAllTy _ _) (FunTy _ _)    = GT
1121 cmpTypeX _ (ForAllTy _ _) (TyConApp _ _) = GT
1122
1123 cmpTypeX _ (PredTy _)     _              = GT
1124
1125 cmpTypeX _ _              _              = LT
1126
1127 -------------
1128 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1129 cmpTypesX _   []        []        = EQ
1130 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1131 cmpTypesX _   []        _         = LT
1132 cmpTypesX _   _         []        = GT
1133
1134 -------------
1135 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1136 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1137         -- Compare names only for implicit parameters
1138         -- This comparison is used exclusively (I believe)
1139         -- for the Avails finite map built in TcSimplify
1140         -- If the types differ we keep them distinct so that we see
1141         -- a distinct pair to run improvement on
1142 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTypesX env tys1 tys2)
1143 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1144
1145 -- Constructor order: IParam < ClassP < EqPred
1146 cmpPredX _   (IParam {})     _              = LT
1147 cmpPredX _   (ClassP {})    (IParam {})     = GT
1148 cmpPredX _   (ClassP {})    (EqPred {})     = LT
1149 cmpPredX _   (EqPred {})    _               = GT
1150 \end{code}
1151
1152 PredTypes are used as a FM key in TcSimplify,
1153 so we take the easy path and make them an instance of Ord
1154
1155 \begin{code}
1156 instance Eq  PredType where { (==)    = tcEqPred }
1157 instance Ord PredType where { compare = tcCmpPred }
1158 \end{code}
1159
1160
1161 %************************************************************************
1162 %*                                                                      *
1163                 Type substitutions
1164 %*                                                                      *
1165 %************************************************************************
1166
1167 \begin{code}
1168 data TvSubst
1169   = TvSubst InScopeSet  -- The in-scope type variables
1170             TvSubstEnv  -- The substitution itself
1171         -- See Note [Apply Once]
1172         -- and Note [Extending the TvSubstEnv]
1173
1174 {- ----------------------------------------------------------
1175
1176 Note [Apply Once]
1177 ~~~~~~~~~~~~~~~~~
1178 We use TvSubsts to instantiate things, and we might instantiate
1179         forall a b. ty
1180 \with the types
1181         [a, b], or [b, a].
1182 So the substition might go [a->b, b->a].  A similar situation arises in Core
1183 when we find a beta redex like
1184         (/\ a /\ b -> e) b a
1185 Then we also end up with a substition that permutes type variables. Other
1186 variations happen to; for example [a -> (a, b)].
1187
1188         ***************************************************
1189         *** So a TvSubst must be applied precisely once ***
1190         ***************************************************
1191
1192 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1193 we use during unifications, it must not be repeatedly applied.
1194
1195 Note [Extending the TvSubst]
1196 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1197 The following invariant should hold of a TvSubst
1198
1199         The in-scope set is needed *only* to
1200         guide the generation of fresh uniques
1201
1202         In particular, the *kind* of the type variables in
1203         the in-scope set is not relevant
1204
1205 This invariant allows a short-cut when the TvSubstEnv is empty:
1206 if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
1207 then (substTy subst ty) does nothing.
1208
1209 For example, consider:
1210         (/\a. /\b:(a~Int). ...b..) Int
1211 We substitute Int for 'a'.  The Unique of 'b' does not change, but
1212 nevertheless we add 'b' to the TvSubstEnv, because b's type does change
1213
1214 This invariant has several crucial consequences:
1215
1216 * In substTyVarBndr, we need extend the TvSubstEnv
1217         - if the unique has changed
1218         - or if the kind has changed
1219
1220 * In substTyVar, we do not need to consult the in-scope set;
1221   the TvSubstEnv is enough
1222
1223 * In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
1224
1225
1226 -------------------------------------------------------------- -}
1227
1228
1229 type TvSubstEnv = TyVarEnv Type
1230         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1231         -- invariant discussed in Note [Apply Once]), and also independently
1232         -- in the middle of matching, and unification (see Types.Unify)
1233         -- So you have to look at the context to know if it's idempotent or
1234         -- apply-once or whatever
1235 emptyTvSubstEnv :: TvSubstEnv
1236 emptyTvSubstEnv = emptyVarEnv
1237
1238 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1239 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1240 -- It assumes that both are idempotent
1241 -- Typically, env1 is the refinement to a base substitution env2
1242 composeTvSubst in_scope env1 env2
1243   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1244         -- First apply env1 to the range of env2
1245         -- Then combine the two, making sure that env1 loses if
1246         -- both bind the same variable; that's why env1 is the
1247         --  *left* argument to plusVarEnv, because the right arg wins
1248   where
1249     subst1 = TvSubst in_scope env1
1250
1251 emptyTvSubst :: TvSubst
1252 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1253
1254 isEmptyTvSubst :: TvSubst -> Bool
1255          -- See Note [Extending the TvSubstEnv]
1256 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1257
1258 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1259 mkTvSubst = TvSubst
1260
1261 getTvSubstEnv :: TvSubst -> TvSubstEnv
1262 getTvSubstEnv (TvSubst _ env) = env
1263
1264 getTvInScope :: TvSubst -> InScopeSet
1265 getTvInScope (TvSubst in_scope _) = in_scope
1266
1267 isInScope :: Var -> TvSubst -> Bool
1268 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1269
1270 notElemTvSubst :: TyVar -> TvSubst -> Bool
1271 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1272
1273 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1274 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1275
1276 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1277 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1278
1279 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1280 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1281
1282 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1283 extendTvSubstList (TvSubst in_scope env) tvs tys
1284   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1285
1286 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1287 -- the types given; but it's just a thunk so with a bit of luck
1288 -- it'll never be evaluated
1289
1290 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1291 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1292
1293 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1294 zipOpenTvSubst tyvars tys
1295 #ifdef DEBUG
1296   | length tyvars /= length tys
1297   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1298   | otherwise
1299 #endif
1300   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1301
1302 -- mkTopTvSubst is called when doing top-level substitutions.
1303 -- Here we expect that the free vars of the range of the
1304 -- substitution will be empty.
1305 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1306 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1307
1308 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1309 zipTopTvSubst tyvars tys
1310 #ifdef DEBUG
1311   | length tyvars /= length tys
1312   = pprTrace "zipTopTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1313   | otherwise
1314 #endif
1315   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1316
1317 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1318 zipTyEnv tyvars tys
1319 #ifdef DEBUG
1320   | length tyvars /= length tys
1321   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1322   | otherwise
1323 #endif
1324   = zip_ty_env tyvars tys emptyVarEnv
1325
1326 -- Later substitutions in the list over-ride earlier ones,
1327 -- but there should be no loops
1328 zip_ty_env :: [TyVar] -> [Type] -> TvSubstEnv -> TvSubstEnv
1329 zip_ty_env []       []       env = env
1330 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1331         -- There used to be a special case for when
1332         --      ty == TyVarTy tv
1333         -- (a not-uncommon case) in which case the substitution was dropped.
1334         -- But the type-tidier changes the print-name of a type variable without
1335         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1336         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1337         -- And it happened that t was the type variable of the class.  Post-tiding,
1338         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1339         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1340         -- and so generated a rep type mentioning t not t2.
1341         --
1342         -- Simplest fix is to nuke the "optimisation"
1343 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1344 -- zip_ty_env _ _ env = env
1345
1346 instance Outputable TvSubst where
1347   ppr (TvSubst ins env)
1348     = brackets $ sep[ ptext SLIT("TvSubst"),
1349                       nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1350                       nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1351 \end{code}
1352
1353 %************************************************************************
1354 %*                                                                      *
1355                 Performing type substitutions
1356 %*                                                                      *
1357 %************************************************************************
1358
1359 \begin{code}
1360 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1361 substTyWith tvs tys = ASSERT( length tvs == length tys )
1362                       substTy (zipOpenTvSubst tvs tys)
1363
1364 substTy :: TvSubst -> Type  -> Type
1365 substTy subst ty | isEmptyTvSubst subst = ty
1366                  | otherwise            = subst_ty subst ty
1367
1368 substTys :: TvSubst -> [Type] -> [Type]
1369 substTys subst tys | isEmptyTvSubst subst = tys
1370                    | otherwise            = map (subst_ty subst) tys
1371
1372 substTheta :: TvSubst -> ThetaType -> ThetaType
1373 substTheta subst theta
1374   | isEmptyTvSubst subst = theta
1375   | otherwise            = map (substPred subst) theta
1376
1377 substPred :: TvSubst -> PredType -> PredType
1378 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1379 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1380 substPred subst (EqPred ty1 ty2)  = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1381
1382 deShadowTy :: TyVarSet -> Type -> Type  -- Remove any nested binders mentioning tvs
1383 deShadowTy tvs ty
1384   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1385   where
1386     in_scope = mkInScopeSet tvs
1387
1388 subst_ty :: TvSubst -> Type -> Type
1389 -- subst_ty is the main workhorse for type substitution
1390 --
1391 -- Note that the in_scope set is poked only if we hit a forall
1392 -- so it may often never be fully computed
1393 subst_ty subst ty
1394    = go ty
1395   where
1396     go (TyVarTy tv)                = substTyVar subst tv
1397     go (TyConApp tc tys)           = let args = map go tys
1398                                      in  args `seqList` TyConApp tc args
1399
1400     go (PredTy p)                  = PredTy $! (substPred subst p)
1401
1402     go (NoteTy (FTVNote _) ty2)    = go ty2 -- Discard the free tyvar note
1403
1404     go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
1405     go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
1406                 -- The mkAppTy smart constructor is important
1407                 -- we might be replacing (a Int), represented with App
1408                 -- by [Int], represented with TyConApp
1409     go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
1410                                      (subst', tv') ->
1411                                          ForAllTy tv' $! (subst_ty subst' ty)
1412
1413 substTyVar :: TvSubst -> TyVar  -> Type
1414 substTyVar subst@(TvSubst _ _) tv
1415   = case lookupTyVar subst tv of {
1416         Nothing -> TyVarTy tv;
1417         Just ty -> ty   -- See Note [Apply Once]
1418     }
1419
1420 substTyVars :: TvSubst -> [TyVar] -> [Type]
1421 substTyVars subst tvs = map (substTyVar subst) tvs
1422
1423 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1424         -- See Note [Extending the TvSubst]
1425 lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
1426
1427 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1428 substTyVarBndr subst@(TvSubst in_scope env) old_var
1429   = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1430   where
1431     is_co_var = isCoVar old_var
1432
1433     new_env | no_change = delVarEnv env old_var
1434             | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1435
1436     no_change = new_var == old_var && not is_co_var
1437         -- no_change means that the new_var is identical in
1438         -- all respects to the old_var (same unique, same kind)
1439         -- See Note [Extending the TvSubst]
1440         --
1441         -- In that case we don't need to extend the substitution
1442         -- to map old to new.  But instead we must zap any
1443         -- current substitution for the variable. For example:
1444         --      (\x.e) with id_subst = [x |-> e']
1445         -- Here we must simply zap the substitution for x
1446
1447     new_var = uniqAway in_scope subst_old_var
1448         -- The uniqAway part makes sure the new variable is not already in scope
1449
1450     subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1451                   -- It's only worth doing the substitution for coercions,
1452                   -- becuase only they can have free type variables
1453         | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
1454         | otherwise = old_var
1455 \end{code}
1456
1457 ----------------------------------------------------
1458 -- Kind Stuff
1459
1460 Kinds
1461 ~~~~~
1462 There's a little subtyping at the kind level:
1463
1464                  ?
1465                 / \
1466                /   \
1467               ??   (#)
1468              /  \
1469             *   #
1470
1471 where   *    [LiftedTypeKind]   means boxed type
1472         #    [UnliftedTypeKind] means unboxed type
1473         (#)  [UbxTupleKind]     means unboxed tuple
1474         ??   [ArgTypeKind]      is the lub of *,#
1475         ?    [OpenTypeKind]     means any type at all
1476
1477 In particular:
1478
1479         error :: forall a:?. String -> a
1480         (->)  :: ?? -> ? -> *
1481         (\(x::t) -> ...)        Here t::?? (i.e. not unboxed tuple)
1482
1483 \begin{code}
1484 type KindVar = TyVar  -- invariant: KindVar will always be a
1485                       -- TcTyVar with details MetaTv TauTv ...
1486 -- kind var constructors and functions are in TcType
1487
1488 type SimpleKind = Kind
1489 \end{code}
1490
1491 Kind inference
1492 ~~~~~~~~~~~~~~
1493 During kind inference, a kind variable unifies only with
1494 a "simple kind", sk
1495         sk ::= * | sk1 -> sk2
1496 For example
1497         data T a = MkT a (T Int#)
1498 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1499 with # (the kind of Int#).
1500
1501 Type inference
1502 ~~~~~~~~~~~~~~
1503 When creating a fresh internal type variable, we give it a kind to express
1504 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
1505 with kind ??.
1506
1507 During unification we only bind an internal type variable to a type
1508 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1509
1510 When unifying two internal type variables, we collect their kind constraints by
1511 finding the GLB of the two.  Since the partial order is a tree, they only
1512 have a glb if one is a sub-kind of the other.  In that case, we bind the
1513 less-informative one to the more informative one.  Neat, eh?
1514
1515
1516 \begin{code}
1517
1518 \end{code}
1519
1520 %************************************************************************
1521 %*                                                                      *
1522         Functions over Kinds
1523 %*                                                                      *
1524 %************************************************************************
1525
1526 \begin{code}
1527 kindFunResult :: Kind -> Kind
1528 kindFunResult k = funResultTy k
1529
1530 splitKindFunTys :: Kind -> ([Kind],Kind)
1531 splitKindFunTys k = splitFunTys k
1532
1533 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1534 splitKindFunTysN k = splitFunTysN k
1535
1536 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1537 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
1538         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
1539
1540 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
1541
1542 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1543 isOpenTypeKind _               = False
1544
1545 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1546
1547 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1548 isUbxTupleKind _               = False
1549
1550 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1551
1552 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1553 isArgTypeKind _               = False
1554
1555 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1556
1557 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1558 isUnliftedTypeKind _               = False
1559
1560 isSubOpenTypeKind :: Kind -> Bool
1561 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1562 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1563                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1564                                      False
1565 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1566 isSubOpenTypeKind other            = ASSERT( isKind other ) False
1567          -- This is a conservative answer
1568          -- It matters in the call to isSubKind in
1569          -- checkExpectedKind.
1570
1571 isSubArgTypeKindCon kc
1572   | isUnliftedTypeKindCon kc = True
1573   | isLiftedTypeKindCon kc   = True
1574   | isArgTypeKindCon kc      = True
1575   | otherwise                = False
1576
1577 isSubArgTypeKind :: Kind -> Bool
1578 -- True of any sub-kind of ArgTypeKind
1579 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1580 isSubArgTypeKind _                = False
1581
1582 isSuperKind :: Type -> Bool
1583 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1584 isSuperKind _                   = False
1585
1586 isKind :: Kind -> Bool
1587 isKind k = isSuperKind (typeKind k)
1588
1589 isSubKind :: Kind -> Kind -> Bool
1590 -- (k1 `isSubKind` k2) checks that k1 <: k2
1591 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
1592 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1593 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
1594   = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1595 isSubKind _             _                     = False
1596
1597 eqKind :: Kind -> Kind -> Bool
1598 eqKind = tcEqType
1599
1600 isSubKindCon :: TyCon -> TyCon -> Bool
1601 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1602 isSubKindCon kc1 kc2
1603   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
1604   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1605   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
1606   | isOpenTypeKindCon kc2                                  = True
1607                            -- we already know kc1 is not a fun, its a TyCon
1608   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
1609   | otherwise                                              = False
1610
1611 defaultKind :: Kind -> Kind
1612 -- Used when generalising: default kind '?' and '??' to '*'
1613 --
1614 -- When we generalise, we make generic type variables whose kind is
1615 -- simple (* or *->* etc).  So generic type variables (other than
1616 -- built-in constants like 'error') always have simple kinds.  This is important;
1617 -- consider
1618 --      f x = True
1619 -- We want f to get type
1620 --      f :: forall (a::*). a -> Bool
1621 -- Not
1622 --      f :: forall (a::??). a -> Bool
1623 -- because that would allow a call like (f 3#) as well as (f True),
1624 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
1625 defaultKind k
1626   | isSubOpenTypeKind k = liftedTypeKind
1627   | isSubArgTypeKind k  = liftedTypeKind
1628   | otherwise        = k
1629
1630 isEqPred :: PredType -> Bool
1631 isEqPred (EqPred _ _) = True
1632 isEqPred _            = False
1633 \end{code}