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   tcInstTyVars,
  24   tcInstSigTyVars,
  25   tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
  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     ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..),
  40                   tyVarsOfTypes, getTyVar_maybe,
  41                   splitForAllTy, splitRhoTy,
  42                   mkForAllTys, instantiateTy
  43                 )
  44 import TyVar    ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet),
  45                   SYN_IE(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    ( SYN_IE(Usage), GenUsage, SYN_IE(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 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 174 tcInstSigTcType ty
 175   = case tyvars of
 176         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 177         other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
 178                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 179   where
 180     (tyvars, rho) = splitForAllTy ty
 181
 182 tcInstType :: [(GenTyVar flexi,TcType s)]
 183            -> GenType (GenTyVar flexi) UVar
 184            -> NF_TcM s (TcType s)
 185 tcInstType tenv ty_to_inst
 186   = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
 187   where
 188     bind_fn = inst_tyvar UnBound
 189     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 190                          Just ty -> returnNF_Tc ty
 191                          Nothing -> pprPanic "tcInstType:" (ppAboves [ppr PprDebug ty_to_inst,
 192                                                                       ppr PprDebug tyvar])
 193
 194 tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s)
 195 tcInstSigType ty_to_inst
 196   = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst
 197   where
 198     bind_fn = inst_tyvar DontBind
 199     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 200                          Just ty -> returnNF_Tc ty
 201                          Nothing -> pprPanic "tcInstType:" (ppAboves [ppr PprDebug ty_to_inst,
 202                                                                       ppr PprDebug tyvar])
 203
 204 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 205 zonkTcTyVarToTyVar tv
 206   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 207     case tv_ty of       -- Should be a tyvar!
 208
 209       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 210
 211       _ -> pprTrace "zonkTcTyVarToTyVar:" (ppCat [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 212            returnNF_Tc (tcTyVarToTyVar tv)
 213
 214
 215 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 216 zonkTcTypeToType env ty
 217   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 218   where
 219     occ_fn env tyvar
 220       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 221          case maybe_ty of
 222            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 223            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 224            other                    -> lookup env tyvar
 225
 226     lookup env tyvar = case lookupTyVarEnv env tyvar of
 227                           Just ty -> returnNF_Tc ty
 228                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 229
 230
 231 tcConvert bind_fn occ_fn env ty_to_convert
 232   = doo env ty_to_convert
 233   where
 234     doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
 235
 236     doo env (SynTy tycon tys ty)  = mapNF_Tc (doo env) tys      `thenNF_Tc` \ tys' ->
 237                                    doo env ty                   `thenNF_Tc` \ ty' ->
 238                                    returnNF_Tc (SynTy tycon tys' ty')
 239
 240     doo env (FunTy arg res usage) = doo env arg         `thenNF_Tc` \ arg' ->
 241                                    doo env res          `thenNF_Tc` \ res' ->
 242                                    returnNF_Tc (FunTy arg' res' usage)
 243
 244     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 245                                    doo env arg          `thenNF_Tc` \ arg' ->
 246                                    returnNF_Tc (AppTy fun' arg')
 247
 248     doo env (DictTy clas ty usage)= doo env ty          `thenNF_Tc` \ ty' ->
 249                                    returnNF_Tc (DictTy clas ty' usage)
 250
 251     doo env (ForAllUsageTy u us ty) = doo env ty        `thenNF_Tc` \ ty' ->
 252                                      returnNF_Tc (ForAllUsageTy u us ty')
 253
 254         -- The two interesting cases!
 255     doo env (TyVarTy tv)         = occ_fn env tv
 256
 257     doo env (ForAllTy tyvar ty)
 258         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 259           let
 260                 new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
 261           in
 262           doo new_env ty                `thenNF_Tc` \ ty' ->
 263           returnNF_Tc (ForAllTy tyvar' ty')
 264
 265
 266 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
 267 tcInstTheta tenv theta
 268   = mapNF_Tc go theta
 269   where
 270     go (clas,ty) = tcInstType tenv ty   `thenNF_Tc` \ tc_ty ->
 271                    returnNF_Tc (clas, tc_ty)
 272
 273 -- A useful function that takes an occurrence of a global thing
 274 -- and instantiates its type with fresh type variables
 275 tcInstId :: Id
 276          -> NF_TcM s ([TcTyVar s],      -- It's instantiated type
 277                       TcThetaType s,    --
 278                       TcType s)         --
 279
 280 tcInstId id
 281   = let
 282       (tyvars, rho) = splitForAllTy (idType id)
 283     in
 284     tcInstTyVars tyvars         `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
 285     tcInstType tenv rho         `thenNF_Tc` \ rho' ->
 286     let
 287         (theta', tau') = splitRhoTy rho'
 288     in
 289     returnNF_Tc (tyvars', theta', tau')
 290 \end{code}
 291
 292 Reading and writing TcTyVars
 293 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 294 \begin{code}
 295 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 296 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 297 \end{code}
 298
 299 Writing is easy:
 300
 301 \begin{code}
 302 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 303 \end{code}
 304
 305 Reading is more interesting.  The easy thing to do is just to read, thus:
 306 \begin{verbatim}
 307 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 308 \end{verbatim}
 309
 310 But it's more fun to short out indirections on the way: If this
 311 version returns a TyVar, then that TyVar is unbound.  If it returns
 312 any other type, then there might be bound TyVars embedded inside it.
 313
 314 We return Nothing iff the original box was unbound.
 315
 316 \begin{code}
 317 tcReadTyVar (TyVar uniq kind name box)
 318   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 319     case maybe_ty of
 320         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 321                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 322                       returnNF_Tc (BoundTo ty')
 323
 324         other      -> returnNF_Tc other
 325
 326 short_out :: TcType s -> NF_TcM s (TcType s)
 327 short_out ty@(TyVarTy (TyVar uniq kind name box))
 328   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 329     case maybe_ty of
 330         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 331                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 332                        returnNF_Tc ty'
 333
 334         other       -> returnNF_Tc ty
 335
 336 short_out other_ty = returnNF_Tc other_ty
 337 \end{code}
 338
 339
 340 Zonking
 341 ~~~~~~~
 342 \begin{code}
 343 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 344 zonkTcTyVars tyvars
 345   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 346     returnNF_Tc (tyVarsOfTypes tys)
 347
 348 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 349 zonkTcTyVar tyvar
 350   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 351     case maybe_ty of
 352         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty
 353         BoundTo other               -> zonkTcType other
 354         other                       -> returnNF_Tc (TyVarTy tyvar)
 355
 356 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 357
 358 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 359
 360 zonkTcType (AppTy ty1 ty2)
 361   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 362     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 363     returnNF_Tc (AppTy ty1' ty2')
 364
 365 zonkTcType (TyConTy tc u)
 366   = returnNF_Tc (TyConTy tc u)
 367
 368 zonkTcType (SynTy tc tys ty)
 369   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 370     zonkTcType ty               `thenNF_Tc` \ ty' ->
 371     returnNF_Tc (SynTy tc tys' ty')
 372
 373 zonkTcType (ForAllTy tv ty)
 374   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 375     zonkTcType ty               `thenNF_Tc` \ ty' ->
 376     case tv_ty of       -- Should be a tyvar!
 377       TyVarTy tv' ->
 378                      returnNF_Tc (ForAllTy tv' ty')
 379       _ -> pprTrace "zonkTcType:ForAllTy:" (ppCat [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 380
 381            returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 382
 383 zonkTcType (ForAllUsageTy uv uvs ty)
 384   = panic "zonk:ForAllUsageTy"
 385
 386 zonkTcType (FunTy ty1 ty2 u)
 387   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 388     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 389     returnNF_Tc (FunTy ty1' ty2' u)
 390
 391 zonkTcType (DictTy c ty u)
 392   = zonkTcType ty               `thenNF_Tc` \ ty' ->
 393     returnNF_Tc (DictTy c ty' u)
 394 \end{code}