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` \ ty ->
 316     case ty of
 317         TyVarTy tyvar' -> returnNF_Tc tyvar'
 318         _              -> pprTrace "zonkTcTyVarBndr" (ppr tyvar <+> ppr ty) $
 319                           returnNF_Tc tyvar
 320
 321 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
 322 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 323 \end{code}
 324
 325 -----------------  Types
 326
 327 \begin{code}
 328 zonkTcType :: TcType -> NF_TcM s TcType
 329 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 330
 331 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
 332 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 333
 334 zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
 335 zonkTcThetaType theta = mapNF_Tc zonk theta
 336                     where
 337                         zonk (c,ts) = zonkTcTypes ts    `thenNF_Tc` \ new_ts ->
 338                                       returnNF_Tc (c, new_ts)
 339
 340 zonkTcKind :: TcKind -> NF_TcM s TcKind
 341 zonkTcKind = zonkTcType
 342 \end{code}
 343
 344 -------------------  These ...ToType, ...ToKind versions
 345                      are used at the end of type checking
 346
 347 \begin{code}
 348 zonkTcKindToKind :: TcKind -> NF_TcM s Kind
 349 zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
 350   where
 351         -- Zonk a mutable but unbound kind variable to
 352         --      (Type Boxed)    if it has kind superKind
 353         --      Boxed           if it has kind superBoxity
 354     zonk_unbound_kind_var kv
 355         | super_kind == superKind = tcPutTyVar kv boxedTypeKind
 356         | otherwise               = ASSERT( super_kind == superBoxity )
 357                                     tcPutTyVar kv boxedKind
 358         where
 359           super_kind = tyVarKind kv
 360
 361
 362 zonkTcTypeToType :: TcType -> NF_TcM s Type
 363 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 364   where
 365         -- Zonk a mutable but unbound type variable to
 366         --      Void            if it has kind (Type Boxed)
 367         --      Voidxxx         otherwise
 368     zonk_unbound_tyvar tv
 369         = zonkTcKindToKind (tyVarKind tv)       `thenNF_Tc` \ kind ->
 370           if kind == boxedTypeKind then
 371                 tcPutTyVar tv voidTy    -- Just to avoid creating a new tycon in
 372                                         -- this vastly common case
 373           else
 374                 tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 375
 376     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 377                                 -- type variable tv.  Same name too, apart from
 378                                 -- making it start with a colon (sigh)
 379         = mkPrimTyCon tc_name kind 0 [] VoidRep
 380         where
 381           tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
 382
 383 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 384 -- of a type variable, at the *end* of type checking.
 385 -- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
 386 -- zonks its kind, and then makes an immutable version of tv and binds tv to it.
 387 -- Now any bound occurences of the original type variable will get
 388 -- zonked to the immutable version.
 389
 390 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM s TyVar
 391 zonkTcTyVarToTyVar tv
 392   = zonkTcKindToKind (tyVarKind tv)     `thenNF_Tc` \ kind ->
 393     let
 394                 -- Make an immutable version
 395         immut_tv    = mkTyVar (tyVarName tv) kind
 396         immut_tv_ty = mkTyVarTy immut_tv
 397
 398         zap tv = tcPutTyVar tv immut_tv_ty
 399                 -- Bind the mutable version to the immutable one
 400     in
 401         -- If the type variable is mutable, then bind it to immut_tv_ty
 402         -- so that all other occurrences of the tyvar will get zapped too
 403     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 404     ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 405
 406     returnNF_Tc immut_tv
 407 \end{code}
 408
 409
 410 %************************************************************************
 411 %*                                                                      *
 412 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 413 %*                                                                      *
 414 %*              For internal use only!                                  *
 415 %*                                                                      *
 416 %************************************************************************
 417
 418 \begin{code}
 419 -- zonkType is used for Kinds as well
 420
 421 -- For unbound, mutable tyvars, zonkType uses the function given to it
 422 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 423 --      type variable and zonks the kind too
 424
 425 zonkType :: (TcTyVar -> NF_TcM s Type)  -- What to do with unbound mutable type variables
 426                                         -- see zonkTcType, and zonkTcTypeToType
 427          -> TcType
 428          -> NF_TcM s Type
 429 zonkType unbound_var_fn ty
 430   = go ty
 431   where
 432     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 433                                     returnNF_Tc (TyConApp tycon tys')
 434
 435     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 436                                     go ty2              `thenNF_Tc` \ ty2' ->
 437                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 438
 439     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 440
 441     go (NoteTy (UsgNote usg) ty2) = go ty2              `thenNF_Tc` \ ty2' ->
 442                                     returnNF_Tc (NoteTy (UsgNote usg) ty2')
 443
 444     go (NoteTy (UsgForAll uv) ty2)= go ty2              `thenNF_Tc` \ ty2' ->
 445                                     returnNF_Tc (NoteTy (UsgForAll uv) ty2')
 446
 447     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 448                                     go res              `thenNF_Tc` \ res' ->
 449                                     returnNF_Tc (FunTy arg' res')
 450
 451     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 452                                     go arg              `thenNF_Tc` \ arg' ->
 453                                     returnNF_Tc (mkAppTy fun' arg')
 454
 455         -- The two interesting cases!
 456     go (TyVarTy tyvar)            = zonkTyVar unbound_var_fn tyvar
 457
 458     go (ForAllTy tyvar ty)
 459         = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
 460           go ty                         `thenNF_Tc` \ ty' ->
 461           returnNF_Tc (ForAllTy tyvar' ty')
 462
 463
 464 zonkTyVar :: (TcTyVar -> NF_TcM s Type)         -- What to do for an unbound mutable variable
 465           -> TcTyVar -> NF_TcM s TcType
 466 zonkTyVar unbound_var_fn tyvar
 467   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 468                                 -- zonking a forall type, when the bound type variable
 469                                 -- needn't be mutable
 470   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 471     returnNF_Tc (TyVarTy tyvar)
 472
 473   | otherwise
 474   =  tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 475      case maybe_ty of
 476           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 477           Just other_ty -> ASSERT( isNotUsgTy other_ty )
 478                            zonkType unbound_var_fn other_ty     -- Bound
 479 \end{code}
 480
 481 %************************************************************************
 482 %*                                                                      *
 483 \subsection{tcTypeKind}
 484 %*                                                                      *
 485 %************************************************************************
 486
 487 Sadly, we need a Tc version of typeKind, that looks though mutable
 488 kind variables.  See the notes with Type.typeKind for the typeKindF nonsense
 489
 490 This is pretty gruesome.
 491
 492 \begin{code}
 493 tcTypeKind :: TcType -> NF_TcM s TcKind
 494
 495 tcTypeKind (TyVarTy tyvar)      = returnNF_Tc (tyVarKind tyvar)
 496 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
 497 tcTypeKind (NoteTy _ ty)        = tcTypeKind ty
 498 tcTypeKind (AppTy fun arg)      = tcTypeKind fun        `thenNF_Tc` \ fun_kind ->
 499                                   tcFunResultTy fun_kind
 500 tcTypeKind (FunTy fun arg)      = tcTypeKindF arg
 501 tcTypeKind (ForAllTy _ ty)      = tcTypeKindF ty
 502
 503 tcTypeKindF :: TcType -> NF_TcM s TcKind
 504 tcTypeKindF (NoteTy _ ty)   = tcTypeKindF ty
 505 tcTypeKindF (FunTy _ ty)    = tcTypeKindF ty
 506 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
 507 tcTypeKindF other           = tcTypeKind other  `thenNF_Tc` \ kind ->
 508                               fix_up kind
 509   where
 510     fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
 511                 -- Functions at the type level are always boxed
 512     fix_up (NoteTy _ kind)   = fix_up kind
 513     fix_up kind@(TyVarTy tv) = tcGetTyVar tv    `thenNF_Tc` \ maybe_ty ->
 514                                case maybe_ty of
 515                                   Just kind' -> fix_up kind'
 516                                   Nothing  -> returnNF_Tc kind
 517     fix_up kind              = returnNF_Tc kind
 518
 519 tcFunResultTy (NoteTy _ ty)   = tcFunResultTy ty
 520 tcFunResultTy (FunTy arg res) = returnNF_Tc res
 521 tcFunResultTy (TyVarTy tv)    = tcGetTyVar tv   `thenNF_Tc` \ maybe_ty ->
 522                                 case maybe_ty of
 523                                   Just ty' -> tcFunResultTy ty'
 524         -- The Nothing case, and the other cases for tcFunResultTy
 525         -- should never happen... pattern match failure
 526 \end{code}