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