ghc/compiler/typecheck/TcType.lhs

   1 \begin{code}
   2 #include "HsVersions.h"
   3
   4 module TcType (
   5
   6   SYN_IE(TcTyVar),
   7   newTcTyVar,
   8   newTyVarTy,   -- Kind -> NF_TcM s (TcType s)
   9   newTyVarTys,  -- Int -> Kind -> NF_TcM s [TcType s]
  10
  11
  12   SYN_IE(TcTyVarSet),
  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
  52 -- others:
  53 import Class    ( GenClass, SYN_IE(Class) )
  54 import TyCon    ( isFunTyCon )
  55 import Id       ( idType, SYN_IE(Id) )
  56 import Kind     ( Kind )
  57 import TcKind   ( TcKind )
  58 import TcMonad
  59 import Usage    ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
  60
  61 import TysPrim          ( voidTy )
  62
  63 IMP_Ubiq()
  64 import Unique           ( Unique )
  65 import UniqFM           ( UniqFM )
  66 import Maybes           ( assocMaybe )
  67 import Util             ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
  68
  69 --import Outputable     ( Outputable(..) )      -- Debugging messages
  70 --import PprType                ( GenTyVar, GenType )
  71 --import Pretty                                 -- ditto
  72 --import PprStyle               ( PprStyle(..) )        -- ditto
  73 \end{code}
  74
  75
  76
  77 Data types
  78 ~~~~~~~~~~
  79
  80 \begin{code}
  81 type TcType s = GenType (TcTyVar s) UVar        -- Used during typechecker
  82         -- Invariant on ForAllTy in TcTypes:
  83         --      forall a. T
  84         -- a cannot occur inside a MutTyVar in T; that is,
  85         -- T is "flattened" before quantifying over a
  86
  87 type TcThetaType s = [(Class, TcType s)]
  88 type TcRhoType s   = TcType s           -- No ForAllTys
  89 type TcTauType s   = TcType s           -- No DictTys or ForAllTys
  90
  91 type Box s = MutableVar s (TcMaybe s)
  92
  93 data TcMaybe s = UnBound
  94                | BoundTo (TcType s)
  95                | DontBind               -- This variant is used for tyvars
  96                                         -- arising from type signatures, or
  97                                         -- existentially quantified tyvars;
  98                                         -- The idea is that we must not unify
  99                                         -- such tyvars with anything except
 100                                         -- themselves.
 101
 102 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
 103 -- because you get a synonym loop if you do!
 104
 105 type TcTyVar s    = GenTyVar (Box s)
 106 type TcTyVarSet s = GenTyVarSet (Box s)
 107 \end{code}
 108
 109 \begin{code}
 110 tcTyVarToTyVar :: TcTyVar s -> TyVar
 111 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
 112 \end{code}
 113
 114 Utility functions
 115 ~~~~~~~~~~~~~~~~~
 116 These tcSplit functions are like their non-Tc analogues, but they
 117 follow through bound type variables.
 118
 119 \begin{code}
 120 tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 121 tcSplitForAllTy t
 122   = go t t []
 123   where
 124     go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
 125     go syn_t (SynTy _ _ t)   tvs = go syn_t t tvs
 126     go syn_t (TyVarTy tv)    tvs = tcReadTyVar tv       `thenNF_Tc` \ maybe_ty ->
 127                                    case maybe_ty of
 128                                         BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
 129                                         other                           -> returnNF_Tc (reverse tvs, syn_t)
 130     go syn_t t               tvs = returnNF_Tc (reverse tvs, syn_t)
 131
 132 tcSplitRhoTy :: TcType s -> NF_TcM s ([(Class,TcType s)], TcType s)
 133 tcSplitRhoTy t
 134   = go t t []
 135  where
 136     go syn_t (FunTy (DictTy c t _) r _) ts = go r r ((c,t):ts)
 137     go syn_t (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
 138                               | isFunTyCon tycon
 139                               = go r r ((c,t):ts)
 140     go syn_t (SynTy _ _ t) ts = go syn_t t ts
 141     go syn_t (TyVarTy tv)  ts = tcReadTyVar tv  `thenNF_Tc` \ maybe_ty ->
 142                                 case maybe_ty of
 143                                   BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
 144                                   other                           -> returnNF_Tc (reverse ts, syn_t)
 145     go syn_t t             ts = returnNF_Tc (reverse ts, syn_t)
 146 \end{code}
 147
 148
 149 Type instantiation
 150 ~~~~~~~~~~~~~~~~~~
 151
 152 \begin{code}
 153 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 154 newTcTyVar kind
 155   = tcGetUnique         `thenNF_Tc` \ uniq ->
 156     tcNewMutVar UnBound `thenNF_Tc` \ box ->
 157     returnNF_Tc (TyVar uniq kind Nothing box)
 158
 159 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 160 newTyVarTy kind
 161   = newTcTyVar kind     `thenNF_Tc` \ tc_tyvar ->
 162     returnNF_Tc (TyVarTy tc_tyvar)
 163
 164 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 165 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 166
 167
 168 -- For signature type variables, mark them as "DontBind"
 169 tcInstTyVars, tcInstSigTyVars
 170         :: [GenTyVar flexi]
 171         -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
 172
 173 tcInstTyVars    tyvars = inst_tyvars UnBound  tyvars
 174 tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
 175
 176 inst_tyvars initial_cts tyvars
 177   = mapNF_Tc (inst_tyvar initial_cts) tyvars    `thenNF_Tc` \ tc_tyvars ->
 178     let
 179         tys = map TyVarTy tc_tyvars
 180     in
 181     returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
 182
 183 inst_tyvar initial_cts (TyVar _ kind name _)
 184   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 185     tcNewMutVar initial_cts     `thenNF_Tc` \ box ->
 186     returnNF_Tc (TyVar uniq kind name box)
 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 UnBound type variables, whereas
 195 tcInstSigType instantiates them with DontBind types 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 :: [(GenTyVar flexi,TcType s)]
 219            -> GenType (GenTyVar flexi) UVar
 220            -> NF_TcM s (TcType s)
 221 tcInstType tenv ty_to_inst
 222   = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
 223   where
 224     bind_fn = inst_tyvar UnBound
 225     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 226                          Just ty -> returnNF_Tc ty
 227                          Nothing -> panic "tcInstType:1" --(vcat [ppr PprDebug ty_to_inst,
 228                                                         --            ppr PprDebug tyvar])
 229
 230 tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s)
 231 tcInstSigType ty_to_inst
 232   = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst
 233   where
 234     bind_fn = inst_tyvar DontBind
 235     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 236                          Just ty -> returnNF_Tc ty
 237                          Nothing -> panic "tcInstType:2"-- (vcat [ppr PprDebug ty_to_inst,
 238                                                         --            ppr PprDebug tyvar])
 239
 240 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 241 zonkTcTyVarToTyVar tv
 242   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 243     case tv_ty of       -- Should be a tyvar!
 244
 245       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 246
 247       _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 248            returnNF_Tc (tcTyVarToTyVar tv)
 249
 250
 251 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 252 zonkTcTypeToType env ty
 253   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 254   where
 255     occ_fn env tyvar
 256       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 257          case maybe_ty of
 258            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 259            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 260            other                    -> lookup env tyvar
 261
 262     lookup env tyvar = case lookupTyVarEnv env tyvar of
 263                           Just ty -> returnNF_Tc ty
 264                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 265
 266
 267 tcConvert bind_fn occ_fn env ty_to_convert
 268   = doo env ty_to_convert
 269   where
 270     doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
 271
 272     doo env (SynTy tycon tys ty)  = mapNF_Tc (doo env) tys      `thenNF_Tc` \ tys' ->
 273                                    doo env ty                   `thenNF_Tc` \ ty' ->
 274                                    returnNF_Tc (SynTy tycon tys' ty')
 275
 276     doo env (FunTy arg res usage) = doo env arg         `thenNF_Tc` \ arg' ->
 277                                    doo env res          `thenNF_Tc` \ res' ->
 278                                    returnNF_Tc (FunTy arg' res' usage)
 279
 280     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 281                                    doo env arg          `thenNF_Tc` \ arg' ->
 282                                    returnNF_Tc (AppTy fun' arg')
 283
 284     doo env (DictTy clas ty usage)= doo env ty          `thenNF_Tc` \ ty' ->
 285                                    returnNF_Tc (DictTy clas ty' usage)
 286
 287     doo env (ForAllUsageTy u us ty) = doo env ty        `thenNF_Tc` \ ty' ->
 288                                      returnNF_Tc (ForAllUsageTy u us ty')
 289
 290         -- The two interesting cases!
 291     doo env (TyVarTy tv)         = occ_fn env tv
 292
 293     doo env (ForAllTy tyvar ty)
 294         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 295           let
 296                 new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
 297           in
 298           doo new_env ty                `thenNF_Tc` \ ty' ->
 299           returnNF_Tc (ForAllTy tyvar' ty')
 300
 301
 302 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
 303 tcInstTheta tenv theta
 304   = mapNF_Tc go theta
 305   where
 306     go (clas,ty) = tcInstType tenv ty   `thenNF_Tc` \ tc_ty ->
 307                    returnNF_Tc (clas, tc_ty)
 308
 309 -- A useful function that takes an occurrence of a global thing
 310 -- and instantiates its type with fresh type variables
 311 tcInstId :: Id
 312          -> NF_TcM s ([TcTyVar s],      -- It's instantiated type
 313                       TcThetaType s,    --
 314                       TcType s)         --
 315
 316 tcInstId id
 317   = let
 318       (tyvars, rho) = splitForAllTy (idType id)
 319     in
 320     tcInstTyVars tyvars         `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
 321     tcInstType tenv rho         `thenNF_Tc` \ rho' ->
 322     let
 323         (theta', tau') = splitRhoTy rho'
 324     in
 325     returnNF_Tc (tyvars', theta', tau')
 326 \end{code}
 327
 328 Reading and writing TcTyVars
 329 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 330 \begin{code}
 331 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 332 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 333 \end{code}
 334
 335 Writing is easy:
 336
 337 \begin{code}
 338 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 339 \end{code}
 340
 341 Reading is more interesting.  The easy thing to do is just to read, thus:
 342 \begin{verbatim}
 343 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 344 \end{verbatim}
 345
 346 But it's more fun to short out indirections on the way: If this
 347 version returns a TyVar, then that TyVar is unbound.  If it returns
 348 any other type, then there might be bound TyVars embedded inside it.
 349
 350 We return Nothing iff the original box was unbound.
 351
 352 \begin{code}
 353 tcReadTyVar (TyVar uniq kind name box)
 354   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 355     case maybe_ty of
 356         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 357                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 358                       returnNF_Tc (BoundTo ty')
 359
 360         other      -> returnNF_Tc other
 361
 362 short_out :: TcType s -> NF_TcM s (TcType s)
 363 short_out ty@(TyVarTy (TyVar uniq kind name box))
 364   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 365     case maybe_ty of
 366         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 367                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 368                        returnNF_Tc ty'
 369
 370         other       -> returnNF_Tc ty
 371
 372 short_out other_ty = returnNF_Tc other_ty
 373 \end{code}
 374
 375
 376 Zonking
 377 ~~~~~~~
 378 \begin{code}
 379 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 380 zonkTcTyVars tyvars
 381   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 382     returnNF_Tc (tyVarsOfTypes tys)
 383
 384 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 385 zonkTcTyVar tyvar
 386   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 387     case maybe_ty of
 388         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty
 389         BoundTo other               -> zonkTcType other
 390         other                       -> returnNF_Tc (TyVarTy tyvar)
 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 (AppTy ty1' ty2')
 400
 401 zonkTcType (TyConTy tc u)
 402   = returnNF_Tc (TyConTy tc u)
 403
 404 zonkTcType (SynTy tc tys ty)
 405   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 406     zonkTcType ty               `thenNF_Tc` \ ty' ->
 407     returnNF_Tc (SynTy tc tys' ty')
 408
 409 zonkTcType (ForAllTy tv ty)
 410   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 411     zonkTcType ty               `thenNF_Tc` \ ty' ->
 412     case tv_ty of       -- Should be a tyvar!
 413       TyVarTy tv' ->
 414                      returnNF_Tc (ForAllTy tv' ty')
 415       _ -> --pprTrace "zonkTcType:ForAllTy:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 416
 417            returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 418
 419 zonkTcType (ForAllUsageTy uv uvs ty)
 420   = panic "zonk:ForAllUsageTy"
 421
 422 zonkTcType (FunTy ty1 ty2 u)
 423   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 424     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 425     returnNF_Tc (FunTy ty1' ty2' u)
 426
 427 zonkTcType (DictTy c ty u)
 428   = zonkTcType ty               `thenNF_Tc` \ ty' ->
 429     returnNF_Tc (DictTy c ty' u)
 430 \end{code}