2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcType]{Types used in the typechecker}
12 newTyVarTy, -- Kind -> NF_TcM s (TcType s)
13 newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
15 -----------------------------------------
17 TcTauType, TcThetaType, TcRhoType,
19 -- Find the type to which a type variable is bound
20 tcWriteTyVar, -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
21 tcReadTyVar, -- :: TcTyVar s -> NF_TcM (TcMaybe s)
24 tcSplitForAllTy, tcSplitRhoTy,
29 tcInstSigType, tcInstTcType, tcInstSigTcType,
32 zonkTcTyVars, zonkSigTyVar,
33 zonkTcType, zonkTcTypes, zonkTcThetaType,
40 #include "HsVersions.h"
44 import Type ( Type, ThetaType, GenType(..), mkAppTy,
45 tyVarsOfTypes, splitDictTy_maybe,
46 isTyVarTy, instantiateTy
48 import TyVar ( TyVar, GenTyVar(..), GenTyVarSet,
49 TyVarEnv, lookupTyVarEnv, addToTyVarEnv,
50 emptyTyVarEnv, zipTyVarEnv, tyVarSetToList
54 import Class ( Class )
55 import TyCon ( isFunTyCon )
58 import Name ( changeUnique )
60 import TysPrim ( voidTy )
62 import Unique ( Unique )
63 import UniqFM ( UniqFM )
64 import BasicTypes ( unused )
65 import Util ( nOfThem, panic )
75 type TcType s = GenType (TcBox s) -- Used during typechecker
76 -- Invariant on ForAllTy in TcTypes:
78 -- a cannot occur inside a MutTyVar in T; that is,
79 -- T is "flattened" before quantifying over a
81 type TcThetaType s = [(Class, [TcType s])]
82 type TcRhoType s = TcType s -- No ForAllTys
83 type TcTauType s = TcType s -- No DictTys or ForAllTys
85 type TcBox s = TcRef s (TcMaybe s)
87 data TcMaybe s = UnBound
90 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
91 -- because you get a synonym loop if you do!
93 type TcTyVar s = GenTyVar (TcBox s)
94 type TcTyVarSet s = GenTyVarSet (TcBox s)
98 tcTyVarToTyVar :: TcTyVar s -> TyVar
99 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name unused
104 These tcSplit functions are like their non-Tc analogues, but they
105 follow through bound type variables.
108 tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
112 go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
113 go syn_t (SynTy _ t) tvs = go syn_t t tvs
114 go syn_t (TyVarTy tv) tvs = tcReadTyVar tv `thenNF_Tc` \ maybe_ty ->
116 BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
117 other -> returnNF_Tc (reverse tvs, syn_t)
118 go syn_t t tvs = returnNF_Tc (reverse tvs, syn_t)
120 tcSplitRhoTy :: TcType s -> NF_TcM s (TcThetaType s, TcType s)
124 -- A type variable is never instantiated to a dictionary type,
125 -- so we don't need to do a tcReadVar on the "arg".
126 go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
127 Just pair -> go res res (pair:ts)
128 Nothing -> returnNF_Tc (reverse ts, syn_t)
129 go syn_t (SynTy _ t) ts = go syn_t t ts
130 go syn_t (TyVarTy tv) ts = tcReadTyVar tv `thenNF_Tc` \ maybe_ty ->
132 BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
133 other -> returnNF_Tc (reverse ts, syn_t)
134 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
142 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
144 = tcGetUnique `thenNF_Tc` \ uniq ->
145 tcNewMutVar UnBound `thenNF_Tc` \ box ->
146 returnNF_Tc (TyVar uniq kind Nothing box)
148 newTyVarTy :: Kind -> NF_TcM s (TcType s)
150 = newTcTyVar kind `thenNF_Tc` \ tc_tyvar ->
151 returnNF_Tc (TyVarTy tc_tyvar)
153 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
154 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
157 -- For signature type variables, use the user name for the type variable
158 tcInstTyVars, tcInstSigTyVars
160 -> NF_TcM s ([TcTyVar s], [TcType s], TyVarEnv (TcType s))
162 tcInstTyVars tyvars = inst_tyvars inst_tyvar tyvars
163 tcInstSigTyVars tyvars = inst_tyvars inst_sig_tyvar tyvars
165 inst_tyvars inst tyvars
166 = mapNF_Tc inst tyvars `thenNF_Tc` \ tc_tyvars ->
168 tys = map TyVarTy tc_tyvars
170 returnNF_Tc (tc_tyvars, tys, zipTyVarEnv tyvars tys)
172 inst_tyvar (TyVar _ kind name _)
173 = tcGetUnique `thenNF_Tc` \ uniq ->
174 tcNewMutVar UnBound `thenNF_Tc` \ box ->
175 returnNF_Tc (TyVar uniq kind Nothing box)
176 -- The "Nothing" means that it'll always print with its
177 -- unique (or something similar). If we leave the original (Just Name)
178 -- in there then error messages will say "can't match (T a) against (T a)"
180 inst_sig_tyvar (TyVar _ kind name _)
181 = tcGetUnique `thenNF_Tc` \ uniq ->
183 tcNewMutVar UnBound `thenNF_Tc` \ box ->
184 -- Was DontBind, but we've nuked that "optimisation"
188 Just n -> Just (changeUnique n uniq)
191 returnNF_Tc (TyVar uniq kind name' box)
192 -- We propagate the name of the sigature type variable
195 @tcInstType@ and @tcInstSigType@ both create a fresh instance of a
196 type, returning a @TcType@. All inner for-alls are instantiated with
199 The difference is that tcInstType instantiates all forall'd type
200 variables (and their bindees) with anonymous type variables, whereas
201 tcInstSigType instantiates them with named type variables.
202 @tcInstSigType@ also doesn't take an environment.
204 On the other hand, @tcInstTcType@ instantiates a TcType. It uses
205 instantiateTy which could take advantage of sharing some day.
208 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
210 = tcSplitForAllTy ty `thenNF_Tc` \ (tyvars, rho) ->
212 [] -> returnNF_Tc ([], ty) -- Nothing to do
213 other -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
214 returnNF_Tc (tyvars', instantiateTy tenv rho)
216 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
218 = tcSplitForAllTy ty `thenNF_Tc` \ (tyvars, rho) ->
220 [] -> returnNF_Tc ([], ty) -- Nothing to do
221 other -> tcInstSigTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
222 returnNF_Tc (tyvars', instantiateTy tenv rho)
224 tcInstType :: TyVarEnv (TcType s)
226 -> NF_TcM s (TcType s)
227 tcInstType tenv ty_to_inst
228 = tcConvert bind_fn occ_fn tenv ty_to_inst
231 occ_fn env tyvar = case lookupTyVarEnv env tyvar of
232 Just ty -> returnNF_Tc ty
233 Nothing -> panic "tcInstType:1" --(vcat [ppr ty_to_inst,
236 tcInstSigType :: GenType flexi -> NF_TcM s (TcType s)
237 tcInstSigType ty_to_inst
238 = tcConvert bind_fn occ_fn emptyTyVarEnv ty_to_inst
240 bind_fn = inst_sig_tyvar -- Note: inst_sig_tyvar, not inst_tyvar
241 -- I don't think that can lead to strange error messages
242 -- of the form can't match (T a) against (T a)
243 -- See notes with inst_tyvar
245 occ_fn env tyvar = case lookupTyVarEnv env tyvar of
246 Just ty -> returnNF_Tc ty
247 Nothing -> panic "tcInstType:2"-- (vcat [ppr ty_to_inst,
250 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
251 zonkTcTyVarToTyVar tv
252 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
253 case tv_ty of -- Should be a tyvar!
255 TyVarTy tv' -> returnNF_Tc (tcTyVarToTyVar tv')
257 _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr tv, ppr tv_ty]) $
258 returnNF_Tc (tcTyVarToTyVar tv)
261 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
262 zonkTcTypeToType env ty
263 = tcConvert zonkTcTyVarToTyVar occ_fn env ty
266 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
268 BoundTo (TyVarTy tyvar') -> lookup env tyvar'
269 BoundTo other_ty -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
270 other -> lookup env tyvar
272 lookup env tyvar = case lookupTyVarEnv env tyvar of
273 Just ty -> returnNF_Tc ty
274 Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
277 tcConvert bind_fn occ_fn env ty_to_convert
278 = doo env ty_to_convert
280 doo env (TyConApp tycon tys) = mapNF_Tc (doo env) tys `thenNF_Tc` \ tys' ->
281 returnNF_Tc (TyConApp tycon tys')
283 doo env (SynTy ty1 ty2) = doo env ty1 `thenNF_Tc` \ ty1' ->
284 doo env ty2 `thenNF_Tc` \ ty2' ->
285 returnNF_Tc (SynTy ty1' ty2')
287 doo env (FunTy arg res) = doo env arg `thenNF_Tc` \ arg' ->
288 doo env res `thenNF_Tc` \ res' ->
289 returnNF_Tc (FunTy arg' res')
291 doo env (AppTy fun arg) = doo env fun `thenNF_Tc` \ fun' ->
292 doo env arg `thenNF_Tc` \ arg' ->
293 returnNF_Tc (mkAppTy fun' arg')
295 -- The two interesting cases!
296 doo env (TyVarTy tv) = occ_fn env tv
298 doo env (ForAllTy tyvar ty)
299 = bind_fn tyvar `thenNF_Tc` \ tyvar' ->
301 new_env = addToTyVarEnv env tyvar (TyVarTy tyvar')
303 doo new_env ty `thenNF_Tc` \ ty' ->
304 returnNF_Tc (ForAllTy tyvar' ty')
307 tcInstTheta :: TyVarEnv (TcType s) -> ThetaType -> NF_TcM s (TcThetaType s)
308 tcInstTheta tenv theta
311 go (clas,tys) = mapNF_Tc (tcInstType tenv) tys `thenNF_Tc` \ tc_tys ->
312 returnNF_Tc (clas, tc_tys)
315 Reading and writing TcTyVars
316 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
318 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
319 tcReadTyVar :: TcTyVar s -> NF_TcM s (TcMaybe s)
325 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
328 Reading is more interesting. The easy thing to do is just to read, thus:
330 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
333 But it's more fun to short out indirections on the way: If this
334 version returns a TyVar, then that TyVar is unbound. If it returns
335 any other type, then there might be bound TyVars embedded inside it.
337 We return Nothing iff the original box was unbound.
340 tcReadTyVar (TyVar uniq kind name box)
341 = tcReadMutVar box `thenNF_Tc` \ maybe_ty ->
343 BoundTo ty -> short_out ty `thenNF_Tc` \ ty' ->
344 tcWriteMutVar box (BoundTo ty') `thenNF_Tc_`
345 returnNF_Tc (BoundTo ty')
347 other -> returnNF_Tc other
349 short_out :: TcType s -> NF_TcM s (TcType s)
350 short_out ty@(TyVarTy (TyVar uniq kind name box))
351 = tcReadMutVar box `thenNF_Tc` \ maybe_ty ->
353 BoundTo ty' -> short_out ty' `thenNF_Tc` \ ty' ->
354 tcWriteMutVar box (BoundTo ty') `thenNF_Tc_`
357 other -> returnNF_Tc ty
359 short_out other_ty = returnNF_Tc other_ty
366 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
368 = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars) `thenNF_Tc` \ tys ->
369 returnNF_Tc (tyVarsOfTypes tys)
371 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
373 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
375 BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty -- tcReadTyVar never returns a bound tyvar
376 BoundTo other -> zonkTcType other
377 other -> returnNF_Tc (TyVarTy tyvar)
379 -- Signature type variables only get bound to each other,
381 zonkSigTyVar :: TcTyVar s -> NF_TcM s (TcTyVar s)
383 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
385 BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc tyvar' -- tcReadTyVar never returns a bound tyvar
386 BoundTo other -> panic "zonkSigTyVar" -- Should only be bound to another tyvar
387 other -> returnNF_Tc tyvar
389 zonkTcTypes :: [TcType s] -> NF_TcM s [TcType s]
390 zonkTcTypes tys = mapNF_Tc zonkTcType tys
392 zonkTcThetaType :: TcThetaType s -> NF_TcM s (TcThetaType s)
393 zonkTcThetaType theta = mapNF_Tc zonk theta
395 zonk (c,ts) = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
396 returnNF_Tc (c, new_ts)
398 zonkTcType :: TcType s -> NF_TcM s (TcType s)
400 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
402 zonkTcType (AppTy ty1 ty2)
403 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
404 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
405 returnNF_Tc (mkAppTy ty1' ty2')
407 zonkTcType (TyConApp tc tys)
408 = mapNF_Tc zonkTcType tys `thenNF_Tc` \ tys' ->
409 returnNF_Tc (TyConApp tc tys')
411 zonkTcType (SynTy ty1 ty2)
412 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
413 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
414 returnNF_Tc (SynTy ty1' ty2')
416 zonkTcType (ForAllTy tv ty)
417 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
418 zonkTcType ty `thenNF_Tc` \ ty' ->
419 case tv_ty of -- Should be a tyvar!
420 TyVarTy tv' -> returnNF_Tc (ForAllTy tv' ty')
421 _ -> panic "zonkTcType"
422 -- pprTrace "zonkTcType:ForAllTy:" (hsep [ppr tv, ppr tv_ty]) $
423 -- returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
425 zonkTcType (FunTy ty1 ty2)
426 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
427 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
428 returnNF_Tc (FunTy ty1' ty2')