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