ghc/compiler/typecheck/TcType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcType]{Types used in the typechecker}
   5
   6 \begin{code}
   7 module TcType (
   8
   9   TcTyVar,
  10   TcTyVarSet,
  11   newTyVar,
  12   newTyVarTy,           -- Kind -> NF_TcM TcType
  13   newTyVarTys,          -- Int -> Kind -> NF_TcM [TcType]
  14
  15   -----------------------------------------
  16   TcType, TcTauType, TcThetaType, TcRhoType, TcClassContext,
  17
  18         -- Find the type to which a type variable is bound
  19   tcPutTyVar,           -- :: TcTyVar -> TcType -> NF_TcM TcType
  20   tcGetTyVar,           -- :: TcTyVar -> NF_TcM (Maybe TcType)  does shorting out
  21
  22
  23   tcSplitRhoTy,
  24
  25   tcInstTyVar, tcInstTyVars,
  26   tcInstSigVar,
  27   tcInstType,
  28
  29   --------------------------------
  30   TcKind,
  31   newKindVar, newKindVars, newBoxityVar,
  32
  33   --------------------------------
  34   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
  35   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  36
  37   zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
  38
  39   ) where
  40
  41 #include "HsVersions.h"
  42
  43
  44 -- friends:
  45 import TypeRep          ( Type(..), Kind, TyNote(..) )  -- friend
  46 import Type             ( PredType(..),
  47                           getTyVar, mkAppTy, mkUTy,
  48                           splitPredTy_maybe, splitForAllTys,
  49                           isTyVarTy, mkTyVarTy, mkTyVarTys,
  50                           openTypeKind, liftedTypeKind,
  51                           superKind, superBoxity, tyVarsOfTypes,
  52                           defaultKind, liftedBoxity
  53                         )
  54 import Subst            ( Subst, mkTopTyVarSubst, substTy )
  55 import TyCon            ( mkPrimTyCon )
  56 import PrimRep          ( PrimRep(VoidRep) )
  57 import Var              ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
  58
  59 -- others:
  60 import TcMonad          -- TcType, amongst others
  61 import TysWiredIn       ( voidTy )
  62
  63 import Name             ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
  64                           mkLocalName, mkDerivedTyConOcc
  65                         )
  66 import Unique           ( Uniquable(..) )
  67 import SrcLoc           ( noSrcLoc )
  68 import Util             ( nOfThem )
  69 import Outputable
  70 \end{code}
  71
  72
  73 Utility functions
  74 ~~~~~~~~~~~~~~~~~
  75 These tcSplit functions are like their non-Tc analogues, but they
  76 follow through bound type variables.
  77
  78 No need for tcSplitForAllTy because a type variable can't be instantiated
  79 to a for-all type.
  80
  81 \begin{code}
  82 tcSplitRhoTy :: TcType -> NF_TcM (TcThetaType, TcType)
  83 tcSplitRhoTy t
  84   = go t t []
  85  where
  86         -- A type variable is never instantiated to a dictionary type,
  87         -- so we don't need to do a tcReadVar on the "arg".
  88     go syn_t (FunTy arg res) ts = case splitPredTy_maybe arg of
  89                                         Just pair -> go res res (pair:ts)
  90                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
  91     go syn_t (NoteTy _ t)    ts = go syn_t t ts
  92     go syn_t (TyVarTy tv)    ts = tcGetTyVar tv         `thenNF_Tc` \ maybe_ty ->
  93                                   case maybe_ty of
  94                                     Just ty | not (isTyVarTy ty) -> go syn_t ty ts
  95                                     other                        -> returnNF_Tc (reverse ts, syn_t)
  96     go syn_t (UsageTy _ t)   ts = go syn_t t ts
  97     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
  98 \end{code}
  99
 100
 101 %************************************************************************
 102 %*                                                                      *
 103 \subsection{New type variables}
 104 %*                                                                      *
 105 %************************************************************************
 106
 107 \begin{code}
 108 newTyVar :: Kind -> NF_TcM TcTyVar
 109 newTyVar kind
 110   = tcGetUnique         `thenNF_Tc` \ uniq ->
 111     tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
 112
 113 newTyVarTy  :: Kind -> NF_TcM TcType
 114 newTyVarTy kind
 115   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
 116     returnNF_Tc (TyVarTy tc_tyvar)
 117
 118 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 119 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 120
 121 newKindVar :: NF_TcM TcKind
 122 newKindVar
 123   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 124     tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind     `thenNF_Tc` \ kv ->
 125     returnNF_Tc (TyVarTy kv)
 126
 127 newKindVars :: Int -> NF_TcM [TcKind]
 128 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 129
 130 newBoxityVar :: NF_TcM TcKind
 131 newBoxityVar
 132   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 133     tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity  `thenNF_Tc` \ kv ->
 134     returnNF_Tc (TyVarTy kv)
 135 \end{code}
 136
 137
 138 %************************************************************************
 139 %*                                                                      *
 140 \subsection{Type instantiation}
 141 %*                                                                      *
 142 %************************************************************************
 143
 144 Instantiating a bunch of type variables
 145
 146 \begin{code}
 147 tcInstTyVars :: [TyVar]
 148              -> NF_TcM ([TcTyVar], [TcType], Subst)
 149
 150 tcInstTyVars tyvars
 151   = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
 152     let
 153         tys = mkTyVarTys tc_tyvars
 154     in
 155     returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
 156                 -- Since the tyvars are freshly made,
 157                 -- they cannot possibly be captured by
 158                 -- any existing for-alls.  Hence mkTopTyVarSubst
 159
 160 tcInstTyVar tyvar
 161   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 162     let
 163         name = setNameUnique (tyVarName tyvar) uniq
 164         -- Note that we don't change the print-name
 165         -- This won't confuse the type checker but there's a chance
 166         -- that two different tyvars will print the same way
 167         -- in an error message.  -dppr-debug will show up the difference
 168         -- Better watch out for this.  If worst comes to worst, just
 169         -- use mkSysLocalName.
 170     in
 171     tcNewMutTyVar name (tyVarKind tyvar)
 172
 173 tcInstSigVar tyvar      -- Very similar to tcInstTyVar
 174   = tcGetUnique         `thenNF_Tc` \ uniq ->
 175     let
 176         name = setNameUnique (tyVarName tyvar) uniq
 177         kind = tyVarKind tyvar
 178     in
 179     ASSERT( not (kind == openTypeKind) )        -- Shouldn't happen
 180     tcNewSigTyVar name kind
 181 \end{code}
 182
 183 @tcInstType@ instantiates the outer-level for-alls of a TcType with
 184 fresh type variables, splits off the dictionary part, and returns the results.
 185
 186 \begin{code}
 187 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
 188 tcInstType ty
 189   = case splitForAllTys ty of
 190         ([],     _)   -> returnNF_Tc ([], [], ty)        -- Nothing to do
 191         (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
 192                          tcSplitRhoTy (substTy tenv rho)        `thenNF_Tc` \ (theta, tau) ->
 193                          returnNF_Tc (tyvars', theta, tau)
 194 \end{code}
 195
 196
 197
 198 %************************************************************************
 199 %*                                                                      *
 200 \subsection{Putting and getting  mutable type variables}
 201 %*                                                                      *
 202 %************************************************************************
 203
 204 \begin{code}
 205 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
 206 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 207 \end{code}
 208
 209 Putting is easy:
 210
 211 \begin{code}
 212 tcPutTyVar tyvar ty
 213   | not (isMutTyVar tyvar)
 214   = pprTrace "tcPutTyVar" (ppr tyvar) $
 215     returnNF_Tc ty
 216
 217   | otherwise
 218   = ASSERT( isMutTyVar tyvar )
 219     UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
 220     tcWriteMutTyVar tyvar (Just ty)     `thenNF_Tc_`
 221     returnNF_Tc ty
 222 \end{code}
 223
 224 Getting is more interesting.  The easy thing to do is just to read, thus:
 225
 226 \begin{verbatim}
 227 tcGetTyVar tyvar = tcReadMutTyVar tyvar
 228 \end{verbatim}
 229
 230 But it's more fun to short out indirections on the way: If this
 231 version returns a TyVar, then that TyVar is unbound.  If it returns
 232 any other type, then there might be bound TyVars embedded inside it.
 233
 234 We return Nothing iff the original box was unbound.
 235
 236 \begin{code}
 237 tcGetTyVar tyvar
 238   | not (isMutTyVar tyvar)
 239   = pprTrace "tcGetTyVar" (ppr tyvar) $
 240     returnNF_Tc (Just (mkTyVarTy tyvar))
 241
 242   | otherwise
 243   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 244     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 245     case maybe_ty of
 246         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 247                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 248                    returnNF_Tc (Just ty')
 249
 250         Nothing    -> returnNF_Tc Nothing
 251
 252 short_out :: TcType -> NF_TcM TcType
 253 short_out ty@(TyVarTy tyvar)
 254   | not (isMutTyVar tyvar)
 255   = returnNF_Tc ty
 256
 257   | otherwise
 258   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 259     case maybe_ty of
 260         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 261                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 262                     returnNF_Tc ty'
 263
 264         other    -> returnNF_Tc ty
 265
 266 short_out other_ty = returnNF_Tc other_ty
 267 \end{code}
 268
 269
 270 %************************************************************************
 271 %*                                                                      *
 272 \subsection{Zonking -- the exernal interfaces}
 273 %*                                                                      *
 274 %************************************************************************
 275
 276 -----------------  Type variables
 277
 278 \begin{code}
 279 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 280 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 281
 282 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
 283 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars  `thenNF_Tc` \ tys ->
 284                            returnNF_Tc (tyVarsOfTypes tys)
 285
 286 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 287 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 288
 289 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
 290 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
 291 -- Usually this job is done by checkSigTyVars, but in a couple of places
 292 -- that is overkill, so we use this simpler chap
 293 zonkTcSigTyVars tyvars
 294   = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
 295     returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
 296 \end{code}
 297
 298 -----------------  Types
 299
 300 \begin{code}
 301 zonkTcType :: TcType -> NF_TcM TcType
 302 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 303
 304 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
 305 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 306
 307 zonkTcClassConstraints cts = mapNF_Tc zonk cts
 308     where zonk (clas, tys)
 309             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
 310               returnNF_Tc (clas, new_tys)
 311
 312 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
 313 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
 314
 315 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
 316 zonkTcPredType (Class c ts) =
 317     zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 318     returnNF_Tc (Class c new_ts)
 319 zonkTcPredType (IParam n t) =
 320     zonkTcType t        `thenNF_Tc` \ new_t ->
 321     returnNF_Tc (IParam n new_t)
 322 \end{code}
 323
 324 -------------------  These ...ToType, ...ToKind versions
 325                      are used at the end of type checking
 326
 327 \begin{code}
 328 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
 329 zonkKindEnv pairs
 330   = mapNF_Tc zonk_it pairs
 331  where
 332     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
 333                               returnNF_Tc (name, kind)
 334
 335         -- When zonking a kind, we want to
 336         --      zonk a *kind* variable to (Type *)
 337         --      zonk a *boxity* variable to *
 338     zonk_unbound_kind_var kv | tyVarKind kv == superKind   = tcPutTyVar kv liftedTypeKind
 339                              | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
 340                              | otherwise                   = pprPanic "zonkKindEnv" (ppr kv)
 341
 342 zonkTcTypeToType :: TcType -> NF_TcM Type
 343 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 344   where
 345         -- Zonk a mutable but unbound type variable to
 346         --      Void            if it has kind Lifted
 347         --      :Void           otherwise
 348     zonk_unbound_tyvar tv
 349         | kind == liftedTypeKind || kind == openTypeKind
 350         = tcPutTyVar tv voidTy  -- Just to avoid creating a new tycon in
 351                                 -- this vastly common case
 352         | otherwise
 353         = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 354         where
 355           kind = tyVarKind tv
 356
 357     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 358                                 -- type variable tv.  Same name too, apart from
 359                                 -- making it start with a colon (sigh)
 360                 -- I dread to think what will happen if this gets out into an
 361                 -- interface file.  Catastrophe likely.  Major sigh.
 362         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
 363           mkPrimTyCon tc_name kind 0 [] VoidRep
 364         where
 365           tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 366
 367 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 368 -- of a type variable, at the *end* of type checking.  It changes
 369 -- the *mutable* type variable into an *immutable* one.
 370 --
 371 -- It does this by making an immutable version of tv and binds tv to it.
 372 -- Now any bound occurences of the original type variable will get
 373 -- zonked to the immutable version.
 374
 375 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 376 zonkTcTyVarToTyVar tv
 377   = let
 378                 -- Make an immutable version, defaulting
 379                 -- the kind to lifted if necessary
 380         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 381         immut_tv_ty = mkTyVarTy immut_tv
 382
 383         zap tv = tcPutTyVar tv immut_tv_ty
 384                 -- Bind the mutable version to the immutable one
 385     in
 386         -- If the type variable is mutable, then bind it to immut_tv_ty
 387         -- so that all other occurrences of the tyvar will get zapped too
 388     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 389
 390     WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 391
 392     returnNF_Tc immut_tv
 393 \end{code}
 394
 395
 396 %************************************************************************
 397 %*                                                                      *
 398 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 399 %*                                                                      *
 400 %*              For internal use only!                                  *
 401 %*                                                                      *
 402 %************************************************************************
 403
 404 \begin{code}
 405 -- zonkType is used for Kinds as well
 406
 407 -- For unbound, mutable tyvars, zonkType uses the function given to it
 408 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 409 --      type variable and zonks the kind too
 410
 411 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 412                                         -- see zonkTcType, and zonkTcTypeToType
 413          -> TcType
 414          -> NF_TcM Type
 415 zonkType unbound_var_fn ty
 416   = go ty
 417   where
 418     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 419                                     returnNF_Tc (TyConApp tycon tys')
 420
 421     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 422                                     go ty2              `thenNF_Tc` \ ty2' ->
 423                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 424
 425     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 426
 427     go (PredTy p)                 = go_pred p           `thenNF_Tc` \ p' ->
 428                                     returnNF_Tc (PredTy p')
 429
 430     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 431                                     go res              `thenNF_Tc` \ res' ->
 432                                     returnNF_Tc (FunTy arg' res')
 433
 434     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 435                                     go arg              `thenNF_Tc` \ arg' ->
 436                                     returnNF_Tc (mkAppTy fun' arg')
 437
 438     go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
 439                                     go ty               `thenNF_Tc` \ ty' ->
 440                                     returnNF_Tc (mkUTy u' ty')
 441
 442         -- The two interesting cases!
 443     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 444
 445     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 446                              go ty                      `thenNF_Tc` \ ty' ->
 447                              returnNF_Tc (ForAllTy tyvar' ty')
 448
 449     go_pred (Class c tys) = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 450                             returnNF_Tc (Class c tys')
 451     go_pred (IParam n ty) = go ty               `thenNF_Tc` \ ty' ->
 452                             returnNF_Tc (IParam n ty')
 453
 454 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 455           -> TcTyVar -> NF_TcM TcType
 456 zonkTyVar unbound_var_fn tyvar
 457   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 458                                 -- zonking a forall type, when the bound type variable
 459                                 -- needn't be mutable
 460   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 461     returnNF_Tc (TyVarTy tyvar)
 462
 463   | otherwise
 464   =  tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 465      case maybe_ty of
 466           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 467           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 468 \end{code}
 469