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