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