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