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, TcBox,
  10   TcTyVarSet,
  11   newTcTyVar,
  12   newTyVarTy,   -- Kind -> NF_TcM s (TcType s)
  13   newTyVarTys,  -- Int -> Kind -> NF_TcM s [TcType s]
  14
  15   -----------------------------------------
  16   TcType, TcMaybe(..),
  17   TcTauType, TcThetaType, TcRhoType,
  18
  19         -- Find the type to which a type variable is bound
  20   tcWriteTyVar,         -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
  21   tcReadTyVar,          -- :: TcTyVar s -> NF_TcM (TcMaybe s)
  22
  23
  24   tcSplitRhoTy,
  25
  26   tcInstTyVars,
  27   tcInstTcType,
  28
  29   typeToTcType,
  30
  31   --------------------------------
  32   TcKind,
  33   newKindVar, newKindVars,
  34   kindToTcKind,
  35   zonkTcKind,
  36
  37   --------------------------------
  38   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
  39   zonkTcType, zonkTcTypes, zonkTcThetaType,
  40
  41   zonkTcTypeToType, zonkTcTyVarToTyVar,
  42   zonkTcKindToKind
  43
  44   ) where
  45
  46 #include "HsVersions.h"
  47
  48
  49 -- friends:
  50 import PprType          ()
  51 import Type             ( Type, Kind, ThetaType, GenType(..), TyNote(..),
  52                           mkAppTy,
  53                           splitDictTy_maybe, splitForAllTys,
  54                           isTyVarTy, mkTyVarTys,
  55                           fullSubstTy, substFlexiTy,
  56                           boxedTypeKind, superKind
  57                         )
  58 import VarEnv
  59 import VarSet           ( emptyVarSet )
  60 import Var              ( TyVar, GenTyVar, tyVarKind, tyVarFlexi, tyVarName,
  61                           mkFlexiTyVar, removeTyVarFlexi, isFlexiTyVar, isTyVar
  62                         )
  63
  64 -- others:
  65 import TcMonad
  66 import Name             ( changeUnique )
  67
  68 import TysWiredIn       ( voidTy )
  69
  70 import Name             ( NamedThing(..), changeUnique, mkSysLocalName )
  71 import Unique           ( Unique )
  72 import Util             ( nOfThem )
  73 import Outputable
  74 \end{code}
  75
  76
  77
  78 Data types
  79 ~~~~~~~~~~
  80 See TcMonad.lhs
  81
  82 \begin{code}
  83 tcTyVarToTyVar :: TcTyVar s -> TyVar
  84 tcTyVarToTyVar = removeTyVarFlexi
  85 \end{code}
  86
  87 Utility functions
  88 ~~~~~~~~~~~~~~~~~
  89 These tcSplit functions are like their non-Tc analogues, but they
  90 follow through bound type variables.
  91
  92 No need for tcSplitForAllTy because a type variable can't be instantiated
  93 to a for-all type.
  94
  95 \begin{code}
  96 tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s)
  97 tcSplitRhoTy t
  98   = go t t []
  99  where
 100         -- A type variable is never instantiated to a dictionary type,
 101         -- so we don't need to do a tcReadVar on the "arg".
 102     go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
 103                                         Just pair -> go res res (pair:ts)
 104                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
 105     go syn_t (NoteTy _ t)    ts = go syn_t t ts
 106     go syn_t (TyVarTy tv)    ts = tcReadTyVar tv        `thenNF_Tc` \ maybe_ty ->
 107                                   case maybe_ty of
 108                                     BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
 109                                     other                           -> returnNF_Tc (reverse ts, syn_t)
 110     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
 111 \end{code}
 112
 113
 114 New type variables
 115 ~~~~~~~~~~~~~~~~~~
 116
 117 \begin{code}
 118 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 119 newTcTyVar kind
 120   = tcGetUnique         `thenNF_Tc` \ uniq ->
 121     tcNewMutVar UnBound `thenNF_Tc` \ box ->
 122     let
 123         name = mkSysLocalName uniq
 124     in
 125     returnNF_Tc (mkFlexiTyVar name kind box)
 126
 127 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 128 newTyVarTy kind
 129   = newTcTyVar kind     `thenNF_Tc` \ tc_tyvar ->
 130     returnNF_Tc (TyVarTy tc_tyvar)
 131
 132 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 133 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 134
 135 newKindVar :: NF_TcM s (TcKind s)
 136 newKindVar = newTyVarTy superKind
 137
 138 newKindVars :: Int -> NF_TcM s [TcKind s]
 139 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 140 \end{code}
 141
 142 Type instantiation
 143 ~~~~~~~~~~~~~~~~~~
 144
 145 Instantiating a bunch of type variables
 146
 147 \begin{code}
 148 tcInstTyVars :: [GenTyVar flexi]
 149              -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
 150
 151 tcInstTyVars tyvars
 152   = mapNF_Tc inst_tyvar tyvars  `thenNF_Tc` \ tc_tyvars ->
 153     let
 154         tys = mkTyVarTys tc_tyvars
 155     in
 156     returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
 157
 158 inst_tyvar tyvar        -- Could use the name from the tyvar?
 159   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 160     tcNewMutVar UnBound         `thenNF_Tc` \ box ->
 161     let
 162         name = changeUnique (tyVarName tyvar) uniq
 163         -- Note that we don't change the print-name
 164         -- This won't confuse the type checker but there's a chance
 165         -- that two different tyvars will print the same way
 166         -- in an error message.  -dppr-debug will show up the difference
 167         -- Better watch out for this.  If worst comes to worst, just
 168         -- use mkSysLocalName.
 169     in
 170     returnNF_Tc (mkFlexiTyVar name (tyVarKind tyvar) box)
 171 \end{code}
 172
 173 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with
 174 fresh type variables, returning them and the instantiated body of the for-all.
 175
 176
 177 \begin{code}
 178 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 179 tcInstTcType ty
 180   = let
 181         (tyvars, rho) = splitForAllTys ty
 182     in
 183     case tyvars of
 184         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 185         other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 186                  returnNF_Tc (tyvars', fullSubstTy tenv emptyVarSet rho)
 187                                         -- Since the tyvars are freshly made,
 188                                         -- they cannot possibly be captured by
 189                                         -- any existing for-alls.  Hence emptyVarSet
 190 \end{code}
 191
 192 Sometimes we have to convert a Type to a TcType.  I wonder whether we could
 193 do this less than we do?
 194
 195 \begin{code}
 196 typeToTcType :: Type -> TcType s
 197 typeToTcType t = substFlexiTy emptyVarEnv t
 198
 199 kindToTcKind :: Kind -> TcKind s
 200 kindToTcKind = typeToTcType
 201 \end{code}
 202
 203
 204 Reading and writing TcTyVars
 205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 206 \begin{code}
 207 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 208 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 209 \end{code}
 210
 211 Writing is easy:
 212
 213 \begin{code}
 214 tcWriteTyVar tyvar ty = tcWriteMutVar (tyVarFlexi tyvar) (BoundTo ty)
 215 \end{code}
 216
 217 Reading is more interesting.  The easy thing to do is just to read, thus:
 218 \begin{verbatim}
 219 tcReadTyVar tyvar = tcReadMutVar (tyVarFlexi tyvar)
 220 \end{verbatim}
 221
 222 But it's more fun to short out indirections on the way: If this
 223 version returns a TyVar, then that TyVar is unbound.  If it returns
 224 any other type, then there might be bound TyVars embedded inside it.
 225
 226 We return Nothing iff the original box was unbound.
 227
 228 \begin{code}
 229 tcReadTyVar tyvar
 230   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 231     case maybe_ty of
 232         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 233                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 234                       returnNF_Tc (BoundTo ty')
 235
 236         other      -> returnNF_Tc other
 237   where
 238     box = tyVarFlexi tyvar
 239
 240 short_out :: TcType s -> NF_TcM s (TcType s)
 241 short_out ty@(TyVarTy tyvar)
 242   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 243     case maybe_ty of
 244         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 245                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 246                        returnNF_Tc ty'
 247
 248         other       -> returnNF_Tc ty
 249   where
 250     box = tyVarFlexi tyvar
 251
 252 short_out other_ty = returnNF_Tc other_ty
 253 \end{code}
 254
 255
 256 Zonking Tc types to Tc types
 257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 258 \begin{code}
 259 zonkTcTyVars :: [TcTyVar s] -> NF_TcM s [TcType s]
 260 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 261
 262 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 263 zonkTcTyVar tyvar
 264   | not (isFlexiTyVar tyvar)    -- Not a flexi tyvar.  This can happen when
 265                                 -- zonking a forall type, when the bound type variable
 266                                 -- needn't be a flexi.
 267   = ASSERT( isTyVar tyvar )
 268     returnNF_Tc (TyVarTy tyvar)
 269
 270   | otherwise   -- Is a flexi tyvar
 271   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 272     case maybe_ty of
 273         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty           -- tcReadTyVar never returns a bound tyvar
 274         BoundTo other               -> zonkTcType other
 275         other                       -> returnNF_Tc (TyVarTy tyvar)
 276
 277 zonkTcTyVarBndr :: TcTyVar s -> NF_TcM s (TcTyVar s)
 278 zonkTcTyVarBndr tyvar
 279   = zonkTcTyVar tyvar   `thenNF_Tc` \ (TyVarTy tyvar') ->
 280     returnNF_Tc tyvar'
 281
 282 zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
 283 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 284
 285 zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
 286 zonkTcThetaType theta = mapNF_Tc zonk theta
 287                     where
 288                       zonk (c,ts) = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 289                                     returnNF_Tc (c, new_ts)
 290
 291 zonkTcKind :: TcKind s -> NF_TcM s (TcKind s)
 292 zonkTcKind = zonkTcType
 293
 294 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 295
 296 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 297
 298 zonkTcType (AppTy ty1 ty2)
 299   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 300     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 301     returnNF_Tc (mkAppTy ty1' ty2')
 302
 303 zonkTcType (TyConApp tc tys)
 304   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 305     returnNF_Tc (TyConApp tc tys')
 306
 307 zonkTcType (NoteTy (SynNote ty1) ty2)
 308   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 309     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 310     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 311
 312 zonkTcType (NoteTy (FTVNote _) ty2) = zonkTcType ty2
 313
 314 zonkTcType (ForAllTy tv ty)
 315   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 316     zonkTcType ty               `thenNF_Tc` \ ty' ->
 317     case tv_ty of       -- Should be a tyvar!
 318       TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
 319       _ -> panic "zonkTcType"
 320            -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
 321            -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 322
 323 zonkTcType (FunTy ty1 ty2)
 324   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 325     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 326     returnNF_Tc (FunTy ty1' ty2')
 327 \end{code}
 328
 329 Zonking Tc types to Type/Kind
 330 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 331 \begin{code}
 332 zonkTcKindToKind :: TcKind s -> NF_TcM s Kind
 333 zonkTcKindToKind kind = zonkTcToType boxedTypeKind emptyVarEnv kind
 334
 335 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 336 zonkTcTypeToType env ty = zonkTcToType voidTy env ty
 337
 338 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 339 zonkTcTyVarToTyVar tv
 340   = zonkTcTyVarBndr tv  `thenNF_Tc` \ tv' ->
 341     returnNF_Tc (tcTyVarToTyVar tv')
 342
 343 -- zonkTcToType is used for Kinds as well
 344 zonkTcToType :: Type -> TyVarEnv Type -> TcType s -> NF_TcM s Type
 345 zonkTcToType unbound_var_ty env ty
 346   = go ty
 347   where
 348     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 349                                     returnNF_Tc (TyConApp tycon tys')
 350
 351     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 352                                     go ty2              `thenNF_Tc` \ ty2' ->
 353                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 354
 355     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 356
 357     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 358                                     go res              `thenNF_Tc` \ res' ->
 359                                     returnNF_Tc (FunTy arg' res')
 360
 361     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 362                                     go arg              `thenNF_Tc` \ arg' ->
 363                                     returnNF_Tc (mkAppTy fun' arg')
 364
 365         -- The two interesting cases!
 366         -- c.f. zonkTcTyVar
 367     go (TyVarTy tyvar)
 368         | not (isFlexiTyVar tyvar) = lookup env tyvar
 369
 370         | otherwise     =  tcReadTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 371                            case maybe_ty of
 372                               BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 373                               BoundTo other_ty         -> go other_ty
 374                               other                    -> lookup env tyvar
 375
 376     go (ForAllTy tyvar ty)
 377         = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
 378           let
 379              new_env = extendVarEnv env tyvar (TyVarTy tyvar')
 380           in
 381           zonkTcToType unbound_var_ty new_env ty        `thenNF_Tc` \ ty' ->
 382           returnNF_Tc (ForAllTy tyvar' ty')
 383
 384
 385     lookup env tyvar = returnNF_Tc (case lookupVarEnv env tyvar of
 386                                           Just ty -> ty
 387                                           Nothing -> unbound_var_ty)
 388 \end{code}
 389
 390