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