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