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