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