ghc/compiler/types/Type.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1998
   3 %
   4 \section[Type]{Type - public interface}
   5
   6 \begin{code}
   7 module Type (
   8         -- re-exports from TypeRep
   9         TyThing(..), Type, PredType(..), ThetaType,
  10         funTyCon,
  11
  12         -- Re-exports from Kind
  13         module Kind,
  14
  15         -- Re-exports from TyCon
  16         PrimRep(..),
  17
  18         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, isTyVarTy,
  19
  20         mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe,
  21
  22         mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
  23         splitFunTys, splitFunTysN,
  24         funResultTy, funArgTy, zipFunTys, isFunTy,
  25
  26         mkGenTyConApp, mkTyConApp, mkTyConTy,
  27         tyConAppTyCon, tyConAppArgs,
  28         splitTyConApp_maybe, splitTyConApp,
  29
  30         mkSynTy,
  31
  32         repType, typePrimRep, coreView, deepCoreView,
  33
  34         mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys,
  35         applyTy, applyTys, isForAllTy, dropForAlls,
  36
  37         -- Source types
  38         predTypeRep, mkPredTy, mkPredTys,
  39
  40         -- Newtypes
  41         splitRecNewType_maybe,
  42
  43         -- Lifting and boxity
  44         isUnLiftedType, isUnboxedTupleType, isAlgType, isPrimitiveType,
  45         isStrictType, isStrictPred,
  46
  47         -- Free variables
  48         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
  49         typeKind, addFreeTyVars,
  50
  51         -- Tidying up for printing
  52         tidyType,      tidyTypes,
  53         tidyOpenType,  tidyOpenTypes,
  54         tidyTyVarBndr, tidyFreeTyVars,
  55         tidyOpenTyVar, tidyOpenTyVars,
  56         tidyTopType,   tidyPred,
  57         tidyKind,
  58
  59         -- Comparison
  60         coreEqType, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
  61         tcEqPred, tcCmpPred, tcEqTypeX,
  62
  63         -- Seq
  64         seqType, seqTypes,
  65
  66         -- Type substitutions
  67         TvSubstEnv, emptyTvSubstEnv,    -- Representation widely visible
  68         TvSubst(..), emptyTvSubst,      -- Representation visible to a few friends
  69         mkTvSubst, mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
  70         getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
  71         extendTvSubst, extendTvSubstList, isInScope, composeTvSubst,
  72
  73         -- Performing substitution on types
  74         substTy, substTys, substTyWith, substTheta,
  75         substPred, substTyVar, substTyVarBndr, deShadowTy,
  76
  77         -- Pretty-printing
  78         pprType, pprParendType, pprTyThingCategory,
  79         pprPred, pprTheta, pprThetaArrow, pprClassPred
  80     ) where
  81
  82 #include "HsVersions.h"
  83
  84 -- We import the representation and primitive functions from TypeRep.
  85 -- Many things are reexported, but not the representation!
  86
  87 import TypeRep
  88
  89 -- friends:
  90 import Kind
  91 import Var      ( Var, TyVar, tyVarKind, tyVarName, setTyVarName, mkTyVar )
  92 import VarEnv
  93 import VarSet
  94
  95 import Name     ( NamedThing(..), mkInternalName, tidyOccName )
  96 import Class    ( Class, classTyCon )
  97 import TyCon    ( TyCon, isRecursiveTyCon, isPrimTyCon,
  98                   isUnboxedTupleTyCon, isUnLiftedTyCon,
  99                   isFunTyCon, isNewTyCon, newTyConRep, newTyConRhs,
 100                   isAlgTyCon, isSynTyCon, tyConArity, newTyConRhs_maybe,
 101                   tyConKind, getSynTyConDefn, PrimRep(..), tyConPrimRep,
 102                 )
 103
 104 -- others
 105 import StaticFlags      ( opt_DictsStrict )
 106 import SrcLoc           ( noSrcLoc )
 107 import Unique           ( Uniquable(..) )
 108 import Util             ( mapAccumL, seqList, lengthIs, snocView, thenCmp, isEqual )
 109 import Outputable
 110 import UniqSet          ( sizeUniqSet )         -- Should come via VarSet
 111 import Maybe            ( isJust )
 112 \end{code}
 113
 114
 115 %************************************************************************
 116 %*                                                                      *
 117                 Type representation
 118 %*                                                                      *
 119 %************************************************************************
 120
 121 In Core, we "look through" non-recursive newtypes and PredTypes.
 122
 123 \begin{code}
 124 {-# INLINE coreView #-}
 125 coreView :: Type -> Maybe Type
 126 -- Srips off the *top layer only* of a type to give
 127 -- its underlying representation type.
 128 -- Returns Nothing if there is nothing to look through.
 129 --
 130 -- By being non-recursive and inlined, this case analysis gets efficiently
 131 -- joined onto the case analysis that the caller is already doing
 132 coreView (NoteTy _ ty)     = Just ty
 133 coreView (PredTy p)        = Just (predTypeRep p)
 134 coreView (TyConApp tc tys) = expandNewTcApp tc tys
 135 coreView ty                = Nothing
 136
 137 deepCoreView :: Type -> Type
 138 -- Apply coreView recursively
 139 deepCoreView ty
 140   | Just ty' <- coreView ty    = deepCoreView ty'
 141 deepCoreView (TyVarTy tv)      = TyVarTy tv
 142 deepCoreView (TyConApp tc tys) = TyConApp tc (map deepCoreView tys)
 143 deepCoreView (AppTy t1 t2)     = AppTy (deepCoreView t1) (deepCoreView t2)
 144 deepCoreView (FunTy t1 t2)     = FunTy (deepCoreView t1) (deepCoreView t2)
 145 deepCoreView (ForAllTy tv ty)  = ForAllTy tv (deepCoreView ty)
 146         -- No NoteTy, no PredTy
 147
 148 expandNewTcApp :: TyCon -> [Type] -> Maybe Type
 149 -- A local helper function (not exported)
 150 -- Expands *the outermoset level of* a newtype application to
 151 --      *either* a vanilla TyConApp (recursive newtype, or non-saturated)
 152 --      *or*     the newtype representation (otherwise), meaning the
 153 --                      type written in the RHS of the newtype decl,
 154 --                      which may itself be a newtype
 155 --
 156 -- Example: newtype R = MkR S
 157 --          newtype S = MkS T
 158 --          newtype T = MkT (T -> T)
 159 --   expandNewTcApp on R gives Just S
 160 --                  on S gives Just T
 161 --                  on T gives Nothing   (no expansion)
 162
 163 expandNewTcApp tc tys = case newTyConRhs_maybe tc tys of
 164                           Nothing          -> Nothing
 165                           Just (tenv, rhs) -> Just (substTy (mkTopTvSubst tenv) rhs)
 166 \end{code}
 167
 168
 169 %************************************************************************
 170 %*                                                                      *
 171 \subsection{Constructor-specific functions}
 172 %*                                                                      *
 173 %************************************************************************
 174
 175
 176 ---------------------------------------------------------------------
 177                                 TyVarTy
 178                                 ~~~~~~~
 179 \begin{code}
 180 mkTyVarTy  :: TyVar   -> Type
 181 mkTyVarTy  = TyVarTy
 182
 183 mkTyVarTys :: [TyVar] -> [Type]
 184 mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
 185
 186 getTyVar :: String -> Type -> TyVar
 187 getTyVar msg ty = case getTyVar_maybe ty of
 188                     Just tv -> tv
 189                     Nothing -> panic ("getTyVar: " ++ msg)
 190
 191 isTyVarTy :: Type -> Bool
 192 isTyVarTy ty = isJust (getTyVar_maybe ty)
 193
 194 getTyVar_maybe :: Type -> Maybe TyVar
 195 getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
 196 getTyVar_maybe (TyVarTy tv)                 = Just tv
 197 getTyVar_maybe other                        = Nothing
 198 \end{code}
 199
 200
 201 ---------------------------------------------------------------------
 202                                 AppTy
 203                                 ~~~~~
 204 We need to be pretty careful with AppTy to make sure we obey the
 205 invariant that a TyConApp is always visibly so.  mkAppTy maintains the
 206 invariant: use it.
 207
 208 \begin{code}
 209 mkAppTy orig_ty1 orig_ty2
 210   = mk_app orig_ty1
 211   where
 212     mk_app (NoteTy _ ty1)    = mk_app ty1
 213     mk_app (TyConApp tc tys) = mkGenTyConApp tc (tys ++ [orig_ty2])
 214     mk_app ty1               = AppTy orig_ty1 orig_ty2
 215         -- We call mkGenTyConApp because the TyConApp could be an
 216         -- under-saturated type synonym.  GHC allows that; e.g.
 217         --      type Foo k = k a -> k a
 218         --      type Id x = x
 219         --      foo :: Foo Id -> Foo Id
 220         --
 221         -- Here Id is partially applied in the type sig for Foo,
 222         -- but once the type synonyms are expanded all is well
 223
 224 mkAppTys :: Type -> [Type] -> Type
 225 mkAppTys orig_ty1 []        = orig_ty1
 226         -- This check for an empty list of type arguments
 227         -- avoids the needless loss of a type synonym constructor.
 228         -- For example: mkAppTys Rational []
 229         --   returns to (Ratio Integer), which has needlessly lost
 230         --   the Rational part.
 231 mkAppTys orig_ty1 orig_tys2
 232   = mk_app orig_ty1
 233   where
 234     mk_app (NoteTy _ ty1)    = mk_app ty1
 235     mk_app (TyConApp tc tys) = mkGenTyConApp tc (tys ++ orig_tys2)
 236                                 -- mkGenTyConApp: see notes with mkAppTy
 237     mk_app ty1               = foldl AppTy orig_ty1 orig_tys2
 238
 239 splitAppTy_maybe :: Type -> Maybe (Type, Type)
 240 splitAppTy_maybe ty | Just ty' <- coreView ty = splitAppTy_maybe ty'
 241 splitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
 242 splitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
 243 splitAppTy_maybe (TyConApp tc tys) = case snocView tys of
 244                                         Nothing         -> Nothing
 245                                         Just (tys',ty') -> Just (TyConApp tc tys', ty')
 246 splitAppTy_maybe other             = Nothing
 247
 248 splitAppTy :: Type -> (Type, Type)
 249 splitAppTy ty = case splitAppTy_maybe ty of
 250                         Just pr -> pr
 251                         Nothing -> panic "splitAppTy"
 252
 253 splitAppTys :: Type -> (Type, [Type])
 254 splitAppTys ty = split ty ty []
 255   where
 256     split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
 257     split orig_ty (AppTy ty arg)        args = split ty ty (arg:args)
 258     split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args)
 259     split orig_ty (FunTy ty1 ty2)       args = ASSERT( null args )
 260                                                (TyConApp funTyCon [], [ty1,ty2])
 261     split orig_ty ty                    args = (orig_ty, args)
 262 \end{code}
 263
 264
 265 ---------------------------------------------------------------------
 266                                 FunTy
 267                                 ~~~~~
 268
 269 \begin{code}
 270 mkFunTy :: Type -> Type -> Type
 271 mkFunTy arg res = FunTy arg res
 272
 273 mkFunTys :: [Type] -> Type -> Type
 274 mkFunTys tys ty = foldr FunTy ty tys
 275
 276 isFunTy :: Type -> Bool
 277 isFunTy ty = isJust (splitFunTy_maybe ty)
 278
 279 splitFunTy :: Type -> (Type, Type)
 280 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
 281 splitFunTy (FunTy arg res)   = (arg, res)
 282 splitFunTy other             = pprPanic "splitFunTy" (ppr other)
 283
 284 splitFunTy_maybe :: Type -> Maybe (Type, Type)
 285 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
 286 splitFunTy_maybe (FunTy arg res)   = Just (arg, res)
 287 splitFunTy_maybe other             = Nothing
 288
 289 splitFunTys :: Type -> ([Type], Type)
 290 splitFunTys ty = split [] ty ty
 291   where
 292     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
 293     split args orig_ty (FunTy arg res)   = split (arg:args) res res
 294     split args orig_ty ty                = (reverse args, orig_ty)
 295
 296 splitFunTysN :: Int -> Type -> ([Type], Type)
 297 -- Split off exactly n arg tys
 298 splitFunTysN 0 ty = ([], ty)
 299 splitFunTysN n ty = case splitFunTy ty of { (arg, res) ->
 300                     case splitFunTysN (n-1) res of { (args, res) ->
 301                     (arg:args, res) }}
 302
 303 zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type)
 304 zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty
 305   where
 306     split acc []     nty ty                = (reverse acc, nty)
 307     split acc xs     nty ty
 308           | Just ty' <- coreView ty        = split acc xs nty ty'
 309     split acc (x:xs) nty (FunTy arg res)   = split ((x,arg):acc) xs res res
 310     split acc (x:xs) nty ty                = pprPanic "zipFunTys" (ppr orig_xs <+> ppr orig_ty)
 311
 312 funResultTy :: Type -> Type
 313 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
 314 funResultTy (FunTy arg res)   = res
 315 funResultTy ty                = pprPanic "funResultTy" (ppr ty)
 316
 317 funArgTy :: Type -> Type
 318 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
 319 funArgTy (FunTy arg res)   = arg
 320 funArgTy ty                = pprPanic "funArgTy" (ppr ty)
 321 \end{code}
 322
 323
 324 ---------------------------------------------------------------------
 325                                 TyConApp
 326                                 ~~~~~~~~
 327 @mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or PredTy,
 328 as apppropriate.
 329
 330 \begin{code}
 331 mkGenTyConApp :: TyCon -> [Type] -> Type
 332 mkGenTyConApp tc tys
 333   | isSynTyCon tc = mkSynTy tc tys
 334   | otherwise     = mkTyConApp tc tys
 335
 336 mkTyConApp :: TyCon -> [Type] -> Type
 337 -- Assumes TyCon is not a SynTyCon; use mkSynTy instead for those
 338 mkTyConApp tycon tys
 339   | isFunTyCon tycon, [ty1,ty2] <- tys
 340   = FunTy ty1 ty2
 341
 342   | otherwise
 343   = ASSERT(not (isSynTyCon tycon))
 344     TyConApp tycon tys
 345
 346 mkTyConTy :: TyCon -> Type
 347 mkTyConTy tycon = mkTyConApp tycon []
 348
 349 -- splitTyConApp "looks through" synonyms, because they don't
 350 -- mean a distinct type, but all other type-constructor applications
 351 -- including functions are returned as Just ..
 352
 353 tyConAppTyCon :: Type -> TyCon
 354 tyConAppTyCon ty = fst (splitTyConApp ty)
 355
 356 tyConAppArgs :: Type -> [Type]
 357 tyConAppArgs ty = snd (splitTyConApp ty)
 358
 359 splitTyConApp :: Type -> (TyCon, [Type])
 360 splitTyConApp ty = case splitTyConApp_maybe ty of
 361                         Just stuff -> stuff
 362                         Nothing    -> pprPanic "splitTyConApp" (ppr ty)
 363
 364 splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 365 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
 366 splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
 367 splitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
 368 splitTyConApp_maybe other             = Nothing
 369 \end{code}
 370
 371
 372 ---------------------------------------------------------------------
 373                                 SynTy
 374                                 ~~~~~
 375
 376 \begin{code}
 377 mkSynTy tycon tys
 378   | n_args == arity     -- Exactly saturated
 379   = mk_syn tys
 380   | n_args >  arity     -- Over-saturated
 381   = case splitAt arity tys of { (as,bs) -> mkAppTys (mk_syn as) bs }
 382         -- Its important to use mkAppTys, rather than (foldl AppTy),
 383         -- because (mk_syn as) might well return a partially-applied
 384         -- type constructor; indeed, usually will!
 385   | otherwise           -- Un-saturated
 386   = TyConApp tycon tys
 387         -- For the un-saturated case we build TyConApp directly
 388         -- (mkTyConApp ASSERTs that the tc isn't a SynTyCon).
 389         -- Here we are relying on checkValidType to find
 390         -- the error.  What we can't do is use mkSynTy with
 391         -- too few arg tys, because that is utterly bogus.
 392
 393   where
 394     mk_syn tys = NoteTy (SynNote (TyConApp tycon tys))
 395                         (substTyWith tyvars tys body)
 396
 397     (tyvars, body) = ASSERT( isSynTyCon tycon ) getSynTyConDefn tycon
 398     arity          = tyConArity tycon
 399     n_args         = length tys
 400 \end{code}
 401
 402 Notes on type synonyms
 403 ~~~~~~~~~~~~~~~~~~~~~~
 404 The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
 405 to return type synonyms whereever possible. Thus
 406
 407         type Foo a = a -> a
 408
 409 we want
 410         splitFunTys (a -> Foo a) = ([a], Foo a)
 411 not                                ([a], a -> a)
 412
 413 The reason is that we then get better (shorter) type signatures in
 414 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 415
 416
 417                 Representation types
 418                 ~~~~~~~~~~~~~~~~~~~~
 419 repType looks through
 420         (a) for-alls, and
 421         (b) synonyms
 422         (c) predicates
 423         (d) usage annotations
 424         (e) all newtypes, including recursive ones
 425 It's useful in the back end.
 426
 427 \begin{code}
 428 repType :: Type -> Type
 429 -- Only applied to types of kind *; hence tycons are saturated
 430 repType (ForAllTy _ ty)   = repType ty
 431 repType (NoteTy   _ ty)   = repType ty
 432 repType (PredTy  p)       = repType (predTypeRep p)
 433 repType (TyConApp tc tys)
 434   | isNewTyCon tc         = ASSERT( tys `lengthIs` tyConArity tc )
 435                             repType (new_type_rep tc tys)
 436 repType ty                = ty
 437
 438 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
 439 -- of inspecting the type directly.
 440 typePrimRep :: Type -> PrimRep
 441 typePrimRep ty = case repType ty of
 442                    TyConApp tc _ -> tyConPrimRep tc
 443                    FunTy _ _     -> PtrRep
 444                    AppTy _ _     -> PtrRep      -- See note below
 445                    TyVarTy _     -> PtrRep
 446                    other         -> pprPanic "typePrimRep" (ppr ty)
 447         -- Types of the form 'f a' must be of kind *, not *#, so
 448         -- we are guaranteed that they are represented by pointers.
 449         -- The reason is that f must have kind *->*, not *->*#, because
 450         -- (we claim) there is no way to constrain f's kind any other
 451         -- way.
 452
 453 -- new_type_rep doesn't ask any questions:
 454 -- it just expands newtype, whether recursive or not
 455 new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
 456                              case newTyConRep new_tycon of
 457                                  (tvs, rep_ty) -> substTyWith tvs tys rep_ty
 458 \end{code}
 459
 460
 461 ---------------------------------------------------------------------
 462                                 ForAllTy
 463                                 ~~~~~~~~
 464
 465 \begin{code}
 466 mkForAllTy :: TyVar -> Type -> Type
 467 mkForAllTy tyvar ty
 468   = mkForAllTys [tyvar] ty
 469
 470 mkForAllTys :: [TyVar] -> Type -> Type
 471 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 472
 473 isForAllTy :: Type -> Bool
 474 isForAllTy (NoteTy _ ty)  = isForAllTy ty
 475 isForAllTy (ForAllTy _ _) = True
 476 isForAllTy other_ty       = False
 477
 478 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 479 splitForAllTy_maybe ty = splitFAT_m ty
 480   where
 481     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
 482     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
 483     splitFAT_m _                            = Nothing
 484
 485 splitForAllTys :: Type -> ([TyVar], Type)
 486 splitForAllTys ty = split ty ty []
 487    where
 488      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
 489      split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
 490      split orig_ty t                 tvs = (reverse tvs, orig_ty)
 491
 492 dropForAlls :: Type -> Type
 493 dropForAlls ty = snd (splitForAllTys ty)
 494 \end{code}
 495
 496 -- (mkPiType now in CoreUtils)
 497
 498 applyTy, applyTys
 499 ~~~~~~~~~~~~~~~~~
 500 Instantiate a for-all type with one or more type arguments.
 501 Used when we have a polymorphic function applied to type args:
 502         f t1 t2
 503 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
 504 the expression.
 505
 506 \begin{code}
 507 applyTy :: Type -> Type -> Type
 508 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
 509 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
 510 applyTy other            arg = panic "applyTy"
 511
 512 applyTys :: Type -> [Type] -> Type
 513 -- This function is interesting because
 514 --      a) the function may have more for-alls than there are args
 515 --      b) less obviously, it may have fewer for-alls
 516 -- For case (b) think of
 517 --      applyTys (forall a.a) [forall b.b, Int]
 518 -- This really can happen, via dressing up polymorphic types with newtype
 519 -- clothing.  Here's an example:
 520 --      newtype R = R (forall a. a->a)
 521 --      foo = case undefined :: R of
 522 --              R f -> f ()
 523
 524 applyTys orig_fun_ty []      = orig_fun_ty
 525 applyTys orig_fun_ty arg_tys
 526   | n_tvs == n_args     -- The vastly common case
 527   = substTyWith tvs arg_tys rho_ty
 528   | n_tvs > n_args      -- Too many for-alls
 529   = substTyWith (take n_args tvs) arg_tys
 530                 (mkForAllTys (drop n_args tvs) rho_ty)
 531   | otherwise           -- Too many type args
 532   = ASSERT2( n_tvs > 0, ppr orig_fun_ty )       -- Zero case gives infnite loop!
 533     applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
 534              (drop n_tvs arg_tys)
 535   where
 536     (tvs, rho_ty) = splitForAllTys orig_fun_ty
 537     n_tvs = length tvs
 538     n_args = length arg_tys
 539 \end{code}
 540
 541
 542 %************************************************************************
 543 %*                                                                      *
 544 \subsection{Source types}
 545 %*                                                                      *
 546 %************************************************************************
 547
 548 A "source type" is a type that is a separate type as far as the type checker is
 549 concerned, but which has low-level representation as far as the back end is concerned.
 550
 551 Source types are always lifted.
 552
 553 The key function is predTypeRep which gives the representation of a source type:
 554
 555 \begin{code}
 556 mkPredTy :: PredType -> Type
 557 mkPredTy pred = PredTy pred
 558
 559 mkPredTys :: ThetaType -> [Type]
 560 mkPredTys preds = map PredTy preds
 561
 562 predTypeRep :: PredType -> Type
 563 -- Convert a PredType to its "representation type";
 564 -- the post-type-checking type used by all the Core passes of GHC.
 565 -- Unwraps only the outermost level; for example, the result might
 566 -- be a newtype application
 567 predTypeRep (IParam _ ty)     = ty
 568 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
 569         -- Result might be a newtype application, but the consumer will
 570         -- look through that too if necessary
 571 \end{code}
 572
 573
 574 %************************************************************************
 575 %*                                                                      *
 576                 NewTypes
 577 %*                                                                      *
 578 %************************************************************************
 579
 580 \begin{code}
 581 splitRecNewType_maybe :: Type -> Maybe Type
 582 -- Sometimes we want to look through a recursive newtype, and that's what happens here
 583 -- It only strips *one layer* off, so the caller will usually call itself recursively
 584 -- Only applied to types of kind *, hence the newtype is always saturated
 585 splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
 586 splitRecNewType_maybe (TyConApp tc tys)
 587   | isNewTyCon tc
 588   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitRecNewType_maybe only be applied
 589                                                 --      to *types* (of kind *)
 590     ASSERT( isRecursiveTyCon tc )               -- Guaranteed by coreView
 591     case newTyConRhs tc of
 592         (tvs, rep_ty) -> ASSERT( length tvs == length tys )
 593                          Just (substTyWith tvs tys rep_ty)
 594
 595 splitRecNewType_maybe other = Nothing
 596 \end{code}
 597
 598
 599 %************************************************************************
 600 %*                                                                      *
 601 \subsection{Kinds and free variables}
 602 %*                                                                      *
 603 %************************************************************************
 604
 605 ---------------------------------------------------------------------
 606                 Finding the kind of a type
 607                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 608 \begin{code}
 609 typeKind :: Type -> Kind
 610
 611 typeKind (TyVarTy tyvar)        = tyVarKind tyvar
 612 typeKind (TyConApp tycon tys)   = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
 613 typeKind (NoteTy _ ty)          = typeKind ty
 614 typeKind (PredTy _)             = liftedTypeKind -- Predicates are always
 615                                                  -- represented by lifted types
 616 typeKind (AppTy fun arg)        = kindFunResult (typeKind fun)
 617 typeKind (FunTy arg res)        = liftedTypeKind
 618 typeKind (ForAllTy tv ty)       = typeKind ty
 619 \end{code}
 620
 621
 622 ---------------------------------------------------------------------
 623                 Free variables of a type
 624                 ~~~~~~~~~~~~~~~~~~~~~~~~
 625 \begin{code}
 626 tyVarsOfType :: Type -> TyVarSet
 627 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
 628 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
 629 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
 630 tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty2      -- See note [Syn] below
 631 tyVarsOfType (PredTy sty)               = tyVarsOfPred sty
 632 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 633 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
 634 tyVarsOfType (ForAllTy tyvar ty)        = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
 635
 636 --                      Note [Syn]
 637 -- Consider
 638 --      type T a = Int
 639 -- What are the free tyvars of (T x)?  Empty, of course!
 640 -- Here's the example that Ralf Laemmel showed me:
 641 --      foo :: (forall a. C u a -> C u a) -> u
 642 --      mappend :: Monoid u => u -> u -> u
 643 --
 644 --      bar :: Monoid u => u
 645 --      bar = foo (\t -> t `mappend` t)
 646 -- We have to generalise at the arg to f, and we don't
 647 -- want to capture the constraint (Monad (C u a)) because
 648 -- it appears to mention a.  Pretty silly, but it was useful to him.
 649
 650
 651 tyVarsOfTypes :: [Type] -> TyVarSet
 652 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 653
 654 tyVarsOfPred :: PredType -> TyVarSet
 655 tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
 656 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
 657
 658 tyVarsOfTheta :: ThetaType -> TyVarSet
 659 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
 660
 661 -- Add a Note with the free tyvars to the top of the type
 662 addFreeTyVars :: Type -> Type
 663 addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
 664 addFreeTyVars ty                             = NoteTy (FTVNote (tyVarsOfType ty)) ty
 665 \end{code}
 666
 667 %************************************************************************
 668 %*                                                                      *
 669 \subsection{TidyType}
 670 %*                                                                      *
 671 %************************************************************************
 672
 673 tidyTy tidies up a type for printing in an error message, or in
 674 an interface file.
 675
 676 It doesn't change the uniques at all, just the print names.
 677
 678 \begin{code}
 679 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 680 tidyTyVarBndr (tidy_env, subst) tyvar
 681   = case tidyOccName tidy_env (getOccName name) of
 682       (tidy', occ') ->  ((tidy', subst'), tyvar')
 683                     where
 684                         subst' = extendVarEnv subst tyvar tyvar'
 685                         tyvar' = setTyVarName tyvar name'
 686                         name'  = mkInternalName (getUnique name) occ' noSrcLoc
 687                                 -- Note: make a *user* tyvar, so it printes nicely
 688                                 -- Could extract src loc, but no need.
 689   where
 690     name = tyVarName tyvar
 691
 692 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
 693 -- Add the free tyvars to the env in tidy form,
 694 -- so that we can tidy the type they are free in
 695 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
 696
 697 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
 698 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
 699
 700 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 701 -- Treat a new tyvar as a binder, and give it a fresh tidy name
 702 tidyOpenTyVar env@(tidy_env, subst) tyvar
 703   = case lookupVarEnv subst tyvar of
 704         Just tyvar' -> (env, tyvar')            -- Already substituted
 705         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
 706
 707 tidyType :: TidyEnv -> Type -> Type
 708 tidyType env@(tidy_env, subst) ty
 709   = go ty
 710   where
 711     go (TyVarTy tv)         = case lookupVarEnv subst tv of
 712                                 Nothing  -> TyVarTy tv
 713                                 Just tv' -> TyVarTy tv'
 714     go (TyConApp tycon tys) = let args = map go tys
 715                               in args `seqList` TyConApp tycon args
 716     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
 717     go (PredTy sty)         = PredTy (tidyPred env sty)
 718     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
 719     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
 720     go (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
 721                               where
 722                                 (envp, tvp) = tidyTyVarBndr env tv
 723
 724     go_note (SynNote ty)        = SynNote $! (go ty)
 725     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
 726
 727 tidyTypes env tys = map (tidyType env) tys
 728
 729 tidyPred :: TidyEnv -> PredType -> PredType
 730 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
 731 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
 732 \end{code}
 733
 734
 735 @tidyOpenType@ grabs the free type variables, tidies them
 736 and then uses @tidyType@ to work over the type itself
 737
 738 \begin{code}
 739 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
 740 tidyOpenType env ty
 741   = (env', tidyType env' ty)
 742   where
 743     env' = tidyFreeTyVars env (tyVarsOfType ty)
 744
 745 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
 746 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
 747
 748 tidyTopType :: Type -> Type
 749 tidyTopType ty = tidyType emptyTidyEnv ty
 750 \end{code}
 751
 752
 753 %************************************************************************
 754 %*                                                                      *
 755                 Tidying Kinds
 756 %*                                                                      *
 757 %************************************************************************
 758
 759 We use a grevious hack for tidying KindVars.  A TidyEnv contains
 760 a (VarEnv Var) substitution, to express the renaming; but
 761 KindVars are not Vars.  The Right Thing ultimately is to make them
 762 into Vars (and perhaps make Kinds into Types), but I just do a hack
 763 here: I make up a TyVar just to remember the new OccName for the
 764 renamed KindVar
 765
 766 \begin{code}
 767 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
 768 tidyKind env@(tidy_env, subst) (KindVar kvar)
 769   | Just tv <- lookupVarEnv_Directly subst uniq
 770   = (env, KindVar (setKindVarOcc kvar (getOccName tv)))
 771   | otherwise
 772   = ((tidy', subst'), KindVar kvar')
 773   where
 774     uniq = kindVarUniq kvar
 775     (tidy', occ') = tidyOccName tidy_env (kindVarOcc kvar)
 776     kvar'   = setKindVarOcc kvar occ'
 777     fake_tv = mkTyVar tv_name (panic "tidyKind:fake tv kind")
 778     tv_name = mkInternalName uniq occ' noSrcLoc
 779     subst'  = extendVarEnv subst fake_tv fake_tv
 780
 781 tidyKind env (FunKind k1 k2)
 782   = (env2, FunKind k1' k2')
 783   where
 784     (env1, k1') = tidyKind env  k1
 785     (env2, k2') = tidyKind env1 k2
 786
 787 tidyKind env k = (env, k)       -- Atomic kinds
 788 \end{code}
 789
 790
 791 %************************************************************************
 792 %*                                                                      *
 793 \subsection{Liftedness}
 794 %*                                                                      *
 795 %************************************************************************
 796
 797 \begin{code}
 798 isUnLiftedType :: Type -> Bool
 799         -- isUnLiftedType returns True for forall'd unlifted types:
 800         --      x :: forall a. Int#
 801         -- I found bindings like these were getting floated to the top level.
 802         -- They are pretty bogus types, mind you.  It would be better never to
 803         -- construct them
 804
 805 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
 806 isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
 807 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
 808 isUnLiftedType other             = False
 809
 810 isUnboxedTupleType :: Type -> Bool
 811 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
 812                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
 813                            other              -> False
 814
 815 -- Should only be applied to *types*; hence the assert
 816 isAlgType :: Type -> Bool
 817 isAlgType ty = case splitTyConApp_maybe ty of
 818                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 819                                               isAlgTyCon tc
 820                         other              -> False
 821 \end{code}
 822
 823 @isStrictType@ computes whether an argument (or let RHS) should
 824 be computed strictly or lazily, based only on its type.
 825 Works just like isUnLiftedType, except that it has a special case
 826 for dictionaries.  Since it takes account of ClassP, you might think
 827 this function should be in TcType, but isStrictType is used by DataCon,
 828 which is below TcType in the hierarchy, so it's convenient to put it here.
 829
 830 \begin{code}
 831 isStrictType (PredTy pred)     = isStrictPred pred
 832 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
 833 isStrictType (ForAllTy tv ty)  = isStrictType ty
 834 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
 835 isStrictType other             = False
 836
 837 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
 838 isStrictPred other           = False
 839         -- We may be strict in dictionary types, but only if it
 840         -- has more than one component.
 841         -- [Being strict in a single-component dictionary risks
 842         --  poking the dictionary component, which is wrong.]
 843 \end{code}
 844
 845 \begin{code}
 846 isPrimitiveType :: Type -> Bool
 847 -- Returns types that are opaque to Haskell.
 848 -- Most of these are unlifted, but now that we interact with .NET, we
 849 -- may have primtive (foreign-imported) types that are lifted
 850 isPrimitiveType ty = case splitTyConApp_maybe ty of
 851                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 852                                               isPrimTyCon tc
 853                         other              -> False
 854 \end{code}
 855
 856
 857 %************************************************************************
 858 %*                                                                      *
 859 \subsection{Sequencing on types
 860 %*                                                                      *
 861 %************************************************************************
 862
 863 \begin{code}
 864 seqType :: Type -> ()
 865 seqType (TyVarTy tv)      = tv `seq` ()
 866 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
 867 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
 868 seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
 869 seqType (PredTy p)        = seqPred p
 870 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 871 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
 872
 873 seqTypes :: [Type] -> ()
 874 seqTypes []       = ()
 875 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 876
 877 seqNote :: TyNote -> ()
 878 seqNote (SynNote ty)  = seqType ty
 879 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 880
 881 seqPred :: PredType -> ()
 882 seqPred (ClassP c tys) = c  `seq` seqTypes tys
 883 seqPred (IParam n ty)  = n  `seq` seqType ty
 884 \end{code}
 885
 886
 887 %************************************************************************
 888 %*                                                                      *
 889                 Comparison of types
 890         (We don't use instances so that we know where it happens)
 891 %*                                                                      *
 892 %************************************************************************
 893
 894 Two flavours:
 895
 896 * tcEqType, tcCmpType do *not* look through newtypes, PredTypes
 897 * coreEqType *does* look through them
 898
 899 Note that eqType can respond 'False' for partial applications of newtypes.
 900 Consider
 901         newtype Parser m a = MkParser (Foogle m a)
 902 Does
 903         Monad (Parser m) `eqType` Monad (Foogle m)
 904 Well, yes, but eqType won't see that they are the same.
 905 I don't think this is harmful, but it's soemthing to watch out for.
 906
 907 First, the external interface
 908
 909 \begin{code}
 910 coreEqType :: Type -> Type -> Bool
 911 coreEqType t1 t2 = isEqual $ cmpType (deepCoreView t1) (deepCoreView t2)
 912
 913 tcEqType :: Type -> Type -> Bool
 914 tcEqType t1 t2 = isEqual $ cmpType t1 t2
 915
 916 tcEqTypes :: [Type] -> [Type] -> Bool
 917 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
 918
 919 tcCmpType :: Type -> Type -> Ordering
 920 tcCmpType t1 t2 = cmpType t1 t2
 921
 922 tcCmpTypes :: [Type] -> [Type] -> Ordering
 923 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
 924
 925 tcEqPred :: PredType -> PredType -> Bool
 926 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
 927
 928 tcCmpPred :: PredType -> PredType -> Ordering
 929 tcCmpPred p1 p2 = cmpPred p1 p2
 930
 931 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
 932 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
 933 \end{code}
 934
 935 Now here comes the real worker
 936
 937 \begin{code}
 938 cmpType :: Type -> Type -> Ordering
 939 cmpType t1 t2 = cmpTypeX rn_env t1 t2
 940   where
 941     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
 942
 943 cmpTypes :: [Type] -> [Type] -> Ordering
 944 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
 945   where
 946     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
 947
 948 cmpPred :: PredType -> PredType -> Ordering
 949 cmpPred p1 p2 = cmpPredX rn_env p1 p2
 950   where
 951     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
 952
 953 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
 954
 955 -- NB: we *cannot* short-cut the newtype comparison thus:
 956 -- eqTypeX env (NewTcApp tc1 tys1) (NewTcApp tc2 tys2)
 957 --      | (tc1 == tc2) = (eqTypeXs env tys1 tys2)
 958 --
 959 -- Consider:
 960 --      newtype T a = MkT [a]
 961 --      newtype Foo m = MkFoo (forall a. m a -> Int)
 962 --      w1 :: Foo []
 963 --      w1 = ...
 964 --
 965 --      w2 :: Foo T
 966 --      w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)
 967 --
 968 -- We end up with w2 = w1; so we need that Foo T = Foo []
 969 -- but we can only expand saturated newtypes, so just comparing
 970 -- T with [] won't do.
 971
 972 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
 973 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
 974 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 975 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 976 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
 977 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
 978 cmpTypeX env (NoteTy _ t1)      t2                   = cmpTypeX env t1 t2
 979 cmpTypeX env t1                 (NoteTy _ t2)        = cmpTypeX env t1 t2
 980
 981     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
 982 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
 983
 984 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
 985 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
 986
 987 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
 988 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
 989 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
 990
 991 cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
 992 cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
 993 cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
 994 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
 995
 996 cmpTypeX env (PredTy _)   t2            = GT
 997
 998 cmpTypeX env _ _ = LT
 999
1000 -------------
1001 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1002 cmpTypesX env []        []        = EQ
1003 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1004 cmpTypesX env []        tys       = LT
1005 cmpTypesX env ty        []        = GT
1006
1007 -------------
1008 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1009 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1010         -- Compare types as well as names for implicit parameters
1011         -- This comparison is used exclusively (I think) for the
1012         -- finite map built in TcSimplify
1013 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
1014 cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
1015 cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
1016 \end{code}
1017
1018 PredTypes are used as a FM key in TcSimplify,
1019 so we take the easy path and make them an instance of Ord
1020
1021 \begin{code}
1022 instance Eq  PredType where { (==)    = tcEqPred }
1023 instance Ord PredType where { compare = tcCmpPred }
1024 \end{code}
1025
1026
1027 %************************************************************************
1028 %*                                                                      *
1029                 Type substitutions
1030 %*                                                                      *
1031 %************************************************************************
1032
1033 \begin{code}
1034 data TvSubst
1035   = TvSubst InScopeSet  -- The in-scope type variables
1036             TvSubstEnv  -- The substitution itself
1037                         -- See Note [Apply Once]
1038
1039 {- ----------------------------------------------------------
1040                 Note [Apply Once]
1041
1042 We use TvSubsts to instantiate things, and we might instantiate
1043         forall a b. ty
1044 \with the types
1045         [a, b], or [b, a].
1046 So the substition might go [a->b, b->a].  A similar situation arises in Core
1047 when we find a beta redex like
1048         (/\ a /\ b -> e) b a
1049 Then we also end up with a substition that permutes type variables. Other
1050 variations happen to; for example [a -> (a, b)].
1051
1052         ***************************************************
1053         *** So a TvSubst must be applied precisely once ***
1054         ***************************************************
1055
1056 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1057 we use during unifications, it must not be repeatedly applied.
1058 -------------------------------------------------------------- -}
1059
1060
1061 type TvSubstEnv = TyVarEnv Type
1062         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1063         -- invariant discussed in Note [Apply Once]), and also independently
1064         -- in the middle of matching, and unification (see Types.Unify)
1065         -- So you have to look at the context to know if it's idempotent or
1066         -- apply-once or whatever
1067 emptyTvSubstEnv :: TvSubstEnv
1068 emptyTvSubstEnv = emptyVarEnv
1069
1070 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1071 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1072 -- It assumes that both are idempotent
1073 -- Typically, env1 is the refinement to a base substitution env2
1074 composeTvSubst in_scope env1 env2
1075   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1076         -- First apply env1 to the range of env2
1077         -- Then combine the two, making sure that env1 loses if
1078         -- both bind the same variable; that's why env1 is the
1079         --  *left* argument to plusVarEnv, because the right arg wins
1080   where
1081     subst1 = TvSubst in_scope env1
1082
1083 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1084 isEmptyTvSubst :: TvSubst -> Bool
1085 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1086
1087 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1088 mkTvSubst = TvSubst
1089
1090 getTvSubstEnv :: TvSubst -> TvSubstEnv
1091 getTvSubstEnv (TvSubst _ env) = env
1092
1093 getTvInScope :: TvSubst -> InScopeSet
1094 getTvInScope (TvSubst in_scope _) = in_scope
1095
1096 isInScope :: Var -> TvSubst -> Bool
1097 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1098
1099 notElemTvSubst :: TyVar -> TvSubst -> Bool
1100 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1101
1102 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1103 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1104
1105 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1106 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1107
1108 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1109 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1110
1111 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1112 extendTvSubstList (TvSubst in_scope env) tvs tys
1113   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1114
1115 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1116 -- the types given; but it's just a thunk so with a bit of luck
1117 -- it'll never be evaluated
1118
1119 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1120 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1121
1122 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1123 zipOpenTvSubst tyvars tys
1124 #ifdef DEBUG
1125   | length tyvars /= length tys
1126   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1127   | otherwise
1128 #endif
1129   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1130
1131 -- mkTopTvSubst is called when doing top-level substitutions.
1132 -- Here we expect that the free vars of the range of the
1133 -- substitution will be empty.
1134 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1135 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1136
1137 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1138 zipTopTvSubst tyvars tys
1139 #ifdef DEBUG
1140   | length tyvars /= length tys
1141   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1142   | otherwise
1143 #endif
1144   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1145
1146 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1147 zipTyEnv tyvars tys
1148 #ifdef DEBUG
1149   | length tyvars /= length tys
1150   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1151   | otherwise
1152 #endif
1153   = zip_ty_env tyvars tys emptyVarEnv
1154
1155 -- Later substitutions in the list over-ride earlier ones,
1156 -- but there should be no loops
1157 zip_ty_env []       []       env = env
1158 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1159         -- There used to be a special case for when
1160         --      ty == TyVarTy tv
1161         -- (a not-uncommon case) in which case the substitution was dropped.
1162         -- But the type-tidier changes the print-name of a type variable without
1163         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1164         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1165         -- And it happened that t was the type variable of the class.  Post-tiding,
1166         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1167         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1168         -- and so generated a rep type mentioning t not t2.
1169         --
1170         -- Simplest fix is to nuke the "optimisation"
1171 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1172 -- zip_ty_env _ _ env = env
1173
1174 instance Outputable TvSubst where
1175   ppr (TvSubst ins env)
1176     = sep[ ptext SLIT("<TvSubst"),
1177            nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1178            nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1179 \end{code}
1180
1181 %************************************************************************
1182 %*                                                                      *
1183                 Performing type substitutions
1184 %*                                                                      *
1185 %************************************************************************
1186
1187 \begin{code}
1188 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1189 substTyWith tvs tys = ASSERT( length tvs == length tys )
1190                       substTy (zipOpenTvSubst tvs tys)
1191
1192 substTy :: TvSubst -> Type  -> Type
1193 substTy subst ty | isEmptyTvSubst subst = ty
1194                  | otherwise            = subst_ty subst ty
1195
1196 substTys :: TvSubst -> [Type] -> [Type]
1197 substTys subst tys | isEmptyTvSubst subst = tys
1198                    | otherwise            = map (subst_ty subst) tys
1199
1200 deShadowTy :: Type -> Type              -- Remove any shadowing from the type
1201 deShadowTy ty = subst_ty emptyTvSubst ty
1202
1203 substTheta :: TvSubst -> ThetaType -> ThetaType
1204 substTheta subst theta
1205   | isEmptyTvSubst subst = theta
1206   | otherwise            = map (substPred subst) theta
1207
1208 substPred :: TvSubst -> PredType -> PredType
1209 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1210 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1211
1212 -- Note that the in_scope set is poked only if we hit a forall
1213 -- so it may often never be fully computed
1214 subst_ty subst ty
1215    = go ty
1216   where
1217     go (TyVarTy tv)                = substTyVar subst tv
1218     go (TyConApp tc tys)           = let args = map go tys
1219                                      in  args `seqList` TyConApp tc args
1220
1221     go (PredTy p)                  = PredTy $! (substPred subst p)
1222
1223     go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote $! (go ty1)) $! (go ty2)
1224     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
1225
1226     go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
1227     go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
1228                 -- The mkAppTy smart constructor is important
1229                 -- we might be replacing (a Int), represented with App
1230                 -- by [Int], represented with TyConApp
1231     go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
1232                                         (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1233
1234 substTyVar :: TvSubst -> TyVar  -> Type
1235 substTyVar (TvSubst in_scope env) tv
1236   = case (lookupVarEnv env tv) of
1237         Nothing  -> TyVarTy tv
1238         Just ty' -> ty' -- See Note [Apply Once]
1239
1240 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1241 substTyVarBndr subst@(TvSubst in_scope env) old_var
1242   | old_var == new_var  -- No need to clone
1243                         -- But we *must* zap any current substitution for the variable.
1244                         --  For example:
1245                         --      (\x.e) with id_subst = [x |-> e']
1246                         -- Here we must simply zap the substitution for x
1247                         --
1248                         -- The new_id isn't cloned, but it may have a different type
1249                         -- etc, so we must return it, not the old id
1250   = (TvSubst (in_scope `extendInScopeSet` new_var)
1251              (delVarEnv env old_var),
1252      new_var)
1253
1254   | otherwise   -- The new binder is in scope so
1255                 -- we'd better rename it away from the in-scope variables
1256                 -- Extending the substitution to do this renaming also
1257                 -- has the (correct) effect of discarding any existing
1258                 -- substitution for that variable
1259   = (TvSubst (in_scope `extendInScopeSet` new_var)
1260              (extendVarEnv env old_var (TyVarTy new_var)),
1261      new_var)
1262   where
1263     new_var = uniqAway in_scope old_var
1264         -- The uniqAway part makes sure the new variable is not already in scope
1265 \end{code}