ghc/compiler/typecheck/TcType.lhs

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