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, tcInstTheta, tcInstId,
  24
  25   zonkTcTyVars,
  26   zonkTcType,
  27   zonkTcTypeToType,
  28   zonkTcTyVarToTyVar
  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                   TyVarEnv(..), lookupTyVarEnv, addOneToTyVarEnv, mkTyVarEnv,
  41                   tyVarSetToList
  42                 )
  43
  44 -- others:
  45 import Class    ( GenClass )
  46 import Id       ( idType )
  47 import Kind     ( Kind )
  48 import TcKind   ( TcKind )
  49 import TcMonad  hiding ( rnMtoTcM )
  50 import Usage    ( Usage(..), GenUsage, UVar(..), duffUsage )
  51
  52 import TysWiredIn       ( voidTy )
  53
  54 import Ubiq
  55 import Unique           ( Unique )
  56 import UniqFM           ( UniqFM )
  57 import Maybes           ( assocMaybe )
  58 import Util             ( zipEqual, nOfThem, panic, pprPanic )
  59
  60 import Outputable       ( Outputable(..) )      -- Debugging messages
  61 import PprType          ( GenTyVar, GenType )
  62 import Pretty                                   -- ditto
  63 import PprStyle         ( PprStyle(..) )        -- ditto
  64 \end{code}
  65
  66
  67
  68 Data types
  69 ~~~~~~~~~~
  70
  71 \begin{code}
  72 type TcType s = GenType (TcTyVar s) UVar        -- Used during typechecker
  73         -- Invariant on ForAllTy in TcTypes:
  74         --      forall a. T
  75         -- a cannot occur inside a MutTyVar in T; that is,
  76         -- T is "flattened" before quantifying over a
  77
  78 type TcThetaType s = [(Class, TcType s)]
  79 type TcRhoType s   = TcType s           -- No ForAllTys
  80 type TcTauType s   = TcType s           -- No DictTys or ForAllTys
  81
  82 type Box s = MutableVar s (TcMaybe s)
  83
  84 data TcMaybe s = UnBound
  85                | BoundTo (TcType s)
  86                | DontBind               -- This variant is used for tyvars
  87                                         -- arising from type signatures, or
  88                                         -- existentially quantified tyvars;
  89                                         -- The idea is that we must not unify
  90                                         -- such tyvars with anything except
  91                                         -- themselves.
  92
  93 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
  94 -- because you get a synonym loop if you do!
  95
  96 type TcTyVar s    = GenTyVar (Box s)
  97 type TcTyVarSet s = GenTyVarSet (Box s)
  98 \end{code}
  99
 100 \begin{code}
 101 tcTyVarToTyVar :: TcTyVar s -> TyVar
 102 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
 103 \end{code}
 104
 105 Type instantiation
 106 ~~~~~~~~~~~~~~~~~~
 107
 108 \begin{code}
 109 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 110 newTcTyVar kind
 111   = tcGetUnique         `thenNF_Tc` \ uniq ->
 112     tcNewMutVar UnBound `thenNF_Tc` \ box ->
 113     returnNF_Tc (TyVar uniq kind Nothing box)
 114
 115 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 116 newTyVarTy kind
 117   = newTcTyVar kind     `thenNF_Tc` \ tc_tyvar ->
 118     returnNF_Tc (TyVarTy tc_tyvar)
 119
 120 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 121 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 122
 123
 124
 125 -- For signature type variables, mark them as "DontBind"
 126 tcInstTyVars, tcInstSigTyVars
 127         :: [GenTyVar flexi]
 128         -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
 129 tcInstTyVars    tyvars = inst_tyvars UnBound  tyvars
 130 tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
 131
 132
 133 inst_tyvars initial_cts tyvars
 134   = mapNF_Tc (inst_tyvar initial_cts) tyvars    `thenNF_Tc` \ tc_tyvars ->
 135     let
 136         tys = map TyVarTy tc_tyvars
 137     in
 138     returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
 139
 140 inst_tyvar initial_cts (TyVar _ kind name _)
 141   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 142     tcNewMutVar initial_cts     `thenNF_Tc` \ box ->
 143     returnNF_Tc (TyVar uniq kind name box)
 144 \end{code}
 145
 146 @tcInstType@ and @tcInstTcType@ both create a fresh instance of a
 147 type, returning a @TcType@. All inner for-alls are instantiated with
 148 fresh TcTyVars.
 149
 150 There are two versions, one for instantiating a @Type@, and one for a @TcType@.
 151 The former must instantiate everything; all tyvars must be bound either
 152 by a forall or by an environment passed in.  The latter can do some sharing,
 153 and is happy with free tyvars (which is vital when instantiating the type
 154 of local functions).  In the future @tcInstType@ may try to be clever about not
 155 instantiating constant sub-parts.
 156
 157 \begin{code}
 158 tcInstType :: [(GenTyVar flexi,TcType s)]
 159            -> GenType (GenTyVar flexi) UVar
 160            -> NF_TcM s (TcType s)
 161 tcInstType tenv ty_to_inst
 162   = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
 163   where
 164     bind_fn = inst_tyvar DontBind
 165     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 166                          Just ty -> returnNF_Tc ty
 167                          Nothing -> pprPanic "tcInstType:" (ppAboves [ppr PprDebug ty_to_inst,
 168                                                                       ppr PprDebug tyvar])
 169
 170 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 171 zonkTcTyVarToTyVar tyvar
 172   = zonkTcTyVar tyvar   `thenNF_Tc` \ (TyVarTy tyvar') ->
 173     returnNF_Tc (tcTyVarToTyVar tyvar')
 174
 175 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 176 zonkTcTypeToType env ty
 177   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 178   where
 179     occ_fn env tyvar
 180       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 181          case maybe_ty of
 182            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 183            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 184            other                    -> lookup env tyvar
 185
 186     lookup env tyvar = case lookupTyVarEnv env tyvar of
 187                           Just ty -> returnNF_Tc ty
 188                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 189
 190
 191 tcConvert bind_fn occ_fn env ty_to_convert
 192   = do env ty_to_convert
 193   where
 194     do env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
 195
 196     do env (SynTy tycon tys ty)  = mapNF_Tc (do env) tys        `thenNF_Tc` \ tys' ->
 197                                    do env ty                    `thenNF_Tc` \ ty' ->
 198                                    returnNF_Tc (SynTy tycon tys' ty')
 199
 200     do env (FunTy arg res usage) = do env arg           `thenNF_Tc` \ arg' ->
 201                                    do env res           `thenNF_Tc` \ res' ->
 202                                    returnNF_Tc (FunTy arg' res' usage)
 203
 204     do env (AppTy fun arg)       = do env fun           `thenNF_Tc` \ fun' ->
 205                                    do env arg           `thenNF_Tc` \ arg' ->
 206                                    returnNF_Tc (AppTy fun' arg')
 207
 208     do env (DictTy clas ty usage)= do env ty            `thenNF_Tc` \ ty' ->
 209                                    returnNF_Tc (DictTy clas ty' usage)
 210
 211     do env (ForAllUsageTy u us ty) = do env ty  `thenNF_Tc` \ ty' ->
 212                                      returnNF_Tc (ForAllUsageTy u us ty')
 213
 214         -- The two interesting cases!
 215     do env (TyVarTy tv)          = occ_fn env tv
 216
 217     do env (ForAllTy tyvar ty)
 218         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 219           let
 220                 new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
 221           in
 222           do new_env ty         `thenNF_Tc` \ ty' ->
 223           returnNF_Tc (ForAllTy tyvar' ty')
 224
 225
 226 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
 227 tcInstTheta tenv theta
 228   = mapNF_Tc go theta
 229   where
 230     go (clas,ty) = tcInstType tenv ty   `thenNF_Tc` \ tc_ty ->
 231                    returnNF_Tc (clas, tc_ty)
 232
 233 -- A useful function that takes an occurrence of a global thing
 234 -- and instantiates its type with fresh type variables
 235 tcInstId :: Id
 236          -> NF_TcM s ([TcTyVar s],      -- It's instantiated type
 237                       TcThetaType s,    --
 238                       TcType s)         --
 239
 240 tcInstId id
 241   = let
 242       (tyvars, rho) = splitForAllTy (idType id)
 243     in
 244     tcInstTyVars tyvars         `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
 245     tcInstType tenv rho         `thenNF_Tc` \ rho' ->
 246     let
 247         (theta', tau') = splitRhoTy rho'
 248     in
 249     returnNF_Tc (tyvars', theta', tau')
 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 \begin{code}
 303 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 304 zonkTcTyVars tyvars
 305   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 306     returnNF_Tc (tyVarsOfTypes tys)
 307
 308 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 309 zonkTcTyVar tyvar
 310   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 311     case maybe_ty of
 312         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty
 313         BoundTo other               -> zonkTcType other
 314         other                       -> returnNF_Tc (TyVarTy tyvar)
 315
 316 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 317
 318 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 319
 320 zonkTcType (AppTy ty1 ty2)
 321   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 322     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 323     returnNF_Tc (AppTy ty1' ty2')
 324
 325 zonkTcType (TyConTy tc u)
 326   = returnNF_Tc (TyConTy tc u)
 327
 328 zonkTcType (SynTy tc tys ty)
 329   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 330     zonkTcType ty               `thenNF_Tc` \ ty' ->
 331     returnNF_Tc (SynTy tc tys' ty')
 332
 333 zonkTcType (ForAllTy tv ty)
 334   = zonkTcTyVar tv              `thenNF_Tc` \ (TyVarTy tv') ->  -- Should be a tyvar!
 335     zonkTcType ty               `thenNF_Tc` \ ty' ->
 336     returnNF_Tc (ForAllTy tv' ty')
 337
 338 zonkTcType (ForAllUsageTy uv uvs ty)
 339   = panic "zonk:ForAllUsageTy"
 340
 341 zonkTcType (FunTy ty1 ty2 u)
 342   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 343     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 344     returnNF_Tc (FunTy ty1' ty2' u)
 345
 346 zonkTcType (DictTy c ty u)
 347   = zonkTcType ty               `thenNF_Tc` \ ty' ->
 348     returnNF_Tc (DictTy c ty' u)
 349 \end{code}