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