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