compiler/types/Type.lhs

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