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