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