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   newTyVarTy_OpenKind,  -- NF_TcM s TcType
  16   newOpenTypeKind,      -- NF_TcM s TcKind
  17
  18   -----------------------------------------
  19   TcType, TcTauType, TcThetaType, TcRhoType,
  20
  21         -- Find the type to which a type variable is bound
  22   tcPutTyVar,           -- :: TcTyVar -> TcType -> NF_TcM TcType
  23   tcGetTyVar,           -- :: TcTyVar -> NF_TcM (Maybe TcType)  does shorting out
  24
  25
  26   tcSplitRhoTy,
  27
  28   tcInstTyVars,
  29   tcInstTcType,
  30
  31   typeToTcType,
  32
  33   tcTypeKind,           -- :: TcType -> NF_TcM s TcKind
  34   --------------------------------
  35   TcKind,
  36   newKindVar, newKindVars,
  37   kindToTcKind,
  38   zonkTcKind,
  39
  40   --------------------------------
  41   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
  42   zonkTcType, zonkTcTypes, zonkTcThetaType,
  43
  44   zonkTcTypeToType, zonkTcTyVarToTyVar,
  45   zonkTcKindToKind
  46
  47   ) where
  48
  49 #include "HsVersions.h"
  50
  51
  52 -- friends:
  53 import PprType          ( pprType )
  54 import Type             ( Type(..), Kind, ThetaType, TyNote(..),
  55                           mkAppTy, mkTyConApp,
  56                           splitDictTy_maybe, splitForAllTys,
  57                           isTyVarTy, mkTyVarTy, mkTyVarTys,
  58                           fullSubstTy, substTopTy,
  59                           typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
  60                         )
  61 import TyCon            ( tyConKind, mkPrimTyCon )
  62 import PrimRep          ( PrimRep(VoidRep) )
  63 import VarEnv
  64 import VarSet           ( emptyVarSet )
  65 import Var              ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
  66
  67 -- others:
  68 import TcMonad
  69 import TysWiredIn       ( voidTy )
  70
  71 import Name             ( NamedThing(..), setNameUnique, mkSysLocalName,
  72                           mkDerivedName, mkDerivedTyConOcc
  73                         )
  74 import Unique           ( Unique, Uniquable(..) )
  75 import Util             ( nOfThem )
  76 import Outputable
  77 \end{code}
  78
  79
  80
  81 Coercions
  82 ~~~~~~~~~~
  83 Type definitions are in TcMonad.lhs
  84
  85 \begin{code}
  86 typeToTcType :: Type -> TcType
  87 typeToTcType ty =  ty
  88
  89 kindToTcKind :: Kind -> TcKind
  90 kindToTcKind kind = kind
  91 \end{code}
  92
  93 Utility functions
  94 ~~~~~~~~~~~~~~~~~
  95 These tcSplit functions are like their non-Tc analogues, but they
  96 follow through bound type variables.
  97
  98 No need for tcSplitForAllTy because a type variable can't be instantiated
  99 to a for-all type.
 100
 101 \begin{code}
 102 tcSplitRhoTy :: TcType -> NF_TcM s (TcThetaType, TcType)
 103 tcSplitRhoTy t
 104   = go t t []
 105  where
 106         -- A type variable is never instantiated to a dictionary type,
 107         -- so we don't need to do a tcReadVar on the "arg".
 108     go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
 109                                         Just pair -> go res res (pair:ts)
 110                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
 111     go syn_t (NoteTy _ t)    ts = go syn_t t ts
 112     go syn_t (TyVarTy tv)    ts = tcGetTyVar tv         `thenNF_Tc` \ maybe_ty ->
 113                                   case maybe_ty of
 114                                     Just ty | not (isTyVarTy ty) -> go syn_t ty ts
 115                                     other                        -> returnNF_Tc (reverse ts, syn_t)
 116     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
 117 \end{code}
 118
 119
 120 %************************************************************************
 121 %*                                                                      *
 122 \subsection{New type variables}
 123 %*                                                                      *
 124 %************************************************************************
 125
 126 \begin{code}
 127 newTyVar :: Kind -> NF_TcM s TcTyVar
 128 newTyVar kind
 129   = tcGetUnique         `thenNF_Tc` \ uniq ->
 130     tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
 131
 132 newTyVarTy  :: Kind -> NF_TcM s TcType
 133 newTyVarTy kind
 134   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
 135     returnNF_Tc (TyVarTy tc_tyvar)
 136
 137 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType]
 138 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 139
 140 newKindVar :: NF_TcM s TcKind
 141 newKindVar
 142   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 143     tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind     `thenNF_Tc` \ kv ->
 144     returnNF_Tc (TyVarTy kv)
 145
 146 newKindVars :: Int -> NF_TcM s [TcKind]
 147 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 148
 149 -- Returns a type variable of kind (Type bv) where bv is a new boxity var
 150 -- Used when you need a type variable that's definitely a , but you don't know
 151 -- what kind of type (boxed or unboxed).
 152 newTyVarTy_OpenKind :: NF_TcM s TcType
 153 newTyVarTy_OpenKind = newOpenTypeKind   `thenNF_Tc` \ kind ->
 154                       newTyVarTy kind
 155
 156 newOpenTypeKind :: NF_TcM s TcKind
 157 newOpenTypeKind = newTyVarTy superBoxity        `thenNF_Tc` \ bv ->
 158                   returnNF_Tc (mkTyConApp typeCon [bv])
 159 \end{code}
 160
 161
 162 %************************************************************************
 163 %*                                                                      *
 164 \subsection{Type instantiation}
 165 %*                                                                      *
 166 %************************************************************************
 167
 168 Instantiating a bunch of type variables
 169
 170 \begin{code}
 171 tcInstTyVars :: [TyVar]
 172              -> NF_TcM s ([TcTyVar], [TcType], TyVarEnv TcType)
 173
 174 tcInstTyVars tyvars
 175   = mapNF_Tc inst_tyvar tyvars  `thenNF_Tc` \ tc_tyvars ->
 176     let
 177         tys = mkTyVarTys tc_tyvars
 178     in
 179     returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
 180
 181 inst_tyvar tyvar        -- Could use the name from the tyvar?
 182   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 183     let
 184         kind = tyVarKind tyvar
 185         name = setNameUnique (tyVarName tyvar) uniq
 186         -- Note that we don't change the print-name
 187         -- This won't confuse the type checker but there's a chance
 188         -- that two different tyvars will print the same way
 189         -- in an error message.  -dppr-debug will show up the difference
 190         -- Better watch out for this.  If worst comes to worst, just
 191         -- use mkSysLocalName.
 192     in
 193     tcNewMutTyVar name kind
 194 \end{code}
 195
 196 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
 197 fresh type variables, returning them and the instantiated body of the for-all.
 198
 199 \begin{code}
 200 tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
 201 tcInstTcType ty
 202   = case splitForAllTys ty of
 203         ([], _)       -> returnNF_Tc ([], ty)   -- Nothing to do
 204         (tyvars, rho) -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 205                          returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
 206                                         -- Since the tyvars are freshly made,
 207                                         -- they cannot possibly be captured by
 208                                         -- any existing for-alls.  Hence emptyVarSet
 209 \end{code}
 210
 211
 212
 213 %************************************************************************
 214 %*                                                                      *
 215 \subsection{Putting and getting  mutable type variables}
 216 %*                                                                      *
 217 %************************************************************************
 218
 219 \begin{code}
 220 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
 221 tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
 222 \end{code}
 223
 224 Putting is easy:
 225
 226 \begin{code}
 227 tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty)   `thenNF_Tc_`
 228                       returnNF_Tc ty
 229 \end{code}
 230
 231 Getting is more interesting.  The easy thing to do is just to read, thus:
 232
 233 \begin{verbatim}
 234 tcGetTyVar tyvar = tcReadMutTyVar tyvar
 235 \end{verbatim}
 236
 237 But it's more fun to short out indirections on the way: If this
 238 version returns a TyVar, then that TyVar is unbound.  If it returns
 239 any other type, then there might be bound TyVars embedded inside it.
 240
 241 We return Nothing iff the original box was unbound.
 242
 243 \begin{code}
 244 tcGetTyVar tyvar
 245   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 246     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 247     case maybe_ty of
 248         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 249                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 250                    returnNF_Tc (Just ty')
 251
 252         Nothing    -> returnNF_Tc Nothing
 253
 254 short_out :: TcType -> NF_TcM s TcType
 255 short_out ty@(TyVarTy tyvar)
 256   | not (isMutTyVar tyvar)
 257   = returnNF_Tc ty
 258
 259   | otherwise
 260   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 261     case maybe_ty of
 262         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 263                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 264                     returnNF_Tc ty'
 265
 266         other    -> returnNF_Tc ty
 267
 268 short_out other_ty = returnNF_Tc other_ty
 269 \end{code}
 270
 271
 272 %************************************************************************
 273 %*                                                                      *
 274 \subsection{Zonking -- the exernal interfaces}
 275 %*                                                                      *
 276 %************************************************************************
 277
 278 -----------------  Type variables
 279
 280 \begin{code}
 281 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
 282 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 283
 284 zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
 285 zonkTcTyVarBndr tyvar
 286   = zonkTcTyVar tyvar   `thenNF_Tc` \ (TyVarTy tyvar') ->
 287     returnNF_Tc tyvar'
 288
 289 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
 290 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 291 \end{code}
 292
 293 -----------------  Types
 294
 295 \begin{code}
 296 zonkTcType :: TcType -> NF_TcM s TcType
 297 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 298
 299 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
 300 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 301
 302 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
 303 zonkTcThetaType theta = mapNF_Tc zonk theta
 304                     where
 305                         zonk (c,ts) = zonkTcTypes ts    `thenNF_Tc` \ new_ts ->
 306                                       returnNF_Tc (c, new_ts)
 307
 308 zonkTcKind :: TcKind -> NF_TcM s TcKind
 309 zonkTcKind = zonkTcType
 310 \end{code}
 311
 312 -------------------  These ...ToType, ...ToKind versions
 313                      are used at the end of type checking
 314
 315 \begin{code}
 316 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
 317 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
 318   where
 319         -- Zonk a mutable but unbound kind variable to
 320         --      (Type Boxed)    if it has kind superKind
 321         --      Boxed           if it has kind superBoxity
 322     zonk_unbound_kind_var kv
 323         | super_kind == superKind = tcPutTyVar kv boxedTypeKind
 324         | otherwise               = ASSERT( super_kind == superBoxity )
 325                                     tcPutTyVar kv boxedKind
 326         where
 327           super_kind = tyVarKind kv
 328
 329
 330 zonkTcTypeToType :: TcType -> NF_TcM s Type
 331 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 332   where
 333         -- Zonk a mutable but unbound type variable to
 334         --      Void            if it has kind (Type Boxed)
 335         --      Voidxxx         otherwise
 336     zonk_unbound_tyvar tv
 337         = zonkTcKindToKind (tyVarKind tv)       `thenNF_Tc` \ kind ->
 338           if kind == boxedTypeKind then
 339                 tcPutTyVar tv voidTy    -- Just to avoid creating a new tycon in
 340                                         -- this vastly common case
 341           else
 342                 tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 343
 344     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 345                                 -- type variable tv.  Same name too, apart from
 346                                 -- making it start with a colon (sigh)
 347         = mkPrimTyCon tc_name kind 0 VoidRep
 348         where
 349           tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
 350
 351 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 352 -- of a type variable, at the *end* of type checking.
 353 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
 354 -- zonks its kind, and then makes 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 s TyVar
 359 zonkTcTyVarToTyVar tv
 360   = zonkTcKindToKind (tyVarKind tv)     `thenNF_Tc` \ kind ->
 361     let
 362                 -- Make an immutable version
 363         immut_tv    = mkTyVar (tyVarName tv) kind
 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     ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 373
 374     returnNF_Tc immut_tv
 375 \end{code}
 376
 377
 378 %************************************************************************
 379 %*                                                                      *
 380 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 381 %*                                                                      *
 382 %*              For internal use only!                                  *
 383 %*                                                                      *
 384 %************************************************************************
 385
 386 \begin{code}
 387 -- zonkType is used for Kinds as well
 388
 389 -- For unbound, mutable tyvars, zonkType uses the function given to it
 390 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 391 --      type variable and zonks the kind too
 392
 393 zonkType :: (TcTyVar -> NF_TcM s Type)  -- What to do with unbound mutable type variables
 394                                         -- see zonkTcType, and zonkTcTypeToType
 395          -> TcType
 396          -> NF_TcM s Type
 397 zonkType unbound_var_fn ty
 398   = go ty
 399   where
 400     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 401                                     returnNF_Tc (TyConApp tycon tys')
 402
 403     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 404                                     go ty2              `thenNF_Tc` \ ty2' ->
 405                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 406
 407     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 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         -- The two interesting cases!
 418     go (TyVarTy tyvar)            = zonkTyVar unbound_var_fn tyvar
 419
 420     go (ForAllTy tyvar ty)
 421         = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
 422           go ty                         `thenNF_Tc` \ ty' ->
 423           returnNF_Tc (ForAllTy tyvar' ty')
 424
 425
 426 zonkTyVar :: (TcTyVar -> NF_TcM s Type)         -- What to do for an unbound mutable variable
 427           -> TcTyVar -> NF_TcM s TcType
 428 zonkTyVar unbound_var_fn tyvar
 429   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 430                                 -- zonking a forall type, when the bound type variable
 431                                 -- needn't be mutable
 432   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 433     returnNF_Tc (TyVarTy tyvar)
 434
 435   | otherwise
 436   =  tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 437      case maybe_ty of
 438           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 439           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 440 \end{code}
 441
 442 %************************************************************************
 443 %*                                                                      *
 444 \subsection{tcTypeKind}
 445 %*                                                                      *
 446 %************************************************************************
 447
 448 Sadly, we need a Tc version of typeKind, that looks though mutable
 449 kind variables.  See the notes with Type.typeKind for the typeKindF nonsense
 450
 451 This is pretty gruesome.
 452
 453 \begin{code}
 454 tcTypeKind :: TcType -> NF_TcM s TcKind
 455
 456 tcTypeKind (TyVarTy tyvar)      = returnNF_Tc (tyVarKind tyvar)
 457 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
 458 tcTypeKind (NoteTy _ ty)        = tcTypeKind ty
 459 tcTypeKind (AppTy fun arg)      = tcTypeKind fun        `thenNF_Tc` \ fun_kind ->
 460                                   tcFunResultTy fun_kind
 461 tcTypeKind (FunTy fun arg)      = tcTypeKindF arg
 462 tcTypeKind (ForAllTy _ ty)      = tcTypeKindF ty
 463
 464 tcTypeKindF :: TcType -> NF_TcM s TcKind
 465 tcTypeKindF (NoteTy _ ty)   = tcTypeKindF ty
 466 tcTypeKindF (FunTy _ ty)    = tcTypeKindF ty
 467 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
 468 tcTypeKindF other           = tcTypeKind other  `thenNF_Tc` \ kind ->
 469                               fix_up kind
 470   where
 471     fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
 472                 -- Functions at the type level are always boxed
 473     fix_up (NoteTy _ kind)   = fix_up kind
 474     fix_up kind@(TyVarTy tv) = tcGetTyVar tv    `thenNF_Tc` \ maybe_ty ->
 475                                case maybe_ty of
 476                                   Just kind' -> fix_up kind'
 477                                   Nothing  -> returnNF_Tc kind
 478     fix_up kind              = returnNF_Tc kind
 479
 480 tcFunResultTy (NoteTy _ ty)   = tcFunResultTy ty
 481 tcFunResultTy (FunTy arg res) = returnNF_Tc res
 482 tcFunResultTy (TyVarTy tv)    = tcGetTyVar tv   `thenNF_Tc` \ maybe_ty ->
 483                                 case maybe_ty of
 484                                   Just ty' -> tcFunResultTy ty'
 485         -- The Nothing case, and the other cases for tcFunResultTy
 486         -- should never happen... pattern match failure
 487 \end{code}