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                                 -- of the form can't match (T a) against (T a)
 237                                 -- See notes with inst_tyvar
 238
 239     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 240                          Just ty -> returnNF_Tc ty
 241                          Nothing -> panic "tcInstType:2"-- (vcat [ppr ty_to_inst,
 242                                                         --            ppr tyvar])
 243
 244 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 245 zonkTcTyVarToTyVar tv
 246   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 247     case tv_ty of       -- Should be a tyvar!
 248
 249       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 250
 251       _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr tv, ppr tv_ty]) $
 252            returnNF_Tc (tcTyVarToTyVar tv)
 253
 254
 255 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 256 zonkTcTypeToType env ty
 257   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 258   where
 259     occ_fn env tyvar
 260       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 261          case maybe_ty of
 262            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 263            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 264            other                    -> lookup env tyvar
 265
 266     lookup env tyvar = case lookupTyVarEnv env tyvar of
 267                           Just ty -> returnNF_Tc ty
 268                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 269
 270
 271 tcConvert bind_fn occ_fn env ty_to_convert
 272   = doo env ty_to_convert
 273   where
 274     doo env (TyConApp tycon tys) = mapNF_Tc (doo env) tys       `thenNF_Tc` \ tys' ->
 275                                    returnNF_Tc (TyConApp tycon tys')
 276
 277     doo env (SynTy ty1 ty2)      = doo env ty1                  `thenNF_Tc` \ ty1' ->
 278                                    doo env ty2                  `thenNF_Tc` \ ty2' ->
 279                                    returnNF_Tc (SynTy ty1' ty2')
 280
 281     doo env (FunTy arg res)      = doo env arg          `thenNF_Tc` \ arg' ->
 282                                    doo env res          `thenNF_Tc` \ res' ->
 283                                    returnNF_Tc (FunTy arg' res')
 284
 285     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 286                                    doo env arg          `thenNF_Tc` \ arg' ->
 287                                    returnNF_Tc (mkAppTy fun' arg')
 288
 289         -- The two interesting cases!
 290     doo env (TyVarTy tv)         = occ_fn env tv
 291
 292     doo env (ForAllTy tyvar ty)
 293         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 294           let
 295                 new_env = addToTyVarEnv env tyvar (TyVarTy tyvar')
 296           in
 297           doo new_env ty                `thenNF_Tc` \ ty' ->
 298           returnNF_Tc (ForAllTy tyvar' ty')
 299
 300
 301 tcInstTheta :: TyVarEnv (TcType s) -> ThetaType -> NF_TcM s (TcThetaType s)
 302 tcInstTheta tenv theta
 303   = mapNF_Tc go theta
 304   where
 305     go (clas,tys) = mapNF_Tc (tcInstType tenv) tys      `thenNF_Tc` \ tc_tys ->
 306                     returnNF_Tc (clas, tc_tys)
 307 \end{code}
 308
 309 Reading and writing TcTyVars
 310 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 311 \begin{code}
 312 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 313 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 314 \end{code}
 315
 316 Writing is easy:
 317
 318 \begin{code}
 319 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 320 \end{code}
 321
 322 Reading is more interesting.  The easy thing to do is just to read, thus:
 323 \begin{verbatim}
 324 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 325 \end{verbatim}
 326
 327 But it's more fun to short out indirections on the way: If this
 328 version returns a TyVar, then that TyVar is unbound.  If it returns
 329 any other type, then there might be bound TyVars embedded inside it.
 330
 331 We return Nothing iff the original box was unbound.
 332
 333 \begin{code}
 334 tcReadTyVar (TyVar uniq kind name box)
 335   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 336     case maybe_ty of
 337         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 338                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 339                       returnNF_Tc (BoundTo ty')
 340
 341         other      -> returnNF_Tc other
 342
 343 short_out :: TcType s -> NF_TcM s (TcType s)
 344 short_out ty@(TyVarTy (TyVar uniq kind name box))
 345   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 346     case maybe_ty of
 347         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 348                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 349                        returnNF_Tc ty'
 350
 351         other       -> returnNF_Tc ty
 352
 353 short_out other_ty = returnNF_Tc other_ty
 354 \end{code}
 355
 356
 357 Zonking
 358 ~~~~~~~
 359 \begin{code}
 360 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 361 zonkTcTyVars tyvars
 362   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 363     returnNF_Tc (tyVarsOfTypes tys)
 364
 365 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 366 zonkTcTyVar tyvar
 367   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 368     case maybe_ty of
 369         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty           -- tcReadTyVar never returns a bound tyvar
 370         BoundTo other               -> zonkTcType other
 371         other                       -> returnNF_Tc (TyVarTy tyvar)
 372
 373 -- Signature type variables only get bound to each other,
 374 -- never to a type
 375 zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s)
 376 zonkSigTyVar tyvar
 377   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 378     case maybe_ty of
 379         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar'       -- tcReadTyVar never returns a bound tyvar
 380         BoundTo other               -> panic "zonkSigTyVar"     -- Should only be bound to another tyvar
 381         other                       -> returnNF_Tc tyvar
 382
 383 zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
 384 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 385
 386 zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
 387 zonkTcThetaType theta = mapNF_Tc zonk theta
 388                     where
 389                       zonk (c,ts) = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 390                                     returnNF_Tc (c, new_ts)
 391
 392 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 393
 394 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 395
 396 zonkTcType (AppTy ty1 ty2)
 397   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 398     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 399     returnNF_Tc (mkAppTy ty1' ty2')
 400
 401 zonkTcType (TyConApp tc tys)
 402   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 403     returnNF_Tc (TyConApp tc tys')
 404
 405 zonkTcType (SynTy ty1 ty2)
 406   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 407     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 408     returnNF_Tc (SynTy ty1' ty2')
 409
 410 zonkTcType (ForAllTy tv ty)
 411   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 412     zonkTcType ty               `thenNF_Tc` \ ty' ->
 413     case tv_ty of       -- Should be a tyvar!
 414       TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
 415       _ -> panic "zonkTcType"
 416            -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
 417            -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 418
 419 zonkTcType (FunTy ty1 ty2)
 420   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 421     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 422     returnNF_Tc (FunTy ty1' ty2')
 423 \end{code}