ghc/compiler/typecheck/TcType.lhs

   1 \begin{code}
   2 module TcType (
   3
   4   TcTyVar, TcBox,
   5   TcTyVarSet,
   6   newTcTyVar,
   7   newTyVarTy,   -- Kind -> NF_TcM s (TcType s)
   8   newTyVarTys,  -- Int -> Kind -> NF_TcM s [TcType s]
   9
  10   -----------------------------------------
  11   TcType, TcMaybe(..),
  12   TcTauType, TcThetaType, TcRhoType,
  13
  14         -- Find the type to which a type variable is bound
  15   tcWriteTyVar,         -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
  16   tcReadTyVar,          -- :: TcTyVar s -> NF_TcM (TcMaybe s)
  17
  18
  19   tcSplitForAllTy, tcSplitRhoTy,
  20
  21   tcInstTyVars,
  22   tcInstSigTyVars,
  23   tcInstType,
  24   tcInstSigType, tcInstTcType, tcInstSigTcType,
  25   tcInstTheta,
  26
  27   zonkTcTyVars, zonkSigTyVar,
  28   zonkTcType, zonkTcTypes, zonkTcThetaType,
  29   zonkTcTypeToType,
  30   zonkTcTyVar,
  31   zonkTcTyVarToTyVar
  32
  33   ) where
  34
  35 #include "HsVersions.h"
  36
  37
  38 -- friends:
  39 import Type     ( Type, ThetaType, GenType(..), mkAppTy,
  40                   tyVarsOfTypes, getTyVar_maybe, splitDictTy_maybe,
  41                   splitForAllTys, splitRhoTy, isTyVarTy,
  42                   mkForAllTys, instantiateTy
  43                 )
  44 import TyVar    ( TyVar, GenTyVar(..), TyVarSet, GenTyVarSet,
  45                   TyVarEnv, lookupTyVarEnv, addToTyVarEnv,
  46                   emptyTyVarEnv, mkTyVarEnv, zipTyVarEnv,
  47                   tyVarSetToList
  48                 )
  49
  50 -- others:
  51 import Class    ( Class )
  52 import TyCon    ( isFunTyCon )
  53 import Kind     ( Kind )
  54 import TcKind   ( TcKind )
  55 import TcMonad
  56
  57 import TysPrim          ( voidTy )
  58
  59 import Name             ( NamedThing(..) )
  60 import Unique           ( Unique )
  61 import UniqFM           ( UniqFM )
  62 import Maybes           ( assocMaybe )
  63 import BasicTypes       ( unused )
  64 import Util             ( zipEqual, nOfThem )
  65 import Outputable
  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
 186     returnNF_Tc (TyVar uniq kind name box)
 187         -- We propagate the name of the sigature type variable
 188 \end{code}
 189
 190 @tcInstType@ and @tcInstSigType@ both create a fresh instance of a
 191 type, returning a @TcType@. All inner for-alls are instantiated with
 192 fresh TcTyVars.
 193
 194 The difference is that tcInstType instantiates all forall'd type
 195 variables (and their bindees) with anonymous type variables, whereas
 196 tcInstSigType instantiates them with named type variables.
 197 @tcInstSigType@ also doesn't take an environment.
 198
 199 On the other hand, @tcInstTcType@ instantiates a TcType. It uses
 200 instantiateTy which could take advantage of sharing some day.
 201
 202 \begin{code}
 203 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 204 tcInstTcType ty
 205   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 206     case tyvars of
 207         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 208         other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 209                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 210
 211 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 212 tcInstSigTcType ty
 213   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 214     case tyvars of
 215         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 216         other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
 217                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 218
 219 tcInstType :: TyVarEnv (TcType s)
 220            -> GenType flexi
 221            -> NF_TcM s (TcType s)
 222 tcInstType tenv ty_to_inst
 223   = tcConvert bind_fn occ_fn tenv ty_to_inst
 224   where
 225     bind_fn = inst_tyvar
 226     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 227                          Just ty -> returnNF_Tc ty
 228                          Nothing -> panic "tcInstType:1" --(vcat [ppr ty_to_inst,
 229                                                         --            ppr tyvar])
 230
 231 tcInstSigType :: GenType flexi -> NF_TcM s (TcType s)
 232 tcInstSigType ty_to_inst
 233   = tcConvert bind_fn occ_fn emptyTyVarEnv ty_to_inst
 234   where
 235     bind_fn = inst_sig_tyvar    -- Note: inst_sig_tyvar, not inst_tyvar
 236                                 -- I don't think that can lead to strange error messages
 237     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 238                          Just ty -> returnNF_Tc ty
 239                          Nothing -> panic "tcInstType:2"-- (vcat [ppr ty_to_inst,
 240                                                         --            ppr tyvar])
 241
 242 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 243 zonkTcTyVarToTyVar tv
 244   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 245     case tv_ty of       -- Should be a tyvar!
 246
 247       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 248
 249       _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr tv, ppr tv_ty]) $
 250            returnNF_Tc (tcTyVarToTyVar tv)
 251
 252
 253 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 254 zonkTcTypeToType env ty
 255   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 256   where
 257     occ_fn env tyvar
 258       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 259          case maybe_ty of
 260            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 261            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 262            other                    -> lookup env tyvar
 263
 264     lookup env tyvar = case lookupTyVarEnv env tyvar of
 265                           Just ty -> returnNF_Tc ty
 266                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 267
 268
 269 tcConvert bind_fn occ_fn env ty_to_convert
 270   = doo env ty_to_convert
 271   where
 272     doo env (TyConApp tycon tys) = mapNF_Tc (doo env) tys       `thenNF_Tc` \ tys' ->
 273                                    returnNF_Tc (TyConApp tycon tys')
 274
 275     doo env (SynTy ty1 ty2)      = doo env ty1                  `thenNF_Tc` \ ty1' ->
 276                                    doo env ty2                  `thenNF_Tc` \ ty2' ->
 277                                    returnNF_Tc (SynTy ty1' ty2')
 278
 279     doo env (FunTy arg res)      = doo env arg          `thenNF_Tc` \ arg' ->
 280                                    doo env res          `thenNF_Tc` \ res' ->
 281                                    returnNF_Tc (FunTy arg' res')
 282
 283     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 284                                    doo env arg          `thenNF_Tc` \ arg' ->
 285                                    returnNF_Tc (mkAppTy fun' arg')
 286
 287         -- The two interesting cases!
 288     doo env (TyVarTy tv)         = occ_fn env tv
 289
 290     doo env (ForAllTy tyvar ty)
 291         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 292           let
 293                 new_env = addToTyVarEnv env tyvar (TyVarTy tyvar')
 294           in
 295           doo new_env ty                `thenNF_Tc` \ ty' ->
 296           returnNF_Tc (ForAllTy tyvar' ty')
 297
 298
 299 tcInstTheta :: TyVarEnv (TcType s) -> ThetaType -> NF_TcM s (TcThetaType s)
 300 tcInstTheta tenv theta
 301   = mapNF_Tc go theta
 302   where
 303     go (clas,tys) = mapNF_Tc (tcInstType tenv) tys      `thenNF_Tc` \ tc_tys ->
 304                     returnNF_Tc (clas, tc_tys)
 305 \end{code}
 306
 307 Reading and writing TcTyVars
 308 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 309 \begin{code}
 310 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 311 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 312 \end{code}
 313
 314 Writing is easy:
 315
 316 \begin{code}
 317 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 318 \end{code}
 319
 320 Reading is more interesting.  The easy thing to do is just to read, thus:
 321 \begin{verbatim}
 322 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 323 \end{verbatim}
 324
 325 But it's more fun to short out indirections on the way: If this
 326 version returns a TyVar, then that TyVar is unbound.  If it returns
 327 any other type, then there might be bound TyVars embedded inside it.
 328
 329 We return Nothing iff the original box was unbound.
 330
 331 \begin{code}
 332 tcReadTyVar (TyVar uniq kind name box)
 333   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 334     case maybe_ty of
 335         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 336                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 337                       returnNF_Tc (BoundTo ty')
 338
 339         other      -> returnNF_Tc other
 340
 341 short_out :: TcType s -> NF_TcM s (TcType s)
 342 short_out ty@(TyVarTy (TyVar uniq kind name box))
 343   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 344     case maybe_ty of
 345         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 346                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 347                        returnNF_Tc ty'
 348
 349         other       -> returnNF_Tc ty
 350
 351 short_out other_ty = returnNF_Tc other_ty
 352 \end{code}
 353
 354
 355 Zonking
 356 ~~~~~~~
 357 \begin{code}
 358 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 359 zonkTcTyVars tyvars
 360   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 361     returnNF_Tc (tyVarsOfTypes tys)
 362
 363 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 364 zonkTcTyVar tyvar
 365   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 366     case maybe_ty of
 367         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty           -- tcReadTyVar never returns a bound tyvar
 368         BoundTo other               -> zonkTcType other
 369         other                       -> returnNF_Tc (TyVarTy tyvar)
 370
 371 -- Signature type variables only get bound to each other,
 372 -- never to a type
 373 zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s)
 374 zonkSigTyVar tyvar
 375   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 376     case maybe_ty of
 377         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar'       -- tcReadTyVar never returns a bound tyvar
 378         BoundTo other               -> panic "zonkSigTyVar"     -- Should only be bound to another tyvar
 379         other                       -> returnNF_Tc tyvar
 380
 381 zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
 382 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 383
 384 zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
 385 zonkTcThetaType theta = mapNF_Tc zonk theta
 386                     where
 387                       zonk (c,ts) = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 388                                     returnNF_Tc (c, new_ts)
 389
 390 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 391
 392 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 393
 394 zonkTcType (AppTy ty1 ty2)
 395   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 396     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 397     returnNF_Tc (mkAppTy ty1' ty2')
 398
 399 zonkTcType (TyConApp tc tys)
 400   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 401     returnNF_Tc (TyConApp tc tys')
 402
 403 zonkTcType (SynTy ty1 ty2)
 404   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 405     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 406     returnNF_Tc (SynTy ty1' ty2')
 407
 408 zonkTcType (ForAllTy tv ty)
 409   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 410     zonkTcType ty               `thenNF_Tc` \ ty' ->
 411     case tv_ty of       -- Should be a tyvar!
 412       TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
 413       _ -> panic "zonkTcType"
 414            -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
 415            -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 416
 417 zonkTcType (FunTy ty1 ty2)
 418   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 419     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 420     returnNF_Tc (FunTy ty1' ty2')
 421 \end{code}