ghc/compiler/typecheck/TcType.lhs

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