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') -> ForAllTy tv' $! (subst_ty subst' ty)
1416
1417 substTyVar :: TvSubst -> TyVar  -> Type
1418 substTyVar subst@(TvSubst _ _) tv
1419   = case lookupTyVar subst tv of {
1420         Nothing -> TyVarTy tv;
1421         Just ty -> ty   -- See Note [Apply Once]
1422     }
1423
1424 substTyVars :: TvSubst -> [TyVar] -> [Type]
1425 substTyVars subst tvs = map (substTyVar subst) tvs
1426
1427 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1428         -- See Note [Extending the TvSubst]
1429 lookupTyVar (TvSubst _ env) tv = lookupVarEnv env tv
1430
1431 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1432 substTyVarBndr subst@(TvSubst in_scope env) old_var
1433   = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1434   where
1435     is_co_var = isCoVar old_var
1436
1437     new_env | no_change = delVarEnv env old_var
1438             | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1439
1440     no_change = new_var == old_var && not is_co_var
1441         -- no_change means that the new_var is identical in
1442         -- all respects to the old_var (same unique, same kind)
1443         -- See Note [Extending the TvSubst]
1444         --
1445         -- In that case we don't need to extend the substitution
1446         -- to map old to new.  But instead we must zap any
1447         -- current substitution for the variable. For example:
1448         --      (\x.e) with id_subst = [x |-> e']
1449         -- Here we must simply zap the substitution for x
1450
1451     new_var = uniqAway in_scope subst_old_var
1452         -- The uniqAway part makes sure the new variable is not already in scope
1453
1454     subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1455                   -- It's only worth doing the substitution for coercions,
1456                   -- becuase only they can have free type variables
1457         | is_co_var = setTyVarKind old_var (substTy subst (tyVarKind old_var))
1458         | otherwise = old_var
1459 \end{code}
1460
1461 ----------------------------------------------------
1462 -- Kind Stuff
1463
1464 Kinds
1465 ~~~~~
1466 There's a little subtyping at the kind level:
1467
1468                  ?
1469                 / \
1470                /   \
1471               ??   (#)
1472              /  \
1473             *   #
1474
1475 where   *    [LiftedTypeKind]   means boxed type
1476         #    [UnliftedTypeKind] means unboxed type
1477         (#)  [UbxTupleKind]     means unboxed tuple
1478         ??   [ArgTypeKind]      is the lub of *,#
1479         ?    [OpenTypeKind]     means any type at all
1480
1481 In particular:
1482
1483         error :: forall a:?. String -> a
1484         (->)  :: ?? -> ? -> *
1485         (\(x::t) -> ...)        Here t::?? (i.e. not unboxed tuple)
1486
1487 \begin{code}
1488 type KindVar = TyVar  -- invariant: KindVar will always be a
1489                       -- TcTyVar with details MetaTv TauTv ...
1490 -- kind var constructors and functions are in TcType
1491
1492 type SimpleKind = Kind
1493 \end{code}
1494
1495 Kind inference
1496 ~~~~~~~~~~~~~~
1497 During kind inference, a kind variable unifies only with
1498 a "simple kind", sk
1499         sk ::= * | sk1 -> sk2
1500 For example
1501         data T a = MkT a (T Int#)
1502 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1503 with # (the kind of Int#).
1504
1505 Type inference
1506 ~~~~~~~~~~~~~~
1507 When creating a fresh internal type variable, we give it a kind to express
1508 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
1509 with kind ??.
1510
1511 During unification we only bind an internal type variable to a type
1512 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1513
1514 When unifying two internal type variables, we collect their kind constraints by
1515 finding the GLB of the two.  Since the partial order is a tree, they only
1516 have a glb if one is a sub-kind of the other.  In that case, we bind the
1517 less-informative one to the more informative one.  Neat, eh?
1518
1519
1520 \begin{code}
1521
1522 \end{code}
1523
1524 %************************************************************************
1525 %*                                                                      *
1526         Functions over Kinds
1527 %*                                                                      *
1528 %************************************************************************
1529
1530 \begin{code}
1531 kindFunResult :: Kind -> Kind
1532 kindFunResult k = funResultTy k
1533
1534 splitKindFunTys :: Kind -> ([Kind],Kind)
1535 splitKindFunTys k = splitFunTys k
1536
1537 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1538 splitKindFunTysN k = splitFunTysN k
1539
1540 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1541 isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
1542         isUnliftedTypeKindCon, isSubArgTypeKindCon      :: TyCon -> Bool
1543
1544 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
1545
1546 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1547 isOpenTypeKind _               = False
1548
1549 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1550
1551 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1552 isUbxTupleKind _               = False
1553
1554 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1555
1556 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1557 isArgTypeKind _               = False
1558
1559 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1560
1561 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1562 isUnliftedTypeKind _               = False
1563
1564 isSubOpenTypeKind :: Kind -> Bool
1565 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1566 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1567                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1568                                      False
1569 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1570 isSubOpenTypeKind other            = ASSERT( isKind other ) False
1571          -- This is a conservative answer
1572          -- It matters in the call to isSubKind in
1573          -- checkExpectedKind.
1574
1575 isSubArgTypeKindCon kc
1576   | isUnliftedTypeKindCon kc = True
1577   | isLiftedTypeKindCon kc   = True
1578   | isArgTypeKindCon kc      = True
1579   | otherwise                = False
1580
1581 isSubArgTypeKind :: Kind -> Bool
1582 -- True of any sub-kind of ArgTypeKind
1583 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1584 isSubArgTypeKind _                = False
1585
1586 isSuperKind :: Type -> Bool
1587 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1588 isSuperKind _                   = False
1589
1590 isKind :: Kind -> Bool
1591 isKind k = isSuperKind (typeKind k)
1592
1593 isSubKind :: Kind -> Kind -> Bool
1594 -- (k1 `isSubKind` k2) checks that k1 <: k2
1595 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc2
1596 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1597 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
1598   = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1599 isSubKind _             _                     = False
1600
1601 eqKind :: Kind -> Kind -> Bool
1602 eqKind = tcEqType
1603
1604 isSubKindCon :: TyCon -> TyCon -> Bool
1605 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1606 isSubKindCon kc1 kc2
1607   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
1608   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1609   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
1610   | isOpenTypeKindCon kc2                                  = True
1611                            -- we already know kc1 is not a fun, its a TyCon
1612   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
1613   | otherwise                                              = False
1614
1615 defaultKind :: Kind -> Kind
1616 -- Used when generalising: default kind '?' and '??' to '*'
1617 --
1618 -- When we generalise, we make generic type variables whose kind is
1619 -- simple (* or *->* etc).  So generic type variables (other than
1620 -- built-in constants like 'error') always have simple kinds.  This is important;
1621 -- consider
1622 --      f x = True
1623 -- We want f to get type
1624 --      f :: forall (a::*). a -> Bool
1625 -- Not
1626 --      f :: forall (a::??). a -> Bool
1627 -- because that would allow a call like (f 3#) as well as (f True),
1628 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
1629 defaultKind k
1630   | isSubOpenTypeKind k = liftedTypeKind
1631   | isSubArgTypeKind k  = liftedTypeKind
1632   | otherwise        = k
1633
1634 isEqPred :: PredType -> Bool
1635 isEqPred (EqPred _ _) = True
1636 isEqPred _            = False
1637 \end{code}