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