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