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