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, isNotUsgTy,
  58                           isTyVarTy, mkTyVarTy, mkTyVarTys,
  59                           typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
  60                         )
  61 import Subst            ( Subst, mkTopTyVarSubst, substTy )
  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], Subst)
 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, mkTopTyVarSubst tyvars tys)
 181                 -- Since the tyvars are freshly made,
 182                 -- they cannot possibly be captured by
 183                 -- any existing for-alls.  Hence mkTopTyVarSubst
 184
 185 tcInstTyVar tyvar
 186   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 187     let
 188         name = setNameUnique (tyVarName tyvar) uniq
 189         -- Note that we don't change the print-name
 190         -- This won't confuse the type checker but there's a chance
 191         -- that two different tyvars will print the same way
 192         -- in an error message.  -dppr-debug will show up the difference
 193         -- Better watch out for this.  If worst comes to worst, just
 194         -- use mkSysLocalName.
 195
 196         kind = tyVarKind tyvar
 197     in
 198
 199         -- Hack alert!  Certain system functions (like error) are quantified
 200         -- over type variables with an 'open' kind (a :: ?).  When we instantiate
 201         -- these tyvars we want to make a type variable whose kind is (Type bv)
 202         -- where bv is a boxity variable.  This makes sure it's a type, but
 203         -- is open about its boxity.  We *don't* want to give the thing the
 204         -- kind '?' (= Type AnyBox).
 205         --
 206         -- This is all a hack to avoid giving error it's "proper" type:
 207         --       error :: forall bv. forall a::Type bv. String -> a
 208
 209     (if kind == openTypeKind then
 210         newOpenTypeKind
 211      else
 212         returnNF_Tc kind)       `thenNF_Tc` \ kind' ->
 213
 214     tcNewMutTyVar name kind'
 215
 216 tcInstSigVar tyvar      -- Very similar to tcInstTyVar
 217   = tcGetUnique         `thenNF_Tc` \ uniq ->
 218     let
 219         name = setNameUnique (tyVarName tyvar) uniq
 220         kind = tyVarKind tyvar
 221     in
 222     ASSERT( not (kind == openTypeKind) )        -- Shouldn't happen
 223     tcNewSigTyVar name kind
 224 \end{code}
 225
 226 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
 227 fresh type variables, returning them and the instantiated body of the for-all.
 228
 229 \begin{code}
 230 tcInstTcType :: TcType -> NF_TcM s ([TcTyVar], TcType)
 231 tcInstTcType ty
 232   = case splitForAllTys ty of
 233         ([], _)       -> returnNF_Tc ([], ty)   -- Nothing to do
 234         (tyvars, rho) -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 235                          returnNF_Tc (tyvars', substTy tenv rho)
 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 (NoteTy (UsgNote usg) ty2) = go ty2              `thenNF_Tc` \ ty2' ->
 437                                     returnNF_Tc (NoteTy (UsgNote usg) ty2')
 438
 439     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 440                                     go res              `thenNF_Tc` \ res' ->
 441                                     returnNF_Tc (FunTy arg' res')
 442
 443     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 444                                     go arg              `thenNF_Tc` \ arg' ->
 445                                     returnNF_Tc (mkAppTy fun' arg')
 446
 447         -- The two interesting cases!
 448     go (TyVarTy tyvar)            = zonkTyVar unbound_var_fn tyvar
 449
 450     go (ForAllTy tyvar ty)
 451         = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
 452           go ty                         `thenNF_Tc` \ ty' ->
 453           returnNF_Tc (ForAllTy tyvar' ty')
 454
 455
 456 zonkTyVar :: (TcTyVar -> NF_TcM s Type)         -- What to do for an unbound mutable variable
 457           -> TcTyVar -> NF_TcM s TcType
 458 zonkTyVar unbound_var_fn tyvar
 459   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 460                                 -- zonking a forall type, when the bound type variable
 461                                 -- needn't be mutable
 462   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 463     returnNF_Tc (TyVarTy tyvar)
 464
 465   | otherwise
 466   =  tcGetTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 467      case maybe_ty of
 468           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 469           Just other_ty -> ASSERT( isNotUsgTy other_ty )
 470                            zonkType unbound_var_fn other_ty     -- Bound
 471 \end{code}
 472
 473 %************************************************************************
 474 %*                                                                      *
 475 \subsection{tcTypeKind}
 476 %*                                                                      *
 477 %************************************************************************
 478
 479 Sadly, we need a Tc version of typeKind, that looks though mutable
 480 kind variables.  See the notes with Type.typeKind for the typeKindF nonsense
 481
 482 This is pretty gruesome.
 483
 484 \begin{code}
 485 tcTypeKind :: TcType -> NF_TcM s TcKind
 486
 487 tcTypeKind (TyVarTy tyvar)      = returnNF_Tc (tyVarKind tyvar)
 488 tcTypeKind (TyConApp tycon tys) = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
 489 tcTypeKind (NoteTy _ ty)        = tcTypeKind ty
 490 tcTypeKind (AppTy fun arg)      = tcTypeKind fun        `thenNF_Tc` \ fun_kind ->
 491                                   tcFunResultTy fun_kind
 492 tcTypeKind (FunTy fun arg)      = tcTypeKindF arg
 493 tcTypeKind (ForAllTy _ ty)      = tcTypeKindF ty
 494
 495 tcTypeKindF :: TcType -> NF_TcM s TcKind
 496 tcTypeKindF (NoteTy _ ty)   = tcTypeKindF ty
 497 tcTypeKindF (FunTy _ ty)    = tcTypeKindF ty
 498 tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
 499 tcTypeKindF other           = tcTypeKind other  `thenNF_Tc` \ kind ->
 500                               fix_up kind
 501   where
 502     fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
 503                 -- Functions at the type level are always boxed
 504     fix_up (NoteTy _ kind)   = fix_up kind
 505     fix_up kind@(TyVarTy tv) = tcGetTyVar tv    `thenNF_Tc` \ maybe_ty ->
 506                                case maybe_ty of
 507                                   Just kind' -> fix_up kind'
 508                                   Nothing  -> returnNF_Tc kind
 509     fix_up kind              = returnNF_Tc kind
 510
 511 tcFunResultTy (NoteTy _ ty)   = tcFunResultTy ty
 512 tcFunResultTy (FunTy arg res) = returnNF_Tc res
 513 tcFunResultTy (TyVarTy tv)    = tcGetTyVar tv   `thenNF_Tc` \ maybe_ty ->
 514                                 case maybe_ty of
 515                                   Just ty' -> tcFunResultTy ty'
 516         -- The Nothing case, and the other cases for tcFunResultTy
 517         -- should never happen... pattern match failure
 518 \end{code}