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