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         name = setNameUnique (tyVarName tyvar) uniq
 185         -- Note that we don't change the print-name
 186         -- This won't confuse the type checker but there's a chance
 187         -- that two different tyvars will print the same way
 188         -- in an error message.  -dppr-debug will show up the difference
 189         -- Better watch out for this.  If worst comes to worst, just
 190         -- use mkSysLocalName.
 191
 192         kind = tyVarKind tyvar
 193     in
 194
 195         -- Hack alert!  Certain system functions (like error) are quantified
 196         -- over type variables with an 'open' kind (a :: ?).  When we instantiate
 197         -- these tyvars we want to make a type variable whose kind is (Type bv)
 198         -- where bv is a boxity variable.  This makes sure it's a type, but
 199         -- is open about its boxity.  We *don't* want to give the thing the
 200         -- kind '?' (= Type AnyBox).
 201         --
 202         -- This is all a hack to avoid giving error it's "proper" type:
 203         --       error :: forall bv. forall a::Type bv. String -> a
 204
 205     (if kind == openTypeKind then
 206         newOpenTypeKind
 207      else
 208         returnNF_Tc kind)       `thenNF_Tc` \ kind' ->
 209
 210     tcNewMutTyVar name kind'
 211 \end{code}
 212
 213 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
 214 fresh type variables, returning them and the instantiated body of the for-all.
 215
 216 \begin{code}
 217 tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
 218 tcInstTcType ty
 219   = case splitForAllTys ty of
 220         ([], _)       -> returnNF_Tc ([], ty)   -- Nothing to do
 221         (tyvars, rho) -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 222                          returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
 223                                         -- Since the tyvars are freshly made,
 224                                         -- they cannot possibly be captured by
 225                                         -- any existing for-alls.  Hence emptyVarSet
 226 \end{code}
 227
 228
 229
 230 %************************************************************************
 231 %*                                                                      *
 232 \subsection{Putting and getting  mutable type variables}
 233 %*                                                                      *
 234 %************************************************************************
 235
 236 \begin{code}
 237 tcPutTyVar :: TcTyVar -> TcType -> NF_TcM s TcType
 238 tcGetTyVar :: TcTyVar -> NF_TcM s (Maybe TcType)
 239 \end{code}
 240
 241 Putting is easy:
 242
 243 \begin{code}
 244 tcPutTyVar tyvar ty = tcWriteMutTyVar tyvar (Just ty)   `thenNF_Tc_`
 245                       returnNF_Tc ty
 246 \end{code}
 247
 248 Getting is more interesting.  The easy thing to do is just to read, thus:
 249
 250 \begin{verbatim}
 251 tcGetTyVar tyvar = tcReadMutTyVar tyvar
 252 \end{verbatim}
 253
 254 But it's more fun to short out indirections on the way: If this
 255 version returns a TyVar, then that TyVar is unbound.  If it returns
 256 any other type, then there might be bound TyVars embedded inside it.
 257
 258 We return Nothing iff the original box was unbound.
 259
 260 \begin{code}
 261 tcGetTyVar tyvar
 262   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 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 (Just ty')
 268
 269         Nothing    -> returnNF_Tc Nothing
 270
 271 short_out :: TcType -> NF_TcM s TcType
 272 short_out ty@(TyVarTy tyvar)
 273   | not (isMutTyVar tyvar)
 274   = returnNF_Tc ty
 275
 276   | otherwise
 277   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 278     case maybe_ty of
 279         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 280                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 281                     returnNF_Tc ty'
 282
 283         other    -> returnNF_Tc ty
 284
 285 short_out other_ty = returnNF_Tc other_ty
 286 \end{code}
 287
 288
 289 %************************************************************************
 290 %*                                                                      *
 291 \subsection{Zonking -- the exernal interfaces}
 292 %*                                                                      *
 293 %************************************************************************
 294
 295 -----------------  Type variables
 296
 297 \begin{code}
 298 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
 299 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 300
 301 zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
 302 zonkTcTyVarBndr tyvar
 303   = zonkTcTyVar tyvar   `thenNF_Tc` \ (TyVarTy tyvar') ->
 304     returnNF_Tc tyvar'
 305
 306 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
 307 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 308 \end{code}
 309
 310 -----------------  Types
 311
 312 \begin{code}
 313 zonkTcType :: TcType -> NF_TcM s TcType
 314 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 315
 316 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
 317 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 318
 319 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
 320 zonkTcThetaType theta = mapNF_Tc zonk theta
 321                     where
 322                         zonk (c,ts) = zonkTcTypes ts    `thenNF_Tc` \ new_ts ->
 323                                       returnNF_Tc (c, new_ts)
 324
 325 zonkTcKind :: TcKind -> NF_TcM s TcKind
 326 zonkTcKind = zonkTcType
 327 \end{code}
 328
 329 -------------------  These ...ToType, ...ToKind versions
 330                      are used at the end of type checking
 331
 332 \begin{code}
 333 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
 334 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
 335   where
 336         -- Zonk a mutable but unbound kind variable to
 337         --      (Type Boxed)    if it has kind superKind
 338         --      Boxed           if it has kind superBoxity
 339     zonk_unbound_kind_var kv
 340         | super_kind == superKind = tcPutTyVar kv boxedTypeKind
 341         | otherwise               = ASSERT( super_kind == superBoxity )
 342                                     tcPutTyVar kv boxedKind
 343         where
 344           super_kind = tyVarKind kv
 345
 346
 347 zonkTcTypeToType :: TcType -> NF_TcM s 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 (Type Boxed)
 352         --      Voidxxx         otherwise
 353     zonk_unbound_tyvar tv
 354         = zonkTcKindToKind (tyVarKind tv)       `thenNF_Tc` \ kind ->
 355           if kind == boxedTypeKind then
 356                 tcPutTyVar tv voidTy    -- Just to avoid creating a new tycon in
 357                                         -- this vastly common case
 358           else
 359                 tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 360
 361     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 362                                 -- type variable tv.  Same name too, apart from
 363                                 -- making it start with a colon (sigh)
 364         = mkPrimTyCon tc_name kind 0 VoidRep
 365         where
 366           tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
 367
 368 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 369 -- of a type variable, at the *end* of type checking.
 370 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
 371 -- zonks its kind, and then makes an immutable version of tv and binds tv to it.
 372 -- Now any bound occurences of the original type variable will get
 373 -- zonked to the immutable version.
 374
 375 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
 376 zonkTcTyVarToTyVar tv
 377   = zonkTcKindToKind (tyVarKind tv)     `thenNF_Tc` \ kind ->
 378     let
 379                 -- Make an immutable version
 380         immut_tv    = mkTyVar (tyVarName tv) kind
 381         immut_tv_ty = mkTyVarTy immut_tv
 382
 383         zap tv = tcPutTyVar tv immut_tv_ty
 384                 -- Bind the mutable version to the immutable one
 385     in
 386         -- If the type variable is mutable, then bind it to immut_tv_ty
 387         -- so that all other occurrences of the tyvar will get zapped too
 388     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 389     ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 390
 391     returnNF_Tc immut_tv
 392 \end{code}
 393
 394
 395 %************************************************************************
 396 %*                                                                      *
 397 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 398 %*                                                                      *
 399 %*              For internal use only!                                  *
 400 %*                                                                      *
 401 %************************************************************************
 402
 403 \begin{code}
 404 -- zonkType is used for Kinds as well
 405
 406 -- For unbound, mutable tyvars, zonkType uses the function given to it
 407 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 408 --      type variable and zonks the kind too
 409
 410 zonkType :: (TcTyVar -> NF_TcM s Type)  -- What to do with unbound mutable type variables
 411                                         -- see zonkTcType, and zonkTcTypeToType
 412          -> TcType
 413          -> NF_TcM s Type
 414 zonkType unbound_var_fn ty
 415   = go ty
 416   where
 417     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 418                                     returnNF_Tc (TyConApp tycon tys')
 419
 420     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 421                                     go ty2              `thenNF_Tc` \ ty2' ->
 422                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 423
 424     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 425
 426     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 427                                     go res              `thenNF_Tc` \ res' ->
 428                                     returnNF_Tc (FunTy arg' res')
 429
 430     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 431                                     go arg              `thenNF_Tc` \ arg' ->
 432                                     returnNF_Tc (mkAppTy fun' arg')
 433
 434         -- The two interesting cases!
 435     go (TyVarTy tyvar)            = zonkTyVar unbound_var_fn tyvar
 436
 437     go (ForAllTy tyvar ty)
 438         = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
 439           go ty                         `thenNF_Tc` \ ty' ->
 440           returnNF_Tc (ForAllTy tyvar' ty')
 441
 442
 443 zonkTyVar :: (TcTyVar -> NF_TcM s Type)         -- What to do for an unbound mutable variable
 444           -> TcTyVar -> NF_TcM s TcType
 445 zonkTyVar unbound_var_fn tyvar
 446   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 447                                 -- zonking a forall type, when the bound type variable
 448                                 -- needn't be mutable
 449   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 450     returnNF_Tc (TyVarTy tyvar)
 451
 452   | otherwise
 453   =  tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 454      case maybe_ty of
 455           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 456           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 457 \end{code}
 458
 459 %************************************************************************
 460 %*                                                                      *
 461 \subsection{tcTypeKind}
 462 %*                                                                      *
 463 %************************************************************************
 464
 465 Sadly, we need a Tc version of typeKind, that looks though mutable
 466 kind variables.  See the notes with Type.typeKind for the typeKindF nonsense
 467
 468 This is pretty gruesome.
 469
 470 \begin{code}
 471 tcTypeKind :: TcType -> NF_TcM s TcKind
 472
 473 tcTypeKind (TyVarTy tyvar)      = returnNF_Tc (tyVarKind tyvar)
 474 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
 475 tcTypeKind (NoteTy _ ty)        = tcTypeKind ty
 476 tcTypeKind (AppTy fun arg)      = tcTypeKind fun        `thenNF_Tc` \ fun_kind ->
 477                                   tcFunResultTy fun_kind
 478 tcTypeKind (FunTy fun arg)      = tcTypeKindF arg
 479 tcTypeKind (ForAllTy _ ty)      = tcTypeKindF ty
 480
 481 tcTypeKindF :: TcType -> NF_TcM s TcKind
 482 tcTypeKindF (NoteTy _ ty)   = tcTypeKindF ty
 483 tcTypeKindF (FunTy _ ty)    = tcTypeKindF ty
 484 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
 485 tcTypeKindF other           = tcTypeKind other  `thenNF_Tc` \ kind ->
 486                               fix_up kind
 487   where
 488     fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
 489                 -- Functions at the type level are always boxed
 490     fix_up (NoteTy _ kind)   = fix_up kind
 491     fix_up kind@(TyVarTy tv) = tcGetTyVar tv    `thenNF_Tc` \ maybe_ty ->
 492                                case maybe_ty of
 493                                   Just kind' -> fix_up kind'
 494                                   Nothing  -> returnNF_Tc kind
 495     fix_up kind              = returnNF_Tc kind
 496
 497 tcFunResultTy (NoteTy _ ty)   = tcFunResultTy ty
 498 tcFunResultTy (FunTy arg res) = returnNF_Tc res
 499 tcFunResultTy (TyVarTy tv)    = tcGetTyVar tv   `thenNF_Tc` \ maybe_ty ->
 500                                 case maybe_ty of
 501                                   Just ty' -> tcFunResultTy ty'
 502         -- The Nothing case, and the other cases for tcFunResultTy
 503         -- should never happen... pattern match failure
 504 \end{code}