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