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, liftedTypeKind,
  51                           superKind, superBoxity,
  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 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
 184 fresh type variables, returning them and the instantiated body of the for-all.
 185
 186 \begin{code}
 187 tcInstTcType :: TcType -> NF_TcM ([TcTyVar], TcType)
 188 tcInstTcType ty
 189   = case splitForAllTys ty of
 190         ([], _)       -> returnNF_Tc ([], ty)   -- Nothing to do
 191         (tyvars, rho) -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 192                          returnNF_Tc (tyvars', substTy tenv rho)
 193 \end{code}
 194
 195
 196
 197 %************************************************************************
 198 %*                                                                      *
 199 \subsection{Putting and getting  mutable type variables}
 200 %*                                                                      *
 201 %************************************************************************
 202
 203 \begin{code}
 204 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM TcType
 205 tcGetTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 206 \end{code}
 207
 208 Putting is easy:
 209
 210 \begin{code}
 211 tcPutTyVar tyvar ty = UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
 212                       tcWriteMutTyVar tyvar (Just ty)   `thenNF_Tc_`
 213                       returnNF_Tc ty
 214 \end{code}
 215
 216 Getting is more interesting.  The easy thing to do is just to read, thus:
 217
 218 \begin{verbatim}
 219 tcGetTyVar tyvar = tcReadMutTyVar tyvar
 220 \end{verbatim}
 221
 222 But it's more fun to short out indirections on the way: If this
 223 version returns a TyVar, then that TyVar is unbound.  If it returns
 224 any other type, then there might be bound TyVars embedded inside it.
 225
 226 We return Nothing iff the original box was unbound.
 227
 228 \begin{code}
 229 tcGetTyVar tyvar
 230   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 231     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 232     case maybe_ty of
 233         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 234                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 235                    returnNF_Tc (Just ty')
 236
 237         Nothing    -> returnNF_Tc Nothing
 238
 239 short_out :: TcType -> NF_TcM TcType
 240 short_out ty@(TyVarTy tyvar)
 241   | not (isMutTyVar tyvar)
 242   = returnNF_Tc ty
 243
 244   | otherwise
 245   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 246     case maybe_ty of
 247         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 248                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 249                     returnNF_Tc ty'
 250
 251         other    -> returnNF_Tc ty
 252
 253 short_out other_ty = returnNF_Tc other_ty
 254 \end{code}
 255
 256
 257 %************************************************************************
 258 %*                                                                      *
 259 \subsection{Zonking -- the exernal interfaces}
 260 %*                                                                      *
 261 %************************************************************************
 262
 263 -----------------  Type variables
 264
 265 \begin{code}
 266 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 267 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 268
 269 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 270 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 271
 272 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
 273 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
 274 -- Usually this job is done by checkSigTyVars, but in a couple of places
 275 -- that is overkill, so we use this simpler chap
 276 zonkTcSigTyVars tyvars
 277   = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
 278     returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
 279 \end{code}
 280
 281 -----------------  Types
 282
 283 \begin{code}
 284 zonkTcType :: TcType -> NF_TcM TcType
 285 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 286
 287 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
 288 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 289
 290 zonkTcClassConstraints cts = mapNF_Tc zonk cts
 291     where zonk (clas, tys)
 292             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
 293               returnNF_Tc (clas, new_tys)
 294
 295 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
 296 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
 297
 298 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
 299 zonkTcPredType (Class c ts) =
 300     zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 301     returnNF_Tc (Class c new_ts)
 302 zonkTcPredType (IParam n t) =
 303     zonkTcType t        `thenNF_Tc` \ new_t ->
 304     returnNF_Tc (IParam n new_t)
 305 \end{code}
 306
 307 -------------------  These ...ToType, ...ToKind versions
 308                      are used at the end of type checking
 309
 310 \begin{code}
 311 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
 312 zonkKindEnv pairs
 313   = mapNF_Tc zonk_it pairs
 314  where
 315     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
 316                               returnNF_Tc (name, kind)
 317
 318         -- When zonking a kind, we want to
 319         --      zonk a *kind* variable to (Type *)
 320         --      zonk a *boxity* variable to *
 321     zonk_unbound_kind_var kv | tyVarKind kv == superKind   = tcPutTyVar kv liftedTypeKind
 322                              | tyVarKind kv == superBoxity = tcPutTyVar kv liftedBoxity
 323                              | otherwise                   = pprPanic "zonkKindEnv" (ppr kv)
 324
 325 zonkTcTypeToType :: TcType -> NF_TcM Type
 326 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 327   where
 328         -- Zonk a mutable but unbound type variable to
 329         --      Void            if it has kind Lifted
 330         --      :Void           otherwise
 331     zonk_unbound_tyvar tv
 332         | kind == liftedTypeKind
 333         = tcPutTyVar tv voidTy  -- Just to avoid creating a new tycon in
 334                                 -- this vastly common case
 335         | otherwise
 336         = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 337         where
 338           kind = tyVarKind tv
 339
 340     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 341                                 -- type variable tv.  Same name too, apart from
 342                                 -- making it start with a colon (sigh)
 343                 -- I dread to think what will happen if this gets out into an
 344                 -- interface file.  Catastrophe likely.  Major sigh.
 345         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
 346           mkPrimTyCon tc_name kind 0 [] VoidRep
 347         where
 348           tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 349
 350 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 351 -- of a type variable, at the *end* of type checking.  It changes
 352 -- the *mutable* type variable into an *immutable* one.
 353 --
 354 -- It does this by making an immutable version of tv and binds tv to it.
 355 -- Now any bound occurences of the original type variable will get
 356 -- zonked to the immutable version.
 357
 358 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 359 zonkTcTyVarToTyVar tv
 360   = let
 361                 -- Make an immutable version, defaulting
 362                 -- the kind to lifted if necessary
 363         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 364         immut_tv_ty = mkTyVarTy immut_tv
 365
 366         zap tv = tcPutTyVar tv immut_tv_ty
 367                 -- Bind the mutable version to the immutable one
 368     in
 369         -- If the type variable is mutable, then bind it to immut_tv_ty
 370         -- so that all other occurrences of the tyvar will get zapped too
 371     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 372
 373     WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 374
 375     returnNF_Tc immut_tv
 376 \end{code}
 377
 378
 379 %************************************************************************
 380 %*                                                                      *
 381 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 382 %*                                                                      *
 383 %*              For internal use only!                                  *
 384 %*                                                                      *
 385 %************************************************************************
 386
 387 \begin{code}
 388 -- zonkType is used for Kinds as well
 389
 390 -- For unbound, mutable tyvars, zonkType uses the function given to it
 391 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 392 --      type variable and zonks the kind too
 393
 394 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 395                                         -- see zonkTcType, and zonkTcTypeToType
 396          -> TcType
 397          -> NF_TcM Type
 398 zonkType unbound_var_fn ty
 399   = go ty
 400   where
 401     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 402                                     returnNF_Tc (TyConApp tycon tys')
 403
 404     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 405                                     go ty2              `thenNF_Tc` \ ty2' ->
 406                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 407
 408     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 409
 410     go (PredTy p)                 = go_pred p           `thenNF_Tc` \ p' ->
 411                                     returnNF_Tc (PredTy p')
 412
 413     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 414                                     go res              `thenNF_Tc` \ res' ->
 415                                     returnNF_Tc (FunTy arg' res')
 416
 417     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 418                                     go arg              `thenNF_Tc` \ arg' ->
 419                                     returnNF_Tc (mkAppTy fun' arg')
 420
 421     go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
 422                                     go ty               `thenNF_Tc` \ ty' ->
 423                                     returnNF_Tc (mkUTy u' ty')
 424
 425         -- The two interesting cases!
 426     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 427
 428     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 429                              go ty                      `thenNF_Tc` \ ty' ->
 430                              returnNF_Tc (ForAllTy tyvar' ty')
 431
 432     go_pred (Class c tys) = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 433                             returnNF_Tc (Class c tys')
 434     go_pred (IParam n ty) = go ty               `thenNF_Tc` \ ty' ->
 435                             returnNF_Tc (IParam n ty')
 436
 437 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 438           -> TcTyVar -> NF_TcM TcType
 439 zonkTyVar unbound_var_fn tyvar
 440   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 441                                 -- zonking a forall type, when the bound type variable
 442                                 -- needn't be mutable
 443   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 444     returnNF_Tc (TyVarTy tyvar)
 445
 446   | otherwise
 447   =  tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 448      case maybe_ty of
 449           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 450           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 451 \end{code}
 452