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 (ForAllTy _ ty)   = repType ty
 427 repType (NoteTy   _ ty)   = repType ty
 428 repType (PredTy  p)       = repType (predTypeRep p)
 429 repType (TyConApp tc tys)
 430   | isNewTyCon tc         = ASSERT( tys `lengthIs` tyConArity tc )
 431                             repType (new_type_rep tc tys)
 432 repType ty                = ty
 433
 434 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
 435 -- of inspecting the type directly.
 436 typePrimRep :: Type -> PrimRep
 437 typePrimRep ty = case repType ty of
 438                    TyConApp tc _ -> tyConPrimRep tc
 439                    FunTy _ _     -> PtrRep
 440                    AppTy _ _     -> PtrRep      -- See note below
 441                    TyVarTy _     -> PtrRep
 442                    other         -> pprPanic "typePrimRep" (ppr ty)
 443         -- Types of the form 'f a' must be of kind *, not *#, so
 444         -- we are guaranteed that they are represented by pointers.
 445         -- The reason is that f must have kind *->*, not *->*#, because
 446         -- (we claim) there is no way to constrain f's kind any other
 447         -- way.
 448
 449 -- new_type_rep doesn't ask any questions:
 450 -- it just expands newtype, whether recursive or not
 451 new_type_rep new_tycon tys = ASSERT( tys `lengthIs` tyConArity new_tycon )
 452                              case newTyConRep new_tycon of
 453                                  (tvs, rep_ty) -> substTyWith tvs tys rep_ty
 454 \end{code}
 455
 456
 457 ---------------------------------------------------------------------
 458                                 ForAllTy
 459                                 ~~~~~~~~
 460
 461 \begin{code}
 462 mkForAllTy :: TyVar -> Type -> Type
 463 mkForAllTy tyvar ty
 464   = mkForAllTys [tyvar] ty
 465
 466 mkForAllTys :: [TyVar] -> Type -> Type
 467 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 468
 469 isForAllTy :: Type -> Bool
 470 isForAllTy (NoteTy _ ty)  = isForAllTy ty
 471 isForAllTy (ForAllTy _ _) = True
 472 isForAllTy other_ty       = False
 473
 474 splitForAllTy_maybe :: Type -> Maybe (TyVar, Type)
 475 splitForAllTy_maybe ty = splitFAT_m ty
 476   where
 477     splitFAT_m ty | Just ty' <- coreView ty = splitFAT_m ty'
 478     splitFAT_m (ForAllTy tyvar ty)          = Just(tyvar, ty)
 479     splitFAT_m _                            = Nothing
 480
 481 splitForAllTys :: Type -> ([TyVar], Type)
 482 splitForAllTys ty = split ty ty []
 483    where
 484      split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
 485      split orig_ty (ForAllTy tv ty)  tvs = split ty ty (tv:tvs)
 486      split orig_ty t                 tvs = (reverse tvs, orig_ty)
 487
 488 dropForAlls :: Type -> Type
 489 dropForAlls ty = snd (splitForAllTys ty)
 490 \end{code}
 491
 492 -- (mkPiType now in CoreUtils)
 493
 494 applyTy, applyTys
 495 ~~~~~~~~~~~~~~~~~
 496 Instantiate a for-all type with one or more type arguments.
 497 Used when we have a polymorphic function applied to type args:
 498         f t1 t2
 499 Then we use (applyTys type-of-f [t1,t2]) to compute the type of
 500 the expression.
 501
 502 \begin{code}
 503 applyTy :: Type -> Type -> Type
 504 applyTy ty arg | Just ty' <- coreView ty = applyTy ty' arg
 505 applyTy (ForAllTy tv ty) arg = substTyWith [tv] [arg] ty
 506 applyTy other            arg = panic "applyTy"
 507
 508 applyTys :: Type -> [Type] -> Type
 509 -- This function is interesting because
 510 --      a) the function may have more for-alls than there are args
 511 --      b) less obviously, it may have fewer for-alls
 512 -- For case (b) think of
 513 --      applyTys (forall a.a) [forall b.b, Int]
 514 -- This really can happen, via dressing up polymorphic types with newtype
 515 -- clothing.  Here's an example:
 516 --      newtype R = R (forall a. a->a)
 517 --      foo = case undefined :: R of
 518 --              R f -> f ()
 519
 520 applyTys orig_fun_ty []      = orig_fun_ty
 521 applyTys orig_fun_ty arg_tys
 522   | n_tvs == n_args     -- The vastly common case
 523   = substTyWith tvs arg_tys rho_ty
 524   | n_tvs > n_args      -- Too many for-alls
 525   = substTyWith (take n_args tvs) arg_tys
 526                 (mkForAllTys (drop n_args tvs) rho_ty)
 527   | otherwise           -- Too many type args
 528   = ASSERT2( n_tvs > 0, ppr orig_fun_ty )       -- Zero case gives infnite loop!
 529     applyTys (substTyWith tvs (take n_tvs arg_tys) rho_ty)
 530              (drop n_tvs arg_tys)
 531   where
 532     (tvs, rho_ty) = splitForAllTys orig_fun_ty
 533     n_tvs = length tvs
 534     n_args = length arg_tys
 535 \end{code}
 536
 537
 538 %************************************************************************
 539 %*                                                                      *
 540 \subsection{Source types}
 541 %*                                                                      *
 542 %************************************************************************
 543
 544 A "source type" is a type that is a separate type as far as the type checker is
 545 concerned, but which has low-level representation as far as the back end is concerned.
 546
 547 Source types are always lifted.
 548
 549 The key function is predTypeRep which gives the representation of a source type:
 550
 551 \begin{code}
 552 mkPredTy :: PredType -> Type
 553 mkPredTy pred = PredTy pred
 554
 555 mkPredTys :: ThetaType -> [Type]
 556 mkPredTys preds = map PredTy preds
 557
 558 predTypeRep :: PredType -> Type
 559 -- Convert a PredType to its "representation type";
 560 -- the post-type-checking type used by all the Core passes of GHC.
 561 -- Unwraps only the outermost level; for example, the result might
 562 -- be a newtype application
 563 predTypeRep (IParam _ ty)     = ty
 564 predTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys
 565         -- Result might be a newtype application, but the consumer will
 566         -- look through that too if necessary
 567 \end{code}
 568
 569
 570 %************************************************************************
 571 %*                                                                      *
 572                 NewTypes
 573 %*                                                                      *
 574 %************************************************************************
 575
 576 \begin{code}
 577 splitRecNewType_maybe :: Type -> Maybe Type
 578 -- Sometimes we want to look through a recursive newtype, and that's what happens here
 579 -- It only strips *one layer* off, so the caller will usually call itself recursively
 580 -- Only applied to types of kind *, hence the newtype is always saturated
 581 splitRecNewType_maybe ty | Just ty' <- coreView ty = splitRecNewType_maybe ty'
 582 splitRecNewType_maybe (TyConApp tc tys)
 583   | isNewTyCon tc
 584   = ASSERT( tys `lengthIs` tyConArity tc )      -- splitRecNewType_maybe only be applied
 585                                                 --      to *types* (of kind *)
 586     ASSERT( isRecursiveTyCon tc )               -- Guaranteed by coreView
 587     case newTyConRhs tc of
 588         (tvs, rep_ty) -> ASSERT( length tvs == length tys )
 589                          Just (substTyWith tvs tys rep_ty)
 590
 591 splitRecNewType_maybe other = Nothing
 592 \end{code}
 593
 594
 595 %************************************************************************
 596 %*                                                                      *
 597 \subsection{Kinds and free variables}
 598 %*                                                                      *
 599 %************************************************************************
 600
 601 ---------------------------------------------------------------------
 602                 Finding the kind of a type
 603                 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 604 \begin{code}
 605 typeKind :: Type -> Kind
 606
 607 typeKind (TyVarTy tyvar)        = tyVarKind tyvar
 608 typeKind (TyConApp tycon tys)   = foldr (\_ k -> kindFunResult k) (tyConKind tycon) tys
 609 typeKind (NoteTy _ ty)          = typeKind ty
 610 typeKind (PredTy _)             = liftedTypeKind -- Predicates are always
 611                                                  -- represented by lifted types
 612 typeKind (AppTy fun arg)        = kindFunResult (typeKind fun)
 613 typeKind (FunTy arg res)        = liftedTypeKind
 614 typeKind (ForAllTy tv ty)       = typeKind ty
 615 \end{code}
 616
 617
 618 ---------------------------------------------------------------------
 619                 Free variables of a type
 620                 ~~~~~~~~~~~~~~~~~~~~~~~~
 621 \begin{code}
 622 tyVarsOfType :: Type -> TyVarSet
 623 tyVarsOfType (TyVarTy tv)               = unitVarSet tv
 624 tyVarsOfType (TyConApp tycon tys)       = tyVarsOfTypes tys
 625 tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs
 626 tyVarsOfType (PredTy sty)               = tyVarsOfPred sty
 627 tyVarsOfType (FunTy arg res)            = tyVarsOfType arg `unionVarSet` tyVarsOfType res
 628 tyVarsOfType (AppTy fun arg)            = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
 629 tyVarsOfType (ForAllTy tyvar ty)        = tyVarsOfType ty `minusVarSet` unitVarSet tyvar
 630
 631 --                      Note [Syn]
 632 -- Consider
 633 --      type T a = Int
 634 -- What are the free tyvars of (T x)?  Empty, of course!
 635 -- Here's the example that Ralf Laemmel showed me:
 636 --      foo :: (forall a. C u a -> C u a) -> u
 637 --      mappend :: Monoid u => u -> u -> u
 638 --
 639 --      bar :: Monoid u => u
 640 --      bar = foo (\t -> t `mappend` t)
 641 -- We have to generalise at the arg to f, and we don't
 642 -- want to capture the constraint (Monad (C u a)) because
 643 -- it appears to mention a.  Pretty silly, but it was useful to him.
 644
 645
 646 tyVarsOfTypes :: [Type] -> TyVarSet
 647 tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys
 648
 649 tyVarsOfPred :: PredType -> TyVarSet
 650 tyVarsOfPred (IParam _ ty)  = tyVarsOfType ty
 651 tyVarsOfPred (ClassP _ tys) = tyVarsOfTypes tys
 652
 653 tyVarsOfTheta :: ThetaType -> TyVarSet
 654 tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet
 655
 656 -- Add a Note with the free tyvars to the top of the type
 657 addFreeTyVars :: Type -> Type
 658 addFreeTyVars ty@(NoteTy (FTVNote _) _)      = ty
 659 addFreeTyVars ty                             = NoteTy (FTVNote (tyVarsOfType ty)) ty
 660 \end{code}
 661
 662 %************************************************************************
 663 %*                                                                      *
 664 \subsection{TidyType}
 665 %*                                                                      *
 666 %************************************************************************
 667
 668 tidyTy tidies up a type for printing in an error message, or in
 669 an interface file.
 670
 671 It doesn't change the uniques at all, just the print names.
 672
 673 \begin{code}
 674 tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 675 tidyTyVarBndr (tidy_env, subst) tyvar
 676   = case tidyOccName tidy_env (getOccName name) of
 677       (tidy', occ') ->  ((tidy', subst'), tyvar')
 678                     where
 679                         subst' = extendVarEnv subst tyvar tyvar'
 680                         tyvar' = setTyVarName tyvar name'
 681                         name'  = mkInternalName (getUnique name) occ' noSrcLoc
 682                                 -- Note: make a *user* tyvar, so it printes nicely
 683                                 -- Could extract src loc, but no need.
 684   where
 685     name = tyVarName tyvar
 686
 687 tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
 688 -- Add the free tyvars to the env in tidy form,
 689 -- so that we can tidy the type they are free in
 690 tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
 691
 692 tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
 693 tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
 694
 695 tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
 696 -- Treat a new tyvar as a binder, and give it a fresh tidy name
 697 tidyOpenTyVar env@(tidy_env, subst) tyvar
 698   = case lookupVarEnv subst tyvar of
 699         Just tyvar' -> (env, tyvar')            -- Already substituted
 700         Nothing     -> tidyTyVarBndr env tyvar  -- Treat it as a binder
 701
 702 tidyType :: TidyEnv -> Type -> Type
 703 tidyType env@(tidy_env, subst) ty
 704   = go ty
 705   where
 706     go (TyVarTy tv)         = case lookupVarEnv subst tv of
 707                                 Nothing  -> TyVarTy tv
 708                                 Just tv' -> TyVarTy tv'
 709     go (TyConApp tycon tys) = let args = map go tys
 710                               in args `seqList` TyConApp tycon args
 711     go (NoteTy note ty)     = (NoteTy $! (go_note note)) $! (go ty)
 712     go (PredTy sty)         = PredTy (tidyPred env sty)
 713     go (AppTy fun arg)      = (AppTy $! (go fun)) $! (go arg)
 714     go (FunTy fun arg)      = (FunTy $! (go fun)) $! (go arg)
 715     go (ForAllTy tv ty)     = ForAllTy tvp $! (tidyType envp ty)
 716                               where
 717                                 (envp, tvp) = tidyTyVarBndr env tv
 718
 719     go_note note@(FTVNote ftvs) = note  -- No need to tidy the free tyvars
 720
 721 tidyTypes env tys = map (tidyType env) tys
 722
 723 tidyPred :: TidyEnv -> PredType -> PredType
 724 tidyPred env (IParam n ty)     = IParam n (tidyType env ty)
 725 tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
 726 \end{code}
 727
 728
 729 @tidyOpenType@ grabs the free type variables, tidies them
 730 and then uses @tidyType@ to work over the type itself
 731
 732 \begin{code}
 733 tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
 734 tidyOpenType env ty
 735   = (env', tidyType env' ty)
 736   where
 737     env' = tidyFreeTyVars env (tyVarsOfType ty)
 738
 739 tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
 740 tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
 741
 742 tidyTopType :: Type -> Type
 743 tidyTopType ty = tidyType emptyTidyEnv ty
 744 \end{code}
 745
 746
 747 %************************************************************************
 748 %*                                                                      *
 749                 Tidying Kinds
 750 %*                                                                      *
 751 %************************************************************************
 752
 753 We use a grevious hack for tidying KindVars.  A TidyEnv contains
 754 a (VarEnv Var) substitution, to express the renaming; but
 755 KindVars are not Vars.  The Right Thing ultimately is to make them
 756 into Vars (and perhaps make Kinds into Types), but I just do a hack
 757 here: I make up a TyVar just to remember the new OccName for the
 758 renamed KindVar
 759
 760 \begin{code}
 761 tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
 762 tidyKind env@(tidy_env, subst) (KindVar kvar)
 763   | Just tv <- lookupVarEnv_Directly subst uniq
 764   = (env, KindVar (setKindVarOcc kvar (getOccName tv)))
 765   | otherwise
 766   = ((tidy', subst'), KindVar kvar')
 767   where
 768     uniq = kindVarUniq kvar
 769     (tidy', occ') = tidyOccName tidy_env (kindVarOcc kvar)
 770     kvar'   = setKindVarOcc kvar occ'
 771     fake_tv = mkTyVar tv_name (panic "tidyKind:fake tv kind")
 772     tv_name = mkInternalName uniq occ' noSrcLoc
 773     subst'  = extendVarEnv subst fake_tv fake_tv
 774
 775 tidyKind env (FunKind k1 k2)
 776   = (env2, FunKind k1' k2')
 777   where
 778     (env1, k1') = tidyKind env  k1
 779     (env2, k2') = tidyKind env1 k2
 780
 781 tidyKind env k = (env, k)       -- Atomic kinds
 782 \end{code}
 783
 784
 785 %************************************************************************
 786 %*                                                                      *
 787 \subsection{Liftedness}
 788 %*                                                                      *
 789 %************************************************************************
 790
 791 \begin{code}
 792 isUnLiftedType :: Type -> Bool
 793         -- isUnLiftedType returns True for forall'd unlifted types:
 794         --      x :: forall a. Int#
 795         -- I found bindings like these were getting floated to the top level.
 796         -- They are pretty bogus types, mind you.  It would be better never to
 797         -- construct them
 798
 799 isUnLiftedType ty | Just ty' <- coreView ty = isUnLiftedType ty'
 800 isUnLiftedType (ForAllTy tv ty)  = isUnLiftedType ty
 801 isUnLiftedType (TyConApp tc _)   = isUnLiftedTyCon tc
 802 isUnLiftedType other             = False
 803
 804 isUnboxedTupleType :: Type -> Bool
 805 isUnboxedTupleType ty = case splitTyConApp_maybe ty of
 806                            Just (tc, ty_args) -> isUnboxedTupleTyCon tc
 807                            other              -> False
 808
 809 -- Should only be applied to *types*; hence the assert
 810 isAlgType :: Type -> Bool
 811 isAlgType ty = case splitTyConApp_maybe ty of
 812                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 813                                               isAlgTyCon tc
 814                         other              -> False
 815 \end{code}
 816
 817 @isStrictType@ computes whether an argument (or let RHS) should
 818 be computed strictly or lazily, based only on its type.
 819 Works just like isUnLiftedType, except that it has a special case
 820 for dictionaries.  Since it takes account of ClassP, you might think
 821 this function should be in TcType, but isStrictType is used by DataCon,
 822 which is below TcType in the hierarchy, so it's convenient to put it here.
 823
 824 \begin{code}
 825 isStrictType (PredTy pred)     = isStrictPred pred
 826 isStrictType ty | Just ty' <- coreView ty = isStrictType ty'
 827 isStrictType (ForAllTy tv ty)  = isStrictType ty
 828 isStrictType (TyConApp tc _)   = isUnLiftedTyCon tc
 829 isStrictType other             = False
 830
 831 isStrictPred (ClassP clas _) = opt_DictsStrict && not (isNewTyCon (classTyCon clas))
 832 isStrictPred other           = False
 833         -- We may be strict in dictionary types, but only if it
 834         -- has more than one component.
 835         -- [Being strict in a single-component dictionary risks
 836         --  poking the dictionary component, which is wrong.]
 837 \end{code}
 838
 839 \begin{code}
 840 isPrimitiveType :: Type -> Bool
 841 -- Returns types that are opaque to Haskell.
 842 -- Most of these are unlifted, but now that we interact with .NET, we
 843 -- may have primtive (foreign-imported) types that are lifted
 844 isPrimitiveType ty = case splitTyConApp_maybe ty of
 845                         Just (tc, ty_args) -> ASSERT( ty_args `lengthIs` tyConArity tc )
 846                                               isPrimTyCon tc
 847                         other              -> False
 848 \end{code}
 849
 850
 851 %************************************************************************
 852 %*                                                                      *
 853 \subsection{Sequencing on types
 854 %*                                                                      *
 855 %************************************************************************
 856
 857 \begin{code}
 858 seqType :: Type -> ()
 859 seqType (TyVarTy tv)      = tv `seq` ()
 860 seqType (AppTy t1 t2)     = seqType t1 `seq` seqType t2
 861 seqType (FunTy t1 t2)     = seqType t1 `seq` seqType t2
 862 seqType (NoteTy note t2)  = seqNote note `seq` seqType t2
 863 seqType (PredTy p)        = seqPred p
 864 seqType (TyConApp tc tys) = tc `seq` seqTypes tys
 865 seqType (ForAllTy tv ty)  = tv `seq` seqType ty
 866
 867 seqTypes :: [Type] -> ()
 868 seqTypes []       = ()
 869 seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
 870
 871 seqNote :: TyNote -> ()
 872 seqNote (FTVNote set) = sizeUniqSet set `seq` ()
 873
 874 seqPred :: PredType -> ()
 875 seqPred (ClassP c tys) = c  `seq` seqTypes tys
 876 seqPred (IParam n ty)  = n  `seq` seqType ty
 877 \end{code}
 878
 879
 880 %************************************************************************
 881 %*                                                                      *
 882                 Equality for Core types
 883         (We don't use instances so that we know where it happens)
 884 %*                                                                      *
 885 %************************************************************************
 886
 887 Note that eqType works right even for partial applications of newtypes.
 888 See Note [Newtype eta] in TyCon.lhs
 889
 890 \begin{code}
 891 coreEqType :: Type -> Type -> Bool
 892 coreEqType t1 t2
 893   = eq rn_env t1 t2
 894   where
 895     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
 896
 897     eq env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
 898     eq env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = eq (rnBndr2 env tv1 tv2) t1 t2
 899     eq env (AppTy s1 t1)       (AppTy s2 t2)     = eq env s1 s2 && eq env t1 t2
 900     eq env (FunTy s1 t1)       (FunTy s2 t2)     = eq env s1 s2 && eq env t1 t2
 901     eq env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 902         | tc1 == tc2, all2 (eq env) tys1 tys2 = True
 903                         -- The lengths should be equal because
 904                         -- the two types have the same kind
 905         -- NB: if the type constructors differ that does not
 906         --     necessarily mean that the types aren't equal
 907         --     (synonyms, newtypes)
 908         -- Even if the type constructors are the same, but the arguments
 909         -- differ, the two types could be the same (e.g. if the arg is just
 910         -- ignored in the RHS).  In both these cases we fall through to an
 911         -- attempt to expand one side or the other.
 912
 913         -- Now deal with newtypes, synonyms, pred-tys
 914     eq env t1 t2 | Just t1' <- coreView t1 = eq env t1' t2
 915                  | Just t2' <- coreView t2 = eq env t1 t2'
 916
 917         -- Fall through case; not equal!
 918     eq env t1 t2 = False
 919 \end{code}
 920
 921
 922 %************************************************************************
 923 %*                                                                      *
 924                 Comparision for source types
 925         (We don't use instances so that we know where it happens)
 926 %*                                                                      *
 927 %************************************************************************
 928
 929 Note that
 930         tcEqType, tcCmpType
 931 do *not* look through newtypes, PredTypes
 932
 933 \begin{code}
 934 tcEqType :: Type -> Type -> Bool
 935 tcEqType t1 t2 = isEqual $ cmpType t1 t2
 936
 937 tcEqTypes :: [Type] -> [Type] -> Bool
 938 tcEqTypes tys1 tys2 = isEqual $ cmpTypes tys1 tys2
 939
 940 tcCmpType :: Type -> Type -> Ordering
 941 tcCmpType t1 t2 = cmpType t1 t2
 942
 943 tcCmpTypes :: [Type] -> [Type] -> Ordering
 944 tcCmpTypes tys1 tys2 = cmpTypes tys1 tys2
 945
 946 tcEqPred :: PredType -> PredType -> Bool
 947 tcEqPred p1 p2 = isEqual $ cmpPred p1 p2
 948
 949 tcCmpPred :: PredType -> PredType -> Ordering
 950 tcCmpPred p1 p2 = cmpPred p1 p2
 951
 952 tcEqTypeX :: RnEnv2 -> Type -> Type -> Bool
 953 tcEqTypeX env t1 t2 = isEqual $ cmpTypeX env t1 t2
 954 \end{code}
 955
 956 Now here comes the real worker
 957
 958 \begin{code}
 959 cmpType :: Type -> Type -> Ordering
 960 cmpType t1 t2 = cmpTypeX rn_env t1 t2
 961   where
 962     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType t1 `unionVarSet` tyVarsOfType t2))
 963
 964 cmpTypes :: [Type] -> [Type] -> Ordering
 965 cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
 966   where
 967     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfTypes ts1 `unionVarSet` tyVarsOfTypes ts2))
 968
 969 cmpPred :: PredType -> PredType -> Ordering
 970 cmpPred p1 p2 = cmpPredX rn_env p1 p2
 971   where
 972     rn_env = mkRnEnv2 (mkInScopeSet (tyVarsOfPred p1 `unionVarSet` tyVarsOfPred p2))
 973
 974 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
 975 cmpTypeX env t1 t2 | Just t1' <- tcView t1 = cmpTypeX env t1' t2
 976                    | Just t2' <- tcView t2 = cmpTypeX env t1 t2'
 977
 978 cmpTypeX env (TyVarTy tv1)       (TyVarTy tv2)       = rnOccL env tv1 `compare` rnOccR env tv2
 979 cmpTypeX env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTypeX (rnBndr2 env tv1 tv2) t1 t2
 980 cmpTypeX env (AppTy s1 t1)       (AppTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 981 cmpTypeX env (FunTy s1 t1)       (FunTy s2 t2)       = cmpTypeX env s1 s2 `thenCmp` cmpTypeX env t1 t2
 982 cmpTypeX env (PredTy p1)         (PredTy p2)         = cmpPredX env p1 p2
 983 cmpTypeX env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` cmpTypesX env tys1 tys2
 984 cmpTypeX env t1                 (NoteTy _ t2)        = cmpTypeX env t1 t2
 985
 986     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
 987 cmpTypeX env (AppTy _ _) (TyVarTy _) = GT
 988
 989 cmpTypeX env (FunTy _ _) (TyVarTy _) = GT
 990 cmpTypeX env (FunTy _ _) (AppTy _ _) = GT
 991
 992 cmpTypeX env (TyConApp _ _) (TyVarTy _) = GT
 993 cmpTypeX env (TyConApp _ _) (AppTy _ _) = GT
 994 cmpTypeX env (TyConApp _ _) (FunTy _ _) = GT
 995
 996 cmpTypeX env (ForAllTy _ _) (TyVarTy _)    = GT
 997 cmpTypeX env (ForAllTy _ _) (AppTy _ _)    = GT
 998 cmpTypeX env (ForAllTy _ _) (FunTy _ _)    = GT
 999 cmpTypeX env (ForAllTy _ _) (TyConApp _ _) = GT
1000
1001 cmpTypeX env (PredTy _)   t2            = GT
1002
1003 cmpTypeX env _ _ = LT
1004
1005 -------------
1006 cmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
1007 cmpTypesX env []        []        = EQ
1008 cmpTypesX env (t1:tys1) (t2:tys2) = cmpTypeX env t1 t2 `thenCmp` cmpTypesX env tys1 tys2
1009 cmpTypesX env []        tys       = LT
1010 cmpTypesX env ty        []        = GT
1011
1012 -------------
1013 cmpPredX :: RnEnv2 -> PredType -> PredType -> Ordering
1014 cmpPredX env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` cmpTypeX env ty1 ty2
1015         -- Compare types as well as names for implicit parameters
1016         -- This comparison is used exclusively (I think) for the
1017         -- finite map built in TcSimplify
1018 cmpPredX env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` cmpTypesX env tys1 tys2
1019 cmpPredX env (IParam _ _)     (ClassP _ _)     = LT
1020 cmpPredX env (ClassP _ _)     (IParam _ _)     = GT
1021 \end{code}
1022
1023 PredTypes are used as a FM key in TcSimplify,
1024 so we take the easy path and make them an instance of Ord
1025
1026 \begin{code}
1027 instance Eq  PredType where { (==)    = tcEqPred }
1028 instance Ord PredType where { compare = tcCmpPred }
1029 \end{code}
1030
1031
1032 %************************************************************************
1033 %*                                                                      *
1034                 Type substitutions
1035 %*                                                                      *
1036 %************************************************************************
1037
1038 \begin{code}
1039 data TvSubst
1040   = TvSubst InScopeSet  -- The in-scope type variables
1041             TvSubstEnv  -- The substitution itself
1042                         -- See Note [Apply Once]
1043
1044 {- ----------------------------------------------------------
1045                 Note [Apply Once]
1046
1047 We use TvSubsts to instantiate things, and we might instantiate
1048         forall a b. ty
1049 \with the types
1050         [a, b], or [b, a].
1051 So the substition might go [a->b, b->a].  A similar situation arises in Core
1052 when we find a beta redex like
1053         (/\ a /\ b -> e) b a
1054 Then we also end up with a substition that permutes type variables. Other
1055 variations happen to; for example [a -> (a, b)].
1056
1057         ***************************************************
1058         *** So a TvSubst must be applied precisely once ***
1059         ***************************************************
1060
1061 A TvSubst is not idempotent, but, unlike the non-idempotent substitution
1062 we use during unifications, it must not be repeatedly applied.
1063 -------------------------------------------------------------- -}
1064
1065
1066 type TvSubstEnv = TyVarEnv Type
1067         -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
1068         -- invariant discussed in Note [Apply Once]), and also independently
1069         -- in the middle of matching, and unification (see Types.Unify)
1070         -- So you have to look at the context to know if it's idempotent or
1071         -- apply-once or whatever
1072 emptyTvSubstEnv :: TvSubstEnv
1073 emptyTvSubstEnv = emptyVarEnv
1074
1075 composeTvSubst :: InScopeSet -> TvSubstEnv -> TvSubstEnv -> TvSubstEnv
1076 -- (compose env1 env2)(x) is env1(env2(x)); i.e. apply env2 then env1
1077 -- It assumes that both are idempotent
1078 -- Typically, env1 is the refinement to a base substitution env2
1079 composeTvSubst in_scope env1 env2
1080   = env1 `plusVarEnv` mapVarEnv (substTy subst1) env2
1081         -- First apply env1 to the range of env2
1082         -- Then combine the two, making sure that env1 loses if
1083         -- both bind the same variable; that's why env1 is the
1084         --  *left* argument to plusVarEnv, because the right arg wins
1085   where
1086     subst1 = TvSubst in_scope env1
1087
1088 emptyTvSubst = TvSubst emptyInScopeSet emptyVarEnv
1089
1090 isEmptyTvSubst :: TvSubst -> Bool
1091 isEmptyTvSubst (TvSubst _ env) = isEmptyVarEnv env
1092
1093 mkTvSubst :: InScopeSet -> TvSubstEnv -> TvSubst
1094 mkTvSubst = TvSubst
1095
1096 getTvSubstEnv :: TvSubst -> TvSubstEnv
1097 getTvSubstEnv (TvSubst _ env) = env
1098
1099 getTvInScope :: TvSubst -> InScopeSet
1100 getTvInScope (TvSubst in_scope _) = in_scope
1101
1102 isInScope :: Var -> TvSubst -> Bool
1103 isInScope v (TvSubst in_scope _) = v `elemInScopeSet` in_scope
1104
1105 notElemTvSubst :: TyVar -> TvSubst -> Bool
1106 notElemTvSubst tv (TvSubst _ env) = not (tv `elemVarEnv` env)
1107
1108 setTvSubstEnv :: TvSubst -> TvSubstEnv -> TvSubst
1109 setTvSubstEnv (TvSubst in_scope _) env = TvSubst in_scope env
1110
1111 extendTvInScope :: TvSubst -> [Var] -> TvSubst
1112 extendTvInScope (TvSubst in_scope env) vars = TvSubst (extendInScopeSetList in_scope vars) env
1113
1114 extendTvSubst :: TvSubst -> TyVar -> Type -> TvSubst
1115 extendTvSubst (TvSubst in_scope env) tv ty = TvSubst in_scope (extendVarEnv env tv ty)
1116
1117 extendTvSubstList :: TvSubst -> [TyVar] -> [Type] -> TvSubst
1118 extendTvSubstList (TvSubst in_scope env) tvs tys
1119   = TvSubst in_scope (extendVarEnvList env (tvs `zip` tys))
1120
1121 -- mkOpenTvSubst and zipOpenTvSubst generate the in-scope set from
1122 -- the types given; but it's just a thunk so with a bit of luck
1123 -- it'll never be evaluated
1124
1125 mkOpenTvSubst :: TvSubstEnv -> TvSubst
1126 mkOpenTvSubst env = TvSubst (mkInScopeSet (tyVarsOfTypes (varEnvElts env))) env
1127
1128 zipOpenTvSubst :: [TyVar] -> [Type] -> TvSubst
1129 zipOpenTvSubst tyvars tys
1130 #ifdef DEBUG
1131   | length tyvars /= length tys
1132   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1133   | otherwise
1134 #endif
1135   = TvSubst (mkInScopeSet (tyVarsOfTypes tys)) (zipTyEnv tyvars tys)
1136
1137 -- mkTopTvSubst is called when doing top-level substitutions.
1138 -- Here we expect that the free vars of the range of the
1139 -- substitution will be empty.
1140 mkTopTvSubst :: [(TyVar, Type)] -> TvSubst
1141 mkTopTvSubst prs = TvSubst emptyInScopeSet (mkVarEnv prs)
1142
1143 zipTopTvSubst :: [TyVar] -> [Type] -> TvSubst
1144 zipTopTvSubst tyvars tys
1145 #ifdef DEBUG
1146   | length tyvars /= length tys
1147   = pprTrace "zipOpenTvSubst" (ppr tyvars $$ ppr tys) emptyTvSubst
1148   | otherwise
1149 #endif
1150   = TvSubst emptyInScopeSet (zipTyEnv tyvars tys)
1151
1152 zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
1153 zipTyEnv tyvars tys
1154 #ifdef DEBUG
1155   | length tyvars /= length tys
1156   = pprTrace "mkTopTvSubst" (ppr tyvars $$ ppr tys) emptyVarEnv
1157   | otherwise
1158 #endif
1159   = zip_ty_env tyvars tys emptyVarEnv
1160
1161 -- Later substitutions in the list over-ride earlier ones,
1162 -- but there should be no loops
1163 zip_ty_env []       []       env = env
1164 zip_ty_env (tv:tvs) (ty:tys) env = zip_ty_env tvs tys (extendVarEnv env tv ty)
1165         -- There used to be a special case for when
1166         --      ty == TyVarTy tv
1167         -- (a not-uncommon case) in which case the substitution was dropped.
1168         -- But the type-tidier changes the print-name of a type variable without
1169         -- changing the unique, and that led to a bug.   Why?  Pre-tidying, we had
1170         -- a type {Foo t}, where Foo is a one-method class.  So Foo is really a newtype.
1171         -- And it happened that t was the type variable of the class.  Post-tiding,
1172         -- it got turned into {Foo t2}.  The ext-core printer expanded this using
1173         -- sourceTypeRep, but that said "Oh, t == t2" because they have the same unique,
1174         -- and so generated a rep type mentioning t not t2.
1175         --
1176         -- Simplest fix is to nuke the "optimisation"
1177 zip_ty_env tvs      tys      env   = pprTrace "Var/Type length mismatch: " (ppr tvs $$ ppr tys) env
1178 -- zip_ty_env _ _ env = env
1179
1180 instance Outputable TvSubst where
1181   ppr (TvSubst ins env)
1182     = sep[ ptext SLIT("<TvSubst"),
1183            nest 2 (ptext SLIT("In scope:") <+> ppr ins),
1184            nest 2 (ptext SLIT("Env:") <+> ppr env) ]
1185 \end{code}
1186
1187 %************************************************************************
1188 %*                                                                      *
1189                 Performing type substitutions
1190 %*                                                                      *
1191 %************************************************************************
1192
1193 \begin{code}
1194 substTyWith :: [TyVar] -> [Type] -> Type -> Type
1195 substTyWith tvs tys = ASSERT( length tvs == length tys )
1196                       substTy (zipOpenTvSubst tvs tys)
1197
1198 substTy :: TvSubst -> Type  -> Type
1199 substTy subst ty | isEmptyTvSubst subst = ty
1200                  | otherwise            = subst_ty subst ty
1201
1202 substTys :: TvSubst -> [Type] -> [Type]
1203 substTys subst tys | isEmptyTvSubst subst = tys
1204                    | otherwise            = map (subst_ty subst) tys
1205
1206 substTheta :: TvSubst -> ThetaType -> ThetaType
1207 substTheta subst theta
1208   | isEmptyTvSubst subst = theta
1209   | otherwise            = map (substPred subst) theta
1210
1211 substPred :: TvSubst -> PredType -> PredType
1212 substPred subst (IParam n ty)     = IParam n (subst_ty subst ty)
1213 substPred subst (ClassP clas tys) = ClassP clas (map (subst_ty subst) tys)
1214
1215 deShadowTy :: TyVarSet -> Type -> Type  -- Remove any nested binders mentioning tvs
1216 deShadowTy tvs ty
1217   = subst_ty (mkTvSubst in_scope emptyTvSubstEnv) ty
1218   where
1219     in_scope = mkInScopeSet tvs
1220
1221 -- Note that the in_scope set is poked only if we hit a forall
1222 -- so it may often never be fully computed
1223 subst_ty subst ty
1224    = go ty
1225   where
1226     go (TyVarTy tv)                = substTyVar subst tv
1227     go (TyConApp tc tys)           = let args = map go tys
1228                                      in  args `seqList` TyConApp tc args
1229
1230     go (PredTy p)                  = PredTy $! (substPred subst p)
1231
1232     go (NoteTy (FTVNote _) ty2)    = go ty2             -- Discard the free tyvar note
1233
1234     go (FunTy arg res)             = (FunTy $! (go arg)) $! (go res)
1235     go (AppTy fun arg)             = mkAppTy (go fun) $! (go arg)
1236                 -- The mkAppTy smart constructor is important
1237                 -- we might be replacing (a Int), represented with App
1238                 -- by [Int], represented with TyConApp
1239     go (ForAllTy tv ty)            = case substTyVarBndr subst tv of
1240                                         (subst', tv') -> ForAllTy tv' $! (subst_ty subst' ty)
1241
1242 substTyVar :: TvSubst -> TyVar  -> Type
1243 substTyVar (TvSubst in_scope env) tv
1244   = case (lookupVarEnv env tv) of
1245         Nothing  -> TyVarTy tv
1246         Just ty' -> ty' -- See Note [Apply Once]
1247
1248 substTyVarBndr :: TvSubst -> TyVar -> (TvSubst, TyVar)
1249 substTyVarBndr subst@(TvSubst in_scope env) old_var
1250   | old_var == new_var  -- No need to clone
1251                         -- But we *must* zap any current substitution for the variable.
1252                         --  For example:
1253                         --      (\x.e) with id_subst = [x |-> e']
1254                         -- Here we must simply zap the substitution for x
1255                         --
1256                         -- The new_id isn't cloned, but it may have a different type
1257                         -- etc, so we must return it, not the old id
1258   = (TvSubst (in_scope `extendInScopeSet` new_var)
1259              (delVarEnv env old_var),
1260      new_var)
1261
1262   | otherwise   -- The new binder is in scope so
1263                 -- we'd better rename it away from the in-scope variables
1264                 -- Extending the substitution to do this renaming also
1265                 -- has the (correct) effect of discarding any existing
1266                 -- substitution for that variable
1267   = (TvSubst (in_scope `extendInScopeSet` new_var)
1268              (extendVarEnv env old_var (TyVarTy new_var)),
1269      new_var)
1270   where
1271     new_var = uniqAway in_scope old_var
1272         -- The uniqAway part makes sure the new variable is not already in scope
1273 \end{code}