ghc/compiler/typecheck/TcType.lhs

   1 \begin{code}
   2 #include "HsVersions.h"
   3
   4 module TcType (
   5
   6   SYN_IE(TcTyVar),
   7   newTcTyVar,
   8   newTyVarTy,   -- Kind -> NF_TcM s (TcType s)
   9   newTyVarTys,  -- Int -> Kind -> NF_TcM s [TcType s]
  10
  11
  12   SYN_IE(TcTyVarSet),
  13
  14   -----------------------------------------
  15   SYN_IE(TcType), TcMaybe(..),
  16   SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(TcRhoType),
  17
  18         -- Find the type to which a type variable is bound
  19   tcWriteTyVar,         -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
  20   tcReadTyVar,          -- :: TcTyVar s -> NF_TcM (TcMaybe s)
  21
  22
  23   tcSplitForAllTy, tcSplitRhoTy,
  24
  25   tcInstTyVars,
  26   tcInstSigTyVars,
  27   tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
  28   tcInstTheta, tcInstId,
  29
  30   zonkTcTyVars,
  31   zonkTcType,
  32   zonkTcTypeToType,
  33   zonkTcTyVar,
  34   zonkTcTyVarToTyVar
  35
  36   ) where
  37
  38
  39
  40 -- friends:
  41 import Type     ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..),
  42                   tyVarsOfTypes, getTyVar_maybe,
  43                   splitForAllTy, splitRhoTy, isTyVarTy,
  44                   mkForAllTys, instantiateTy
  45                 )
  46 import TyVar    ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet),
  47                   SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv,
  48                   nullTyVarEnv, mkTyVarEnv,
  49                   tyVarSetToList
  50                 )
  51
  52 -- others:
  53 import Class    ( GenClass, SYN_IE(Class) )
  54 import TyCon    ( isFunTyCon )
  55 import Id       ( idType, SYN_IE(Id) )
  56 import Kind     ( Kind )
  57 import TcKind   ( TcKind )
  58 import TcMonad
  59 import Usage    ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
  60
  61 import TysPrim          ( voidTy )
  62
  63 IMP_Ubiq()
  64 import Unique           ( Unique )
  65 import UniqFM           ( UniqFM )
  66 import Maybes           ( assocMaybe )
  67 import Util             ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
  68 \end{code}
  69
  70
  71
  72 Data types
  73 ~~~~~~~~~~
  74
  75 \begin{code}
  76 type TcType s = GenType (TcTyVar s) UVar        -- Used during typechecker
  77         -- Invariant on ForAllTy in TcTypes:
  78         --      forall a. T
  79         -- a cannot occur inside a MutTyVar in T; that is,
  80         -- T is "flattened" before quantifying over a
  81
  82 type TcThetaType s = [(Class, TcType s)]
  83 type TcRhoType s   = TcType s           -- No ForAllTys
  84 type TcTauType s   = TcType s           -- No DictTys or ForAllTys
  85
  86 type Box s = MutableVar s (TcMaybe s)
  87
  88 data TcMaybe s = UnBound
  89                | BoundTo (TcType s)
  90                | DontBind               -- This variant is used for tyvars
  91                                         -- arising from type signatures, or
  92                                         -- existentially quantified tyvars;
  93                                         -- The idea is that we must not unify
  94                                         -- such tyvars with anything except
  95                                         -- themselves.
  96
  97 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
  98 -- because you get a synonym loop if you do!
  99
 100 type TcTyVar s    = GenTyVar (Box s)
 101 type TcTyVarSet s = GenTyVarSet (Box s)
 102 \end{code}
 103
 104 \begin{code}
 105 tcTyVarToTyVar :: TcTyVar s -> TyVar
 106 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
 107 \end{code}
 108
 109 Utility functions
 110 ~~~~~~~~~~~~~~~~~
 111 These tcSplit functions are like their non-Tc analogues, but they
 112 follow through bound type variables.
 113
 114 \begin{code}
 115 tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 116 tcSplitForAllTy t
 117   = go t t []
 118   where
 119     go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
 120     go syn_t (SynTy _ _ t)   tvs = go syn_t t tvs
 121     go syn_t (TyVarTy tv)    tvs = tcReadTyVar tv       `thenNF_Tc` \ maybe_ty ->
 122                                    case maybe_ty of
 123                                         BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
 124                                         other                           -> returnNF_Tc (reverse tvs, syn_t)
 125     go syn_t t               tvs = returnNF_Tc (reverse tvs, syn_t)
 126
 127 tcSplitRhoTy :: TcType s -> NF_TcM s ([(Class,TcType s)], TcType s)
 128 tcSplitRhoTy t
 129   = go t t []
 130  where
 131     go syn_t (FunTy (DictTy c t _) r _) ts = go r r ((c,t):ts)
 132     go syn_t (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
 133                               | isFunTyCon tycon
 134                               = go r r ((c,t):ts)
 135     go syn_t (SynTy _ _ t) ts = go syn_t t ts
 136     go syn_t (TyVarTy tv)  ts = tcReadTyVar tv  `thenNF_Tc` \ maybe_ty ->
 137                                 case maybe_ty of
 138                                   BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
 139                                   other                           -> returnNF_Tc (reverse ts, syn_t)
 140     go syn_t t             ts = returnNF_Tc (reverse ts, syn_t)
 141 \end{code}
 142
 143
 144 Type instantiation
 145 ~~~~~~~~~~~~~~~~~~
 146
 147 \begin{code}
 148 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
 149 newTcTyVar kind
 150   = tcGetUnique         `thenNF_Tc` \ uniq ->
 151     tcNewMutVar UnBound `thenNF_Tc` \ box ->
 152     returnNF_Tc (TyVar uniq kind Nothing box)
 153
 154 newTyVarTy  :: Kind -> NF_TcM s (TcType s)
 155 newTyVarTy kind
 156   = newTcTyVar kind     `thenNF_Tc` \ tc_tyvar ->
 157     returnNF_Tc (TyVarTy tc_tyvar)
 158
 159 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
 160 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 161
 162
 163 -- For signature type variables, mark them as "DontBind"
 164 tcInstTyVars, tcInstSigTyVars
 165         :: [GenTyVar flexi]
 166         -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
 167
 168 tcInstTyVars    tyvars = inst_tyvars UnBound  tyvars
 169 tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
 170
 171 inst_tyvars initial_cts tyvars
 172   = mapNF_Tc (inst_tyvar initial_cts) tyvars    `thenNF_Tc` \ tc_tyvars ->
 173     let
 174         tys = map TyVarTy tc_tyvars
 175     in
 176     returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
 177
 178 inst_tyvar initial_cts (TyVar _ kind name _)
 179   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 180     tcNewMutVar initial_cts     `thenNF_Tc` \ box ->
 181     returnNF_Tc (TyVar uniq kind Nothing box)
 182         -- The "Nothing" means that it'll always print with its
 183         -- unique (or something similar).  If we leave the original (Just Name)
 184         -- in there then error messages will say "can't match (T a) against (T a)"
 185 \end{code}
 186
 187 @tcInstType@ and @tcInstSigType@ both create a fresh instance of a
 188 type, returning a @TcType@. All inner for-alls are instantiated with
 189 fresh TcTyVars.
 190
 191 The difference is that tcInstType instantiates all forall'd type
 192 variables (and their bindees) with UnBound type variables, whereas
 193 tcInstSigType instantiates them with DontBind types variables.
 194 @tcInstSigType@ also doesn't take an environment.
 195
 196 On the other hand, @tcInstTcType@ instantiates a TcType. It uses
 197 instantiateTy which could take advantage of sharing some day.
 198
 199 \begin{code}
 200 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 201 tcInstTcType ty
 202   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 203     case tyvars of
 204         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 205         other -> tcInstTyVars tyvars            `thenNF_Tc` \ (tyvars', _, tenv)  ->
 206                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 207
 208 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
 209 tcInstSigTcType ty
 210   = tcSplitForAllTy ty          `thenNF_Tc` \ (tyvars, rho) ->
 211     case tyvars of
 212         []    -> returnNF_Tc ([], ty)   -- Nothing to do
 213         other -> tcInstSigTyVars tyvars         `thenNF_Tc` \ (tyvars', _, tenv)  ->
 214                  returnNF_Tc (tyvars', instantiateTy tenv rho)
 215
 216 tcInstType :: [(GenTyVar flexi,TcType s)]
 217            -> GenType (GenTyVar flexi) UVar
 218            -> NF_TcM s (TcType s)
 219 tcInstType tenv ty_to_inst
 220   = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
 221   where
 222     bind_fn = inst_tyvar UnBound
 223     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 224                          Just ty -> returnNF_Tc ty
 225                          Nothing -> panic "tcInstType:1" --(vcat [ppr PprDebug ty_to_inst,
 226                                                         --            ppr PprDebug tyvar])
 227
 228 tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s)
 229 tcInstSigType ty_to_inst
 230   = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst
 231   where
 232     bind_fn = inst_tyvar DontBind
 233     occ_fn env tyvar = case lookupTyVarEnv env tyvar of
 234                          Just ty -> returnNF_Tc ty
 235                          Nothing -> panic "tcInstType:2"-- (vcat [ppr PprDebug ty_to_inst,
 236                                                         --            ppr PprDebug tyvar])
 237
 238 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
 239 zonkTcTyVarToTyVar tv
 240   = zonkTcTyVar tv      `thenNF_Tc` \ tv_ty ->
 241     case tv_ty of       -- Should be a tyvar!
 242
 243       TyVarTy tv' ->    returnNF_Tc (tcTyVarToTyVar tv')
 244
 245       _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 246            returnNF_Tc (tcTyVarToTyVar tv)
 247
 248
 249 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
 250 zonkTcTypeToType env ty
 251   = tcConvert zonkTcTyVarToTyVar occ_fn env ty
 252   where
 253     occ_fn env tyvar
 254       =  tcReadTyVar tyvar      `thenNF_Tc` \ maybe_ty ->
 255          case maybe_ty of
 256            BoundTo (TyVarTy tyvar') -> lookup env tyvar'
 257            BoundTo other_ty         -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
 258            other                    -> lookup env tyvar
 259
 260     lookup env tyvar = case lookupTyVarEnv env tyvar of
 261                           Just ty -> returnNF_Tc ty
 262                           Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
 263
 264
 265 tcConvert bind_fn occ_fn env ty_to_convert
 266   = doo env ty_to_convert
 267   where
 268     doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
 269
 270     doo env (SynTy tycon tys ty)  = mapNF_Tc (doo env) tys      `thenNF_Tc` \ tys' ->
 271                                    doo env ty                   `thenNF_Tc` \ ty' ->
 272                                    returnNF_Tc (SynTy tycon tys' ty')
 273
 274     doo env (FunTy arg res usage) = doo env arg         `thenNF_Tc` \ arg' ->
 275                                    doo env res          `thenNF_Tc` \ res' ->
 276                                    returnNF_Tc (FunTy arg' res' usage)
 277
 278     doo env (AppTy fun arg)      = doo env fun          `thenNF_Tc` \ fun' ->
 279                                    doo env arg          `thenNF_Tc` \ arg' ->
 280                                    returnNF_Tc (AppTy fun' arg')
 281
 282     doo env (DictTy clas ty usage)= doo env ty          `thenNF_Tc` \ ty' ->
 283                                    returnNF_Tc (DictTy clas ty' usage)
 284
 285     doo env (ForAllUsageTy u us ty) = doo env ty        `thenNF_Tc` \ ty' ->
 286                                      returnNF_Tc (ForAllUsageTy u us ty')
 287
 288         -- The two interesting cases!
 289     doo env (TyVarTy tv)         = occ_fn env tv
 290
 291     doo env (ForAllTy tyvar ty)
 292         = bind_fn tyvar         `thenNF_Tc` \ tyvar' ->
 293           let
 294                 new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
 295           in
 296           doo new_env ty                `thenNF_Tc` \ ty' ->
 297           returnNF_Tc (ForAllTy tyvar' ty')
 298
 299
 300 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
 301 tcInstTheta tenv theta
 302   = mapNF_Tc go theta
 303   where
 304     go (clas,ty) = tcInstType tenv ty   `thenNF_Tc` \ tc_ty ->
 305                    returnNF_Tc (clas, tc_ty)
 306
 307 -- A useful function that takes an occurrence of a global thing
 308 -- and instantiates its type with fresh type variables
 309 tcInstId :: Id
 310          -> NF_TcM s ([TcTyVar s],      -- It's instantiated type
 311                       TcThetaType s,    --
 312                       TcType s)         --
 313
 314 tcInstId id
 315   = let
 316       (tyvars, rho) = splitForAllTy (idType id)
 317     in
 318     tcInstTyVars tyvars         `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
 319     tcInstType tenv rho         `thenNF_Tc` \ rho' ->
 320     let
 321         (theta', tau') = splitRhoTy rho'
 322     in
 323     returnNF_Tc (tyvars', theta', tau')
 324 \end{code}
 325
 326 Reading and writing TcTyVars
 327 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 328 \begin{code}
 329 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
 330 tcReadTyVar  :: TcTyVar s -> NF_TcM s (TcMaybe s)
 331 \end{code}
 332
 333 Writing is easy:
 334
 335 \begin{code}
 336 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
 337 \end{code}
 338
 339 Reading is more interesting.  The easy thing to do is just to read, thus:
 340 \begin{verbatim}
 341 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
 342 \end{verbatim}
 343
 344 But it's more fun to short out indirections on the way: If this
 345 version returns a TyVar, then that TyVar is unbound.  If it returns
 346 any other type, then there might be bound TyVars embedded inside it.
 347
 348 We return Nothing iff the original box was unbound.
 349
 350 \begin{code}
 351 tcReadTyVar (TyVar uniq kind name box)
 352   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 353     case maybe_ty of
 354         BoundTo ty -> short_out ty                      `thenNF_Tc` \ ty' ->
 355                       tcWriteMutVar box (BoundTo ty')   `thenNF_Tc_`
 356                       returnNF_Tc (BoundTo ty')
 357
 358         other      -> returnNF_Tc other
 359
 360 short_out :: TcType s -> NF_TcM s (TcType s)
 361 short_out ty@(TyVarTy (TyVar uniq kind name box))
 362   = tcReadMutVar box    `thenNF_Tc` \ maybe_ty ->
 363     case maybe_ty of
 364         BoundTo ty' -> short_out ty'                    `thenNF_Tc` \ ty' ->
 365                        tcWriteMutVar box (BoundTo ty')  `thenNF_Tc_`
 366                        returnNF_Tc ty'
 367
 368         other       -> returnNF_Tc ty
 369
 370 short_out other_ty = returnNF_Tc other_ty
 371 \end{code}
 372
 373
 374 Zonking
 375 ~~~~~~~
 376 \begin{code}
 377 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
 378 zonkTcTyVars tyvars
 379   = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars)        `thenNF_Tc` \ tys ->
 380     returnNF_Tc (tyVarsOfTypes tys)
 381
 382 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
 383 zonkTcTyVar tyvar
 384   = tcReadTyVar tyvar           `thenNF_Tc` \ maybe_ty ->
 385     case maybe_ty of
 386         BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty
 387         BoundTo other               -> zonkTcType other
 388         other                       -> returnNF_Tc (TyVarTy tyvar)
 389
 390 zonkTcType :: TcType s -> NF_TcM s (TcType s)
 391
 392 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
 393
 394 zonkTcType (AppTy ty1 ty2)
 395   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 396     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 397     returnNF_Tc (AppTy ty1' ty2')
 398
 399 zonkTcType (TyConTy tc u)
 400   = returnNF_Tc (TyConTy tc u)
 401
 402 zonkTcType (SynTy tc tys ty)
 403   = mapNF_Tc zonkTcType tys     `thenNF_Tc` \ tys' ->
 404     zonkTcType ty               `thenNF_Tc` \ ty' ->
 405     returnNF_Tc (SynTy tc tys' ty')
 406
 407 zonkTcType (ForAllTy tv ty)
 408   = zonkTcTyVar tv              `thenNF_Tc` \ tv_ty ->
 409     zonkTcType ty               `thenNF_Tc` \ ty' ->
 410     case tv_ty of       -- Should be a tyvar!
 411       TyVarTy tv' ->
 412                      returnNF_Tc (ForAllTy tv' ty')
 413       _ -> --pprTrace "zonkTcType:ForAllTy:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
 414
 415            returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
 416
 417 zonkTcType (ForAllUsageTy uv uvs ty)
 418   = panic "zonk:ForAllUsageTy"
 419
 420 zonkTcType (FunTy ty1 ty2 u)
 421   = zonkTcType ty1              `thenNF_Tc` \ ty1' ->
 422     zonkTcType ty2              `thenNF_Tc` \ ty2' ->
 423     returnNF_Tc (FunTy ty1' ty2' u)
 424
 425 zonkTcType (DictTy c ty u)
 426   = zonkTcType ty               `thenNF_Tc` \ ty' ->
 427     returnNF_Tc (DictTy c ty' u)
 428 \end{code}