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