compiler/types/Type.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4 \section[Type]{Type - public interface}
   5
   6
   7 \begin{code}
   8 module Type (
   9         -- re-exports from TypeRep
  10         TyThing(..), Type, PredType(..), ThetaType,
  11         funTyCon,
  12
  13         -- Kinds
  14         Kind, SimpleKind, KindVar,
  15         kindFunResult, splitKindFunTys, splitKindFunTysN,
  16
  17         liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
  18         argTypeKindTyCon, ubxTupleKindTyCon,
  19
  20         liftedTypeKind, unliftedTypeKind, openTypeKind,
  21         argTypeKind, ubxTupleKind,
  22
  23         tySuperKind, coSuperKind,
  24
  25         isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
  26         isUbxTupleKind, isArgTypeKind, isKind, isTySuperKind,
  27         isCoSuperKind, isSuperKind, isCoercionKind, isEqPred,
  28         mkArrowKind, mkArrowKinds,
  29
  30         isSubArgTypeKind, isSubOpenTypeKind, isSubKind, defaultKind, eqKind,
  31         isSubKindCon,
  32
  33         -- Re-exports from TyCon
  34         PrimRep(..),
  35
  36         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
  37
  38         mkAppTy, mkAppTys, splitAppTy, splitAppTys,
  39         splitAppTy_maybe, repSplitAppTy_maybe,
  40
  41         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
  42         splitFunTys, splitFunTysN,
  43         funResultTy, funArgTy, zipFunTys, isFunTy,
  44
  45         mkTyConApp, mkTyConTy,
  46         tyConAppTyCon, tyConAppArgs,
  47         splitTyConApp_maybe, splitTyConApp,
  48         splitNewTyConApp_maybe, splitNewTyConApp,
  49
  50         repType, typePrimRep, coreView, tcView, kindView,
  51
  52         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
  53         applyTy, applyTys, isForAllTy, dropForAlls,
  54
  55         -- Source types
  56         predTypeRep, mkPredTy, mkPredTys,
  57
  58         -- Newtypes
  59         splitRecNewType_maybe, newTyConInstRhs,
  60
  61         -- Lifting and boxity
  62         isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
  63         isStrictType, isStrictPred,
  64
  65         -- Free variables
  66         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
  67         typeKind, addFreeTyVars,
  68
  69         -- Tidying up for printing
  70         tidyType,      tidyTypes,
  71         tidyOpenType,  tidyOpenTypes,
  72         tidyTyVarBndr, tidyFreeTyVars,
  73         tidyOpenTyVar, tidyOpenTyVars,
  74         tidyTopType,   tidyPred,
  75         tidyKind,
  76
  77         -- Comparison
  78         coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
  79         tcEqPred, tcCmpPred, tcEqTypeX,
  80
  81         -- Seq
  82         seqType, seqTypes,
  83
  84         -- Type substitutions
  85         TvSubstEnv, emptyTvSubstEnv,    -- Representation widely visible
  86         TvSubst(..), emptyTvSubst,      -- Representation visible to a few friends
  87         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
  88         getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
  89         extendTvSubst, extendTvSubstList, isInScope, composeTvSubst, zipTyEnv,
  90
  91         -- Performing substitution on types
  92         substTy, substTys, substTyWith, substTheta,
  93         substPred, substTyVar, substTyVarBndr, deShadowTy, lookupTyVar,
  94
  95         -- Pretty-printing
  96         pprType, pprParendType, pprTyThingCategory,
  97         pprPred, pprTheta, pprThetaArrow, pprClassPred, pprKind, pprParendKind
  98     ) where
  99
 100 #include "HsVersions.h"
 101
 102 -- We import the representation and primitive functions from TypeRep.
 103 -- Many things are reexported, but not the representation!
 104
 105 import TypeRep
 106
 107 -- friends:
 108 import Var      ( Var, TyVar, tyVarKind, tyVarName,
 109                   setTyVarName, setTyVarKind, mkWildCoVar )
 110 import VarEnv
 111 import VarSet
 112
 113 import OccName  ( tidyOccName )
 114 import Name     ( NamedThing(..), tidyNameOcc )
 115 import Class    ( Class, classTyCon )
 116 import PrelNames( openTypeKindTyConKey, unliftedTypeKindTyConKey,
 117                   ubxTupleKindTyConKey, argTypeKindTyConKey )
 118 import TyCon    ( TyCon, isRecursiveTyCon, isPrimTyCon,
 119                   isUnboxedTupleTyCon, isUnLiftedTyCon,
 120                   isFunTyCon, isNewTyCon, isOpenTyCon, newTyConRep,
 121                   newTyConRhs,
 122                   isAlgTyCon, tyConArity, isSuperKindTyCon,
 123                   tcExpandTyCon_maybe, coreExpandTyCon_maybe,
 124                   tyConKind, PrimRep(..), tyConPrimRep, tyConUnique,
 125                   isCoercionTyCon_maybe, isCoercionTyCon
 126                 )
 127
 128 -- others
 129 import StaticFlags      ( opt_DictsStrict )
 130 import Util             ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual, all2 )
 131 import Outputable
 132 import UniqSet          ( sizeUniqSet )         -- Should come via VarSet
 133 import 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 -- get instantiated newtype rhs, the arguments had better saturate
 418 -- the constructor
 419 newTyConInstRhs :: TyCon -> [Type] -> Type
 420 newTyConInstRhs tycon tys =
 421     let (tvs, ty) = newTyConRhs tycon in substTyWith tvs tys ty
 422
 423 \end{code}
 424
 425
 426 ---------------------------------------------------------------------
 427                                 SynTy
 428                                 ~~~~~
 429
 430 Notes on type synonyms
 431 ~~~~~~~~~~~~~~~~~~~~~~
 432 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
 433 to return type synonyms whereever possible. Thus
 434
 435         type Foo a = a -> a
 436
 437 we want
 438         splitFunTys (a -> Foo a) = ([a], Foo a)
 439 not                                ([a], a -> a)
 440
 441 The reason is that we then get better (shorter) type signatures in
 442 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 443
 444
 445                 Representation types
 446                 ~~~~~~~~~~~~~~~~~~~~
 447 repType looks through
 448         (a) for-alls, and
 449         (b) synonyms
 450         (c) predicates
 451         (d) usage annotations
 452         (e) all newtypes, including recursive ones, but not newtype families
 453 It's useful in the back end.
 454
 455 \begin{code}
 456 repType :: Type -> Type
 457 -- Only applied to types of kind *; hence tycons are saturated
 458 repType ty | Just ty' <- coreView ty = repType ty'
 459 repType (ForAllTy _ ty)  = repType ty
 460 repType (TyConApp tc tys)
 461   | isNewTyCon tc &&
 462     not (isOpenTyCon tc) = -- Recursive newtypes are opaque to coreView
 463                            -- but we must expand them here.  Sure to
 464                            -- be saturated because repType is only applied
 465                            -- to types of kind *
 466                            ASSERT( {- isRecursiveTyCon tc && -} tys `lengthIs` tyConArity tc )
 467                            repType (new_type_rep tc tys)
 468 repType ty = ty
 469
 470 -- new_type_rep doesn't ask any questions:
 471 -- it just expands newtype, whether recursive or not
 472 new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
 473                              case newTyConRep new_tycon of
 474                                  (tvs, rep_ty) -> substTyWith tvs tys rep_ty
 475
 476 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
 477 -- of inspecting the type directly.
 478 typePrimRep :: Type -> PrimRep
 479 typePrimRep ty = case repType ty of
 480                    TyConApp tc _ -> tyConPrimRep tc
 481                    FunTy _ _     -> PtrRep
 482                    AppTy _ _     -> PtrRep      -- See note below
 483                    TyVarTy _     -> PtrRep
 484                    other         -> pprPanic "typePrimRep" (ppr ty)
 485         -- Types of the form 'f a' must be of kind *, not *#, so
 486         -- we are guaranteed that they are represented by pointers.
 487         -- The reason is that f must have kind *->*, not *->*#, because
 488         -- (we claim) there is no way to constrain f's kind any other
 489         -- way.
 490
 491 \end{code}
 492
 493
 494 ---------------------------------------------------------------------
 495                                 ForAllTy
 496                                 ~~~~~~~~
 497
 498 \begin{code}
 499 mkForAllTy :: TyVar -> Type -> Type
 500 mkForAllTy tyvar ty
 501   = mkForAllTys [tyvar] ty
 502
 503 mkForAllTys :: [TyVar] -> Type -> Type
 504 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 505
 506 isForAllTy :: Type -> Bool
 507 isForAllTy (NoteTy _ ty)  = isForAllTy ty
 508 isForAllTy (ForAllTy _ _) = True
 509 isForAllTy other_ty       = False
 510
 511 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 512 splitForAllTy_maybe ty = splitFAT_m ty
 513   where
 514     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
 515     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
 516     splitFAT_m _                            = Nothing
 517
 518 splitForAllTys :: Type -> ([TyVar], Type)
 519 splitForAllTys ty = split ty ty []
 520    where
 521      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
 522      split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
 523      split orig_ty t                 tvs = (reverse tvs, orig_ty)
 524
 525 dropForAlls :: Type -> Type
 526 dropForAlls ty = snd (splitForAllTys ty)
 527 \end{code}
 528
 529 -- (mkPiType now in CoreUtils)
 530
 531 applyTy, applyTys
 532 ~~~~~~~~~~~~~~~~~
 533 Instantiate a for-all type with one or more type arguments.
 534 Used when we have a polymorphic function applied to type args:
 535         f t1 t2
 536 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
 537 the expression.
 538
 539 \begin{code}
 540 applyTy :: Type -> Type -> Type
 541 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
 542 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
 543 applyTy other            arg = panic "applyTy"
 544
 545 applyTys :: Type -> [Type] -> Type
 546 -- This function is interesting because
 547 --      a) the function may have more for-alls than there are args
 548 --      b) less obviously, it may have fewer for-alls
 549 -- For case (b) think of
 550 --      applyTys (forall a.a) [forall b.b, Int]
 551 -- This really can happen, via dressing up polymorphic types with newtype
 552 -- clothing.  Here's an example:
 553 --      newtype R = R (forall a. a->a)
 554 --      foo = case undefined :: R of
 555 --              R f -> f ()
 556
 557 applyTys orig_fun_ty []      = orig_fun_ty
 558 applyTys orig_fun_ty arg_tys
 559   | n_tvs == n_args     -- The vastly common case
 560   = substTyWith tvs arg_tys rho_ty
 561   | n_tvs > n_args      -- Too many for-alls
 562   = substTyWith (take n_args tvs) arg_tys
 563                 (mkForAllTys (drop n_args tvs) rho_ty)
 564   | otherwise           -- Too many type args
 565   = ASSERT2( n_tvs > 0, ppr orig_fun_ty )       -- Zero case gives infnite loop!
 566     applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
 567              (drop n_tvs arg_tys)
 568   where
 569     (tvs, rho_ty) = splitForAllTys orig_fun_ty
 570     n_tvs = length tvs
 571     n_args = length arg_tys
 572 \end{code}
 573
 574
 575 %************************************************************************
 576 %*                                                                      *
 577 \subsection{Source types}
 578 %*                                                                      *
 579 %************************************************************************
 580
 581 A "source type" is a type that is a separate type as far as the type checker is
 582 concerned, but which has low-level representation as far as the back end is concerned.
 583
 584 Source types are always lifted.
 585
 586 The key function is predTypeRep which gives the representation of a source type:
 587
 588 \begin{code}
 589 mkPredTy :: PredType -> Type
 590 mkPredTy pred = PredTy pred
 591
 592 mkPredTys :: ThetaType -> [Type]
 593 mkPredTys preds = map PredTy preds
 594
 595 predTypeRep :: PredType -> Type
 596 -- Convert a PredType to its "representation type";
 597 -- the post-type-checking type used by all the Core passes of GHC.
 598 -- Unwraps only the outermost level; for example, the result might
 599 -- be a newtype application
 600 predTypeRep (IParam _ ty)     = ty
 601 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
 602         -- Result might be a newtype application, but the consumer will
 603         -- look through that too if necessary
 604 predTypeRep (EqPred ty1 ty2) = pprPanic "predTypeRep" (ppr (EqPred ty1 ty2))
 605 \end{code}
 606
 607
 608 %************************************************************************
 609 %*                                                                      *
 610                 NewTypes
 611 %*                                                                      *
 612 %************************************************************************
 613
 614 \begin{code}
 615 splitRecNewType_maybe :: Type -> Maybe Type
 616 -- Sometimes we want to look through a recursive newtype, and that's what happens here
 617 -- It only strips *one layer* off, so the caller will usually call itself recursively
 618 -- Only applied to types of kind *, hence the newtype is always saturated
 619 splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
 620 splitRecNewType_maybe (TyConApp tc tys)
 621   | isNewTyCon tc
 622   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitRecNewType_maybe only be applied
 623                                                 --      to *types* (of kind *)
 624     ASSERT( isRecursiveTyCon tc )               -- Guaranteed by coreView
 625     case newTyConRhs tc of
 626         (tvs, rep_ty) -> ASSERT( length tvs == length tys )
 627                          Just (substTyWith tvs tys rep_ty)
 628
 629 splitRecNewType_maybe other = Nothing
 630
 631
 632
 633 \end{code}
 634
 635
 636 %************************************************************************
 637 %*                                                                      *
 638 \subsection{Kinds and free variables}
 639 %*                                                                      *
 640 %************************************************************************
 641
 642 ---------------------------------------------------------------------
 643                 Finding the kind of a type
 644                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 645 \begin{code}
 646 typeKind :: Type -> Kind
 647 typeKind (TyConApp tycon tys) = ASSERT( not (isCoercionTyCon tycon) )
 648                                    -- We should be looking for the coercion kind,
 649                                    -- not the type kind
 650                                 foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
 651 typeKind (NoteTy _ ty)        = typeKind ty
 652 typeKind (PredTy pred)        = predKind pred
 653 typeKind (AppTy fun arg)      = kindFunResult (typeKind fun)
 654 typeKind (ForAllTy tv ty)     = typeKind ty
 655 typeKind (TyVarTy tyvar)      = tyVarKind tyvar
 656 typeKind (FunTy arg res)
 657     -- Hack alert.  The kind of (Int -> Int#) is liftedTypeKind (*),
 658     --              not unliftedTypKind (#)
 659     -- The only things that can be after a function arrow are
 660     --   (a) types (of kind openTypeKind or its sub-kinds)
 661     --   (b) kinds (of super-kind TY) (e.g. * -> (* -> *))
 662     | isTySuperKind k         = k
 663     | otherwise               = ASSERT( isSubOpenTypeKind k) liftedTypeKind
 664     where
 665       k = typeKind res
 666
 667 predKind :: PredType -> Kind
 668 predKind (EqPred {}) = coSuperKind      -- A coercion kind!
 669 predKind (ClassP {}) = liftedTypeKind   -- Class and implicitPredicates are
 670 predKind (IParam {}) = liftedTypeKind   -- always represented by lifted types
 671 \end{code}
 672
 673
 674 ---------------------------------------------------------------------
 675                 Free variables of a type
 676                 ~~~~~~~~~~~~~~~~~~~~~~~~
 677 \begin{code}
 678 tyVarsOfType :: Type -> TyVarSet
 679 -- NB: for type synonyms tyVarsOfType does *not* expand the synonym
 680 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
 681 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
 682 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
 683 tyVarsOfType (PredTy sty)               = tyVarsOfPred sty
 684 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 685 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
 686 tyVarsOfType (ForAllTy tyvar ty)        = delVarSet (tyVarsOfType ty) tyvar
 687
 688 tyVarsOfTypes :: [Type] -> TyVarSet
 689 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 690
 691 tyVarsOfPred :: PredType -> TyVarSet
 692 tyVarsOfPred (IParam _ ty)    = tyVarsOfType ty
 693 tyVarsOfPred (ClassP _ tys)   = tyVarsOfTypes tys
 694 tyVarsOfPred (EqPred ty1 ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 695
 696 tyVarsOfTheta :: ThetaType -> TyVarSet
 697 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
 698
 699 -- Add a Note with the free tyvars to the top of the type
 700 addFreeTyVars :: Type -> Type
 701 addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
 702 addFreeTyVars ty                             = NoteTy (FTVNote (tyVarsOfType ty)) ty
 703 \end{code}
 704
 705
 706 %************************************************************************
 707 %*                                                                      *
 708 \subsection{TidyType}
 709 %*                                                                      *
 710 %************************************************************************
 711
 712 tidyTy tidies up a type for printing in an error message, or in
 713 an interface file.
 714
 715 It doesn't change the uniques at all, just the print names.
 716
 717 \begin{code}
 718 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 719 tidyTyVarBndr (tidy_env, subst) tyvar
 720   = case tidyOccName tidy_env (getOccName name) of
 721       (tidy', occ') ->  ((tidy', subst'), tyvar')
 722                     where
 723                         subst' = extendVarEnv subst tyvar tyvar'
 724                         tyvar' = setTyVarName tyvar name'
 725                         name'  = tidyNameOcc name occ'
 726   where
 727     name = tyVarName tyvar
 728
 729 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
 730 -- Add the free tyvars to the env in tidy form,
 731 -- so that we can tidy the type they are free in
 732 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
 733
 734 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
 735 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
 736
 737 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 738 -- Treat a new tyvar as a binder, and give it a fresh tidy name
 739 tidyOpenTyVar env@(tidy_env, subst) tyvar
 740   = case lookupVarEnv subst tyvar of
 741         Just tyvar' -> (env, tyvar')            -- Already substituted
 742         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
 743
 744 tidyType :: TidyEnv -> Type -> Type
 745 tidyType env@(tidy_env, subst) ty
 746   = go ty
 747   where
 748     go (TyVarTy tv)         = case lookupVarEnv subst tv of
 749                                 Nothing  -> TyVarTy tv
 750                                 Just tv' -> TyVarTy tv'
 751     go (TyConApp tycon tys) = let args = map go tys
 752                               in args `seqList` TyConApp tycon args
 753     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
 754     go (PredTy sty)         = PredTy (tidyPred env sty)
 755     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
 756     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
 757     go (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
 758                               where
 759                                 (envp, tvp) = tidyTyVarBndr env tv
 760
 761     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
 762
 763 tidyTypes env tys = map (tidyType env) tys
 764
 765 tidyPred :: TidyEnv -> PredType -> PredType
 766 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
 767 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
 768 tidyPred env (EqPred ty1 ty2)  = EqPred (tidyType env ty1) (tidyType env ty2)
 769 \end{code}
 770
 771
 772 @tidyOpenType@ grabs the free type variables, tidies them
 773 and then uses @tidyType@ to work over the type itself
 774
 775 \begin{code}
 776 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
 777 tidyOpenType env ty
 778   = (env', tidyType env' ty)
 779   where
 780     env' = tidyFreeTyVars env (tyVarsOfType ty)
 781
 782 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
 783 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
 784
 785 tidyTopType :: Type -> Type
 786 tidyTopType ty = tidyType emptyTidyEnv ty
 787 \end{code}
 788
 789 \begin{code}
 790
 791 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
 792 tidyKind env k = tidyOpenType env k
 793
 794 \end{code}
 795
 796
 797 %************************************************************************
 798 %*                                                                      *
 799 \subsection{Liftedness}
 800 %*                                                                      *
 801 %************************************************************************
 802
 803 \begin{code}
 804 isUnLiftedType :: Type -> Bool
 805         -- isUnLiftedType returns True for forall'd unlifted types:
 806         --      x :: forall a. Int#
 807         -- I found bindings like these were getting floated to the top level.
 808         -- They are pretty bogus types, mind you.  It would be better never to
 809         -- construct them
 810
 811 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
 812 isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
 813 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
 814 isUnLiftedType other             = False
 815
 816 isUnboxedTupleType :: Type -> Bool
 817 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
 818                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
 819                            other              -> False
 820
 821 -- Should only be applied to *types*; hence the assert
 822 isAlgType :: Type -> Bool
 823 isAlgType ty = case splitTyConApp_maybe ty of
 824                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 825                                               isAlgTyCon tc
 826                         other              -> False
 827 \end{code}
 828
 829 @isStrictType@ computes whether an argument (or let RHS) should
 830 be computed strictly or lazily, based only on its type.
 831 Works just like isUnLiftedType, except that it has a special case
 832 for dictionaries.  Since it takes account of ClassP, you might think
 833 this function should be in TcType, but isStrictType is used by DataCon,
 834 which is below TcType in the hierarchy, so it's convenient to put it here.
 835
 836 \begin{code}
 837 isStrictType (PredTy pred)     = isStrictPred pred
 838 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
 839 isStrictType (ForAllTy tv ty)  = isStrictType ty
 840 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
 841 isStrictType other             = False
 842
 843 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
 844 isStrictPred other           = False
 845         -- We may be strict in dictionary types, but only if it
 846         -- has more than one component.
 847         -- [Being strict in a single-component dictionary risks
 848         --  poking the dictionary component, which is wrong.]
 849 \end{code}
 850
 851 \begin{code}
 852 isPrimitiveType :: Type -> Bool
 853 -- Returns types that are opaque to Haskell.
 854 -- Most of these are unlifted, but now that we interact with .NET, we
 855 -- may have primtive (foreign-imported) types that are lifted
 856 isPrimitiveType ty = case splitTyConApp_maybe ty of
 857                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 858                                               isPrimTyCon tc
 859                         other              -> False
 860 \end{code}
 861
 862
 863 %************************************************************************
 864 %*                                                                      *
 865 \subsection{Sequencing on types
 866 %*                                                                      *
 867 %************************************************************************
 868
 869 \begin{code}
 870 seqType :: Type -> ()
 871 seqType (TyVarTy tv)      = tv `seq` ()
 872 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
 873 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
 874 seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
 875 seqType (PredTy p)        = seqPred p
 876 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 877 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
 878
 879 seqTypes :: [Type] -> ()
 880 seqTypes []       = ()
 881 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 882
 883 seqNote :: TyNote -> ()
 884 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 885
 886 seqPred :: PredType -> ()
 887 seqPred (ClassP c tys)   = c `seq` seqTypes tys
 888 seqPred (IParam n ty)    = n `seq` seqType ty
 889 seqPred (EqPred ty1 ty2) = seqType ty1 `seq` seqType ty2
 890 \end{code}
 891
 892
 893 %************************************************************************
 894 %*                                                                      *
 895                 Equality for Core types
 896         (We don't use instances so that we know where it happens)
 897 %*                                                                      *
 898 %************************************************************************
 899
 900 Note that eqType works right even for partial applications of newtypes.
 901 See Note [Newtype eta] in TyCon.lhs
 902
 903 \begin{code}
 904 coreEqType :: Type -> Type -> Bool
 905 coreEqType t1 t2
 906   = eq rn_env t1 t2
 907   where
 908     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
 909
 910     eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
 911     eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
 912     eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
 913     eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
 914     eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 915         | tc1 == tc2, all2 (eq env) tys1 tys2 = True
 916                         -- The lengths should be equal because
 917                         -- the two types have the same kind
 918         -- NB: if the type constructors differ that does not
 919         --     necessarily mean that the types aren't equal
 920         --     (synonyms, newtypes)
 921         -- Even if the type constructors are the same, but the arguments
 922         -- differ, the two types could be the same (e.g. if the arg is just
 923         -- ignored in the RHS).  In both these cases we fall through to an
 924         -- attempt to expand one side or the other.
 925
 926         -- Now deal with newtypes, synonyms, pred-tys
 927     eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
 928                  | Just t2' <- coreView t2 = eq env t1 t2'
 929
 930         -- Fall through case; not equal!
 931     eq env t1 t2 = False
 932 \end{code}
 933
 934
 935 %************************************************************************
 936 %*                                                                      *
 937                 Comparision for source types
 938         (We don't use instances so that we know where it happens)
 939 %*                                                                      *
 940 %************************************************************************
 941
 942 Note that
 943         tcEqType, tcCmpType
 944 do *not* look through newtypes, PredTypes
 945
 946 \begin{code}
 947 tcEqType :: Type -> Type -> Bool
 948 tcEqType t1 t2 = isEqual $ cmpType t1 t2
 949
 950 tcEqTypes :: [Type] -> [Type] -> Bool
 951 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
 952
 953 tcCmpType :: Type -> Type -> Ordering
 954 tcCmpType t1 t2 = cmpType t1 t2
 955
 956 tcCmpTypes :: [Type] -> [Type] -> Ordering
 957 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
 958
 959 tcEqPred :: PredType -> PredType -> Bool
 960 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
 961
 962 tcCmpPred :: PredType -> PredType -> Ordering
 963 tcCmpPred p1 p2 = cmpPred p1 p2
 964
 965 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
 966 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
 967 \end{code}
 968
 969 Now here comes the real worker
 970
 971 \begin{code}
 972 cmpType :: Type -> Type -> Ordering
 973 cmpType t1 t2 = cmpTypeX rn_env t1 t2
 974   where
 975     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
 976
 977 cmpTypes :: [Type] -> [Type] -> Ordering
 978 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
 979   where
 980     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
 981
 982 cmpPred :: PredType -> PredType -> Ordering
 983 cmpPred p1 p2 = cmpPredX rn_env p1 p2
 984   where
 985     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
 986
 987 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
 988 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
 989                    | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
 990
 991 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
 992 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
 993 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 994 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 995 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
 996 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
 997 cmpTypeX env t1                 (NoteTy _ t2)        = cmpTypeX env t1 t2
 998
 999     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
1000 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
1001
1002 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
1003 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
1004
1005 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
1006 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
1007 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
1008
1009 cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
1010 cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
1011 cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
1012 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
1013
1014 cmpTypeX env (PredTy _)   t2            = GT
1015
1016 cmpTypeX env _ _ = LT
1017
1018 -------------
1019 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1020 cmpTypesX env []        []        = EQ
1021 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1022 cmpTypesX env []        tys       = LT
1023 cmpTypesX env ty        []        = GT
1024
1025 -------------
1026 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1027 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1028         -- Compare types as well as names for implicit parameters
1029         -- This comparison is used exclusively (I think) for the
1030         -- finite map built in TcSimplify
1031 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
1032 cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
1033 cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
1034 cmpPredX env (EqPred ty1 ty2) (EqPred ty1' ty2') = (cmpTypeX env ty1 ty1') `thenCmp` (cmpTypeX env ty2 ty2')
1035 \end{code}
1036
1037 PredTypes are used as a FM key in TcSimplify,
1038 so we take the easy path and make them an instance of Ord
1039
1040 \begin{code}
1041 instance Eq  PredType where { (==)    = tcEqPred }
1042 instance Ord PredType where { compare = tcCmpPred }
1043 \end{code}
1044
1045
1046 %************************************************************************
1047 %*                                                                      *
1048                 Type substitutions
1049 %*                                                                      *
1050 %************************************************************************
1051
1052 \begin{code}
1053 data TvSubst
1054   = TvSubst InScopeSet  -- The in-scope type variables
1055             TvSubstEnv  -- The substitution itself
1056                         -- See Note [Apply Once]
1057
1058 {- ----------------------------------------------------------
1059                 Note [Apply Once]
1060
1061 We use TvSubsts to instantiate things, and we might instantiate
1062         forall a b. ty
1063 \with the types
1064         [a, b], or [b, a].
1065 So the substition might go [a->b, b->a].  A similar situation arises in Core
1066 when we find a beta redex like
1067         (/\ a /\ b -> e) b a
1068 Then we also end up with a substition that permutes type variables. Other
1069 variations happen to; for example [a -> (a, b)].
1070
1071         ***************************************************
1072         *** So a TvSubst must be applied precisely once ***
1073         ***************************************************
1074
1075 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1076 we use during unifications, it must not be repeatedly applied.
1077 -------------------------------------------------------------- -}
1078
1079
1080 type TvSubstEnv = TyVarEnv Type
1081         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1082         -- invariant discussed in Note [Apply Once]), and also independently
1083         -- in the middle of matching, and unification (see Types.Unify)
1084         -- So you have to look at the context to know if it's idempotent or
1085         -- apply-once or whatever
1086 emptyTvSubstEnv :: TvSubstEnv
1087 emptyTvSubstEnv = emptyVarEnv
1088
1089 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1090 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1091 -- It assumes that both are idempotent
1092 -- Typically, env1 is the refinement to a base substitution env2
1093 composeTvSubst in_scope env1 env2
1094   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1095         -- First apply env1 to the range of env2
1096         -- Then combine the two, making sure that env1 loses if
1097         -- both bind the same variable; that's why env1 is the
1098         --  *left* argument to plusVarEnv, because the right arg wins
1099   where
1100     subst1 = TvSubst in_scope env1
1101
1102 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1103
1104 isEmptyTvSubst :: TvSubst -> Bool
1105 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1106
1107 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1108 mkTvSubst = TvSubst
1109
1110 getTvSubstEnv :: TvSubst -> TvSubstEnv
1111 getTvSubstEnv (TvSubst _ env) = env
1112
1113 getTvInScope :: TvSubst -> InScopeSet
1114 getTvInScope (TvSubst in_scope _) = in_scope
1115
1116 isInScope :: Var -> TvSubst -> Bool
1117 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1118
1119 notElemTvSubst :: TyVar -> TvSubst -> Bool
1120 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1121
1122 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1123 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1124
1125 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1126 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1127
1128 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1129 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1130
1131 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1132 extendTvSubstList (TvSubst in_scope env) tvs tys
1133   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1134
1135 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1136 -- the types given; but it's just a thunk so with a bit of luck
1137 -- it'll never be evaluated
1138
1139 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1140 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1141
1142 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1143 zipOpenTvSubst tyvars tys
1144 #ifdef DEBUG
1145   | length tyvars /= length tys
1146   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1147   | otherwise
1148 #endif
1149   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1150
1151 -- mkTopTvSubst is called when doing top-level substitutions.
1152 -- Here we expect that the free vars of the range of the
1153 -- substitution will be empty.
1154 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1155 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1156
1157 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1158 zipTopTvSubst tyvars tys
1159 #ifdef DEBUG
1160   | length tyvars /= length tys
1161   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1162   | otherwise
1163 #endif
1164   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1165
1166 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1167 zipTyEnv tyvars tys
1168 #ifdef DEBUG
1169   | length tyvars /= length tys
1170   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1171   | otherwise
1172 #endif
1173   = zip_ty_env tyvars tys emptyVarEnv
1174
1175 -- Later substitutions in the list over-ride earlier ones,
1176 -- but there should be no loops
1177 zip_ty_env []       []       env = env
1178 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1179         -- There used to be a special case for when
1180         --      ty == TyVarTy tv
1181         -- (a not-uncommon case) in which case the substitution was dropped.
1182         -- But the type-tidier changes the print-name of a type variable without
1183         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1184         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1185         -- And it happened that t was the type variable of the class.  Post-tiding,
1186         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1187         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1188         -- and so generated a rep type mentioning t not t2.
1189         --
1190         -- Simplest fix is to nuke the "optimisation"
1191 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1192 -- zip_ty_env _ _ env = env
1193
1194 instance Outputable TvSubst where
1195   ppr (TvSubst ins env)
1196     = brackets $ sep[ ptext SLIT("TvSubst"),
1197                       nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1198                       nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1199 \end{code}
1200
1201 %************************************************************************
1202 %*                                                                      *
1203                 Performing type substitutions
1204 %*                                                                      *
1205 %************************************************************************
1206
1207 \begin{code}
1208 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1209 substTyWith tvs tys = ASSERT( length tvs == length tys )
1210                       substTy (zipOpenTvSubst tvs tys)
1211
1212 substTy :: TvSubst -> Type  -> Type
1213 substTy subst ty | isEmptyTvSubst subst = ty
1214                  | otherwise            = subst_ty subst ty
1215
1216 substTys :: TvSubst -> [Type] -> [Type]
1217 substTys subst tys | isEmptyTvSubst subst = tys
1218                    | otherwise            = map (subst_ty subst) tys
1219
1220 substTheta :: TvSubst -> ThetaType -> ThetaType
1221 substTheta subst theta
1222   | isEmptyTvSubst subst = theta
1223   | otherwise            = map (substPred subst) theta
1224
1225 substPred :: TvSubst -> PredType -> PredType
1226 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1227 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1228 substPred subst (EqPred ty1 ty2)  = EqPred (subst_ty subst ty1) (subst_ty subst ty2)
1229
1230 deShadowTy :: TyVarSet -> Type -> Type  -- Remove any nested binders mentioning tvs
1231 deShadowTy tvs ty
1232   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1233   where
1234     in_scope = mkInScopeSet tvs
1235
1236 subst_ty :: TvSubst -> Type -> Type
1237 -- subst_ty is the main workhorse for type substitution
1238 --
1239 -- Note that the in_scope set is poked only if we hit a forall
1240 -- so it may often never be fully computed
1241 subst_ty subst ty
1242    = go ty
1243   where
1244     go (TyVarTy tv)                = substTyVar subst tv
1245     go (TyConApp tc tys)           = let args = map go tys
1246                                      in  args `seqList` TyConApp tc args
1247
1248     go (PredTy p)                  = PredTy $! (substPred subst p)
1249
1250     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
1251
1252     go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
1253     go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
1254                 -- The mkAppTy smart constructor is important
1255                 -- we might be replacing (a Int), represented with App
1256                 -- by [Int], represented with TyConApp
1257     go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
1258                                         (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1259
1260 substTyVar :: TvSubst -> TyVar  -> Type
1261 substTyVar subst@(TvSubst in_scope env) tv
1262   = case lookupTyVar subst tv of {
1263         Nothing  -> TyVarTy tv;
1264         Just ty -> ty   -- See Note [Apply Once]
1265     }
1266
1267 lookupTyVar :: TvSubst -> TyVar  -> Maybe Type
1268 lookupTyVar (TvSubst in_scope env) tv = lookupVarEnv env tv
1269
1270 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1271 substTyVarBndr subst@(TvSubst in_scope env) old_var
1272   = (TvSubst (in_scope `extendInScopeSet` new_var) new_env, new_var)
1273   where
1274
1275     new_env | no_change = delVarEnv env old_var
1276             | otherwise = extendVarEnv env old_var (TyVarTy new_var)
1277
1278     no_change = new_var == old_var && not is_co_var
1279         -- no_change means that the new_var is identical in
1280         -- all respects to the old_var (same unique, same kind)
1281         --
1282         -- In that case we don't need to extend the substitution
1283         -- to map old to new.  But instead we must zap any
1284         -- current substitution for the variable. For example:
1285         --      (\x.e) with id_subst = [x |-> e']
1286         -- Here we must simply zap the substitution for x
1287
1288     new_var = uniqAway in_scope subst_old_var
1289         -- The uniqAway part makes sure the new variable is not already in scope
1290
1291     subst_old_var -- subst_old_var is old_var with the substitution applied to its kind
1292                  -- It's only worth doing the substitution for coercions,
1293                  -- becuase only they can have free type variables
1294         | is_co_var = setTyVarKind old_var (substTy subst kind)
1295         | otherwise = old_var
1296     kind = tyVarKind old_var
1297     is_co_var = isCoercionKind kind
1298 \end{code}
1299
1300 ----------------------------------------------------
1301 -- Kind Stuff
1302
1303 Kinds
1304 ~~~~~
1305 There's a little subtyping at the kind level:
1306
1307                  ?
1308                 / \
1309                /   \
1310               ??   (#)
1311              /  \
1312             *   #
1313
1314 where   *    [LiftedTypeKind]   means boxed type
1315         #    [UnliftedTypeKind] means unboxed type
1316         (#)  [UbxTupleKind]     means unboxed tuple
1317         ??   [ArgTypeKind]      is the lub of *,#
1318         ?    [OpenTypeKind]     means any type at all
1319
1320 In particular:
1321
1322         error :: forall a:?. String -> a
1323         (->)  :: ?? -> ? -> *
1324         (\(x::t) -> ...)        Here t::?? (i.e. not unboxed tuple)
1325
1326 \begin{code}
1327 type KindVar = TyVar  -- invariant: KindVar will always be a
1328                       -- TcTyVar with details MetaTv TauTv ...
1329 -- kind var constructors and functions are in TcType
1330
1331 type SimpleKind = Kind
1332 \end{code}
1333
1334 Kind inference
1335 ~~~~~~~~~~~~~~
1336 During kind inference, a kind variable unifies only with
1337 a "simple kind", sk
1338         sk ::= * | sk1 -> sk2
1339 For example
1340         data T a = MkT a (T Int#)
1341 fails.  We give T the kind (k -> *), and the kind variable k won't unify
1342 with # (the kind of Int#).
1343
1344 Type inference
1345 ~~~~~~~~~~~~~~
1346 When creating a fresh internal type variable, we give it a kind to express
1347 constraints on it.  E.g. in (\x->e) we make up a fresh type variable for x,
1348 with kind ??.
1349
1350 During unification we only bind an internal type variable to a type
1351 whose kind is lower in the sub-kind hierarchy than the kind of the tyvar.
1352
1353 When unifying two internal type variables, we collect their kind constraints by
1354 finding the GLB of the two.  Since the partial order is a tree, they only
1355 have a glb if one is a sub-kind of the other.  In that case, we bind the
1356 less-informative one to the more informative one.  Neat, eh?
1357
1358
1359 \begin{code}
1360
1361 \end{code}
1362
1363 %************************************************************************
1364 %*                                                                      *
1365         Functions over Kinds
1366 %*                                                                      *
1367 %************************************************************************
1368
1369 \begin{code}
1370 kindFunResult :: Kind -> Kind
1371 kindFunResult k = funResultTy k
1372
1373 splitKindFunTys :: Kind -> ([Kind],Kind)
1374 splitKindFunTys k = splitFunTys k
1375
1376 splitKindFunTysN :: Int -> Kind -> ([Kind],Kind)
1377 splitKindFunTysN k = splitFunTysN k
1378
1379 isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind :: Kind -> Bool
1380
1381 isOpenTypeKindCon tc    = tyConUnique tc == openTypeKindTyConKey
1382
1383 isOpenTypeKind (TyConApp tc _) = isOpenTypeKindCon tc
1384 isOpenTypeKind other           = False
1385
1386 isUbxTupleKindCon tc = tyConUnique tc == ubxTupleKindTyConKey
1387
1388 isUbxTupleKind (TyConApp tc _) = isUbxTupleKindCon tc
1389 isUbxTupleKind other           = False
1390
1391 isArgTypeKindCon tc = tyConUnique tc == argTypeKindTyConKey
1392
1393 isArgTypeKind (TyConApp tc _) = isArgTypeKindCon tc
1394 isArgTypeKind other = False
1395
1396 isUnliftedTypeKindCon tc = tyConUnique tc == unliftedTypeKindTyConKey
1397
1398 isUnliftedTypeKind (TyConApp tc _) = isUnliftedTypeKindCon tc
1399 isUnliftedTypeKind other           = False
1400
1401 isSubOpenTypeKind :: Kind -> Bool
1402 -- True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
1403 isSubOpenTypeKind (FunTy k1 k2)    = ASSERT2 ( isKind k1, text "isSubOpenTypeKind" <+> ppr k1 <+> text "::" <+> ppr (typeKind k1) )
1404                                      ASSERT2 ( isKind k2, text "isSubOpenTypeKind" <+> ppr k2 <+> text "::" <+> ppr (typeKind k2) )
1405                                      False
1406 isSubOpenTypeKind (TyConApp kc []) = ASSERT( isKind (TyConApp kc []) ) True
1407 isSubOpenTypeKind other            = ASSERT( isKind other ) False
1408          -- This is a conservative answer
1409          -- It matters in the call to isSubKind in
1410          -- checkExpectedKind.
1411
1412 isSubArgTypeKindCon kc
1413   | isUnliftedTypeKindCon kc = True
1414   | isLiftedTypeKindCon kc   = True
1415   | isArgTypeKindCon kc      = True
1416   | otherwise                = False
1417
1418 isSubArgTypeKind :: Kind -> Bool
1419 -- True of any sub-kind of ArgTypeKind
1420 isSubArgTypeKind (TyConApp kc []) = isSubArgTypeKindCon kc
1421 isSubArgTypeKind other            = False
1422
1423 isSuperKind :: Type -> Bool
1424 isSuperKind (TyConApp (skc) []) = isSuperKindTyCon skc
1425 isSuperKind other = False
1426
1427 isKind :: Kind -> Bool
1428 isKind k = isSuperKind (typeKind k)
1429
1430
1431
1432 isSubKind :: Kind -> Kind -> Bool
1433 -- (k1 `isSubKind` k2) checks that k1 <: k2
1434 isSubKind (TyConApp kc1 []) (TyConApp kc2 []) = kc1 `isSubKindCon` kc1
1435 isSubKind (FunTy a1 r1) (FunTy a2 r2)         = (a2 `isSubKind` a1) && (r1 `isSubKind` r2)
1436 isSubKind (PredTy (EqPred ty1 ty2)) (PredTy (EqPred ty1' ty2'))
1437   = ty1 `tcEqType` ty1' && ty2 `tcEqType` ty2'
1438 isSubKind k1            k2                    = False
1439
1440 eqKind :: Kind -> Kind -> Bool
1441 eqKind = tcEqType
1442
1443 isSubKindCon :: TyCon -> TyCon -> Bool
1444 -- (kc1 `isSubKindCon` kc2) checks that kc1 <: kc2
1445 isSubKindCon kc1 kc2
1446   | isLiftedTypeKindCon kc1   && isLiftedTypeKindCon kc2   = True
1447   | isUnliftedTypeKindCon kc1 && isUnliftedTypeKindCon kc2 = True
1448   | isUbxTupleKindCon kc1     && isUbxTupleKindCon kc2     = True
1449   | isOpenTypeKindCon kc2                                  = True
1450                            -- we already know kc1 is not a fun, its a TyCon
1451   | isArgTypeKindCon kc2      && isSubArgTypeKindCon kc1   = True
1452   | otherwise                                              = False
1453
1454 defaultKind :: Kind -> Kind
1455 -- Used when generalising: default kind '?' and '??' to '*'
1456 --
1457 -- When we generalise, we make generic type variables whose kind is
1458 -- simple (* or *->* etc).  So generic type variables (other than
1459 -- built-in constants like 'error') always have simple kinds.  This is important;
1460 -- consider
1461 --      f x = True
1462 -- We want f to get type
1463 --      f :: forall (a::*). a -> Bool
1464 -- Not
1465 --      f :: forall (a::??). a -> Bool
1466 -- because that would allow a call like (f 3#) as well as (f True),
1467 --and the calling conventions differ.  This defaulting is done in TcMType.zonkTcTyVarBndr.
1468 defaultKind k
1469   | isSubOpenTypeKind k = liftedTypeKind
1470   | isSubArgTypeKind k  = liftedTypeKind
1471   | otherwise        = k
1472
1473 isCoercionKind :: Kind -> Bool
1474 -- All coercions are of form (ty1 :=: ty2)
1475 -- This function is here rather than in Coercion,
1476 -- because it's used by substTy
1477 isCoercionKind k | Just k' <- kindView k = isCoercionKind k'
1478 isCoercionKind (PredTy (EqPred {}))      = True
1479 isCoercionKind other                     = False
1480
1481 isEqPred :: PredType -> Bool
1482 isEqPred (EqPred _ _) = True
1483 isEqPred other        = False
1484 \end{code}