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   tcSplitForAllTy, tcSplitRhoTy,
  25
  26   tcInstTyVars,
  27   tcInstSigTyVars,
  28   tcInstType,
  29   tcInstSigType, tcInstTcType, tcInstSigTcType,
  30   tcInstTheta,
  31
  32   zonkTcTyVars, zonkSigTyVar,
  33   zonkTcType, zonkTcTypes, zonkTcThetaType,
  34   zonkTcTypeToType,
  35   zonkTcTyVar,
  36   zonkTcTyVarToTyVar
  37
  38   ) where
  39
  40 #include "HsVersions.h"
  41
  42
  43 -- friends:
  44 import Type             ( Type, ThetaType, GenType(..), mkAppTy,
  45                           tyVarsOfTypes, splitDictTy_maybe,
  46                           isTyVarTy, instantiateTy
  47                         )
  48 import TyVar            ( TyVar, GenTyVar(..), GenTyVarSet,
  49                           TyVarEnv, lookupTyVarEnv, addToTyVarEnv,
  50                           emptyTyVarEnv, zipTyVarEnv, tyVarSetToList
  51                         )
  52
  53 -- others:
  54 import Class            ( Class )
  55 import TyCon            ( isFunTyCon )
  56 import Kind             ( Kind )
  57 import TcMonad
  58
  59 import TysPrim          ( voidTy )
  60
  61 import Unique           ( Unique )
  62 import UniqFM           ( UniqFM )
  63 import BasicTypes       ( unused )
  64 import Util             ( nOfThem, panic )
  65 \end{code}
  66
  67
  68
  69 Data types
  70 ~~~~~~~~~~
  71
  72
  73 \begin{code}
  74 type TcType s = GenType (TcBox s)       -- Used during typechecker
  75         -- Invariant on ForAllTy in TcTypes:
  76         --      forall a. T
  77         -- a cannot occur inside a MutTyVar in T; that is,
  78         -- T is "flattened" before quantifying over a
  79
  80 type TcThetaType s = [(Class, [TcType s])]
  81 type TcRhoType s   = TcType s           -- No ForAllTys
  82 type TcTauType s   = TcType s           -- No DictTys or ForAllTys
  83
  84 type TcBox s = TcRef s (TcMaybe s)
  85
  86 data TcMaybe s = UnBound
  87                | BoundTo (TcType s)
  88
  89 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
  90 -- because you get a synonym loop if you do!
  91
  92 type TcTyVar s    = GenTyVar (TcBox s)
  93 type TcTyVarSet s = GenTyVarSet (TcBox s)
  94 \end{code}
  95
  96 \begin{code}
  97 tcTyVarToTyVar :: TcTyVar s -> TyVar
  98 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name unused
  99 \end{code}
 100
 101 Utility functions
 102 ~~~~~~~~~~~~~~~~~
 103 These tcSplit functions are like their non-Tc analogues, but they
 104 follow through bound type variables.
 105
 106 \begin{code}
 107 tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 108 tcSplitForAllTy t
 109   = go t t []
 110   where
 111     go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
 112     go syn_t (SynTy _ t)     tvs = go syn_t t tvs
 113     go syn_t (TyVarTy tv)    tvs = tcReadTyVar tv       `thenNF_Tc` \ maybe_ty ->
 114                                    case maybe_ty of
 115                                         BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
 116                                         other                           -> returnNF_Tc (reverse tvs, syn_t)
 117     go syn_t t               tvs = returnNF_Tc (reverse tvs, syn_t)
 118
 119 tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s)
 120 tcSplitRhoTy t
 121   = go t t []
 122  where
 123         -- A type variable is never instantiated to a dictionary type,
 124         -- so we don't need to do a tcReadVar on the "arg".
 125     go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
 126                                         Just pair -> go res res (pair:ts)
 127                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
 128     go syn_t (SynTy _ t)     ts = go syn_t t ts
 129     go syn_t (TyVarTy tv)    ts = tcReadTyVar tv        `thenNF_Tc` \ maybe_ty ->
 130                                   case maybe_ty of
 131                                     BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
 132                                     other                           -> returnNF_Tc (reverse ts, syn_t)
 133     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
 134 \end{code}
 135
 136
 137 Type instantiation
 138 ~~~~~~~~~~~~~~~~~~
 139
 140 \begin{code}
 141 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 142 newTcTyVar kind
 143   = tcGetUnique         `thenNF_Tc` \ uniq ->
 144     tcNewMutVar UnBound `thenNF_Tc` \ box ->
 145     returnNF_Tc (TyVar uniq kind Nothing box)
 146
 147 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 148 newTyVarTy kind
 149   = newTcTyVar kind     `thenNF_Tc` \ tc_tyvar ->
 150     returnNF_Tc (TyVarTy tc_tyvar)
 151
 152 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 153 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 154
 155
 156 -- For signature type variables, use the user name for the type variable
 157 tcInstTyVars, tcInstSigTyVars
 158         :: [GenTyVar flexi]
 159         -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
 160
 161 tcInstTyVars    tyvars = inst_tyvars inst_tyvar     tyvars
 162 tcInstSigTyVars tyvars = inst_tyvars inst_sig_tyvar tyvars
 163
 164 inst_tyvars inst tyvars
 165   = mapNF_Tc inst tyvars        `thenNF_Tc` \ tc_tyvars ->
 166     let
 167         tys = map TyVarTy tc_tyvars
 168     in
 169     returnNF_Tc (tc_tyvars, tys, zipTyVarEnv tyvars tys)
 170
 171 inst_tyvar (TyVar _ kind name _)
 172   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 173     tcNewMutVar UnBound         `thenNF_Tc` \ box ->
 174     returnNF_Tc (TyVar uniq kind Nothing box)
 175         -- The "Nothing" means that it'll always print with its
 176         -- unique (or something similar).  If we leave the original (Just Name)
 177         -- in there then error messages will say "can't match (T a) against (T a)"
 178
 179 inst_sig_tyvar (TyVar _ kind name _)
 180   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 181
 182     tcNewMutVar UnBound         `thenNF_Tc` \ box ->
 183         -- Was DontBind, but we've nuked that "optimisation"
 184
 185     returnNF_Tc (TyVar uniq kind name box)
 186         -- We propagate the name of the sigature type variable
 187 \end{code}
 188
 189 @tcInstType@ and @tcInstSigType@ both create a fresh instance of a
 190 type, returning a @TcType@. All inner for-alls are instantiated with
 191 fresh TcTyVars.
 192
 193 The difference is that tcInstType instantiates all forall'd type
 194 variables (and their bindees) with anonymous type variables, whereas
 195 tcInstSigType instantiates them with named type variables.
 196 @tcInstSigType@ also doesn't take an environment.
 197
 198 On the other hand, @tcInstTcType@ instantiates a TcType. It uses
 199 instantiateTy which could take advantage of sharing some day.
 200
 201 \begin{code}
 202 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 203 tcInstTcType ty
 204   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 205     case tyvars of
 206         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 207         other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 208                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 209
 210 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 211 tcInstSigTcType ty
 212   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 213     case tyvars of
 214         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 215         other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
 216                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 217
 218 tcInstType :: TyVarEnv (TcType s)
 219            -> GenType flexi
 220            -> NF_TcM s (TcType s)
 221 tcInstType tenv ty_to_inst
 222   = tcConvert bind_fn occ_fn tenv ty_to_inst
 223   where
 224     bind_fn = inst_tyvar
 225     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 226                          Just ty -> returnNF_Tc ty
 227                          Nothing -> panic "tcInstType:1" --(vcat [ppr ty_to_inst,
 228                                                         --            ppr tyvar])
 229
 230 tcInstSigType :: GenType flexi -> NF_TcM s (TcType s)
 231 tcInstSigType ty_to_inst
 232   = tcConvert bind_fn occ_fn emptyTyVarEnv ty_to_inst
 233   where
 234     bind_fn = inst_sig_tyvar    -- Note: inst_sig_tyvar, not inst_tyvar
 235                                 -- I don't think that can lead to strange error messages
 236     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 237                          Just ty -> returnNF_Tc ty
 238                          Nothing -> panic "tcInstType:2"-- (vcat [ppr ty_to_inst,
 239                                                         --            ppr tyvar])
 240
 241 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 242 zonkTcTyVarToTyVar tv
 243   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 244     case tv_ty of       -- Should be a tyvar!
 245
 246       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 247
 248       _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr tv, ppr tv_ty]) $
 249            returnNF_Tc (tcTyVarToTyVar tv)
 250
 251
 252 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 253 zonkTcTypeToType env ty
 254   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 255   where
 256     occ_fn env tyvar
 257       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 258          case maybe_ty of
 259            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 260            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 261            other                    -> lookup env tyvar
 262
 263     lookup env tyvar = case lookupTyVarEnv env tyvar of
 264                           Just ty -> returnNF_Tc ty
 265                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 266
 267
 268 tcConvert bind_fn occ_fn env ty_to_convert
 269   = doo env ty_to_convert
 270   where
 271     doo env (TyConApp tycon tys) = mapNF_Tc (doo env) tys       `thenNF_Tc` \ tys' ->
 272                                    returnNF_Tc (TyConApp tycon tys')
 273
 274     doo env (SynTy ty1 ty2)      = doo env ty1                  `thenNF_Tc` \ ty1' ->
 275                                    doo env ty2                  `thenNF_Tc` \ ty2' ->
 276                                    returnNF_Tc (SynTy ty1' ty2')
 277
 278     doo env (FunTy arg res)      = doo env arg          `thenNF_Tc` \ arg' ->
 279                                    doo env res          `thenNF_Tc` \ res' ->
 280                                    returnNF_Tc (FunTy arg' res')
 281
 282     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 283                                    doo env arg          `thenNF_Tc` \ arg' ->
 284                                    returnNF_Tc (mkAppTy fun' arg')
 285
 286         -- The two interesting cases!
 287     doo env (TyVarTy tv)         = occ_fn env tv
 288
 289     doo env (ForAllTy tyvar ty)
 290         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 291           let
 292                 new_env = addToTyVarEnv env tyvar (TyVarTy tyvar')
 293           in
 294           doo new_env ty                `thenNF_Tc` \ ty' ->
 295           returnNF_Tc (ForAllTy tyvar' ty')
 296
 297
 298 tcInstTheta :: TyVarEnv (TcType s) -> ThetaType -> NF_TcM s (TcThetaType s)
 299 tcInstTheta tenv theta
 300   = mapNF_Tc go theta
 301   where
 302     go (clas,tys) = mapNF_Tc (tcInstType tenv) tys      `thenNF_Tc` \ tc_tys ->
 303                     returnNF_Tc (clas, tc_tys)
 304 \end{code}
 305
 306 Reading and writing TcTyVars
 307 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 308 \begin{code}
 309 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 310 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 311 \end{code}
 312
 313 Writing is easy:
 314
 315 \begin{code}
 316 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 317 \end{code}
 318
 319 Reading is more interesting.  The easy thing to do is just to read, thus:
 320 \begin{verbatim}
 321 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 322 \end{verbatim}
 323
 324 But it's more fun to short out indirections on the way: If this
 325 version returns a TyVar, then that TyVar is unbound.  If it returns
 326 any other type, then there might be bound TyVars embedded inside it.
 327
 328 We return Nothing iff the original box was unbound.
 329
 330 \begin{code}
 331 tcReadTyVar (TyVar uniq kind name box)
 332   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 333     case maybe_ty of
 334         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 335                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 336                       returnNF_Tc (BoundTo ty')
 337
 338         other      -> returnNF_Tc other
 339
 340 short_out :: TcType s -> NF_TcM s (TcType s)
 341 short_out ty@(TyVarTy (TyVar uniq kind name box))
 342   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 343     case maybe_ty of
 344         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 345                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 346                        returnNF_Tc ty'
 347
 348         other       -> returnNF_Tc ty
 349
 350 short_out other_ty = returnNF_Tc other_ty
 351 \end{code}
 352
 353
 354 Zonking
 355 ~~~~~~~
 356 \begin{code}
 357 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 358 zonkTcTyVars tyvars
 359   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 360     returnNF_Tc (tyVarsOfTypes tys)
 361
 362 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 363 zonkTcTyVar tyvar
 364   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 365     case maybe_ty of
 366         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty           -- tcReadTyVar never returns a bound tyvar
 367         BoundTo other               -> zonkTcType other
 368         other                       -> returnNF_Tc (TyVarTy tyvar)
 369
 370 -- Signature type variables only get bound to each other,
 371 -- never to a type
 372 zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s)
 373 zonkSigTyVar tyvar
 374   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 375     case maybe_ty of
 376         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar'       -- tcReadTyVar never returns a bound tyvar
 377         BoundTo other               -> panic "zonkSigTyVar"     -- Should only be bound to another tyvar
 378         other                       -> returnNF_Tc tyvar
 379
 380 zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
 381 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 382
 383 zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
 384 zonkTcThetaType theta = mapNF_Tc zonk theta
 385                     where
 386                       zonk (c,ts) = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 387                                     returnNF_Tc (c, new_ts)
 388
 389 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 390
 391 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 392
 393 zonkTcType (AppTy ty1 ty2)
 394   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 395     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 396     returnNF_Tc (mkAppTy ty1' ty2')
 397
 398 zonkTcType (TyConApp tc tys)
 399   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 400     returnNF_Tc (TyConApp tc tys')
 401
 402 zonkTcType (SynTy ty1 ty2)
 403   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 404     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 405     returnNF_Tc (SynTy ty1' ty2')
 406
 407 zonkTcType (ForAllTy tv ty)
 408   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 409     zonkTcType ty               `thenNF_Tc` \ ty' ->
 410     case tv_ty of       -- Should be a tyvar!
 411       TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
 412       _ -> panic "zonkTcType"
 413            -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
 414            -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 415
 416 zonkTcType (FunTy ty1 ty2)
 417   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 418     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 419     returnNF_Tc (FunTy ty1' ty2')
 420 \end{code}