ghc/compiler/typecheck/TcType.lhs

   1 \begin{code}
   2 #include "HsVersions.h"
   3
   4 module TcType (
   5   SYN_IE(TcIdBndr), TcIdOcc(..),
   6
   7   -----------------------------------------
   8   SYN_IE(TcTyVar),
   9   SYN_IE(TcTyVarSet),
  10   newTcTyVar,
  11   newTyVarTy,   -- Kind -> NF_TcM s (TcType s)
  12   newTyVarTys,  -- Int -> Kind -> NF_TcM s [TcType s]
  13
  14   -----------------------------------------
  15   SYN_IE(TcType), TcMaybe(..),
  16   SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(TcRhoType),
  17
  18         -- Find the type to which a type variable is bound
  19   tcWriteTyVar,         -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
  20   tcReadTyVar,          -- :: TcTyVar s -> NF_TcM (TcMaybe s)
  21
  22
  23   tcSplitForAllTy, tcSplitRhoTy,
  24
  25   tcInstTyVars,
  26   tcInstSigTyVars,
  27   tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
  28   tcInstTheta, tcInstId,
  29
  30   zonkTcTyVars,
  31   zonkTcType,
  32   zonkTcTypeToType,
  33   zonkTcTyVar,
  34   zonkTcTyVarToTyVar
  35
  36   ) where
  37
  38
  39
  40 -- friends:
  41 import Type     ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..),
  42                   tyVarsOfTypes, getTyVar_maybe,
  43                   splitForAllTy, splitRhoTy, isTyVarTy,
  44                   mkForAllTys, instantiateTy
  45                 )
  46 import TyVar    ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet),
  47                   SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv,
  48                   nullTyVarEnv, mkTyVarEnv,
  49                   tyVarSetToList
  50                 )
  51 import PprType  ( GenType, GenTyVar )   -- Instances only
  52
  53 -- others:
  54 import Class    ( GenClass, SYN_IE(Class) )
  55 import TyCon    ( isFunTyCon )
  56 import Id       ( idType, GenId, SYN_IE(Id) )
  57 import Kind     ( Kind )
  58 import TcKind   ( TcKind )
  59 import TcMonad
  60 import Usage    ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
  61
  62 import TysPrim          ( voidTy )
  63
  64 IMP_Ubiq()
  65 import Name             ( NamedThing(..) )
  66 import Unique           ( Unique )
  67 import UniqFM           ( UniqFM )
  68 import Maybes           ( assocMaybe )
  69 import Outputable       ( Outputable(..) )
  70 import Util             ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
  71 \end{code}
  72
  73
  74
  75 Data types
  76 ~~~~~~~~~~
  77
  78 \begin{code}
  79 type TcIdBndr s = GenId  (TcType s)     -- Binders are all TcTypes
  80 data TcIdOcc  s = TcId   (TcIdBndr s)   -- Bindees may be either
  81                 | RealId Id
  82
  83 instance Eq (TcIdOcc s) where
  84   (TcId id1)   == (TcId id2)   = id1 == id2
  85   (RealId id1) == (RealId id2) = id1 == id2
  86   _            == _            = False
  87
  88 instance Outputable (TcIdOcc s) where
  89   ppr sty (TcId id)   = ppr sty id
  90   ppr sty (RealId id) = ppr sty id
  91
  92 instance NamedThing (TcIdOcc s) where
  93   getName (TcId id)   = getName id
  94   getName (RealId id) = getName id
  95 \end{code}
  96
  97
  98 \begin{code}
  99 type TcType s = GenType (TcTyVar s) UVar        -- Used during typechecker
 100         -- Invariant on ForAllTy in TcTypes:
 101         --      forall a. T
 102         -- a cannot occur inside a MutTyVar in T; that is,
 103         -- T is "flattened" before quantifying over a
 104
 105 type TcThetaType s = [(Class, TcType s)]
 106 type TcRhoType s   = TcType s           -- No ForAllTys
 107 type TcTauType s   = TcType s           -- No DictTys or ForAllTys
 108
 109 type Box s = MutableVar s (TcMaybe s)
 110
 111 data TcMaybe s = UnBound
 112                | BoundTo (TcType s)
 113                | DontBind               -- This variant is used for tyvars
 114                                         -- arising from type signatures, or
 115                                         -- existentially quantified tyvars;
 116                                         -- The idea is that we must not unify
 117                                         -- such tyvars with anything except
 118                                         -- themselves.
 119
 120 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
 121 -- because you get a synonym loop if you do!
 122
 123 type TcTyVar s    = GenTyVar (Box s)
 124 type TcTyVarSet s = GenTyVarSet (Box s)
 125 \end{code}
 126
 127 \begin{code}
 128 tcTyVarToTyVar :: TcTyVar s -> TyVar
 129 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
 130 \end{code}
 131
 132 Utility functions
 133 ~~~~~~~~~~~~~~~~~
 134 These tcSplit functions are like their non-Tc analogues, but they
 135 follow through bound type variables.
 136
 137 \begin{code}
 138 tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 139 tcSplitForAllTy t
 140   = go t t []
 141   where
 142     go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
 143     go syn_t (SynTy _ _ t)   tvs = go syn_t t tvs
 144     go syn_t (TyVarTy tv)    tvs = tcReadTyVar tv       `thenNF_Tc` \ maybe_ty ->
 145                                    case maybe_ty of
 146                                         BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
 147                                         other                           -> returnNF_Tc (reverse tvs, syn_t)
 148     go syn_t t               tvs = returnNF_Tc (reverse tvs, syn_t)
 149
 150 tcSplitRhoTy :: TcType s -> NF_TcM s ([(Class,TcType s)], TcType s)
 151 tcSplitRhoTy t
 152   = go t t []
 153  where
 154     go syn_t (FunTy (DictTy c t _) r _) ts = go r r ((c,t):ts)
 155     go syn_t (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
 156                               | isFunTyCon tycon
 157                               = go r r ((c,t):ts)
 158     go syn_t (SynTy _ _ t) ts = go syn_t t ts
 159     go syn_t (TyVarTy tv)  ts = tcReadTyVar tv  `thenNF_Tc` \ maybe_ty ->
 160                                 case maybe_ty of
 161                                   BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
 162                                   other                           -> returnNF_Tc (reverse ts, syn_t)
 163     go syn_t t             ts = returnNF_Tc (reverse ts, syn_t)
 164 \end{code}
 165
 166
 167 Type instantiation
 168 ~~~~~~~~~~~~~~~~~~
 169
 170 \begin{code}
 171 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 172 newTcTyVar kind
 173   = tcGetUnique         `thenNF_Tc` \ uniq ->
 174     tcNewMutVar UnBound `thenNF_Tc` \ box ->
 175     returnNF_Tc (TyVar uniq kind Nothing box)
 176
 177 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 178 newTyVarTy kind
 179   = newTcTyVar kind     `thenNF_Tc` \ tc_tyvar ->
 180     returnNF_Tc (TyVarTy tc_tyvar)
 181
 182 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 183 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 184
 185
 186 -- For signature type variables, mark them as "DontBind"
 187 tcInstTyVars, tcInstSigTyVars
 188         :: [GenTyVar flexi]
 189         -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
 190
 191 tcInstTyVars    tyvars = inst_tyvars UnBound  tyvars
 192 tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
 193
 194 inst_tyvars initial_cts tyvars
 195   = mapNF_Tc (inst_tyvar initial_cts) tyvars    `thenNF_Tc` \ tc_tyvars ->
 196     let
 197         tys = map TyVarTy tc_tyvars
 198     in
 199     returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
 200
 201 inst_tyvar initial_cts (TyVar _ kind name _)
 202   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 203     tcNewMutVar initial_cts     `thenNF_Tc` \ box ->
 204     returnNF_Tc (TyVar uniq kind Nothing box)
 205         -- The "Nothing" means that it'll always print with its
 206         -- unique (or something similar).  If we leave the original (Just Name)
 207         -- in there then error messages will say "can't match (T a) against (T a)"
 208 \end{code}
 209
 210 @tcInstType@ and @tcInstSigType@ both create a fresh instance of a
 211 type, returning a @TcType@. All inner for-alls are instantiated with
 212 fresh TcTyVars.
 213
 214 The difference is that tcInstType instantiates all forall'd type
 215 variables (and their bindees) with UnBound type variables, whereas
 216 tcInstSigType instantiates them with DontBind types variables.
 217 @tcInstSigType@ also doesn't take an environment.
 218
 219 On the other hand, @tcInstTcType@ instantiates a TcType. It uses
 220 instantiateTy which could take advantage of sharing some day.
 221
 222 \begin{code}
 223 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 224 tcInstTcType ty
 225   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 226     case tyvars of
 227         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 228         other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 229                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 230
 231 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 232 tcInstSigTcType ty
 233   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 234     case tyvars of
 235         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 236         other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
 237                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 238
 239 tcInstType :: [(GenTyVar flexi,TcType s)]
 240            -> GenType (GenTyVar flexi) UVar
 241            -> NF_TcM s (TcType s)
 242 tcInstType tenv ty_to_inst
 243   = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
 244   where
 245     bind_fn = inst_tyvar UnBound
 246     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 247                          Just ty -> returnNF_Tc ty
 248                          Nothing -> panic "tcInstType:1" --(vcat [ppr PprDebug ty_to_inst,
 249                                                         --            ppr PprDebug tyvar])
 250
 251 tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s)
 252 tcInstSigType ty_to_inst
 253   = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst
 254   where
 255     bind_fn = inst_tyvar DontBind
 256     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 257                          Just ty -> returnNF_Tc ty
 258                          Nothing -> panic "tcInstType:2"-- (vcat [ppr PprDebug ty_to_inst,
 259                                                         --            ppr PprDebug tyvar])
 260
 261 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 262 zonkTcTyVarToTyVar tv
 263   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 264     case tv_ty of       -- Should be a tyvar!
 265
 266       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 267
 268       _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 269            returnNF_Tc (tcTyVarToTyVar tv)
 270
 271
 272 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 273 zonkTcTypeToType env ty
 274   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 275   where
 276     occ_fn env tyvar
 277       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 278          case maybe_ty of
 279            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 280            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 281            other                    -> lookup env tyvar
 282
 283     lookup env tyvar = case lookupTyVarEnv env tyvar of
 284                           Just ty -> returnNF_Tc ty
 285                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 286
 287
 288 tcConvert bind_fn occ_fn env ty_to_convert
 289   = doo env ty_to_convert
 290   where
 291     doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
 292
 293     doo env (SynTy tycon tys ty)  = mapNF_Tc (doo env) tys      `thenNF_Tc` \ tys' ->
 294                                    doo env ty                   `thenNF_Tc` \ ty' ->
 295                                    returnNF_Tc (SynTy tycon tys' ty')
 296
 297     doo env (FunTy arg res usage) = doo env arg         `thenNF_Tc` \ arg' ->
 298                                    doo env res          `thenNF_Tc` \ res' ->
 299                                    returnNF_Tc (FunTy arg' res' usage)
 300
 301     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 302                                    doo env arg          `thenNF_Tc` \ arg' ->
 303                                    returnNF_Tc (AppTy fun' arg')
 304
 305     doo env (DictTy clas ty usage)= doo env ty          `thenNF_Tc` \ ty' ->
 306                                    returnNF_Tc (DictTy clas ty' usage)
 307
 308     doo env (ForAllUsageTy u us ty) = doo env ty        `thenNF_Tc` \ ty' ->
 309                                      returnNF_Tc (ForAllUsageTy u us ty')
 310
 311         -- The two interesting cases!
 312     doo env (TyVarTy tv)         = occ_fn env tv
 313
 314     doo env (ForAllTy tyvar ty)
 315         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 316           let
 317                 new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
 318           in
 319           doo new_env ty                `thenNF_Tc` \ ty' ->
 320           returnNF_Tc (ForAllTy tyvar' ty')
 321
 322
 323 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
 324 tcInstTheta tenv theta
 325   = mapNF_Tc go theta
 326   where
 327     go (clas,ty) = tcInstType tenv ty   `thenNF_Tc` \ tc_ty ->
 328                    returnNF_Tc (clas, tc_ty)
 329
 330 -- A useful function that takes an occurrence of a global thing
 331 -- and instantiates its type with fresh type variables
 332 tcInstId :: Id
 333          -> NF_TcM s ([TcTyVar s],      -- It's instantiated type
 334                       TcThetaType s,    --
 335                       TcType s)         --
 336
 337 tcInstId id
 338   = let
 339       (tyvars, rho) = splitForAllTy (idType id)
 340     in
 341     tcInstTyVars tyvars         `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
 342     tcInstType tenv rho         `thenNF_Tc` \ rho' ->
 343     let
 344         (theta', tau') = splitRhoTy rho'
 345     in
 346     returnNF_Tc (tyvars', theta', tau')
 347 \end{code}
 348
 349 Reading and writing TcTyVars
 350 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 351 \begin{code}
 352 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 353 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 354 \end{code}
 355
 356 Writing is easy:
 357
 358 \begin{code}
 359 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 360 \end{code}
 361
 362 Reading is more interesting.  The easy thing to do is just to read, thus:
 363 \begin{verbatim}
 364 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 365 \end{verbatim}
 366
 367 But it's more fun to short out indirections on the way: If this
 368 version returns a TyVar, then that TyVar is unbound.  If it returns
 369 any other type, then there might be bound TyVars embedded inside it.
 370
 371 We return Nothing iff the original box was unbound.
 372
 373 \begin{code}
 374 tcReadTyVar (TyVar uniq kind name box)
 375   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 376     case maybe_ty of
 377         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 378                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 379                       returnNF_Tc (BoundTo ty')
 380
 381         other      -> returnNF_Tc other
 382
 383 short_out :: TcType s -> NF_TcM s (TcType s)
 384 short_out ty@(TyVarTy (TyVar uniq kind name box))
 385   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 386     case maybe_ty of
 387         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 388                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 389                        returnNF_Tc ty'
 390
 391         other       -> returnNF_Tc ty
 392
 393 short_out other_ty = returnNF_Tc other_ty
 394 \end{code}
 395
 396
 397 Zonking
 398 ~~~~~~~
 399 \begin{code}
 400 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 401 zonkTcTyVars tyvars
 402   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 403     returnNF_Tc (tyVarsOfTypes tys)
 404
 405 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 406 zonkTcTyVar tyvar
 407   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 408     case maybe_ty of
 409         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty           -- tcReadTyVar never returns a bound tyvar
 410         BoundTo other               -> zonkTcType other
 411         other                       -> returnNF_Tc (TyVarTy tyvar)
 412
 413 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 414
 415 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 416
 417 zonkTcType (AppTy ty1 ty2)
 418   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 419     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 420     returnNF_Tc (AppTy ty1' ty2')
 421
 422 zonkTcType (TyConTy tc u)
 423   = returnNF_Tc (TyConTy tc u)
 424
 425 zonkTcType (SynTy tc tys ty)
 426   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 427     zonkTcType ty               `thenNF_Tc` \ ty' ->
 428     returnNF_Tc (SynTy tc tys' ty')
 429
 430 zonkTcType (ForAllTy tv ty)
 431   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 432     zonkTcType ty               `thenNF_Tc` \ ty' ->
 433     case tv_ty of       -- Should be a tyvar!
 434       TyVarTy tv' ->
 435                      returnNF_Tc (ForAllTy tv' ty')
 436       _ -> --pprTrace "zonkTcType:ForAllTy:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 437
 438            returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 439
 440 zonkTcType (ForAllUsageTy uv uvs ty)
 441   = panic "zonk:ForAllUsageTy"
 442
 443 zonkTcType (FunTy ty1 ty2 u)
 444   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 445     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 446     returnNF_Tc (FunTy ty1' ty2' u)
 447
 448 zonkTcType (DictTy c ty u)
 449   = zonkTcType ty               `thenNF_Tc` \ ty' ->
 450     returnNF_Tc (DictTy c ty' u)
 451 \end{code}